Re: [isabelle] A bug in chained proof mode



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.