Email Gateway (Apr 29 2022 at 16:02): Email Gateway (Apr 29 2022 at 16:02):From: Seung Park <seunghoon.park@cs.ox.ac.uk>
Hi everyone,
I have encountered an unusual behaviour with Eisbach methods/tactics defined within locales.
I have reproduced the problem with the following example:
locale foo =
fixes P :: "'a ⇒ bool"
begin
inductive Q :: "'a ⇒ bool"
where
Rule1: "P a ⟹ Q a"
method bar =
(rule Rule1, blast)
lemma "P a ⟹ Q a"
by bar
end
abbreviation P :: "'a ⇒ bool"
where
"P ≡ λ _. True"
interpretation foo_nat:
foo "P :: nat ⇒ bool"
.
interpretation foo_int:
foo "P :: int ⇒ bool"
.
lemma
fixes x :: int
shows "P x ⟹ foo_int.Q x"
by foo_int.bar (* Works as intended *)
lemma
fixes x :: nat
shows "P x ⟹ foo_nat.Q x"
apply foo_nat.bar (* Does not work *)
oops
lemma
fixes x :: int
shows "P x ⟹ foo_int.Q (x :: int)"
by foo_nat.bar (* Works but is not intended behaviour *)
In the example above, I have defined a locale 'foo' and also defined a tactic 'bar' within the locale.
The intent is that if I were to provide an interpretation named 'int' of this locale and want to use the tactic I defined afterwards, I would use 'int.bar'.
This way, even if I provided another interpretation, I should still be able to use 'int.bar' when proving anything related to 'int'.
When there is only one interpretation given, there are no problems. By removing the interpretation 'foo_int' in the example above, the second lemma can be proved using 'foo_nat.bar'.
However, when two or more interpretations are given, something unusual happens. It seems like the tactic of the most recent interpretation overrides all the tactics of the older interpretations. In the example, the tactic used in the second lemma does not work (noting that the interpretation 'foo_nat' was given before 'foo_int'). However, the same tactic works in the last lemma, strangely enough, as if the method 'foo_nat.bar' has been overriden by 'foo_int.bar'.
Is there a way to select the appropriate tactic in this case? It would be wonderful if there was a solution.
Many thanks,
Simon
Last updated: Jul 15 2022 at 23:21 UTC