fix(StrictOrder): remove trichotomy

RedPRL · Nov 24, 2023 · 6c3702b · 6c3702b
1 parent 26c8f02
commit 6c3702b
Show file tree

Hide file tree

Showing 3 changed files with 57 additions and 94 deletions.
diff --git a/src/Mugen/Algebra/Displacement/FiniteSupport.agda b/src/Mugen/Algebra/Displacement/FiniteSupport.agda
@@ -27,11 +27,10 @@ open import Mugen.Data.List
 -- These are a special case of the Nearly Constant functions where the base is always ε
 -- and are implemented as such.
 
-module FinSupport {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri (Displacement-algebra._<_ 𝒟) x y) where
+module FinSupport {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
   private
     module 𝒟 = Displacement-algebra 𝒟
-    open 𝒟 using (ε; _⊗_)
-    module 𝒩 = NearlyConst 𝒟 cmp
+    module 𝒩 = NearlyConst 𝒟 _≡?_
 
   --------------------------------------------------------------------------------
   -- Finite Support Lists
@@ -47,7 +46,7 @@ module FinSupport {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri
     open 𝒩.SupportList support public
 
     field
-      is-ε : base ≡ ε
+      is-ε : base ≡ 𝒟.ε
 
   open FinSupportList
 
@@ -63,12 +62,12 @@ module FinSupport {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri
   FinSupportList-is-set =
     is-hlevel≃ 2 (Iso→Equiv eqv) $
       Σ-is-hlevel 2 𝒩.SupportList-is-set λ support →
-        is-hlevel-suc 2 𝒟.has-is-set (𝒩.SupportList.base support) ε
+        is-hlevel-suc 2 𝒟.has-is-set (𝒩.SupportList.base support) 𝒟.ε
 
   merge-fin : FinSupportList → FinSupportList → FinSupportList
   merge-fin xs ys .FinSupportList.support = 𝒩.merge (xs .support) (ys .support)
   merge-fin xs ys .FinSupportList.is-ε =
-    𝒩.base-merge (xs .support) (ys .support) ∙ ap₂ _⊗_ (xs .is-ε) (ys .is-ε) ∙ 𝒟.idl
+    𝒩.base-merge (xs .support) (ys .support) ∙ ap₂ 𝒟._⊗_ (xs .is-ε) (ys .is-ε) ∙ 𝒟.idl
 
   empty-fin : FinSupportList
   empty-fin .support = 𝒩.empty
@@ -83,10 +82,10 @@ module FinSupport {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri
 --------------------------------------------------------------------------------
 -- Displacement Algebra
 
-module _ {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri (Displacement-algebra._<_ 𝒟) x y) where
-  open FinSupport 𝒟 cmp
+module _ {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
+  open FinSupport 𝒟 _≡?_
   open FinSupportList
-  private module 𝒩𝒟 = Displacement-algebra (NearlyConstant 𝒟 cmp)
+  private module 𝒩𝒟 = Displacement-algebra (NearlyConstant 𝒟 _≡?_)
 
   FiniteSupport : Displacement-algebra o (o ⊔ r)
   FiniteSupport = to-displacement-algebra mk where
@@ -116,11 +115,11 @@ module _
   {o r}
   {𝒟 : Displacement-algebra o r}
   (let module 𝒟 = Displacement-algebra 𝒟)
-  (cmp : ∀ x y → Tri 𝒟._<_ x y)
+  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
   where
-  open FinSupport 𝒟 cmp
+  open FinSupport 𝒟 _≡?_
 
-  FinSupport⊆NearlyConstant : is-displacement-subalgebra (FiniteSupport 𝒟 cmp) (NearlyConstant 𝒟 cmp)
+  FinSupport⊆NearlyConstant : is-displacement-subalgebra (FiniteSupport 𝒟 _≡?_) (NearlyConstant 𝒟 _≡?_)
   FinSupport⊆NearlyConstant = to-displacement-subalgebra mk where
     mk : make-displacement-subalgebra _ _
     mk .make-displacement-subalgebra.into = FinSupportList.support
@@ -129,11 +128,11 @@ module _
     mk .make-displacement-subalgebra.strictly-mono _ _ xs<ys = xs<ys
     mk .make-displacement-subalgebra.inj = fin-support-list-path
 
-  FinSupport⊆InfProd : is-displacement-subalgebra (FiniteSupport 𝒟 cmp) (InfProd 𝒟)
+  FinSupport⊆InfProd : is-displacement-subalgebra (FiniteSupport 𝒟 _≡?_) (InfProd 𝒟)
   FinSupport⊆InfProd =
     is-displacement-subalgebra-trans
       FinSupport⊆NearlyConstant
-      (NearlyConstant⊆InfProd cmp)
+      (NearlyConstant⊆InfProd _≡?_)
 
 --------------------------------------------------------------------------------
 -- Ordered Monoid
@@ -143,13 +142,13 @@ module _
   {𝒟 : Displacement-algebra o r}
   (let module 𝒟 = Displacement-algebra 𝒟)
   (𝒟-ordered-monoid : has-ordered-monoid 𝒟)
-  (cmp : ∀ x y → Tri 𝒟._<_ x y)
+  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
   where
-  open FinSupport 𝒟 cmp
+  open FinSupport 𝒟 _≡?_
 
-  fin-support-ordered-monoid : has-ordered-monoid (FiniteSupport 𝒟 cmp)
-  fin-support-ordered-monoid = right-invariant→has-ordered-monoid (FiniteSupport 𝒟 cmp) λ {xs} {ys} {zs} xs≤ys →
-    ⊎-mapl fin-support-list-path (≤-right-invariant 𝒟-ordered-monoid cmp (⊎-mapl (ap FinSupportList.support) xs≤ys))
+  fin-support-ordered-monoid : has-ordered-monoid (FiniteSupport 𝒟 _≡?_)
+  fin-support-ordered-monoid = right-invariant→has-ordered-monoid (FiniteSupport 𝒟 _≡?_) λ {xs} {ys} {zs} xs≤ys →
+    ⊎-mapl fin-support-list-path (≤-right-invariant 𝒟-ordered-monoid _≡?_ (⊎-mapl (ap FinSupportList.support) xs≤ys))
 
 --------------------------------------------------------------------------------
 -- Extensionality based on 'finite-support-list' and eventually 'index-inj'
@@ -158,10 +157,10 @@ module _
 module _ {o r}
   {𝒟 : Displacement-algebra o r}
   (let module 𝒟 = Displacement-algebra 𝒟)
-  {cmp : ∀ x y → Tri 𝒟._<_ x y}
+  {_≡?_ : Discrete ⌞ 𝒟 ⌟}
   where
-  module 𝒩 = NearlyConst 𝒟 cmp
-  open FinSupport 𝒟 cmp
+  module 𝒩 = NearlyConst 𝒟 _≡?_
+  open FinSupport 𝒟 _≡?_
   open FinSupportList
 
   Extensional-FinSupportList : ∀ {ℓr} ⦃ s : Extensional 𝒩.SupportList ℓr ⦄ → Extensional FinSupportList ℓr

diff --git a/src/Mugen/Algebra/Displacement/NearlyConstant.agda b/src/Mugen/Algebra/Displacement/NearlyConstant.agda
@@ -44,21 +44,11 @@ open import Mugen.Data.List
 module NearlyConst
   {o r}
   (𝒟 : Displacement-algebra o r)
-  (let module 𝒟 = Displacement-algebra 𝒟)
-  (cmp : ∀ x y → Tri 𝒟._<_ x y)
+  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
   where
-  open 𝒟 using (ε; _⊗_)
+  private module 𝒟 = Displacement-algebra 𝒟
   open Inf 𝒟
 
-  _≡?_ : Discrete ⌞ 𝒟 ⌟
-  x ≡? y =
-    tri-elim
-      (λ _ → Dec (x ≡ y))
-      (λ x<y → no λ x≡y → 𝒟.<→≠ x<y x≡y)
-      yes
-      (λ y<x → no λ x≡y → 𝒟.<→≠ y<x (sym x≡y))
-      (cmp x y)
-
   --------------------------------------------------------------------------------
   -- Raw Support Lists
   --
@@ -310,11 +300,11 @@ module NearlyConst
   merge-with f xs ys .has-is-compact = Raw.compact-is-compact $ Raw.merge-with f (xs .list) (ys .list)
 
   merge : SupportList → SupportList → SupportList
-  merge = merge-with _⊗_
+  merge = merge-with 𝒟._⊗_
 
   -- The empty SupportList
   empty : SupportList
-  empty .list = raw [] ε
+  empty .list = raw [] 𝒟.ε
   empty .has-is-compact = lift tt
 
   _<_ : SupportList → SupportList → Type (o ⊔ r)
@@ -332,14 +322,14 @@ module NearlyConst
       Raw.index-compact (Raw.merge-with f (xs .list) (ys .list)) n
       ∙ Raw.index-merge-with f (xs .list) (ys .list) n
 
-    index-merge : ∀ xs ys n → index (merge xs ys) n ≡ index xs n ⊗ index ys n
-    index-merge = index-merge-with _⊗_
+    index-merge : ∀ xs ys n → index (merge xs ys) n ≡ (index xs n 𝒟.⊗ index ys n)
+    index-merge = index-merge-with 𝒟._⊗_
 
     base-merge-with : ∀ f xs ys → merge-with f xs ys .base ≡ f (xs .base) (ys .base)
     base-merge-with f xs ys = Raw.base-compact (Raw.merge-with f (xs .list) (ys .list))
 
-    base-merge : ∀ xs ys → merge xs ys .base ≡ xs .base ⊗ ys .base
-    base-merge = base-merge-with _⊗_
+    base-merge : ∀ xs ys → merge xs ys .base ≡ (xs .base 𝒟.⊗ ys .base)
+    base-merge = base-merge-with 𝒟._⊗_
 
   abstract
     index-inj : ∀ {xs ys} → ((n : Nat) → index xs n ≡ index ys n) → xs ≡ ys
@@ -359,10 +349,10 @@ module NearlyConst
 --------------------------------------------------------------------------------
 -- Bundled Instances
 
-module _ {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri (Displacement-algebra._<_ 𝒟) x y) where
+module _ {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
   private module 𝒟 = Displacement-algebra 𝒟
   open Inf 𝒟
-  open NearlyConst 𝒟 cmp
+  open NearlyConst 𝒟 _≡?_
 
   NearlyConstant : Displacement-algebra o (o ⊔ r)
   NearlyConstant = to-displacement-algebra mk where
@@ -400,12 +390,12 @@ module _ {o r} (𝒟 : Displacement-algebra o r) (cmp : ∀ x y → Tri (Displac
 --------------------------------------------------------------------------------
 -- Subalgebra Structure
 
-module _ {o r} {𝒟 : Displacement-algebra o r} (cmp : ∀ x y → Tri (Displacement-algebra._<_ 𝒟) x y) where
-  open NearlyConst 𝒟 cmp
+module _ {o r} {𝒟 : Displacement-algebra o r} (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
+  open NearlyConst 𝒟 _≡?_
 
-  NearlyConstant⊆InfProd : is-displacement-subalgebra (NearlyConstant 𝒟 cmp) (InfProd 𝒟)
+  NearlyConstant⊆InfProd : is-displacement-subalgebra (NearlyConstant 𝒟 _≡?_) (InfProd 𝒟)
   NearlyConstant⊆InfProd = to-displacement-subalgebra mk where
-    mk : make-displacement-subalgebra (NearlyConstant 𝒟 cmp) (InfProd 𝒟)
+    mk : make-displacement-subalgebra (NearlyConstant 𝒟 _≡?_) (InfProd 𝒟)
     mk .make-displacement-subalgebra.into = index
     mk .make-displacement-subalgebra.pres-ε = refl
     mk .make-displacement-subalgebra.pres-⊗ xs ys = funext (index-merge xs ys)
@@ -418,37 +408,38 @@ module _ {o r} {𝒟 : Displacement-algebra o r} (cmp : ∀ x y → Tri (Displac
 module _
   {o r}
   {𝒟 : Displacement-algebra o r}
-  (let module 𝒟 = Displacement-algebra 𝒟)
   (𝒟-ordered-monoid : has-ordered-monoid 𝒟)
-  (cmp : ∀ x y → Tri 𝒟._<_ x y)
+  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
   where
-  open NearlyConst 𝒟 cmp
+  private module 𝒟 = Displacement-algebra 𝒟
+  open NearlyConst 𝒟 _≡?_
   open is-ordered-monoid 𝒟-ordered-monoid
 
   ≤-right-invariant : ∀ {xs ys zs} → xs ≤ ys → merge xs zs ≤ merge ys zs
   ≤-right-invariant {xs} {ys} {zs} xs≤ys = ≤-pointwise→≤ λ n →
     coe1→0 (λ i → index-merge xs zs n i 𝒟.≤ index-merge ys zs n i) $
     right-invariant (≤→≤-pointwise xs≤ys n)
 
-  nearly-constant-has-ordered-monoid : has-ordered-monoid (NearlyConstant 𝒟 cmp)
-  nearly-constant-has-ordered-monoid = right-invariant→has-ordered-monoid (NearlyConstant 𝒟 cmp) ≤-right-invariant
+  nearly-constant-has-ordered-monoid : has-ordered-monoid (NearlyConstant 𝒟 _≡?_)
+  nearly-constant-has-ordered-monoid = right-invariant→has-ordered-monoid (NearlyConstant 𝒟 _≡?_) ≤-right-invariant
 
 --------------------------------------------------------------------------------
 -- Joins
 
 module NearlyConstJoins
   {o r}
   {𝒟 : Displacement-algebra o r}
-  (let module 𝒟 = Displacement-algebra 𝒟)
-  (𝒟-joins : has-joins 𝒟) (cmp : ∀ x y → Tri 𝒟._<_ x y)
+  (𝒟-joins : has-joins 𝒟)
+  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
   where
-  open NearlyConst 𝒟 cmp
+  open NearlyConst 𝒟 _≡?_
+  private module 𝒟 = Displacement-algebra 𝒟
   private module 𝒥 = has-joins 𝒟-joins
 
   join : SupportList → SupportList → SupportList
   join = merge-with 𝒥.join
 
-  nearly-constant-has-joins : has-joins (NearlyConstant 𝒟 cmp)
+  nearly-constant-has-joins : has-joins (NearlyConstant 𝒟 _≡?_)
   nearly-constant-has-joins .has-joins.join = join
   nearly-constant-has-joins .has-joins.joinl {xs} {ys} =
     ≤-pointwise→≤ λ n → 𝒟.≤+≡→≤ 𝒥.joinl (sym $ index-merge-with 𝒥.join xs ys n)
@@ -468,7 +459,7 @@ module NearlyConstJoins
     open InfProperties {𝒟 = 𝒟} _≡?_ 𝒟-wlpo
 
     nearly-constant-is-subsemilattice : is-displacement-subsemilattice nearly-constant-has-joins (⊗∞-has-joins 𝒟-joins)
-    nearly-constant-is-subsemilattice .is-displacement-subsemilattice.has-displacement-subalgebra = NearlyConstant⊆InfProd cmp
+    nearly-constant-is-subsemilattice .is-displacement-subsemilattice.has-displacement-subalgebra = NearlyConstant⊆InfProd _≡?_
     nearly-constant-is-subsemilattice .is-displacement-subsemilattice.pres-joins x y = funext (index-preserves-join x y)
 
 --------------------------------------------------------------------------------
@@ -477,38 +468,36 @@ module NearlyConstJoins
 module _
   {o r}
   {𝒟 : Displacement-algebra o r}
-  (let module 𝒟 = Displacement-algebra 𝒟)
   (𝒟-bottom : has-bottom 𝒟)
-  (cmp : ∀ x y → Tri (Displacement-algebra._<_ 𝒟) x y) (b : ⌞ 𝒟 ⌟)
+  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
   where
-  open 𝒟 using (ε; _⊗_; _<_; _≤_)
-  open NearlyConst 𝒟 cmp
-  open Inf 𝒟
-  open SupportList
+  private module 𝒟 = Displacement-algebra 𝒟
+  open NearlyConst 𝒟 _≡?_
   open has-bottom 𝒟-bottom
 
-  nearly-constant-has-bottom : has-bottom (NearlyConstant 𝒟 cmp)
+  nearly-constant-has-bottom : has-bottom (NearlyConstant 𝒟 _≡?_)
   nearly-constant-has-bottom .has-bottom.bot = support-list (raw [] bot) (lift tt)
   nearly-constant-has-bottom .has-bottom.is-bottom xs = ≤-pointwise→≤ λ n → is-bottom _
 
   module _ (𝒟-wlpo : WLPO 𝒟.strict-order _≡?_) where
     open InfProperties {𝒟 = 𝒟} _≡?_ 𝒟-wlpo
 
     nearly-constant-is-bounded-subalgebra : is-bounded-displacement-subalgebra nearly-constant-has-bottom (⊗∞-has-bottom 𝒟-bottom)
-    nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.has-displacement-subalgebra = NearlyConstant⊆InfProd cmp
+    nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.has-displacement-subalgebra = NearlyConstant⊆InfProd _≡?_
     nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.pres-bottom = refl
 
 --------------------------------------------------------------------------------
 -- Extensionality based on 'index-inj'
 
--- 1lab's or Agda's instance search somehow does not seem to deal with
--- explicit arguments, so we re-parametrize things with implicit '𝒟' and 'cmp'.
+-- FIXME: Need to check the accuracy of the following statement again:
+-- 1lab's or Agda's instance search somehow does not seem to deal with explicit arguments?
+-- So we re-parametrize things with implicit '𝒟' and '_≡?_'.
 module _ {o r}
   {𝒟 : Displacement-algebra o r}
-  (let module 𝒟 = Displacement-algebra 𝒟)
-  {cmp : ∀ x y → Tri 𝒟._<_ x y}
+  {_≡?_ : Discrete ⌞ 𝒟 ⌟}
   where
-  open NearlyConst 𝒟 cmp
+  private module 𝒟 = Displacement-algebra 𝒟
+  open NearlyConst 𝒟 _≡?_
 
   Extensional-SupportList : ∀ {ℓr} ⦃ s : Extensional ⌞ 𝒟 ⌟ ℓr ⦄ → Extensional SupportList ℓr
   Extensional-SupportList ⦃ s ⦄ .Pathᵉ xs ys =

diff --git a/src/Mugen/Order/StrictOrder.agda b/src/Mugen/Order/StrictOrder.agda
@@ -222,31 +222,6 @@ strictly-monotone-∘ f g .hom x = f # (g # x)
 strictly-monotone-∘ f g .strict-mono p =
   f .strict-mono (g .strict-mono p)
 
---------------------------------------------------------------------------------
--- Decidability
-
-data Tri {o r} {A : Type o} (_<_ : A → A → Type r) (x y : A) : Type (o ⊔ r) where
-  lt : x < y → Tri _<_ x y
-  eq : x ≡ y → Tri _<_ x y
-  gt : y < x → Tri _<_ x y
-
-module _ {o r} {A : Type o} {_<_ : A → A → Type r} where
-
-
-  tri-elim : ∀ {ℓ x y} (P : Tri _<_ x y → Type ℓ)
-             → ((p : x < y) → P (lt p))
-             → ((p : x ≡ y) → P (eq p))
-             → ((p : y < x) → P (gt p))
-             → (t : Tri _<_ x y) → P t
-  tri-elim P plt peq pgt (lt x) = plt x
-  tri-elim P plt peq pgt (eq x) = peq x
-  tri-elim P plt peq pgt (gt x) = pgt x
-
-  tri-rec : ∀ {ℓ x y} {R : Type ℓ} → R → R → R → Tri _<_ x y → R
-  tri-rec rlt req rgt (lt x) = rlt
-  tri-rec rlt req rgt (eq x) = req
-  tri-rec rlt req rgt (gt x) = rgt
-
 --------------------------------------------------------------------------------
 -- Builders