[Agda] `<' reasoning

[Nils Anders Danielsson]

On 2017-12-08 12:14, Sandro Stucki wrote:
> Another solution is to relax the requirements of
> Relation.Binary.PreorderReasoning to allow reasoning about arbitrary
> transitive relations that respect the underlying equality but are not
> necessarily reflexive. Here's a possible implementation:
> 
>    https://gist.github.com/sstucki/2ce758a6dc62883ecbe54e71c0177fd0

In a proof-relevant setting it can also be nice to avoid inserting extra
steps in proofs. I often use combinators of the following kind:

   finally : ∀ {a} {A : Set a} (x y : A) → x ≡ y → x ≡ y
   finally _ _ x≡y = x≡y

   syntax finally x y x≡y = x ≡⟨ x≡y ⟩∎ y ∎

I also have a library that allows you to mix different relations:

   http://www.cse.chalmers.se/~nad/listings/up-to/Equational-reasoning.html

One key piece is the following abstraction of transitivity:

   record Transitive {a b p q} {A : Set a} {B : Set b}
                     (P : A → A → Set p) (Q : A → B → Set q) :
                     Set (a ⊔ b ⊔ p ⊔ q) where
     constructor is-transitive
     field
       transitive : ∀ {x y z} → P x y → Q y z → Q x z

(I also have one where transitivity goes from P and Q to P.) It is then
up to users of the library to define suitable instances.

-- 
/NAD