Skip to content

Commit 8c2aad4

Browse files
LorenzoMolenaLorenzoMolena
committed
add Rationals.Fast instances as some algebraic and order structures
1 parent f90b3d4 commit 8c2aad4

File tree

9 files changed

+211
-0
lines changed

9 files changed

+211
-0
lines changed

‎Cubical/Algebra/CommRing/Instances/Rationals/Fast.agda‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
{- ℚ is a CommRing -}
2+
3+
module Cubical.Algebra.CommRing.Instances.Rationals.Fast where
4+
5+
open import Cubical.Foundations.Prelude
6+
open import Cubical.Algebra.CommRing
7+
open import Cubical.Data.Rationals.Fast as ℚ
8+
9+
ℚCommRing : CommRing ℓ-zero
10+
ℚCommRing .fst = ℚ
11+
ℚCommRing .snd .CommRingStr.0r = 0
12+
ℚCommRing .snd .CommRingStr.1r = 1
13+
ℚCommRing .snd .CommRingStr._+_ = _+_
14+
ℚCommRing .snd .CommRingStr._·_ = _·_
15+
ℚCommRing .snd .CommRingStr.-_ = -_
16+
ℚCommRing .snd .CommRingStr.isCommRing = p
17+
where
18+
p : IsCommRing 0 1 _+_ _·_ (-_)
19+
p = makeIsCommRing isSetℚ +Assoc +IdR +InvR +Comm ·Assoc ·IdR ·DistL+ ·Comm

‎Cubical/Algebra/OrderedCommRing/Instances/Rationals/Fast.agda‎

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

‎Cubical/Relation/Binary/Order/Loset/Instances/Rationals/Fast.agda‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
module Cubical.Relation.Binary.Order.Loset.Instances.Rationals.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Data.Sum
6+
open import Cubical.HITs.PropositionalTruncation
7+
8+
open import Cubical.Data.Empty as ⊥
9+
10+
open import Cubical.Data.Rationals.Fast
11+
open import Cubical.Data.Rationals.Fast.Order renaming (_<_ to _<ℚ_)
12+
13+
open import Cubical.Relation.Binary.Order.Loset
14+
15+
open LosetStr
16+
17+
ℚ<Loset : Loset ℓ-zero ℓ-zero
18+
fst ℚ<Loset = ℚ
19+
_<_ (snd ℚ<Loset) = _<ℚ_
20+
isLoset (snd ℚ<Loset) = isLosetℚ<
21+
where
22+
open IsLoset
23+
abstract
24+
isLosetℚ< : IsLoset _<ℚ_
25+
isLosetℚ< .is-set = isSetℚ
26+
isLosetℚ< .is-prop-valued = isProp<
27+
isLosetℚ< .is-irrefl = isIrrefl<
28+
isLosetℚ< .is-trans = isTrans<
29+
isLosetℚ< .is-asym = isAsym<
30+
isLosetℚ< .is-weakly-linear = isWeaklyLinear<
31+
isLosetℚ< .is-connected = isConnected<

‎Cubical/Relation/Binary/Order/Poset/Instances/Rationals/Fast.agda‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
module Cubical.Relation.Binary.Order.Poset.Instances.Rationals.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Relation.Binary.Order.Poset
6+
open import Cubical.Relation.Binary.Order.Toset
7+
8+
open import Cubical.Relation.Binary.Order.Toset.Instances.Rationals.Fast
9+
10+
ℚ≤Poset : Poset ℓ-zero ℓ-zero
11+
ℚ≤Poset = Toset→Poset ℚ≤Toset

‎Cubical/Relation/Binary/Order/Proset/Instances/Rationals/Fast.agda‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
module Cubical.Relation.Binary.Order.Proset.Instances.Rationals.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Relation.Binary.Order.Poset
6+
open import Cubical.Relation.Binary.Order.Proset
7+
8+
open import Cubical.Relation.Binary.Order.Poset.Instances.Rationals.Fast
9+
10+
ℚ≤Proset : Proset ℓ-zero ℓ-zero
11+
ℚ≤Proset = Poset→Proset ℚ≤Poset

