Cf. https://github.com/agda/agda-stdlib/issues/185

Reasoning.agda

open import Relation.Binary

module Reasoning {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
  {_≈_ : Rel A ℓ₁} (≈-trans : Transitive _≈_) (≈-sym   : Symmetric _≈_) (≈-refl : Reflexive _≈_)
  {_≤_ : Rel A ℓ₂} (≤-trans : Transitive _≤_) (≤-respˡ-≈ : _≤_ Respectsˡ _≈_) (≤-respʳ-≈ : _≤_ Respectsʳ _≈_) (≤-refl  : Reflexive _≤_)
  {_<_ : Rel A ℓ₃} (<-trans : Transitive _<_) (<-respˡ-≈ : _<_ Respectsˡ _≈_) (<-respʳ-≈ : _<_ Respectsʳ _≈_) (<⇒≤ : _<_ ⇒ _≤_)
  (<-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z)
  (≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z)
  where

open import Level using (Level; _⊔_; Lift; lift)
open import Function using (case_of_; id)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

data _∼_ (x y : A) : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  strict    : (x<y : x < y) → x ∼ y
  nonstrict : (x≤y : x ≤ y) → x ∼ y
  eq        : (x≈y : x ≈ y) → x ∼ y

levelOf : ∀ {x y} → x ∼ y → Level
levelOf (strict x<y)    = ℓ₃
levelOf (nonstrict x≤y) = ℓ₂
levelOf (eq x≈y)        = ℓ₁

relOf : ∀ {x y} (r : x ∼ y) → Rel A (levelOf r)
relOf (strict x<y)    = _<_
relOf (nonstrict x≤y) = _≤_
relOf (eq x≈y)        = _≈_

record Entails {r₁ r₂} (R₁ : Rel A r₁) (R₂ : Rel A r₂) : Set (a ⊔ r₁ ⊔ r₂) where
  field entails : R₁ ⇒ R₂
open Entails {{...}}

instance

  ≈-entails-≤ : Entails _≈_ _≤_
  ≈-entails-≤ = record { entails = λ z → ≤-respʳ-≈ z ≤-refl }

  <-entails-≤ : Entails _<_ _≤_
  <-entails-≤ = record { entails = <⇒≤ }

  id-Entails : ∀ {r} {R : Rel A r} → Entails R R
  id-Entails = record { entails = id }

infix -1 begin_
infixr 0 _<⟨_⟩_ _≤⟨_⟩_ _≈⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
infix  1 _∎

begin_ : ∀ {r x y} {R : Rel A r} (r : x ∼ y) {{ _ : Entails (relOf r) R }} → R x y
begin (strict x<y)    = entails x<y
begin (nonstrict x≤y) = entails x≤y
begin (eq x≈y)        = entails x≈y

_<⟨_⟩_ : ∀ (x : A) {y z} → x < y → y ∼ z → x ∼ z
x <⟨ x<y ⟩ strict y<z    = strict (<-trans x<y y<z)
x <⟨ x<y ⟩ nonstrict y≤z = strict (<-≤-trans x<y y≤z)
x <⟨ x<y ⟩ eq y≈z        = strict (<-respʳ-≈ y≈z x<y)

_≤⟨_⟩_ : ∀ (x : A) {y z} → x ≤ y → y ∼ z → x ∼ z
x ≤⟨ x≤y ⟩ strict y<z    = strict (≤-<-trans x≤y y<z)
x ≤⟨ x≤y ⟩ nonstrict y≤z = nonstrict (≤-trans x≤y y≤z)
x ≤⟨ x≤y ⟩ eq y≈z        = nonstrict (≤-respʳ-≈ y≈z x≤y)

_≈⟨_⟩_ : ∀ (x : A) {y z} → x ≈ y → y ∼ z → x ∼ z
x ≈⟨ x≈y ⟩ strict y<z    = strict (<-respˡ-≈ (≈-sym x≈y) y<z)
x ≈⟨ x≈y ⟩ nonstrict y≤z = nonstrict (≤-respˡ-≈ (≈-sym x≈y) y≤z)
x ≈⟨ x≈y ⟩ eq y≈z        = eq (≈-trans x≈y y≈z)

_≡⟨_⟩_ : ∀ (x : A) {y z} → x ≡ y → y ∼ z → x ∼ z
x ≡⟨ x≡y ⟩ strict y<z    = strict (case x≡y of λ where refl → y<z)
x ≡⟨ x≡y ⟩ nonstrict y≤z = nonstrict (case x≡y of λ where refl → y≤z)
x ≡⟨ x≡y ⟩ eq y≈z        = eq (case x≡y of λ where refl → y≈z)

_≡⟨⟩_ : ∀ (x : A) {y} → x ∼ y → x ∼ y
x ≡⟨⟩ x∼y = x∼y

_∎ : ∀ x → x ∼ x
x ∎ = eq ≈-refl

private
  module Test where
    postulate
      u v w x y z d e : A
      u≈v : u ≈ v
      v≡w : v ≡ w
      w<x : w < x
      x≤y : x ≤ y
      y<z : y < z
      z≡d : z ≡ d
      d≈e : d ≈ e

    u≤c : u < e
    u≤c = begin
      u ≈⟨ u≈v ⟩
      v ≡⟨ v≡w ⟩
      w <⟨ w<x ⟩
      x ≤⟨ x≤y ⟩
      y <⟨ y<z ⟩
      z ≡⟨ z≡d ⟩
      d ≈⟨ d≈e ⟩
      e ∎

    u≤y : u ≤ y
    u≤y = begin
      u ≈⟨ u≈v ⟩
      v ≡⟨ v≡w ⟩
      w ≤⟨ <⇒≤ (<-≤-trans w<x x≤y) ⟩
      y ∎