[Agda] Making ≡ proofs more manageable

[Andreas Abel]

Maybe you should post the complete code after all...

On 13.01.2014 11:52, Mateusz Kowalczyk wrote:
> On 13/01/14 10:48, Andreas Abel wrote:
>> Hi Mateusz,
>>
>> for equaltional proofs, I use the \equiv-Reasoning package.  This way, I
>> can write proof (skeletons) like I would write on paper.
>>
>> assoc x y z = begin
>>       (x <> y) <> z
>>     ≡⟨ ? ⟩
>>       ...
>>     ≡⟨ ? ⟩
>>       x <> (y <> z)
>>     ∎
>>     where open ≡-Reasoning
>>
>> After I have written out the intermediate terms of this equation chain,
>> I fill in the justifications (the ?).
>>
>> Advantages:
>> 0. I can decide when to unfold definitions.
>> 1. I get readable proofs.
>> 2. I understand the intermediate goals without having to read the mess
>> Agda makes of it.
>>
>> Cheers,
>> Andreas
>>
>
> Unfortunately, the goal I posted was in fact from one of the holes
> inside of ≡-Reasoning.
>
> --
> Mateusz K.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/