Skip to content

Commit 172b47a

Browse files
broughjtbroughjt
authored
Add commutative ring and field instances for Data.Rationals (#1260)
1 parent 8888638 commit 172b47a

File tree

5 files changed

+208
-86
lines changed

5 files changed

+208
-86
lines changed

‎Cubical/Algebra/CommRing/Instances/QuoQRationals.agda‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
{-
2+
3+
ℚ (the QuoQ version) is a Commutative Ring
4+
5+
-}
6+
module Cubical.Algebra.CommRing.Instances.QuoQRationals where
7+
8+
open import Cubical.Foundations.Prelude
9+
10+
open import Cubical.Algebra.CommRing
11+
open import Cubical.Data.Rationals.MoreRationals.QuoQ
12+
renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)
13+
14+
open CommRingStr
15+
16+
17+
ℚCommRing : CommRing ℓ-zero
18+
ℚCommRing .fst = ℚType
19+
ℚCommRing .snd .0r = 0
20+
ℚCommRing .snd .1r = 1
21+
ℚCommRing .snd ._+_ = _+ℚ_
22+
ℚCommRing .snd ._·_ = _·ℚ_
23+
ℚCommRing .snd .-_ = -ℚ_
24+
ℚCommRing .snd .isCommRing = isCommRingℚ
25+
where
26+
abstract
27+
isCommRingℚ : IsCommRing 0 1 _+ℚ_ _·ℚ_ -ℚ_
28+
isCommRingℚ = makeIsCommRing
29+
isSetℚ +-assoc +-identityʳ
30+
+-inverseʳ +-comm ·-assoc
31+
·-identityʳ (λ x y z → sym (·-distribˡ x y z)) ·-comm

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

Lines changed: 12 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,23 @@
11
{-
22
3-
ℚ is a Commutative Ring
3+
ℚ is a CommRing
44
55
-}
66
module Cubical.Algebra.CommRing.Instances.Rationals where
77

88
open import Cubical.Foundations.Prelude
9-
109
open import Cubical.Algebra.CommRing
11-
open import Cubical.Data.Rationals.MoreRationals.QuoQ
12-
renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)
13-
14-
open CommRingStr
15-
10+
open import Cubical.Data.Rationals as ℚ
1611

1712
ℚCommRing : CommRing ℓ-zero
18-
ℚCommRing .fst = ℚType
19-
ℚCommRing .snd .0r = 0
20-
ℚCommRing .snd .1r = 1
21-
ℚCommRing .snd ._+_ = _+ℚ_
22-
ℚCommRing .snd ._·_ = _·ℚ_
23-
ℚCommRing .snd .-_ = -ℚ_
24-
ℚCommRing .snd .isCommRing = isCommRingℚ
13+
ℚCommRing .fst = ℚ
14+
ℚCommRing .snd .CommRingStr.0r = 0
15+
ℚCommRing .snd .CommRingStr.1r = 1
16+
ℚCommRing .snd .CommRingStr._+_ = _+_
17+
ℚCommRing .snd .CommRingStr._·_ = _·_
18+
ℚCommRing .snd .CommRingStr.-_ = -_
19+
ℚCommRing .snd .CommRingStr.isCommRing = p
2520
where
26-
abstract
27-
isCommRingℚ : IsCommRing 0 1 _+ℚ_ _·ℚ_ -ℚ_
28-
isCommRingℚ = makeIsCommRing
29-
isSetℚ +-assoc +-identityʳ
30-
+-inverseʳ +-comm ·-assoc
31-
·-identityʳ (λ x y z → sym (·-distribˡ x y z)) ·-comm
21+
p : IsCommRing 0 1 _+_ _·_ (-_)
22+
p = makeIsCommRing isSetℚ +Assoc +IdR +InvR +Comm ·Assoc ·IdR ·DistL+ ·Comm
23+

