Skip to content

Commit 42ff68a

Browse files
LorenzoMolenaLorenzoMolena
committed
add instances of Nat and Int as Pseudolattices, and of Int as OrderedCommRing 
1 parent 904aa21 commit 42ff68a

File tree

7 files changed

+163
-1
lines changed

7 files changed

+163
-1
lines changed

‎Cubical/Algebra/OrderedCommRing/Base.agda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
module Cubical.Algebra.OrderedCommRing.Base where
22
{-
3-
Definition of an commutative ordered ring.
3+
Definition of an ordered commutative ring.
44
-}
55

66
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/OrderedCommRing/Instances/Int.agda‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
module Cubical.Algebra.OrderedCommRing.Instances.Int where
2+
3+
open import Cubical.Foundations.Prelude
4+
open import Cubical.Foundations.Function
5+
open import Cubical.Foundations.Equiv
6+
7+
open import Cubical.Data.Empty as ⊥
8+
9+
open import Cubical.HITs.PropositionalTruncation
10+
11+
open import Cubical.Data.Int as ℤ
12+
renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
13+
open import Cubical.Data.Int.Order
14+
renaming (_<_ to _<ℤ_ ; _≤_ to _≤ℤ_)
15+
16+
open import Cubical.Algebra.CommRing
17+
open import Cubical.Algebra.CommRing.Instances.Int
18+
19+
open import Cubical.Algebra.OrderedCommRing
20+
21+
open import Cubical.Relation.Nullary
22+
23+
open import Cubical.Relation.Binary.Order.StrictOrder
24+
open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Int
25+
26+
open import Cubical.Relation.Binary.Order.Pseudolattice
27+
open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Int
28+
29+
open CommRingStr
30+
open OrderedCommRingStr
31+
open PseudolatticeStr
32+
open StrictOrderStr
33+
34+
ℤOrderedCommRing : OrderedCommRing ℓ-zero ℓ-zero
35+
fst ℤOrderedCommRing = ℤ
36+
0r (snd ℤOrderedCommRing) = 0
37+
1r (snd ℤOrderedCommRing) = 1
38+
_+_ (snd ℤOrderedCommRing) = _+ℤ_
39+
_·_ (snd ℤOrderedCommRing) = _·ℤ_
40+
-_ (snd ℤOrderedCommRing) = -ℤ_
41+
_<_ (snd ℤOrderedCommRing) = _<ℤ_
42+
_≤_ (snd ℤOrderedCommRing) = _≤ℤ_
43+
isOrderedCommRing (snd ℤOrderedCommRing) = isOrderedCommRingℤ
44+
where
45+
open IsOrderedCommRing
46+
47+
isOrderedCommRingℤ : IsOrderedCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_ _<ℤ_ _≤ℤ_
48+
isOrderedCommRingℤ .isCommRing = ℤCommRing .snd .isCommRing
49+
isOrderedCommRingℤ .isPseudolattice = ℤ≤Pseudolattice .snd .is-pseudolattice
50+
isOrderedCommRingℤ .isStrictOrder = ℤ<StrictOrder .snd .isStrictOrder
51+
isOrderedCommRingℤ .<-≤-weaken = λ _ _ → <-weaken
52+
isOrderedCommRingℤ .≤≃¬> = λ x y →
53+
propBiimpl→Equiv isProp≤ (isProp¬ (y <ℤ x))
54+
(λ x≤y y<x → isIrrefl< (≤<-trans x≤y y<x))
55+
(λ ¬y<x → case x ≟ y return (λ _ → x ≤ℤ y) of λ {
56+
(lt x<y) → <-weaken x<y ;
57+
(eq x≡y) → subst (x ≤ℤ_) x≡y isRefl≤ ;
58+
(gt y<z) → ⊥.rec (¬y<x y<z) })
59+
isOrderedCommRingℤ .+MonoR≤ = λ _ _ z → ≤-+o {o = z}
60+
isOrderedCommRingℤ .+MonoR< = λ _ _ z → <-+o {o = z}
61+
isOrderedCommRingℤ .posSum→pos∨pos = λ _ _ → ∣_∣₁ ∘ 0<+ _ _
62+
isOrderedCommRingℤ .<-≤-trans = λ _ _ _ → <≤-trans
63+
isOrderedCommRingℤ .≤-<-trans = λ _ _ _ → ≤<-trans
64+
isOrderedCommRingℤ .·MonoR≤ = λ _ _ _ → 0≤o→≤-·o
65+
isOrderedCommRingℤ .·MonoR< = λ _ _ _ → 0<o→<-·o
66+
isOrderedCommRingℤ .0<1 = isRefl≤

