Email Gateway (Aug 19 2022 at 14:38): Email Gateway (Aug 19 2022 at 14:38):From: Makarius <makarius@sketis.net>
That question is hard to answer in generality. You need to be more
specific what you have in mind, what is the application etc.
Makarius
Email Gateway (Aug 19 2022 at 14:43):From: Eddy Westbrook <westbrook@kestrel.edu>
Hi,
I think I have found a bug in the chained proof mode, that occurs for equality proofs if one of the proof used in the chain is a reflexive proof. As an example, the following proof fails, even though (as far as I understand the chain mode) it should succeed:
lemma chain_bug: "e1 = e2 ⟹ f e1 = f e2"
proof -
assume eq1: "e1 = e2"
have "f e1 = f e2" by (rule arg_cong[OF eq1])
also
have "f e2 = f e2" by (simp)
finally
have "f e1 = f e2".
qed
Although it may seem silly to write a proof that “f e2 = f e2”, the reason it comes up is that the proof is machine-generated, and sometimes it is easier to generate a proof that something equals itself rather than checking explicitly for that fact.
Anyway, just thought I would report this.
Thanks,
-Eddy
Email Gateway (Aug 19 2022 at 14:43):From: Lawrence Paulson <lp15@cam.ac.uk>
One possible explanation of your issue could be that the symbol f has a polymorphic type, so that the two instances don’t match. So it would be better if you could submit a self-contained theory.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:44):From: Lars Noschinski <noschinl@in.tum.de>
On 11.06.2014 07:03, Eddy Westbrook wrote:
Hi,
I think I have found a bug in the chained proof mode, that occurs for equality proofs if one of the proof used in the chain is a reflexive proof. As an example, the following proof fails, even though (as far as I understand the chain mode) it should succeed:
lemma chain_bug: "e1 = e2 ⟹ f e1 = f e2"
proof -
assume eq1: "e1 = e2"
have "f e1 = f e2" by (rule arg_cong[OF eq1])
also
have "f e2 = f e2" by (simp)
finally
have "f e1 = f e2".
qed
This is intended behaviour (although I cannot find it in the
documentation right now):
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-September/msg00058.html
Calculational reasoning not only works with equality, but also with a
lot of other transitivity rules (see the print_trans_rules) for the
currently registered rules. An "also" (or "finally") step applies the
first applicable transitivity rule. If this does not make progress
(i.e., the chained fact before and after is the same), it backtracks and
tries the next applicable rule.
You get notified of this behaviour, if you explicitly request to use the
rule for transitivity of equality:
assume eq1: "e1 = e2"
have "f e1 = f e2" by (rule arg_cong[OF eq1])
also
have "f e2 = f e2" by (simp)
finally (trans)
have "f e1 = f e2".
Gives you:
Vacuous calculation result: f e1 = f e2
derived as projection (1) from:
f e1 = f e2
f e2 = f e2
at the finally step. A closer look at the output of print_trans_rules
shows the the next applicable rules are
HOL.back_subst: ?P ?a ⟹ ?a = ?b ⟹ ?P ?b
HOL.forw_subst: ?a = ?b ⟹ ?P ?b ⟹ ?P ?a
HOL.back_subst produces the same, vacuous result, so finally proceeds to
HOL.forw_subst which then yields "f e1 = f e1" as you observed.
Although it may seem silly to write a proof that “f e2 = f e2”, the reason it comes up is that the proof is machine-generated, and sometimes it is easier to generate a proof that something equals itself rather than checking explicitly for that fact.
Automatically generating theory sources is fragile, in particular when
using the usual user syntax for terms. Apparently, you can use YXML
syntax for the terms instead. Also, it is possible to directly interact
with the prover using Isabelle/Scala.
-- Lars
Email Gateway (Aug 19 2022 at 14:44):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Eddy,
this actually is the intended behavior, the reason of which is explained in:
G. Bauer and M. Wenzel. Calculational reasoning revisited - an
Isabelle/Isar experience. In R. J. Boulton and P. B. Jackson, editors,
Theorem Proving in Higher Order Logics: TPHOLs 2001, volume 2152 of
Lecture Notes in Computer Science. Springer-Verlag, 2001.
According to the isar-ref manual (see Section 2.2.4 "Calculational
reasoning") your example would translate into
assume "e1 = e2"
have "f e1 = f e2" ...
note calculation = this (* "f e1 = fe2" *)
have "f e2 = f e2" ...
note calculation = <TRANS> [OF calculation this] (* "f e1 = f e2" *)
from calculation
have "f e1 = f e2"
where the crucial spot is <TRANS>. That is, the actual content of
"calculation" depends on the chosen rule. And as explained in the above
paper this is done by trying all declared (via [trans] and [sym]; those
can be consulted via "print_trans_rules") lemmas while discarding
results that are mere projections.
cheers
chris
Btw: wispered you should be careful when throwing around words like
"bug" ;)
Email Gateway (Aug 19 2022 at 14:44):From: Eddy Westbrook <westbrook@kestrel.edu>
All,
Thanks for the replies! I understand more about the chained mode now, and will use your suggestions.
Thanks again,
-Eddy
Email Gateway (Aug 19 2022 at 14:45):From: Eddy Westbrook <westbrook@kestrel.edu>
Lars,
Just saw your note about the low-level ways to interact with Isabelle; thanks for the pointer, btw.
Is there any way you could point me to any documentation of / introduction to these features? I found some of Makarius Wenzel’s papers and talks about asynchronous proof processing, which discuss the concepts at a high level, but I haven’t been able to find anything yet to help me figure out the low-level details of how to actually talk directly to Isabelle.
Thanks again,
-Eddy
Last updated: Apr 18 2024 at 20:16 UTC