Email Gateway (Aug 23 2022 at 08:24): Email Gateway (Aug 23 2022 at 08:24):From: "John F. Hughes" <jfh@cs.brown.edu>
I often get to a situation where the "Proof state" panel shows that what I
have and what I'd like to prove appear identical. For instance, at the
"try" in the following incomplete proof ...
theorem parallel_restate_left:
fixes l
fixes m
assumes "(l = m ∨ (∀ P. (¬ a2meets P l) ∨ (¬a2meets P m)))"
shows " a2parallel l m"
unfolding a2parallel_def
proof -
have c1: "(l = m ∨ (∀ P. (¬ a2meets P l) ∨ (¬a2meets P m)))" using
assms by blast
have c2: "(l = m ∨ (∀ P. ¬ (( a2meets P l) ∧ (a2meets P m))))" using c1
by blast
have c3: "(l = m ∨ ¬ (∃ P. ( a2meets P l) ∧ (a2meets P m)))" using c2 by
blast
try
The proof-state panel shows
proof (state)
this:
l = m ∨
(∄P. a2meets P l ∧
a2meets P m)
goal (1 subgoal):
====
I feel as if I could be reasonably forgiven for saying, "OK, seriously,
what more could you want?"
"try", of course, says "Tried in vain". My usual incantations like "show
?thesis try" or "thus ?thesis try", etc., get me nowhere; the latter
reports "Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
l a2|| m"
[I'm assuming that the particulars of my definitions like "a2meets" are
irrelevant here; the gist is that "a2meets P m" means the point P in the
cartesian plane -- i.e., a pair of real numbers -- lies on the line m
(which is either a vertical line defined by an equation like x = 1, or an
"ordinary" line defined by an equation like y = ax + b.]
Any suggestions for getting myself beyond such states?
Email Gateway (Aug 23 2022 at 08:24):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi John,
in the example you give, the goals are not identical. When I don't see
differences, my usual solution is to use git diff: I paste both versions in
two files and I compare them. In your case, this yields:
$ git diff --no-index --ignore-all-space --word-diff goal1 goal2
diff --git a/tmp/ubf1 b/tmp/buf2
index 2635544..03381fc 100644
--- a/tmp/goal1
+++ b/tmp/goal2
@@ -1,3 +1,3 @@
l = m ∨
(∄P. a2meets P l [-∧-]{+∨+}
a2meets P m)
(the git options are important for readability!)
Now, on the second part on the question ?thesis is bound before
unfolding a2parallel_def
and thus show does not work: You need to write l = m ∨ (∄P. a2meets P l
∨ a2meets P m) instead of ?thesis.
Best,
Mathias
Email Gateway (Aug 23 2022 at 08:24):From: "John F. Hughes" <jfh@cs.brown.edu>
Thank you very much. I love the "diff" idea, esp. because the situation
with truly identical "have" and "goals" does come up at other times (when
I've got unjustified assumptions in force, for instance. I was completely
convinced this was one of those situations. :(
--John
Email Gateway (Aug 23 2022 at 08:25):From: "lammich@in.tum.de" <lammich@in.tum.de>
Another beginner's pitfall are types, which are not displayed by default. It's
too easy to end up with something like "P (f []) ==> P (f [])", which, after
note [[show_types]] looks like P (f ([] ::'a list)) ==> P (f ([] ::'b list))
Peter
Last updated: Nov 21 2024 at 12:39 UTC