Email Gateway (Aug 19 2022 at 10:53): Email Gateway (Aug 19 2022 at 10:53):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi.
Recently I've experienced a bit odd behavior of schematic_lemma.
Let's consider this minimal example:
schematic_lemma surprise:
"?A ⟹ ?B ⟹ ?C"
proof -
fix a1 :: 'a
fix a2 :: 'a
fix A :: "'a set"
show "a1 ∈ A ⟹ a2 ∈ A ⟹ a1 = a1 ∧ a2 = a2" by auto
qed
Then what I get as a lemma surprise is the following theorem:
?a1.0 ∈ ?A ⟹ ?B ⟹ ?a1.0 = ?a1.0 ∧ ?a1.0 = ?a1.0
That hints that a2 ∈ A got somehow unified against a1 ∈ A and is not
used any more as an assumption. Thus I get a more special theorem than I
wanted to have.
I guess I am going to get the canonical answer: "it has never been
intended to be used like that" but I am wondering anyway if there is an
easy way to make schematic_lemma working for this kind of situations.
Ondrej
Email Gateway (Aug 19 2022 at 10:53):From: Lars Noschinski <noschinl@in.tum.de>
Not that it helps in your concrete case, but using meta implication in
show will often get you unexpected results and is thus best avoided (by
using assume instead).
-- Lars
Email Gateway (Aug 19 2022 at 10:53):From: Makarius <makarius@sketis.net>
I am still trying to see what you are trying to do, to understand better
from where the actual surprise is coming from.
Maybe it is just a misunderstanding about the scope of a1, a2, A. As
written above, they become arbitrary in the goal context, and unification
gets lots of freedom -- the details of it are explained in the usual
foundational papers about Isabelle/Pure and Isar.
This one might be closer to what you intend:
schematic_lemma no_surprise:
fixes a1 :: 'a
fixes a2 :: 'a
fixes A :: "'a set"
shows "?A ⟹ ?B ⟹ ?C"
proof -
assume "a1 ∈ A" and "a2 ∈ A"
then show "a1 = a1 ∧ a2 = a2" by auto
qed
Makarius
Email Gateway (Aug 19 2022 at 10:53):From: Brian Huffman <huffman.brian.c@gmail.com>
I don't have any workaround to offer, but I think I can explain the
current behavior.
Step 1: When you prove the goal using "show", this proposition is
immediately generalized over a1, a2 and A (i.e. it is "exported"). You
can see the exported result in the goals buffer:
Successful attempt to solve goal by exported rule:
?a1.2 ∈ ?A2 ⟹ ?a2.2 ∈ ?A2 ⟹ ?a1.2 = ?a1.2 ∧ ?a2.2 = ?a2.2
Step 2: The exported rule is applied to the first matching goal in the
current proof state. The new proof state is not shown by default, but
you can see it by inserting a "next" before the "qed":
goal (2 subgoals):
Applying the exported rule usually discharges a goal, but in this case
it has introduced two new ones! This is what happens when you use
meta-implication with "show", as has been discussed several times
before:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-April/msg00052.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-September/msg00044.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-December/msg00043.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-November/msg00022.html
Step 3: Processing "qed" causes all remaining subgoals to be solved by
assumption. Solving goal 1 unifies ?A with "?a1.8 ∈ ?A8", leaving goal
2 looking something like this:
⟦?a1.8 ∈ ?A8; ?B⟧ ⟹ ?a2.8 ∈ ?A8
Now it unifies the conclusion with the first matching assumption, so
?a1.8 gets unified to ?a2.8. Finally this results in the surprising
theorem you found.
Hope this helps,
Email Gateway (Aug 19 2022 at 10:54):From: Ondřej Kunčar <kuncar@in.tum.de>
OK, this really sheds light on what happens there.
Thanks Brian.
Ondrej
Last updated: Apr 24 2024 at 16:18 UTC