Re: [isabelle] A bug in chained proof mode



All,

Thanks for the replies! I understand more about the chained mode now, and will use your suggestions.

Thanks again,
-Eddy

On Jun 11, 2014, at 5:06 AM, Christian Sternagel <c.sternagel at gmail.com> wrote:

> 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" ;)
> 
> On 06/11/2014 07:03 AM, 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
>> 
>> 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
>> 
> 





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