Instances for Pseudolattice and OrderedCommRing

Cubical/Algebra/OrderedCommRing/Base.agda

@@ -1,6 +1,6 @@
 module Cubical.Algebra.OrderedCommRing.Base where
 {-
-  Definition of an commutative ordered ring.
+  Definition of an ordered commutative ring.
 -}
 
 open import Cubical.Foundations.Prelude

Cubical/Algebra/OrderedCommRing/Instances/Int.agda

@@ -0,0 +1,83 @@
+module Cubical.Algebra.OrderedCommRing.Instances.Int where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+
+import Cubical.Functions.Logic as L
+
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty as ⊥
+
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Data.Int as ℤ
+  renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
+open import Cubical.Data.Int.Order
+  renaming (_<_ to _<ℤ_ ; _≤_ to _≤ℤ_)
+open import Cubical.Data.Nat using (ℕ ; zero ; suc)
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Instances.Int
+
+open import Cubical.Algebra.OrderedCommRing
+
+open import Cubical.Relation.Nullary
+
+open import Cubical.Relation.Binary.Order.StrictOrder
+open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Int
+
+open import Cubical.Relation.Binary.Order.Pseudolattice
+open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Int
+
+open CommRingStr
+open OrderedCommRingStr
+open PseudolatticeStr
+open StrictOrderStr
+
+private
+  lemma0<+ : ∀ x y → 0 <ℤ x +ℤ y → (0 <ℤ x) L.⊔′ (0 <ℤ y)
+  lemma0<+ (pos zero)    (pos zero)    = ⊥.rec ∘ isIrrefl<
+  lemma0<+ (pos zero)    (pos (suc n)) = ∣_∣₁ ∘ inr ∘ subst (0 <ℤ_) (sym $ pos0+ _)
+  lemma0<+ (pos (suc m)) (pos n)       = λ _ → ∣ inl (suc-≤-suc zero-≤pos) ∣₁
+  lemma0<+ (pos zero)    (negsuc n)    = ⊥.rec ∘ ¬pos≤negsuc ∘ subst (0 <ℤ_)
+                                        (sym $ pos0+ (negsuc n))
+  lemma0<+ (pos (suc m)) (negsuc n)    = λ _ → ∣ inl (suc-≤-suc zero-≤pos) ∣₁
+  lemma0<+ (negsuc m)    (pos zero)    = ⊥.rec ∘ ¬pos≤negsuc
+  lemma0<+ (negsuc m)    (pos (suc n)) = λ _ → ∣ inr (suc-≤-suc zero-≤pos) ∣₁
+  lemma0<+ (negsuc m)    (negsuc n)    = ⊥.rec ∘ ¬pos≤negsuc ∘ subst (0 <ℤ_)
+                                        (sym $ neg+ (suc m) (suc n))
+
+ℤOrderedCommRing : OrderedCommRing ℓ-zero ℓ-zero
+fst ℤOrderedCommRing = ℤ
+0r  (snd ℤOrderedCommRing) = 0
+1r  (snd ℤOrderedCommRing) = 1
+_+_ (snd ℤOrderedCommRing) = _+ℤ_
+_·_ (snd ℤOrderedCommRing) = _·ℤ_
+-_  (snd ℤOrderedCommRing) = -ℤ_
+_<_ (snd ℤOrderedCommRing) = _<ℤ_
+_≤_ (snd ℤOrderedCommRing) = _≤ℤ_
+isOrderedCommRing (snd ℤOrderedCommRing) = isOrderedCommRingℤ
+  where
+    open IsOrderedCommRing
+
+    isOrderedCommRingℤ : IsOrderedCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_ _<ℤ_ _≤ℤ_
+    isOrderedCommRingℤ .isCommRing      = ℤCommRing .snd .isCommRing
+    isOrderedCommRingℤ .isPseudolattice = ℤ≤Pseudolattice .snd .is-pseudolattice
+    isOrderedCommRingℤ .isStrictOrder   = ℤ<StrictOrder .snd .isStrictOrder
+    isOrderedCommRingℤ .<-≤-weaken      = λ _ _ → <-weaken
+    isOrderedCommRingℤ .≤≃¬>            = λ x y →
+      propBiimpl→Equiv isProp≤ (isProp¬ (y <ℤ x))
+        (λ x≤y y<x → isIrrefl< (≤<-trans x≤y y<x))
+        (λ ¬y<x → case x ≟ y return (λ _ → x ≤ℤ y) of λ {
+          (lt x<y) → <-weaken x<y ;
+          (eq x≡y) → subst (x ≤ℤ_) x≡y isRefl≤ ;
+          (gt y<z) → ⊥.rec (¬y<x y<z) })
+    isOrderedCommRingℤ .+MonoR≤         = λ _ _ z → ≤-+o {o = z}
+    isOrderedCommRingℤ .+MonoR<         = λ _ _ z → <-+o {o = z}
+    isOrderedCommRingℤ .posSum→pos∨pos  = lemma0<+
+    isOrderedCommRingℤ .<-≤-trans       = λ _ _ _ → <≤-trans
+    isOrderedCommRingℤ .≤-<-trans       = λ _ _ _ → ≤<-trans
+    isOrderedCommRingℤ .·MonoR≤         = λ _ _ _ → 0≤o→≤-·o
+    isOrderedCommRingℤ .·MonoR<         = λ _ _ _ → 0<o→<-·o
+    isOrderedCommRingℤ .0<1             = isRefl≤

Cubical/Data/Nat/Order.agda

@@ -277,6 +277,20 @@ min-≤-right {zero} {n} = zero-≤
 min-≤-right {suc m} {zero} = ≤-refl
 min-≤-right {suc m} {suc n} = subst (_≤ _) (sym minSuc) $ suc-≤-suc $ min-≤-right {m} {n}
 
