[Agda] Making ≡ proofs more manageable

[Twan van Laarhoven]

It looks like you can split up this proof as

   goal = cong-mkParser \i₀ a₀ m₀ kf ks →
          cong-runParser x i₀ (A ε) m₀ \i₁ a₁ m₃ _ _ →
          subgoal

where cong-mkParser asserts something like

    ∀ {f g} : (∀ i a m kf ks → f i a m kf ks ≡ g i a m kf ks)
            → mkParser f ≡ mkParser g

and similarly for runParser. Or you could assume extensionality and use 
Relation.Binary.ProposionalEquality.cong. In general when only a few bits 
change, you can write this as

    cong (\x -> constant-stuff x) (equality-of-changing-parts)

Or perhaps cong₂ if more than one thing changes.


Twan

On 13/01/14 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
>