‎Cubical/Algebra/Field/Instances/QuoQRationals.agda‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
{-
2+
3+
ℚ (the QuoQ version) is a Field
4+
5+
-}
6+
module Cubical.Algebra.Field.Instances.QuoQRationals where
7+
8+
open import Cubical.Foundations.Prelude
9+
open import Cubical.Foundations.HLevels
10+
11+
open import Cubical.Data.Sigma
12+
open import Cubical.Data.Empty as Empty
13+
open import Cubical.Data.Nat using (ℕ ; zero ; suc)
14+
open import Cubical.Data.NatPlusOne
15+
open import Cubical.Data.Int.MoreInts.QuoInt
16+
using (ℤ ; spos ; sneg ; pos ; neg ; signed ; posneg ; isSetℤ ; 0≢1-ℤ)
17+
renaming (_·_ to _·ℤ_ ; -_ to -ℤ_
18+
; ·-zeroˡ to ·ℤ-zeroˡ
19+
; ·-identityʳ to ·ℤ-identityʳ)
20+
open import Cubical.HITs.SetQuotients as SetQuot
21+
open import Cubical.Data.Rationals.MoreRationals.QuoQ
22+
using (ℚ ; ℕ₊₁→ℤ ; isEquivRel∼)
23+
24+
open import Cubical.Algebra.Field
25+
open import Cubical.Algebra.CommRing
26+
open import Cubical.Tactics.CommRingSolver
27+
open import Cubical.Algebra.CommRing.Instances.QuoInt
28+
open import Cubical.Algebra.CommRing.Instances.QuoQRationals
29+
30+
open import Cubical.Relation.Nullary
31+
32+
33+
-- It seems there are bugs when applying ring solver to explicit ring.
34+
-- The following is a work-around.
35+
private
36+
module Helpers {ℓ : Level}(𝓡 : CommRing ℓ) where
37+
open CommRingStr (𝓡 .snd)
38+
39+
helper1 : (x y : 𝓡 .fst) → (x · y) · 1r ≡ 1r · (y · x)
40+
helper1 _ _ = solve! 𝓡
41+
42+
helper2 : (x y : 𝓡 .fst) → ((- x) · (- y)) · 1r ≡ 1r · (y · x)
43+
helper2 _ _ = solve! 𝓡
44+
45+
46+
-- A rational number is zero if and only if its numerator is zero
47+
48+
a/b≡0→a≡0 : (x : ℤ × ℕ₊₁) → [ x ] ≡ 0 → x .fst ≡ 0
49+
a/b≡0→a≡0 (a , b) a/b≡0 = sym (·ℤ-identityʳ a) ∙ a·1≡0·b ∙ ·ℤ-zeroˡ (ℕ₊₁→ℤ b)
50+
where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
51+
a·1≡0·b = effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ a/b≡0
52+
53+
a≡0→a/b≡0 : (x : ℤ × ℕ₊₁) → x .fst ≡ 0 → [ x ] ≡ 0
54+
a≡0→a/b≡0 (a , b) a≡0 = eq/ _ _ a·1≡0·b
55+
where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
56+
a·1≡0·b = (λ i → a≡0 i ·ℤ 1) ∙ ·ℤ-zeroˡ {s = spos} 1 ∙ sym (·ℤ-zeroˡ (ℕ₊₁→ℤ b))
57+
58+
59+
-- ℚ is a field
60+
61+
open CommRingStr (ℚCommRing .snd)
62+
open Units ℚCommRing
63+
open Helpers ℤCommRing
64+
65+
66+
hasInverseℚ : (q : ℚ) → ¬ q ≡ 0 → Σ[ p ∈ ℚ ] q · p ≡ 1
67+
hasInverseℚ = SetQuot.elimProp (λ q → isPropΠ (λ _ → inverseUniqueness q))
68+
(λ x x≢0 → let a≢0 = λ a≡0 → x≢0 (a≡0→a/b≡0 x a≡0) in inv-helper x a≢0 , inv·-helper x a≢0)
69+
where
70+
inv-helper : (x : ℤ × ℕ₊₁) → ¬ x .fst ≡ 0 → ℚ
71+
inv-helper (signed spos (suc a) , b) _ = [ ℕ₊₁→ℤ b , 1+ a ]
72+
inv-helper (signed sneg (suc a) , b) _ = [ -ℤ ℕ₊₁→ℤ b , 1+ a ]
73+
inv-helper (signed spos zero , _) a≢0 = Empty.rec (a≢0 refl)
74+
inv-helper (signed sneg zero , _) a≢0 = Empty.rec (a≢0 (sym posneg))
75+
inv-helper (posneg i , _) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))
76+
77+
inv·-helper : (x : ℤ × ℕ₊₁)(a≢0 : ¬ x .fst ≡ 0) → [ x ] · inv-helper x a≢0 ≡ 1
78+
inv·-helper (signed spos zero , b) a≢0 = Empty.rec (a≢0 refl)
79+
inv·-helper (signed sneg zero , b) a≢0 = Empty.rec (a≢0 (sym posneg))
80+
inv·-helper (posneg i , b) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))
81+
inv·-helper (signed spos (suc a) , b) _ = eq/ _ _ (helper1 (pos (suc a)) (ℕ₊₁→ℤ b))
82+
inv·-helper (signed sneg (suc a) , b) _ = eq/ _ _ (helper2 (pos (suc a)) (ℕ₊₁→ℤ b))
83+
84+
0≢1-ℚ : ¬ Path ℚ 0 1
85+
0≢1-ℚ p = 0≢1-ℤ (effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ p)
86+
87+
88+
-- The instance
89+
90+
ℚField : Field ℓ-zero
91+
ℚField = makeFieldFromCommRing ℚCommRing hasInverseℚ 0≢1-ℚ