+maxLUB : ∀ {x} → m ≤ x → n ≤ x → max m n ≤ x
+maxLUB {zero}  {n}     _    n≤x  = n≤x
+maxLUB {suc m} {zero}  sm≤x _    = sm≤x
+maxLUB {suc m} {suc n} sm≤x sn≤x with m <ᵇ n
+... | false = sm≤x
+... | true  = sn≤x
+
+minGLB : ∀ {x} → x ≤ m → x ≤ n → x ≤ min m n
+minGLB {zero}  {n}     x≤0 _     = x≤0
+minGLB {suc m} {zero}  _   x≤0   = x≤0
+minGLB {suc m} {suc n} x≤sm x≤sn with m <ᵇ n
+... | false = x≤sn
+... | true  = x≤sm
+
 -- Boolean order relations and their conversions to/from ≤ and <
 
 _≤ᵇ_ : ℕ → ℕ → Bool

Cubical/Relation/Binary/Order/Pseudolattice/Base.agda

@@ -1,6 +1,9 @@
 module Cubical.Relation.Binary.Order.Pseudolattice.Base where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.SIP
 
 open import Cubical.Relation.Binary.Base
@@ -57,3 +60,33 @@ makeIsPseudolattice {_≤_ = _≤_} is-setL is-prop-valued is-refl is-trans is-a
     PS : IsPseudolattice _≤_
     PS .IsPseudolattice.isPoset = isposet is-setL is-prop-valued is-refl is-trans is-antisym
     PS .IsPseudolattice.isPseudolattice = is-meet-semipseudolattice , is-join-semipseudolattice
+
+module _
+  (P : Poset ℓ ℓ') (_∧_ _∨_ : ⟨ P ⟩ → ⟨ P ⟩ → ⟨ P ⟩) where
+  open PosetStr (str P) renaming (_≤_ to infix 8 _≤_)
+  module _
+    (π₁ : ∀ {a b}   → a ∧ b ≤ a)
+    (π₂ : ∀ {a b}   → a ∧ b ≤ b)
+    (ϕ  : ∀ {a b x} → x ≤ a → x ≤ b → x ≤ a ∧ b)
+    (ι₁ : ∀ {a b}   → a ≤ a ∨ b)
+    (ι₂ : ∀ {a b}   → b ≤ a ∨ b)
+    (ψ  : ∀ {a b x} → a ≤ x → b ≤ x → a ∨ b ≤ x) where
+
+    makePseudolatticeFromPoset : Pseudolattice ℓ ℓ'
+    makePseudolatticeFromPoset .fst = ⟨ P ⟩
+    makePseudolatticeFromPoset .snd .PseudolatticeStr._≤_ = (str P) .PosetStr._≤_
+    makePseudolatticeFromPoset .snd .PseudolatticeStr.is-pseudolattice = isPL where
+      isPL : IsPseudolattice _≤_
+      isPL .IsPseudolattice.isPoset = isPoset
+      isPL .IsPseudolattice.isPseudolattice .fst a b .fst = a ∧ b
+      isPL .IsPseudolattice.isPseudolattice .fst a b .snd x = propBiimpl→Equiv
+        (is-prop-valued _ _)
+        (isProp× (is-prop-valued _ _) (is-prop-valued _ _))
+        (λ x≤a∧b → is-trans _ _ _ x≤a∧b π₁ , is-trans _ _ _ x≤a∧b π₂)
+        (uncurry ϕ)
+      isPL .IsPseudolattice.isPseudolattice .snd a b .fst = a ∨ b
+      isPL .IsPseudolattice.isPseudolattice .snd a b .snd x = propBiimpl→Equiv
+        (is-prop-valued _ _)
+        (isProp× (is-prop-valued _ _) (is-prop-valued _ _))
+        (λ a∨b≤x → is-trans _ _ _ ι₁ a∨b≤x , is-trans _ _ _ ι₂ a∨b≤x)
+        (uncurry ψ)

Cubical/Relation/Binary/Order/Pseudolattice/Instances/Int.agda

@@ -0,0 +1,18 @@
+module Cubical.Relation.Binary.Order.Pseudolattice.Instances.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Int
+open import Cubical.Data.Int.Order renaming (_≤_ to _≤ℤ_)
+
+open import Cubical.Relation.Binary.Order.Poset.Instances.Int
+open import Cubical.Relation.Binary.Order.Pseudolattice
+
+ℤ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
+ℤ≤Pseudolattice = makePseudolatticeFromPoset ℤ≤Poset min max
+  min≤
+  (λ {a b} → subst (_≤ℤ b) (minComm b a) min≤)
+  (λ {a b} x≤a x≤b → subst (_≤ℤ min a b) (minIdem _) (≤MonotoneMin x≤a x≤b))
+  ≤max
+  (λ {a b} → subst (b ≤ℤ_) (maxComm b a) ≤max)
+  (λ {a b} a≤x b≤x → subst (max a b ≤ℤ_) (maxIdem _) (≤MonotoneMax a≤x b≤x))

Cubical/Relation/Binary/Order/Pseudolattice/Instances/Nat.agda

@@ -0,0 +1,18 @@
+module Cubical.Relation.Binary.Order.Pseudolattice.Instances.Nat where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order renaming (_≤_ to _≤ℕ_)
+
+open import Cubical.Relation.Binary.Order.Poset.Instances.Nat
+open import Cubical.Relation.Binary.Order.Pseudolattice
+
+ℕ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
+ℕ≤Pseudolattice = makePseudolatticeFromPoset ℕ≤Poset min max
+  min-≤-left
+  (λ {a b} → min-≤-right {a} {b})
+  minGLB
+  left-≤-max
+  (λ {a b} → right-≤-max {b} {a})
+  maxLUB