*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] A bug in chained proof mode*From*: Eddy Westbrook <westbrook at kestrel.edu>*Date*: Wed, 11 Jun 2014 10:35:49 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <539844E9.6030107@in.tum.de>*References*: <AEAA6C7E-C502-46EA-821C-1872106C56CB@kestrel.edu> <539844E9.6030107@in.tum.de>

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 On Jun 11, 2014, at 5:00 AM, Lars Noschinski <noschinl at in.tum.de> wrote: > 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

**Follow-Ups**:**[isabelle] Interfacing Isabelle***From:*Lars Noschinski

**Re: [isabelle] A bug in chained proof mode***From:*Makarius

**References**:**[isabelle] A bug in chained proof mode***From:*Eddy Westbrook

**Re: [isabelle] A bug in chained proof mode***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Cygwin Isabelle2014 sledgehammer libwww-perl missing
- Next by Date: Re: [isabelle] quotient_type command fails
- Previous by Thread: Re: [isabelle] A bug in chained proof mode
- Next by Thread: [isabelle] Interfacing Isabelle
- Cl-isabelle-users June 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list