From 2167866c53aa7f9cbb52e776bfb64f53acf3fa2c Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Sat, 2 Apr 2022 11:41:51 +0100
Subject: Add more properties for ordered structures.

---
 .../Binary/Properties/StrictTotalOrder.agda        | 122 +++++++++++++++++++++
 1 file changed, 122 insertions(+)
 create mode 100644 src/Helium/Relation/Binary/Properties/StrictTotalOrder.agda

(limited to 'src/Helium/Relation/Binary/Properties/StrictTotalOrder.agda')

diff --git a/src/Helium/Relation/Binary/Properties/StrictTotalOrder.agda b/src/Helium/Relation/Binary/Properties/StrictTotalOrder.agda
new file mode 100644
index 0000000..43f001c
--- /dev/null
+++ b/src/Helium/Relation/Binary/Properties/StrictTotalOrder.agda
@@ -0,0 +1,122 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Relational properties of strict total orders
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Relation.Binary
+
+module Helium.Relation.Binary.Properties.StrictTotalOrder
+  {a ℓ₁ ℓ₂} (STO : StrictTotalOrder a ℓ₁ ℓ₂)
+  where
+
+open import Data.Sum using (inj₁; inj₂)
+open import Function using (flip)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (contradiction)
+
+open StrictTotalOrder STO
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
+
+import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as ToNonStrict
+
+infix 4 _≉_ _≮_ _≤_ _≰_ _>_ _≥_
+
+_≉_ : Rel Carrier ℓ₁
+x ≉ y = ¬ x ≈ y
+
+_≮_ : Rel Carrier ℓ₂
+x ≮ y = ¬ x < y
+
+_≤_ : Rel Carrier _
+_≤_ = ToNonStrict._≤_
+
+_≰_ : Rel Carrier _
+x ≰ y = ¬ x ≤ y
+
+_>_ : Rel Carrier ℓ₂
+_>_ = flip _<_
+
+_≥_ : Rel Carrier _
+_≥_ = flip _≤_
+
+
+<-≤-trans : Trans _<_ _≤_ _<_
+<-≤-trans = ToNonStrict.<-≤-trans <-trans <-respʳ-≈
+
+≤-<-trans : Trans _≤_ _<_ _<_
+≤-<-trans = ToNonStrict.≤-<-trans Eq.sym <-trans <-respˡ-≈
+
+
+≤-respˡ-≈ : _≤_ Respectsˡ _≈_
+≤-respˡ-≈ = ToNonStrict.≤-respˡ-≈ Eq.sym Eq.trans <-respˡ-≈
+
+≤-respʳ-≈ : _≤_ Respectsʳ _≈_
+≤-respʳ-≈ = ToNonStrict.≤-respʳ-≈ Eq.trans <-respʳ-≈
+
+≤-resp-≈ : _≤_ Respects₂ _≈_
+≤-resp-≈ = ToNonStrict.≤-resp-≈ Eq.isEquivalence <-resp-≈
+
+≤-reflexive : _≈_ ⇒ _≤_
+≤-reflexive = ToNonStrict.reflexive
+
+≤-refl : Reflexive _≤_
+≤-refl = ≤-reflexive Eq.refl
+
+≤-trans : Transitive _≤_
+≤-trans = ToNonStrict.trans Eq.isEquivalence <-resp-≈ <-trans
+
+≤-antisym : Antisymmetric _≈_ _≤_
+≤-antisym = ToNonStrict.antisym Eq.isEquivalence <-trans <-irrefl
+
+≤-total : Total _≤_
+≤-total = ToNonStrict.total compare
+
+
+<⇒≤ : _<_ ⇒ _≤_
+<⇒≤ = ToNonStrict.<⇒≤
+
+<⇒≉ : Irreflexive _<_ _≈_
+<⇒≉ = flip <-irrefl
+
+≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y
+≤∧≉⇒< (inj₁ x<y) x≉y = x<y
+≤∧≉⇒< (inj₂ x≈y) x≉y = contradiction x≈y x≉y
+
+
+≤∧≮⇒≈ : ∀ {x y} → x ≤ y → x ≮ y → x ≈ y
+≤∧≮⇒≈ (inj₁ x<y) x≮y = contradiction x<y x≮y
+≤∧≮⇒≈ (inj₂ x≈y) x≮y = x≈y
+
+
+<⇒≱ : Irreflexive _<_ _≥_
+<⇒≱ x<y (inj₁ x>y) = <-asym x<y x>y
+<⇒≱ x<y (inj₂ y≈x) = <-irrefl (Eq.sym y≈x) x<y
+
+≰⇒> : _≰_ ⇒ _>_
+≰⇒> {x} {y} x≰y with compare x y
+... | tri< x<y _ _ = contradiction (<⇒≤ x<y) x≰y
+... | tri≈ _ x≈y _ = contradiction (≤-reflexive x≈y) x≰y
+... | tri> _ _ x>y = x>y
+
+
+≤⇒≯ : Irreflexive _≤_ _>_
+≤⇒≯ = flip <⇒≱
+
+≮⇒≥ : _≮_ ⇒ _≥_
+≮⇒≥ {x} {y} x≮y with compare x y
+... | tri< x<y _ _ = contradiction x<y x≮y
+... | tri≈ _ x≈y _ = ≤-reflexive (Eq.sym x≈y)
+... | tri> _ _ x>y = <⇒≤ x>y
+
+≮∧≯⇒≈ : ∀ {x y} → x ≮ y → y ≮ x → x ≈ y
+≮∧≯⇒≈ {x} {y} x≮y x≯y with compare x y
+... | tri< x<y _ _ = contradiction x<y x≮y
+... | tri≈ _ x≈y _ = x≈y
+... | tri> _ _ x>y = contradiction x>y x≯y
-- 
cgit v1.2.3