Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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 ∎
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment