[Agda] Optimised equational reasoning

[Jacques Carette]

I don't understand why this would make things faster.  What you seem to 
have done is to change from first type-checking x ≡ y to first checking 
y ≡ z  (which will indeed reveal y and z as well).  It seems that this 
would make things faster only when running your bijectional reasoning 
proof 'backwards' is more information-revealing than when running it 
forwards!

Is there something else going on here?  Or is it just the case that very 
often backwards chaining is more information-revealing, so easier to 
typecheck?

Jacques

PS: BTW, thank you for sending such things to the list.  I really 
appreciate the opportunity of getting this deeper understanding.

On 2016-11-04 7:35 AM, Nils Anders Danielsson wrote:
> 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.
>