‎Cubical/Algebra/Field/Instances/Rationals.agda‎

Lines changed: 61 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -5,87 +5,82 @@
55
-}
66
module Cubical.Algebra.Field.Instances.Rationals where
77

8-
open import Cubical.Foundations.Prelude
8+
open import Cubical.Foundations.Function
99
open import Cubical.Foundations.HLevels
10+
open import Cubical.Foundations.Prelude
1011

11-
open import Cubical.Data.Sigma
12-
open import Cubical.Data.Empty as Empty
13-
open import Cubical.Data.Nat using (ℕ ; zero ; suc)
14-
open import Cubical.Data.NatPlusOne
15-
open import Cubical.Data.Int.MoreInts.QuoInt
16-
using (ℤ ; spos ; sneg ; pos ; neg ; signed ; posneg ; isSetℤ ; 0≢1-ℤ)
17-
renaming (_·_ to _·ℤ_ ; -_ to -ℤ_
18-
; ·-zeroˡ to ·ℤ-zeroˡ
19-
; ·-identityʳ to ·ℤ-identityʳ)
20-
open import Cubical.HITs.SetQuotients as SetQuot
21-
open import Cubical.Data.Rationals.MoreRationals.QuoQ
22-
using (ℚ ; ℕ₊₁→ℤ ; isEquivRel∼)
23-
24-
open import Cubical.Algebra.Field
2512
open import Cubical.Algebra.CommRing
26-
open import Cubical.Tactics.CommRingSolver
27-
open import Cubical.Algebra.CommRing.Instances.QuoInt
2813
open import Cubical.Algebra.CommRing.Instances.Rationals
14+
open import Cubical.Algebra.Field
2915

30-
open import Cubical.Relation.Nullary
31-
32-
33-
-- It seems there are bugs when applying ring solver to explicit ring.
34-
-- The following is a work-around.
35-
private
36-
module Helpers {ℓ : Level}(𝓡 : CommRing ℓ) where
37-
open CommRingStr (𝓡 .snd)
38-
39-
helper1 : (x y : 𝓡 .fst) → (x · y) · 1r ≡ 1r · (y · x)
40-
helper1 _ _ = solve! 𝓡
41-
42-
helper2 : (x y : 𝓡 .fst) → ((- x) · (- y)) · 1r ≡ 1r · (y · x)
43-
helper2 _ _ = solve! 𝓡
44-
45-
46-
-- A rational number is zero if and only if its numerator is zero
47-
48-
a/b≡0→a≡0 : (x : ℤ × ℕ₊₁) → [ x ] ≡ 0 → x .fst ≡ 0
49-
a/b≡0→a≡0 (a , b) a/b≡0 = sym (·ℤ-identityʳ a) ∙ a·1≡0·b ∙ ·ℤ-zeroˡ (ℕ₊₁→ℤ b)
50-
where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
51-
a·1≡0·b = effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ a/b≡0
52-
53-
a≡0→a/b≡0 : (x : ℤ × ℕ₊₁) → x .fst ≡ 0 → [ x ] ≡ 0
54-
a≡0→a/b≡0 (a , b) a≡0 = eq/ _ _ a·1≡0·b
55-
where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
56-
a·1≡0·b = (λ i → a≡0 i ·ℤ 1) ∙ ·ℤ-zeroˡ {s = spos} 1 ∙ sym (·ℤ-zeroˡ (ℕ₊₁→ℤ b))
16+
open import Cubical.Data.Empty as Empty
17+
open import Cubical.Data.Int as ℤ
18+
open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc)
19+
open import Cubical.Data.NatPlusOne
20+
open import Cubical.Data.Rationals as ℚ
21+
open import Cubical.Data.Sigma
5722

