*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] A bug in chained proof mode*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 11 Jun 2014 14:00:41 +0200*In-reply-to*: <AEAA6C7E-C502-46EA-821C-1872106C56CB@kestrel.edu>*References*: <AEAA6C7E-C502-46EA-821C-1872106C56CB@kestrel.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.5.0

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**:**Re: [isabelle] A bug in chained proof mode***From:*Eddy Westbrook

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

- Previous by Date: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- Next by Date: Re: [isabelle] A bug in chained proof mode
- Previous by Thread: Re: [isabelle] A bug in chained proof mode
- Next by Thread: Re: [isabelle] A bug in chained proof mode
- 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