[Agda] Optimised equational reasoning

[Nils Anders Danielsson]

Hi,

At the last Agda meeting Ulf and I optimised an equational reasoning
combinator, and I thought others might want to know about the technique
we used.

Consider the following transitivity combinator:

   infixr -2 _≡⟨⟩_

   _≡⟨_⟩_ : ∀ {a} {A : Set a} x {y z : A} → x ≡ y → y ≡ z → x ≡ z
   _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

Agda checks arguments from left to right, so when this combinator is
used in a typical proof Agda first type-checks the x argument, and then
the proof of x ≡ y. The proof is type-checked without prior knowledge of
y. Consider instead the following, optimised definition:

   infixr -2 step-≡

   step-≡ : ∀ {a} {A : Set a} x {y z : A} → y ≡ z → x ≡ y → x ≡ z
   step-≡ _ = flip trans

   syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

When this definition is used Agda is likely to already know both x and y
when type-checking the proof of x ≡ y.

This kind of optimisation can lead to significant performance
improvements. I implemented this optimisation for some "bijectional
reasoning" combinators, and one of my proofs type-checked roughly five
times faster.

-- 
/NAD