[Agda] Making ≡ proofs more manageable

[Mateusz Kowalczyk]

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.