23+
open import Cubical.HITs.SetQuotients as SetQuotients
5824

59-
-- ℚ is a field
25+
open import Cubical.Relation.Nullary
6026

6127
open CommRingStr (ℚCommRing .snd)
6228
open Units ℚCommRing
63-
open Helpers ℤCommRing
6429

65-
66-
hasInverseℚ : (q : ℚ) → ¬ q ≡ 0 → Σ[ p ∈ ℚ ] q · p ≡ 1
67-
hasInverseℚ = SetQuot.elimProp (λ q → isPropΠ (λ _ → inverseUniqueness q))
68-
(λ x x≢0 → let a≢0 = λ a≡0 → x≢0 (a≡0→a/b≡0 x a≡0) in inv-helper x a≢0 , inv·-helper x a≢0)
30+
hasInverseℚ : (x : ℚ) → ¬ x ≡ 0 → Σ[ y ∈ ℚ ] x ℚ.· y ≡ 1
31+
hasInverseℚ = SetQuotients.elimProp
32+
(λ x → isPropΠ (λ _ → inverseUniqueness x))
33+
(λ u p → r u p , q u p)
6934
where
70-
inv-helper : (x : ℤ × ℕ₊₁) → ¬ x .fst ≡ 0 → ℚ
71-
inv-helper (signed spos (suc a) , b) _ = [ ℕ₊₁→ℤ b , 1+ a ]
72-
inv-helper (signed sneg (suc a) , b) _ = [ -ℤ ℕ₊₁→ℤ b , 1+ a ]
73-
inv-helper (signed spos zero , _) a≢0 = Empty.rec (a≢0 refl)
74-
inv-helper (signed sneg zero , _) a≢0 = Empty.rec (a≢0 (sym posneg))
75-
inv-helper (posneg i , _) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))
76-
77-
inv·-helper : (x : ℤ × ℕ₊₁)(a≢0 : ¬ x .fst ≡ 0) → [ x ] · inv-helper x a≢0 ≡ 1
78-
inv·-helper (signed spos zero , b) a≢0 = Empty.rec (a≢0 refl)
79-
inv·-helper (signed sneg zero , b) a≢0 = Empty.rec (a≢0 (sym posneg))
80-
inv·-helper (posneg i , b) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))
81-
inv·-helper (signed spos (suc a) , b) _ = eq/ _ _ (helper1 (pos (suc a)) (ℕ₊₁→ℤ b))
82-
inv·-helper (signed sneg (suc a) , b) _ = eq/ _ _ (helper2 (pos (suc a)) (ℕ₊₁→ℤ b))
35+
r : (u : ℤ × ℕ₊₁) → ¬ [ u ] ≡ 0 → ℚ
36+
r (ℤ.pos zero , b) p =
37+
Empty.rec (p (numerator0→0 ((ℤ.pos zero , b)) refl))
38+
r (ℤ.pos (suc n) , b) _ = [ (ℕ₊₁→ℤ b , (1+ n)) ]
39+
r (ℤ.negsuc n , b) _ = [ (ℤ.- ℕ₊₁→ℤ b , (1+ n)) ]
40+
41+
q : (u : ℤ × ℕ₊₁) (p : ¬ [ u ] ≡ 0) → [ u ] ℚ.· (r u p) ≡ 1
42+
q (ℤ.pos zero , b) p =
43+
Empty.rec (p (numerator0→0 ((ℤ.pos zero , b)) refl))
44+
q (ℤ.pos (suc n) , (1+ m)) _ =
45+
eq/ ((ℤ.pos (suc n) ℤ.· (ℕ₊₁→ℤ (1+ m)) , (1+ m) ·₊₁ (1+ n))) ((1 , 1)) q'
46+
where
47+
q' = (ℤ.pos (suc n) ℤ.· (ℕ₊₁→ℤ (1+ m))) ℤ.· 1
48+
≡⟨ ℤ.·IdR _ ⟩
49+
ℤ.pos (suc n) ℤ.· ℤ.pos (suc m)
50+
≡⟨ sym $ ℤ.pos·pos (suc n) (suc m) ⟩
51+
ℤ.pos ((suc n) ℕ.· (suc m))
52+
≡⟨ cong ℤ.pos (ℕ.·-comm (suc n) (suc m)) ⟩
53+
ℤ.pos ((suc m) ℕ.· (suc n))
54+
≡⟨ refl ⟩
55+
ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))
56+
≡⟨ sym (ℤ.·IdL _) ⟩
57+
1 ℤ.· (ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))) ∎
58+
q (ℤ.negsuc n , (1+ m)) _ =
59+
eq/ ((ℤ.negsuc n ℤ.· ℤ.negsuc m) , ((1+ m) ·₊₁ (1+ n))) ((1 , 1)) q'
60+
where
61+
q' : (ℤ.negsuc n ℤ.· ℤ.negsuc m , (1+ m) ·₊₁ (1+ n)) ∼ (1 , 1)
62+
q' = (ℤ.negsuc n ℤ.· ℤ.negsuc m) ℤ.· 1
63+
≡⟨ ℤ.·IdR _ ⟩
64+
(ℤ.negsuc n ℤ.· ℤ.negsuc m)
65+
≡⟨ negsuc·negsuc n m ⟩
66+
(ℤ.pos (suc n) ℤ.· ℤ.pos (suc m))
67+
≡⟨ sym $ ℤ.pos·pos (suc n) (suc m) ⟩
68+
ℤ.pos ((suc n) ℕ.· (suc m))
69+
≡⟨ cong ℤ.pos (ℕ.·-comm (suc n) (suc m)) ⟩
70+
ℤ.pos ((suc m) ℕ.· (suc n))
71+
≡⟨ refl ⟩
72+
ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))
73+
≡⟨ sym (ℤ.·IdL _) ⟩
74+
1 ℤ.· (ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))) ∎
8375

