[Agda] Optimised equational reasoning

[Jacques Carette]

On 2016-11-04 7:59 AM, Nils Anders Danielsson wrote:
> 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.
>
Of course!  Apparently the mathematician in me is awake (there's no more 
information in proofs in either direction) and the computer scientist is 
still waking up (as in Agda-style proofs, there obviously is more 
information going backwards).

Jacques