[Agda] Making ≡ proofs more manageable

[Mateusz Kowalczyk]

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.