8476
0≢1-ℚ : ¬ Path ℚ 0 1
8577
0≢1-ℚ p = 0≢1-ℤ (effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ p)
8678

87-
88-
-- The instance
89-
9079
ℚField : Field ℓ-zero
9180
ℚField = makeFieldFromCommRing ℚCommRing hasInverseℚ 0≢1-ℚ
81+
82+
_[_]⁻¹ : (x : ℚ) → ¬ x ≡ 0 → ℚ
83+
_[_]⁻¹ = FieldStr._[_]⁻¹ $ snd ℚField
84+
85+
_/_[_] : ℚ → (y : ℚ) → ¬ y ≡ 0 → ℚ
86+
x / y [ p ] = x ℚ.· (y [ p ]⁻¹)

‎Cubical/Data/Rationals/Properties.agda‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -483,3 +483,16 @@ x - y = x + (- y)
483483

484484
+CancelR : ∀ x y z → x + y ≡ z + y → x ≡ z
485485
+CancelR x y z p = +CancelL y x z (+Comm y x ∙ p ∙ +Comm z y)
486+
487+
numerator0→0 : (u : ℤ × ℕ₊₁) → u .fst ≡ 0 → [ u ] ≡ 0
488+
numerator0→0 (a , b) p = eq/ ((a , b)) ((0 , 1)) q
489+
where
490+
q : a ℤ.· (ℕ₊₁→ℤ 1) ≡ 0 ℤ.· (ℕ₊₁→ℤ b)
491+
q =
492+
a ℤ.· (ℕ₊₁→ℤ 1)
493+
≡⟨ ℤ.·IdR a ⟩
494+
a
495+
≡⟨ p ⟩
496+
0
497+
≡⟨ sym (ℤ.·AnnihilL (ℕ₊₁→ℤ b)) ⟩
498+
0 ℤ.· (ℕ₊₁→ℤ b) ∎

0 commit comments

Comments
 (0)