Skip to content

Commit 32d09a9

Browse files
marcinjangrzybowskimarcinjangrzybowski
committed
Merge remote-tracking branch 'lorenzo/premetric-wip' into book-cauchy-reals
2 parents 3140d66 + 8c2aad4 commit 32d09a9

File tree

16 files changed

+472
-38
lines changed

16 files changed

+472
-38
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/Algebra/OrderedCommRing/Properties.agda‎

Lines changed: 238 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,238 @@
1+
module Cubical.Algebra.OrderedCommRing.Properties where
2+
3+
open import Cubical.Foundations.Prelude
4+
open import Cubical.Foundations.Function
5+
open import Cubical.Foundations.Structure
6+
open import Cubical.Foundations.HLevels
7+
open import Cubical.Foundations.SIP using (TypeWithStr)
8+
9+
open import Cubical.HITs.PropositionalTruncation as PT
10+
11+
import Cubical.Functions.Logic as L
12+
13+
open import Cubical.Data.Sum
14+
open import Cubical.Data.Sigma
15+
16+
open import Cubical.Algebra.Semigroup
17+
open import Cubical.Algebra.CommMonoid
18+
open import Cubical.Algebra.Semiring
19+
open import Cubical.Algebra.CommSemiring
20+
open import Cubical.Algebra.Ring
21+
open import Cubical.Algebra.CommRing
22+
open import Cubical.Algebra.OrderedCommRing.Base
23+
24+
open import Cubical.Relation.Binary.Order.Quoset
25+
open import Cubical.Relation.Binary.Order.StrictOrder
26+
open import Cubical.Relation.Binary.Order.Poset hiding (isPseudolattice)
27+
open import Cubical.Relation.Binary.Order.Pseudolattice
28+
29+
open import Cubical.Relation.Binary.Order.QuosetReasoning
30+
31+
32+
private
33+
variable
34+
ℓ ℓ' ℓ'' : Level
35+
36+
OrderedCommRing→StrictOrder : OrderedCommRing ℓ ℓ' → StrictOrder ℓ ℓ'
37+
OrderedCommRing→StrictOrder R .fst = R .fst
38+
OrderedCommRing→StrictOrder R .snd = strictorderstr _ isStrictOrder where
39+
open OrderedCommRingStr (str R)
40+
41+
OrderedCommRing→Ring : OrderedCommRing ℓ ℓ' → Ring ℓ
42+
OrderedCommRing→Ring = CommRing→Ring ∘ OrderedCommRing→CommRing
43+
44+
OrderedCommRing→Poset : OrderedCommRing ℓ ℓ' → Poset ℓ ℓ'
45+
OrderedCommRing→Poset = Pseudolattice→Poset ∘ OrderedCommRing→PseudoLattice
46+
47+
OrderedCommRing→Quoset : OrderedCommRing ℓ ℓ' → Quoset ℓ ℓ'
48+
OrderedCommRing→Quoset = StrictOrder→Quoset ∘ OrderedCommRing→StrictOrder
49+
50+
module _ (R' : OrderedCommRing ℓ ℓ') where
51+
R = fst R'
52+
open OrderedCommRingStr (snd R')
53+
open RingTheory (OrderedCommRing→Ring R')
54+
open JoinProperties (OrderedCommRing→PseudoLattice R') renaming (
55+
L≤∨ to L≤⊔ ; R≤∨ to R≤⊔ ; ∨LUB to ⊔LUB)
56+
57+
open <-≤-Reasoning R
58+
(OrderedCommRing→Poset R' .snd)
59+
(OrderedCommRing→Quoset R' .snd)
60+
(λ x {y} {z} → <-≤-trans x y z)
61+
(λ x {y} {z} → ≤-<-trans x y z)
62+
(λ {x} {y} → <-≤-weaken x y)
63+
open <-syntax
64+
open ≤-syntax
65+
open ≡-syntax
66+
67+
abs : R → R
68+
abs z = z ⊔ (- z)
69+
70+
_#_ : R → R → Type ℓ'
71+
x # y = (x < y) L.⊔′ (y < x)
72+
73+
+MonoL< : ∀ x y z → x < y → z + x < z + y
74+
+MonoL< x y z x<y = begin<
75+
z + x ≡→≤⟨ +Comm z x ⟩ x + z <⟨ +MonoR< x y z x<y ⟩ y + z ≡→≤⟨ +Comm y z ⟩ z + y ◾
76+
77+
+MonoL≤ : ∀ x y z → x ≤ y → z + x ≤ z + y
78+
+MonoL≤ x y z x≤y = begin≤
79+
z + x ≡→≤⟨ +Comm z x ⟩ x + z ≤⟨ +MonoR≤ x y z x≤y ⟩ y + z ≡→≤⟨ +Comm y z ⟩ z + y ◾
80+
81+
·MonoL< : ∀ x y z → 0r < z → x < y → z · x < z · y
82+
·MonoL< x y z 0<z x<y = begin<
83+
z · x ≡→≤⟨ ·Comm z x ⟩ x · z <⟨ ·MonoR< x y z 0<z x<y ⟩ y · z ≡→≤⟨ ·Comm y z ⟩ z · y ◾
84+
85+
·MonoL≤ : ∀ x y z → 0r ≤ z → x ≤ y → z · x ≤ z · y
86+
·MonoL≤ x y z 0≤z x≤y = begin≤
87+
z · x ≡→≤⟨ ·Comm z x ⟩ x · z ≤⟨ ·MonoR≤ x y z 0≤z x≤y ⟩ y · z ≡→≤⟨ ·Comm y z ⟩ z · y ◾
88+
89+
module OrderedCommRingTheory where
90+
-Flip< : ∀ x y → x < y → - y < - x
91+
-Flip< x y x<y = begin<
92+
- y ≡→≤⟨ sym $ +Assoc _ _ _ ∙∙ cong (_- y) (+InvR x) ∙∙ +IdL (- y) ⟩
93+
x + (- x - y) <⟨ +MonoR< x y (- x - y) x<y ⟩
94+
y + (- x - y) ≡→≤⟨ +Assoc-comm1 _ _ _ ∙∙ cong (- x +_) (+InvR y) ∙∙ +IdR (- x) ⟩
95+
- x ◾
96+
97+
≤abs : ∀ z → z ≤ abs z
98+
≤abs z = L≤⊔
99+
100+
-≤abs : ∀ z → - z ≤ abs z
101+
-≤abs z = R≤⊔
102+
103+
#→0<abs : ∀ z → z # 0r → 0r < abs z
104+
#→0<abs z = PT.rec (is-prop-valued< _ _) λ
105+
{ (inl z<0) → begin<
106+
0r ≡→≤⟨ sym 0Selfinverse ⟩
107+
- 0r <⟨ -Flip< z 0r z<0 ⟩
108+
- z ≤⟨ -≤abs _ ⟩
109+
abs z ◾
110+
; (inr 0<z) → begin<
111+
0r <⟨ 0<z ⟩
112+
z ≤⟨ ≤abs _ ⟩
113+
abs z ◾ }
114+
115+
triangularInequality : ∀ x y → abs (x + y) ≤ abs x + abs y
116+
triangularInequality x y = ⊔LUB
117+
(begin≤
118+
x + y ≤⟨ +MonoR≤ _ _ _ (≤abs x) ⟩
119+
abs x + y ≤⟨ +MonoL≤ _ _ _ (≤abs y) ⟩
120+
abs x + abs y ◾)
121+
(begin≤
122+
- (x + y) ≡→≤⟨ sym $ -Dist x y ⟩
123+
(- x) - y ≤⟨ +MonoR≤ _ _ _ (-≤abs x) ⟩
124+
abs x + (- y) ≤⟨ +MonoL≤ _ _ _ (-≤abs y) ⟩
125+
abs x + abs y ◾)
126+
127+
module AdditiveSubType
128+
(P : R → hProp ℓ'')
129+
(+Closed : (x y : R) → ⟨ P x ⟩ → ⟨ P y ⟩ → ⟨ P (x + y) ⟩)
130+
where
131+
132+
subtype = Σ[ x ∈ R ] ⟨ P x ⟩
133+
134+
module AdditiveAndMultiplicativeSubType
135+
(P : R → hProp ℓ'')
136+
(+Closed : (x y : R) → ⟨ P x ⟩ → ⟨ P y ⟩ → ⟨ P (x + y) ⟩)
137+
(·Closed : (x y : R) → ⟨ P x ⟩ → ⟨ P y ⟩ → ⟨ P (x · y) ⟩)
138+
where
139+
open AdditiveSubType P +Closed public
140+
141+
module Positive where
142+
private
143+
0<ₚ_ : R → hProp ℓ'
144+
0<ₚ x = (0r < x) , is-prop-valued< 0r x
145+
146+
0<+Closed : ∀ x y → 0r < x → 0r < y → 0r < x + y
147+
0<+Closed x y 0<x 0<y = begin<
148+
0r <⟨ 0<x ⟩
149+
x ≡→≤⟨ sym $ +IdR x ⟩
150+
x + 0r <⟨ +MonoL< 0r y x 0<y ⟩
151+
x + y ◾
152+
153+
0<·Closed : ∀ x y → 0r < x → 0r < y → 0r < x · y
154+
0<·Closed x y 0<x 0<y = begin<
155+
0r ≡→≤⟨ sym $ 0LeftAnnihilates y ⟩
156+
0r · y <⟨ ·MonoR< 0r x y 0<y 0<x ⟩
157+
x · y ◾
158+
open AdditiveAndMultiplicativeSubType 0<ₚ_ 0<+Closed 0<·Closed
159+
renaming (subtype to R₊)
160+
161+
R₀≡ = Σ≡Prop (is-prop-valued< 0r)
162+
163+
R₊AdditiveSemigroup : Semigroup _
164+
fst R₊AdditiveSemigroup = R₊
165+
SemigroupStr._·_ (snd R₊AdditiveSemigroup) (x , 0<x) (y , 0<y) =
166+
(x + y , 0<+Closed x y 0<x 0<y)
167+
SemigroupStr.isSemigroup (snd R₊AdditiveSemigroup) = isSG
168+
where
169+
isSG : IsSemigroup _
170+
isSG .IsSemigroup.is-set = isSetΣSndProp is-set (is-prop-valued< 0r)
171+
isSG .IsSemigroup.·Assoc = λ _ _ _ → R₀≡ (+Assoc _ _ _)
172+
173+
174+
R₊MultiplicativeCommMonoid : CommMonoid _
175+
fst R₊MultiplicativeCommMonoid = R₊
176+
CommMonoidStr.ε (snd R₊MultiplicativeCommMonoid) = 1r , 0<1
177+
CommMonoidStr._·_ (snd R₊MultiplicativeCommMonoid) (x , 0<x) (y , 0<y) =
178+
(x · y , 0<·Closed x y 0<x 0<y)
179+
CommMonoidStr.isCommMonoid (snd R₊MultiplicativeCommMonoid) =
180+
makeIsCommMonoid
181+
(isSetΣSndProp is-set (is-prop-valued< 0r))
182+
(λ _ _ _ → R₀≡ (·Assoc _ _ _))
183+
(λ _ → R₀≡ (·IdR _))
184+
(λ _ _ → R₀≡ (·Comm _ _))
185+
186+
module NonNegative where
187+
private
188+
0≤ₚ_ : R → hProp ℓ'
189+
0≤ₚ x = (0r ≤ x) , is-prop-valued≤ 0r x
190+
191+
0≤+Closed : ∀ x y → 0r ≤ x → 0r ≤ y → 0r ≤ x + y
192+
0≤+Closed x y 0≤x 0≤y = begin≤
193+
0r ≤⟨ 0≤x ⟩
194+
x ≡→≤⟨ sym $ +IdR x ⟩
195+
x + 0r ≤⟨ +MonoL≤ 0r y x 0≤y ⟩
196+
x + y ◾
197+
198+
0≤·Closed : ∀ x y → 0r ≤ x → 0r ≤ y → 0r ≤ x · y
199+
0≤·Closed x y 0≤x 0≤y = begin≤
200+
0r ≡→≤⟨ sym $ 0LeftAnnihilates y ⟩
201+
0r · y ≤⟨ ·MonoR≤ 0r x y 0≤y 0≤x ⟩
202+
x · y ◾
203+
open AdditiveAndMultiplicativeSubType 0≤ₚ_ 0≤+Closed 0≤·Closed
204+
renaming (subtype to R₀₊)
205+
206+
R₀₊≡ = Σ≡Prop (is-prop-valued≤ 0r)
207+
208+
R₀₊CommSemiring : CommSemiring _
209+
fst R₀₊CommSemiring = R₀₊
210+
CommSemiringStr.0r (snd R₀₊CommSemiring) = 0r , is-refl _
211+
CommSemiringStr.1r (snd R₀₊CommSemiring) = 1r , <-≤-weaken _ _ 0<1
212+
CommSemiringStr._+_ (snd R₀₊CommSemiring) (x , 0≤x) (y , 0≤y) =
213+
(x + y , 0≤+Closed x y 0≤x 0≤y)
214+
CommSemiringStr._·_ (snd R₀₊CommSemiring) (x , 0≤x) (y , 0≤y) =
215+
(x · y , 0≤·Closed x y 0≤x 0≤y)
216+
CommSemiringStr.isCommSemiring (snd R₀₊CommSemiring) =
217+
makeIsCommSemiring
218+
(isSetΣSndProp is-set (is-prop-valued≤ 0r))
219+
(λ _ _ _ → R₀₊≡ (+Assoc _ _ _))
220+
(λ _ → R₀₊≡ (+IdR _))
221+
(λ _ _ → R₀₊≡ (+Comm _ _))
222+
(λ _ _ _ → R₀₊≡ (·Assoc _ _ _))
223+
(λ _ → R₀₊≡ (·IdR _))
224+
(λ _ _ _ → R₀₊≡ (·DistR+ _ _ _))
225+
(λ _ → R₀₊≡ (0LeftAnnihilates _))
226+
(λ _ _ → R₀₊≡ (·Comm _ _))
227+
228+
R₀₊MultiplicativeCommMonoid : CommMonoid _
229+
fst R₀₊MultiplicativeCommMonoid = R₀₊
230+
CommMonoidStr.ε (snd R₀₊MultiplicativeCommMonoid) = 1r , <-≤-weaken _ _ 0<1
231+
CommMonoidStr._·_ (snd R₀₊MultiplicativeCommMonoid) (x , 0≤x) (y , 0≤y) =
232+
(x · y , 0≤·Closed x y 0≤x 0≤y)
233+
CommMonoidStr.isCommMonoid (snd R₀₊MultiplicativeCommMonoid) =
234+
makeIsCommMonoid
235+
(isSetΣSndProp is-set (is-prop-valued≤ 0r))
236+
(λ _ _ _ → R₀₊≡ (·Assoc _ _ _))
237+
(λ _ → R₀₊≡ (·IdR _))
238+
(λ _ _ → R₀₊≡ (·Comm _ _))

‎Cubical/Data/Int/Fast/Base.agda‎

Lines changed: 0 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -38,25 +38,3 @@ sumFinℤ {n = n} f = sumFinGen {n = n} _+_ 0 f
3838
sumFinℤId : (n : ℕ) {f g : Fin n → ℤ}
3939
→ ((x : _) → f x ≡ g x) → sumFinℤ {n = n} f ≡ sumFinℤ {n = n} g
4040
sumFinℤId n t i = sumFinℤ {n = n} λ x → t x i
41-
42-
module _ (m n : ℕ) where
43-
44-
_ : negsuc n
45-
≡ - (1 + pos n)
46-
_ = refl
47-
48-
_ = negsuc (predℕ (suc m ℕ.· suc n)) ≡
49-
- ((1 + pos n) · (1 + pos m))
50-
_ = refl
51-
52-
_ : pos (suc m ℕ.· suc n) ≡ ((1 + pos m) · (1 + pos n))
53-
_ = refl
54-
55-
_ : pos m · pos n ≡ pos (m ℕ.· n)
56-
_ = refl
57-
58-
_ : pos 1 + pos n ≡ pos (suc n)
59-
_ = refl
60-
61-
_ : pos m + - (1 + pos n) ≡ m ℕ- (suc n)
62-
_ = refl

‎Cubical/Data/Int/Fast/Divisibility.agda‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -35,9 +35,9 @@ open import Cubical.Relation.Nullary
3535

3636
open import Cubical.Algebra.CommRing
3737
open import Cubical.Algebra.CommRing.Instances.Int.Fast
38-
3938
open import Cubical.Tactics.CommRingSolver.IntReflection
4039

40+
4141
private
4242
variable
4343
m n k : ℤ
@@ -233,12 +233,8 @@ module _
233233

234234
div·-helper : g · (div₁ · n) ≡ g · (div₂ · m)
235235
div·-helper =
236-
ℤ!
237-
∙ (λ i → divideEq (b .isCD .fst) i · n)
238-
∙ ℤ!
239-
∙ (λ i → divideEq (b .isCD .snd) (~ i) · m)
240-
∙ ℤ!
241-
236+
ℤ! ∙ (λ i → divideEq (b .isCD .fst) i · n)
237+
∙ ℤ! ∙ (λ i → divideEq (b .isCD .snd) (~ i) · m) ∙ ℤ!
242238
div·-g≠0 : ¬ g ≡ 0 → div₁ · n ≡ div₂ · m
243239
div·-g≠0 p = ·lCancel _ _ _ div·-helper p
244240

@@ -311,6 +307,7 @@ module _
311307
euclidStep 0 _ _ h _ = Empty.rec (¬-<-zero h)
312308
euclidStep (suc N) m n h (quotrem div rem quotEq (inl p)) =
313309
let q = subst (λ r → n ≡ div · m + r) p quotEq
310+
314311
in bezout 1 0 m ℤ!
315312
(∣-refl refl , subst (λ k → m ∣ k) (sym q) (subst (m ∣_) (sym (ℤ.+IdR (div · m))) (∣-right {k = div})) )
316313
euclidStep (suc N) m n h (quotrem div rem quotEq (inr p)) =
@@ -386,7 +383,7 @@ private
386383
quotRemNeg : (m : ℤ)(n : ℕ)(¬z : ¬ m ≡ 0) → QuotRem m (- pos n)
387384
quotRemNeg m n ¬z .div = - (quotRemPos m n ¬z .div)
388385
quotRemNeg m n ¬z .rem = - (quotRemPos m n ¬z .rem)
389-
quotRemNeg m n ¬z .quotEq =
386+
quotRemNeg m n ¬z .quotEq =
390387
(λ t → - quotRemPos m n ¬z .quotEq t)
391388
∙ -Dist+ (quotRemPos m n ¬z .div · m) (quotRemPos m n ¬z .rem)
392389
∙ (λ t → -DistL· (quotRemPos m n ¬z .div) m t + - quotRemPos m n ¬z .rem)

0 commit comments

Comments
 (0)