‎Cubical/Data/Int/Order.agda‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ open import Cubical.Data.Int.Properties as ℤ
1010
open import Cubical.Data.Nat as ℕ
1111
open import Cubical.Data.NatPlusOne.Base as ℕ₊₁
1212
open import Cubical.Data.Sigma
13+
open import Cubical.Data.Sum
1314

1415
open import Cubical.Relation.Nullary
1516

@@ -450,6 +451,18 @@ min≤ {negsuc (suc m)} {negsuc (suc n)} = pred-≤-pred (subst (_≤ negsuc m)
450451
cong₂ ℤ.max (≤→max m≤n) (≤→max o≤s))
451452
(≤max {m = ℤ.max m o} {n = ℤ.max n s})
452453

454+
0<+ : ∀ m n → 0 < m ℤ.+ n → (0 < m) ⊎ (0 < n)
455+
0<+ (pos zero) (pos zero) = ⊥.rec ∘ isIrrefl<
456+
0<+ (pos zero) (pos (suc n)) = inr ∘ subst (0 <_) (sym $ pos0+ _)
457+
0<+ (pos (suc m)) (pos n) = λ _ → inl (suc-≤-suc zero-≤pos)
458+
0<+ (pos zero) (negsuc n) = ⊥.rec ∘ ¬pos≤negsuc ∘ subst (0 <_)
459+
(sym $ pos0+ (negsuc n))
460+
0<+ (pos (suc m)) (negsuc n) = λ _ → inl (suc-≤-suc zero-≤pos)
461+
0<+ (negsuc m) (pos zero) = ⊥.rec ∘ ¬pos≤negsuc
462+
0<+ (negsuc m) (pos (suc n)) = λ _ → inr (suc-≤-suc zero-≤pos)
463+
0<+ (negsuc m) (negsuc n) = ⊥.rec ∘ ¬pos≤negsuc ∘ subst (0 <_)
464+
(sym $ neg+ (suc m) (suc n))
465+
453466
≤Dec : ∀ m n → Dec (m ≤ n)
454467
≤Dec (pos zero) (pos n) = yes zero-≤pos
455468
≤Dec (pos (suc m)) (pos zero) = no ¬-pos<-zero

‎Cubical/Data/Nat/Order.agda‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -277,6 +277,20 @@ min-≤-right {zero} {n} = zero-≤
277277
min-≤-right {suc m} {zero} = ≤-refl
278278
min-≤-right {suc m} {suc n} = subst (_≤ _) (sym minSuc) $ suc-≤-suc $ min-≤-right {m} {n}
279279

280+
maxLUB : ∀ {x} → m ≤ x → n ≤ x → max m n ≤ x
281+
maxLUB {zero} {n} _ n≤x = n≤x
282+
maxLUB {suc m} {zero} sm≤x _ = sm≤x
283+
maxLUB {suc m} {suc n} sm≤x sn≤x with m <ᵇ n
284+
... | false = sm≤x
285+
... | true = sn≤x
286+
287+
minGLB : ∀ {x} → x ≤ m → x ≤ n → x ≤ min m n
288+
minGLB {zero} {n} x≤0 _ = x≤0
289+
minGLB {suc m} {zero} _ x≤0 = x≤0
290+
minGLB {suc m} {suc n} x≤sm x≤sn with m <ᵇ n
291+
... | false = x≤sn
292+
... | true = x≤sm
293+
280294
-- Boolean order relations and their conversions to/from ≤ and <
281295

282296
_≤ᵇ_ : ℕ → ℕ → Bool

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

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
module Cubical.Relation.Binary.Order.Pseudolattice.Base where
22

33
open import Cubical.Foundations.Prelude
4+
open import Cubical.Foundations.Function
5+
open import Cubical.Foundations.Equiv
6+
open import Cubical.Foundations.HLevels
47
open import Cubical.Foundations.SIP
58

