[Agda] Making ≡ proofs more manageable

[Andreas Abel]

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

On 13.01.2014 09:30, Mateusz Kowalczyk wrote:
> Hello,
>
> I'm modelling Haskell's Attoparsec behaviour and I currently need to
> prove its associativity, that is ‘x <> y <> z ≡ x <> (y <> z)’ where
> _<>_ is a helper I used to define _∙_ in the record.
>
> I'm not going to bog you down with details unless you ask but just
> know that a lot of original functions look like
>
>> plus :: (Monoid t) => Parser t a -> Parser t a -> Parser t a
>> plus a b = Parser $ \i0 a0 m0 kf ks ->
>>             let kf' i1 a1 m1 _ _ = addS i0 a0 m0 i1 a1 m1 $
>>                                    \ i2 a2 m2 -> runParser b i2 a2 m2 kf ks
>>                 ks' i1 a1 m1 = ks i1 (a0 <> a1) m1
>>             in  noAdds i0 a0 m0 $ \i2 a2 m2 -> runParser a i2 a2 m2  kf' ks'
>
> and I replicate this behaviour. An upside is that once my Agda program
> checks out, I'll have some confidence that the Attoparsec's method
> works. The problem I'm having right now is that Agda is now asking me
> for such inconvenient looking proofs as
>
>> Goal: mkParser
>>        (λ {.r} i₀ a₀ m₀ kf ks →
>>           Parser.runParser x i₀ (A ε) m₀
>>           (λ i₁ a₁ m₃ _ _ →
>>              Parser.runParser y (I (unI i₀ ∙ unA a₁)) (A (ε ∙ unA a₁))
>>              (m₀ .Data.Agdoparsec.Internal.Types.More._.<> m₃)
>>              (λ i₂ a₂ m₄ _ _ →
>>                 Parser.runParser z (I (unI i₀ ∙ unA a₂)) (A (unA a₀ ∙ unA a₂))
>>                 (m₀ .Data.Agdoparsec.Internal.Types.More._.<> m₄) kf ks)
>>              (λ i₂ a₂ → ks i₂ (A (unA a₀ ∙ unA a₂))))
>>           (λ i₁ a₁ → ks i₁ (A (unA a₀ ∙ (ε ∙ unA a₁)))))
>>        ≡
>>        mkParser
>>        (λ {.r} i₀ a₀ m₀ kf ks →
>>           Parser.runParser x i₀ (A ε) m₀
>>           (λ i₁ a₁ m₃ _ _ →
>>              Parser.runParser y (I (unI i₀ ∙ unA a₁)) (A ε)
>>              (m₀ .Data.Agdoparsec.Internal.Types.More._.<> m₃)
>>              (λ i₂ a₂ m₄ _ _ →
>>                 Parser.runParser z (I ((unI i₀ ∙ unA a₁) ∙ unA a₂))
>>                 (A ((unA a₀ ∙ unA a₁) ∙ unA a₂))
>>                 ((m₀ .Data.Agdoparsec.Internal.Types.More._.<> m₃)
>>                  .Data.Agdoparsec.Internal.Types.More._.<> m₄)
>>                 kf ks)
>>              (λ i₂ a₂ → ks i₂ (A ((unA a₀ ∙ unA a₁) ∙ unA a₂))))
>>           (λ i₁ a₁ → ks i₁ (A (unA a₀ ∙ unA a₁))))
>
> Is there any way to make proofs of such form more manageable? Any
> tricks? It's fairly clear that the meat of the proof is just down to
> showing a few bits inside of this rather large goal type. Perhaps
> there's a method to get those in an easier manner rather than retyping
> the whole thing at each step of the proof.
>
> --
> Mateusz K.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>