[Agda] Optimised equational reasoning

[Nils Anders Danielsson]

On 2016-11-04 12:48, Jacques Carette wrote:
> 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!

Consider the following, typical proof, with parentheses added for
emphasis:

   a  ≡⟨ … ⟩
   (b ≡⟨ … ⟩
   (c ≡⟨ … ⟩
   (d ∎)))

Note that the innermost proof is "d ∎", a proof by reflexivity of d ≡ d.

-- 
/NAD