‎Cubical/Relation/Binary/Order/Pseudolattice/Instances/Rationals/Fast.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.Rationals.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Data.Rationals.Fast
6+
open import Cubical.Data.Rationals.Fast.Order renaming (_≤_ to _≤ℚ_)
7+
8+
open import Cubical.Relation.Binary.Order.Poset.Instances.Rationals.Fast
9+
open import Cubical.Relation.Binary.Order.Pseudolattice
10+
11+
ℚ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
12+
ℚ≤Pseudolattice = makePseudolatticeFromPoset ℚ≤Poset min max
13+
(λ {a b} → min≤ a b)
14+
(λ {a b} → subst (_≤ℚ b) (minComm b a) (min≤ b a))
15+
(λ {a b x} x≤a x≤b → subst (_≤ℚ min a b) (minIdem x) (≤MonotoneMin x a x b x≤a x≤b))
16+
(λ {x} {y} → ≤max x y)
17+
(λ {a b} → subst (b ≤ℚ_) (maxComm b a) (≤max b a))
18+
(λ {a b x} a≤x b≤x → subst (max a b ≤ℚ_) (maxIdem x) (≤MonotoneMax a x b x a≤x b≤x))

‎Cubical/Relation/Binary/Order/Quoset/Instances/Rationals/Fast.agda‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
module Cubical.Relation.Binary.Order.Quoset.Instances.Rationals.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Relation.Binary.Order.Quoset
6+
open import Cubical.Relation.Binary.Order.StrictOrder
7+
8+
open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Rationals.Fast
9+
10+
ℚ<Quoset : Quoset ℓ-zero ℓ-zero
11+
ℚ<Quoset = StrictOrder→Quoset ℚ<StrictOrder

‎Cubical/Relation/Binary/Order/StrictOrder/Instances/Rationals/Fast.agda‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
module Cubical.Relation.Binary.Order.StrictOrder.Instances.Rationals.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Relation.Binary.Order.StrictOrder
6+
open import Cubical.Relation.Binary.Order.Loset
7+
8+
open import Cubical.Relation.Binary.Order.Loset.Instances.Rationals.Fast
9+
10+
ℚ<StrictOrder : StrictOrder ℓ-zero ℓ-zero
11+
ℚ<StrictOrder = Loset→StrictOrder ℚ<Loset

‎Cubical/Relation/Binary/Order/Toset/Instances/Rationals/Fast.agda‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
module Cubical.Relation.Binary.Order.Toset.Instances.Rationals.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Data.Sum
6+
open import Cubical.HITs.PropositionalTruncation
7+
8+
open import Cubical.Data.Rationals.Fast
9+
open import Cubical.Data.Rationals.Fast.Order renaming (_≤_ to _≤ℚ_)
10+
11+
open import Cubical.Relation.Binary.Order.Toset
12+
13+
open import Cubical.Relation.Binary
14+
open BinaryRelation
15+
16+
open TosetStr
17+
18+
ℚ≤Toset : Toset ℓ-zero ℓ-zero
19+
fst ℚ≤Toset = ℚ
20+
_≤_ (snd ℚ≤Toset) = _≤ℚ_
21+
isToset (snd ℚ≤Toset) = isTosetℚ≤
22+
where
23+
open IsToset
24+
abstract
25+
isTosetℚ≤ : IsToset _≤ℚ_
26+
isTosetℚ≤ .is-set = isSetℚ
27+
isTosetℚ≤ .is-prop-valued = isProp≤
28+
isTosetℚ≤ .is-refl = isRefl≤
29+
isTosetℚ≤ .is-trans = isTrans≤
30+
isTosetℚ≤ .is-antisym = isAntisym≤
31+
isTosetℚ≤ .is-total = isTotal≤

0 commit comments

Comments
 (0)