69
open import Cubical.Relation.Binary.Base
@@ -57,3 +60,33 @@ makeIsPseudolattice {_≤_ = _≤_} is-setL is-prop-valued is-refl is-trans is-a
5760
PS : IsPseudolattice _≤_
5861
PS .IsPseudolattice.isPoset = isposet is-setL is-prop-valued is-refl is-trans is-antisym
5962
PS .IsPseudolattice.isPseudolattice = is-meet-semipseudolattice , is-join-semipseudolattice
63+
64+
module _
65+
(P : Poset ℓ ℓ') (_∧_ _∨_ : ⟨ P ⟩ → ⟨ P ⟩ → ⟨ P ⟩) where
66+
open PosetStr (str P) renaming (_≤_ to infix 8 _≤_)
67+
module _
68+
(π₁ : ∀ {a b} → a ∧ b ≤ a)
69+
(π₂ : ∀ {a b} → a ∧ b ≤ b)
70+
(ϕ : ∀ {a b x} → x ≤ a → x ≤ b → x ≤ a ∧ b)
71+
(ι₁ : ∀ {a b} → a ≤ a ∨ b)
72+
(ι₂ : ∀ {a b} → b ≤ a ∨ b)
73+
(ψ : ∀ {a b x} → a ≤ x → b ≤ x → a ∨ b ≤ x) where
74+
75+
makePseudolatticeFromPoset : Pseudolattice ℓ ℓ'
76+
makePseudolatticeFromPoset .fst = ⟨ P ⟩
77+
makePseudolatticeFromPoset .snd .PseudolatticeStr._≤_ = (str P) .PosetStr._≤_
78+
makePseudolatticeFromPoset .snd .PseudolatticeStr.is-pseudolattice = isPL where
79+
isPL : IsPseudolattice _≤_
80+
isPL .IsPseudolattice.isPoset = isPoset
81+
isPL .IsPseudolattice.isPseudolattice .fst a b .fst = a ∧ b
82+
isPL .IsPseudolattice.isPseudolattice .fst a b .snd x = propBiimpl→Equiv
83+
(is-prop-valued _ _)
84+
(isProp× (is-prop-valued _ _) (is-prop-valued _ _))
85+
(λ x≤a∧b → is-trans _ _ _ x≤a∧b π₁ , is-trans _ _ _ x≤a∧b π₂)
86+
(uncurry ϕ)
87+
isPL .IsPseudolattice.isPseudolattice .snd a b .fst = a ∨ b
88+
isPL .IsPseudolattice.isPseudolattice .snd a b .snd x = propBiimpl→Equiv
89+
(is-prop-valued _ _)
90+
(isProp× (is-prop-valued _ _) (is-prop-valued _ _))
91+
(λ a∨b≤x → is-trans _ _ _ ι₁ a∨b≤x , is-trans _ _ _ ι₂ a∨b≤x)
92+
(uncurry ψ)

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
module Cubical.Relation.Binary.Order.Pseudolattice.Instances.Int where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Data.Int
6+
open import Cubical.Data.Int.Order renaming (_≤_ to _≤ℤ_)
7+
8+
open import Cubical.Relation.Binary.Order.Poset.Instances.Int
9+
open import Cubical.Relation.Binary.Order.Pseudolattice
10+
11+
ℤ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
12+
ℤ≤Pseudolattice = makePseudolatticeFromPoset ℤ≤Poset min max
13+
min≤
14+
(λ {a b} → subst (_≤ℤ b) (minComm b a) min≤)
15+
(λ {a b} x≤a x≤b → subst (_≤ℤ min a b) (minIdem _) (≤MonotoneMin x≤a x≤b))
16+
≤max
17+
(λ {a b} → subst (b ≤ℤ_) (maxComm b a) ≤max)
18+
(λ {a b} a≤x b≤x → subst (max a b ≤ℤ_) (maxIdem _) (≤MonotoneMax a≤x b≤x))

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
module Cubical.Relation.Binary.Order.Pseudolattice.Instances.Nat where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Data.Nat
6+
open import Cubical.Data.Nat.Order renaming (_≤_ to _≤ℕ_)
7+
8+
open import Cubical.Relation.Binary.Order.Poset.Instances.Nat
9+
open import Cubical.Relation.Binary.Order.Pseudolattice
10+
11+
ℕ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
12+
ℕ≤Pseudolattice = makePseudolatticeFromPoset ℕ≤Poset min max
13+
min-≤-left
14+
(λ {a b} → min-≤-right {a} {b})
15+
minGLB
16+
left-≤-max
17+
(λ {a b} → right-≤-max {b} {a})
18+
maxLUB

0 commit comments

Comments
 (0)