Email Gateway (Aug 18 2022 at 17:57): Email Gateway (Aug 18 2022 at 17:57):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Dear Isabelle users,
I have a theory (the full theory is attached to this mail) with the
following definitions,
datatype tree = LeafA | LeafB | Node "tree" "tree"
fun closure :: "tree \<Rightarrow> tree set" where
"closure (Node r s) = { z. \<exists> r' s'. r' \<in> closure r
\<and> s' \<in> closure s \<and> z = Node r' s' }"
| "closure LeafA = { LeafA }"
| "closure LeafB = { LeafA, LeafB }"
The failure occurs when proving the following lemma.
lemma "closure (Node r (Node s t)) \<subseteq> closure (Node (Node r s) t)"
unfolding closure.simps
First I unfolded a couple of things,
proof (rule subsetI, unfold mem_Collect_eq, elim exE conjE)
and then I essentially copied the resulting goal (this explains the
horrible variable names)
fix x r' s' r'a s'a
assume "r' \<in> closure r" and "x = Node r' s'" and "r'a \<in> closure s"
and "s'a \<in> closure t" and "s' = Node r'a s'a"
thus "\<exists>r' s'.
(\<exists>r'a s'. r'a \<in> closure r \<and> s' \<in> closure s
\<and> r' = Node r'a s') \<and>
s' \<in> closure t \<and> x = Node r' s'"
At this point I get a failure that I don't understand, that this
statement fails to match the goal:
*** Local statement will fail to refine any pending goal
*** Failed attempt to solve goal by exported rule:
...
The failure disappears if I rename the r'a to r'a' inside the existential
quantifier of the conclusion (included as a comment in the attachment),
i.e., simply by doing an alpha conversion. I find this very odd. Can
anybody explain this behaviour?
Thanks in advance,
Bertram
P.S.
isabelle version
Isabelle2011: January 2011
uname -a
Linux host 2.6.39-2-amd64 #1 SMP Wed Jun 8 11:01:04 UTC 2011 x86_64 GNU/Linux
Test.thy
Email Gateway (Aug 18 2022 at 17:58):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm afraid I can't. In general, the name of a bound variable should be irrelevant. I considered the possibility of a hidden effect on type inference, but all variables have the same type, namely tree.
Strange.
Larry Paulson
Email Gateway (Aug 18 2022 at 17:58):From: Lars Noschinski <noschinl@in.tum.de>
Indeed. When I tried to find a minimal example, I found that it goes
away, when I try to remove the initial proof steps:
lemma "⋀x. x ∈ {z. ∃r' s'. r' ∈ closure r ∧ s' ∈ {z. ∃r' s'. r' ∈
closure s ∧ s' ∈ closure t ∧ z = Node r' s'} ∧ z = Node r' s'} ⟹
x ∈ {z. ∃r' s'. r' ∈ {z. ∃r' s'. r' ∈ closure r ∧ s' ∈ closure
s ∧ z = Node r' s'} ∧ s' ∈ closure t ∧ z = Node r' s'}"
apply (unfold mem_Collect_eq)
apply (elim exE conjE)
proof -
fix x r' s' r'a
assume "x = Node r' s'" and "r'a ∈ closure s"
then show "∃r' s'.
(∃r'a s'. r'a ∈ closure r ∧ s' ∈ closure s
∧ r' = Node r'a s') ∧
s' ∈ closure t ∧ x = Node r' s'"
oops
still exhibits this behabiour, but if I remove the unfold too, it goes
away. The show statement in the following snippet works just fine:
lemma "⋀x. ∃r' s'. r' ∈ closure r ∧ (∃r' s'a. r' ∈ closure s ∧ s'a ∈
closure t ∧ s' = Node r' s'a) ∧ x = Node r' s' ⟹
∃r' s'. (∃r'a s'. r'a ∈ closure r ∧ s' ∈ closure s ∧ r' = Node r'a
s') ∧ s' ∈ closure t ∧ x = Node r' s'"
apply (elim exE conjE)
proof -
fix x r' s' r'a
assume "x = Node r' s'" and "r'a ∈ closure s"
then show "∃r' s'.
(∃r'a s'. r'a ∈ closure r ∧ s' ∈ closure s
∧ r' = Node r'a s') ∧
s' ∈ closure t ∧ x = Node r' s'"
sorry
oops
Email Gateway (Aug 18 2022 at 17:58):From: Lars Noschinski <noschinl@in.tum.de>
Hello all,
As Larry stated, this is indeed a strange problem. I tried to find a
minimal example; here is what I came up with:
lemma
shows "⋀c d. d ∈ Z ⟹ x = c ⟹
∃e. e ∈ {_. ∃e. e ∈ Z ∧ y = e}"
apply (unfold mem_Collect_eq)
proof -
fix s t
assume "x = s" and "t ∈ Z"
then show "∃s t. t ∈ Z ∧ y = t"
sorry
qed
The show statement fails with
*** Local statement will fail to refine any pending goal
*** Failed attempt to solve goal by exported rule:
...
Any of the following actions will make this example succeed:
- Rename any of the two existentially bound variables in the shows
statement
- Rename any of the two existentially bound variables in the show
statement
- Rename any of the variables mentioned by fix
- Remove any one of the assume statements
- Remove the "apply (unfold ...)" and state the unfolded goal directly
This was tested on a relatively current repository version of Isabelle
(last week or so).
-- Lars
Email Gateway (Aug 18 2022 at 18:10):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Hi,
[...]
So do we know whether this is an obscure feature or possibly a bug?
(If it's a feature I'd love to hear the underlying story.)
Best regards,
Bertram
Email Gateway (Aug 18 2022 at 18:11):From: Stefan Berghofer <berghofe@in.tum.de>
Bertram Felgenhauer wrote:
So do we know whether this is an obscure feature or possibly a bug?
(If it's a feature I'd love to hear the underlying story.)
Hi,
this problem has now been fixed in the repository version of Isabelle (476a239d3e0e).
It was caused by some rather old code in Isabelle's theorem module that renamed
"all bound variables and some unknowns" in a rule during resolution, in order to preserve
as many of the variable names in the goal as possible. For example, when resolving the rule
?P ?x ==> \<exists>x. P x
with the proof state
\<exists>foo. P foo
this will result in the new proof state
?P ?foo
because the schematic variable ?x in the rule has been renamed to match that of the
bound variable foo in the goal.
Unfortunately, such a renaming of schematic variables can cause two kinds of name clashes,
neither of which were detected by the old code:
If two bound variables in the goal happen to have the same name, this may cause
two schematic variables in the rule to be mapped to the same variable:
lemma R1: "P x ==> Q y ==> (\<exists>x. P x) \<and> (\<exists>y. Q y)"
by auto
lemma "(\<exists>z. P z) \<and> (\<exists>z. Q z)"
apply (rule R1)
oops
If a bound variable in the goal happens to have the same name as a schematic variable
in the rule, it may clash with another schematic variable in the rule after the
renaming.
lemma R2: "P y ==> x = y ==> \<exists>x. P x"
by auto
lemma "\<exists>y. P y"
apply (rule R2)
oops
I have now introduced a check that filters out such problematic renamings.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 18:11):From: Brian Huffman <brianh@cs.pdx.edu>
It certainly looks like a bug to me. I don't have an idea yet of why
it happens, but I found an even smaller example. I constrained
everything to type "nat" just to rule out any weirdness with
polymorphism. Note the repeated bound variable name in the goal (the
argument to Q is the second "c", which pretty-prints as "ca"). This
seems to be necessary to make the error happen.
lemma
shows "⋀(a::nat) (b::nat). P a b ⟹ ∀(c::nat) (c::nat). Q c"
proof -
fix s t :: nat assume "P s t"
thus "∀(s::nat) (t::nat). Q t" (* Local statement will fail to refine... *)
Swapping the order of the bound variable names in the conclusion also
gives the same error:
thus "∀(t::nat) (s::nat). Q s"
Just about any other modification to the lemma or proof that I could
think of seems to make it work again.
Last updated: Nov 21 2024 at 12:39 UTC