Re: [isabelle] A bug in chained proof mode
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.
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:
>> 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])
>> have "f e2 = f e2" by (simp)
>> have "f e1 = f e2".
> This is intended behaviour (although I cannot find it in the
> documentation right now):
> 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])
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and