Add commutative ring and field instances for Data.Rationals

Cubical/Algebra/CommRing/Instances/QuoQRationals.agda

@@ -0,0 +1,31 @@
+{-
+
+ℚ (the QuoQ version) is a Commutative Ring
+
+-}
+module Cubical.Algebra.CommRing.Instances.QuoQRationals where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Data.Rationals.MoreRationals.QuoQ
+  renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)
+
+open CommRingStr
+
+
+ℚCommRing : CommRing ℓ-zero
+ℚCommRing .fst = ℚType
+ℚCommRing .snd .0r = 0
+ℚCommRing .snd .1r = 1
+ℚCommRing .snd ._+_ = _+ℚ_
+ℚCommRing .snd ._·_ = _·ℚ_
+ℚCommRing .snd .-_ = -ℚ_
+ℚCommRing .snd .isCommRing = isCommRingℚ
+  where
+  abstract
+    isCommRingℚ : IsCommRing 0 1 _+ℚ_ _·ℚ_ -ℚ_
+    isCommRingℚ = makeIsCommRing
+      isSetℚ +-assoc +-identityʳ
+      +-inverseʳ +-comm ·-assoc
+      ·-identityʳ (λ x y z → sym (·-distribˡ x y z)) ·-comm

Cubical/Algebra/CommRing/Instances/Rationals.agda

@@ -1,31 +1,23 @@
 {-
 
-ℚ is a Commutative Ring
+ℚ is a CommRing
 
 -}
 module Cubical.Algebra.CommRing.Instances.Rationals where
 
 open import Cubical.Foundations.Prelude
-
 open import Cubical.Algebra.CommRing
-open import Cubical.Data.Rationals.MoreRationals.QuoQ
-  renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)
-
-open CommRingStr
-
+open import Cubical.Data.Rationals as ℚ
 
 ℚCommRing : CommRing ℓ-zero
-ℚCommRing .fst = ℚType
-ℚCommRing .snd .0r = 0
-ℚCommRing .snd .1r = 1
-ℚCommRing .snd ._+_ = _+ℚ_
-ℚCommRing .snd ._·_ = _·ℚ_
-ℚCommRing .snd .-_ = -ℚ_
-ℚCommRing .snd .isCommRing = isCommRingℚ
+ℚCommRing .fst = ℚ
+ℚCommRing .snd .CommRingStr.0r = 0
+ℚCommRing .snd .CommRingStr.1r = 1
+ℚCommRing .snd .CommRingStr._+_ = _+_
+ℚCommRing .snd .CommRingStr._·_ = _·_
+ℚCommRing .snd .CommRingStr.-_  = -_
+ℚCommRing .snd .CommRingStr.isCommRing = p
   where
-  abstract
-    isCommRingℚ : IsCommRing 0 1 _+ℚ_ _·ℚ_ -ℚ_
-    isCommRingℚ = makeIsCommRing
-      isSetℚ +-assoc +-identityʳ
-      +-inverseʳ +-comm ·-assoc
-      ·-identityʳ (λ x y z → sym (·-distribˡ x y z)) ·-comm
+  p : IsCommRing 0 1 _+_ _·_ (-_)
+  p = makeIsCommRing isSetℚ +Assoc +IdR +InvR +Comm ·Assoc ·IdR ·DistL+ ·Comm
+

Cubical/Algebra/Field/Instances/QuoQRationals.agda

@@ -0,0 +1,91 @@
+{-
+
+ℚ (the QuoQ version) is a Field
+
+-}
+module Cubical.Algebra.Field.Instances.QuoQRationals where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty as Empty
+open import Cubical.Data.Nat using (ℕ ; zero ; suc)
+open import Cubical.Data.NatPlusOne
+open import Cubical.Data.Int.MoreInts.QuoInt
+  using    (ℤ ; spos ; sneg ; pos ; neg ; signed ; posneg ; isSetℤ ; 0≢1-ℤ)
+  renaming (_·_ to _·ℤ_ ; -_ to -ℤ_
+           ; ·-zeroˡ to ·ℤ-zeroˡ
+           ; ·-identityʳ to ·ℤ-identityʳ)
+open import Cubical.HITs.SetQuotients as SetQuot
+open import Cubical.Data.Rationals.MoreRationals.QuoQ
+  using    (ℚ ; ℕ₊₁→ℤ ; isEquivRel∼)
+
+open import Cubical.Algebra.Field
+open import Cubical.Algebra.CommRing
+open import Cubical.Tactics.CommRingSolver
+open import Cubical.Algebra.CommRing.Instances.QuoInt
+open import Cubical.Algebra.CommRing.Instances.QuoQRationals
+
+open import Cubical.Relation.Nullary
+
+
+-- It seems there are bugs when applying ring solver to explicit ring.
+-- The following is a work-around.
+private
+  module Helpers {ℓ : Level}(𝓡 : CommRing ℓ) where
+    open CommRingStr (𝓡 .snd)
+
+    helper1 : (x y : 𝓡 .fst) → (x · y) · 1r ≡ 1r · (y · x)
+    helper1 _ _ = solve! 𝓡
+
+    helper2 : (x y : 𝓡 .fst) → ((- x) · (- y)) · 1r ≡ 1r · (y · x)
+    helper2 _ _ = solve! 𝓡
+
+
+-- A rational number is zero if and only if its numerator is zero
+
+a/b≡0→a≡0 : (x : ℤ × ℕ₊₁) → [ x ] ≡ 0 → x .fst ≡ 0
+a/b≡0→a≡0 (a , b) a/b≡0 = sym (·ℤ-identityʳ a) ∙ a·1≡0·b ∙ ·ℤ-zeroˡ (ℕ₊₁→ℤ b)
+  where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
+        a·1≡0·b = effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ a/b≡0
+
+a≡0→a/b≡0 : (x : ℤ × ℕ₊₁) → x .fst ≡ 0 → [ x ] ≡ 0
+a≡0→a/b≡0 (a , b) a≡0 = eq/ _ _ a·1≡0·b
+  where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
+        a·1≡0·b = (λ i → a≡0 i ·ℤ 1) ∙ ·ℤ-zeroˡ {s = spos} 1 ∙ sym (·ℤ-zeroˡ (ℕ₊₁→ℤ b))
+
+
+-- ℚ is a field
+
+open CommRingStr (ℚCommRing .snd)
+open Units        ℚCommRing
+open Helpers      ℤCommRing
+
+
+hasInverseℚ : (q : ℚ) → ¬ q ≡ 0 → Σ[ p ∈ ℚ ] q · p ≡ 1
+hasInverseℚ = SetQuot.elimProp (λ q → isPropΠ (λ _ → inverseUniqueness q))
+  (λ 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)
+  where
+  inv-helper : (x : ℤ × ℕ₊₁) → ¬ x .fst ≡ 0 → ℚ
+  inv-helper (signed spos (suc a) , b) _ = [ ℕ₊₁→ℤ b , 1+ a ]
+  inv-helper (signed sneg (suc a) , b) _ = [ -ℤ ℕ₊₁→ℤ b , 1+ a ]
+  inv-helper (signed spos zero , _) a≢0 = Empty.rec (a≢0 refl)
+  inv-helper (signed sneg zero , _) a≢0 = Empty.rec (a≢0 (sym posneg))
+  inv-helper (posneg i , _) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))
+
+  inv·-helper : (x : ℤ × ℕ₊₁)(a≢0 : ¬ x .fst ≡ 0) → [ x ] · inv-helper x a≢0 ≡ 1
+  inv·-helper (signed spos zero , b) a≢0 = Empty.rec (a≢0 refl)
+  inv·-helper (signed sneg zero , b) a≢0 = Empty.rec (a≢0 (sym posneg))
+  inv·-helper (posneg i , b) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))
+  inv·-helper (signed spos (suc a) , b) _ = eq/ _ _ (helper1 (pos (suc a)) (ℕ₊₁→ℤ b))
+  inv·-helper (signed sneg (suc a) , b) _ = eq/ _ _ (helper2 (pos (suc a)) (ℕ₊₁→ℤ b))
+
+0≢1-ℚ : ¬ Path ℚ 0 1
+0≢1-ℚ p = 0≢1-ℤ (effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ p)
+
+
+-- The instance
+
+ℚField : Field ℓ-zero
+ℚField = makeFieldFromCommRing ℚCommRing hasInverseℚ 0≢1-ℚ

Cubical/Algebra/Field/Instances/Rationals.agda

@@ -5,87 +5,82 @@
 -}
 module Cubical.Algebra.Field.Instances.Rationals where
 
-open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude
 
-open import Cubical.Data.Sigma
-open import Cubical.Data.Empty as Empty
-open import Cubical.Data.Nat using (ℕ ; zero ; suc)
-open import Cubical.Data.NatPlusOne
-open import Cubical.Data.Int.MoreInts.QuoInt
-  using    (ℤ ; spos ; sneg ; pos ; neg ; signed ; posneg ; isSetℤ ; 0≢1-ℤ)
-  renaming (_·_ to _·ℤ_ ; -_ to -ℤ_
-           ; ·-zeroˡ to ·ℤ-zeroˡ
-           ; ·-identityʳ to ·ℤ-identityʳ)
-open import Cubical.HITs.SetQuotients as SetQuot
-open import Cubical.Data.Rationals.MoreRationals.QuoQ
-  using    (ℚ ; ℕ₊₁→ℤ ; isEquivRel∼)
-
-open import Cubical.Algebra.Field
 open import Cubical.Algebra.CommRing
-open import Cubical.Tactics.CommRingSolver
-open import Cubical.Algebra.CommRing.Instances.QuoInt
 open import Cubical.Algebra.CommRing.Instances.Rationals
+open import Cubical.Algebra.Field
 
-open import Cubical.Relation.Nullary
-
-
--- It seems there are bugs when applying ring solver to explicit ring.
--- The following is a work-around.
-private
-  module Helpers {ℓ : Level}(𝓡 : CommRing ℓ) where
-    open CommRingStr (𝓡 .snd)
-
-    helper1 : (x y : 𝓡 .fst) → (x · y) · 1r ≡ 1r · (y · x)
-    helper1 _ _ = solve! 𝓡
-
-    helper2 : (x y : 𝓡 .fst) → ((- x) · (- y)) · 1r ≡ 1r · (y · x)
-    helper2 _ _ = solve! 𝓡
-
-
--- A rational number is zero if and only if its numerator is zero
-
-a/b≡0→a≡0 : (x : ℤ × ℕ₊₁) → [ x ] ≡ 0 → x .fst ≡ 0
-a/b≡0→a≡0 (a , b) a/b≡0 = sym (·ℤ-identityʳ a) ∙ a·1≡0·b ∙ ·ℤ-zeroˡ (ℕ₊₁→ℤ b)
-  where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
-        a·1≡0·b = effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ a/b≡0
-
-a≡0→a/b≡0 : (x : ℤ × ℕ₊₁) → x .fst ≡ 0 → [ x ] ≡ 0
-a≡0→a/b≡0 (a , b) a≡0 = eq/ _ _ a·1≡0·b
-  where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
-        a·1≡0·b = (λ i → a≡0 i ·ℤ 1) ∙ ·ℤ-zeroˡ {s = spos} 1 ∙ sym (·ℤ-zeroˡ (ℕ₊₁→ℤ b))
+open import Cubical.Data.Empty as Empty
+open import Cubical.Data.Int as ℤ
+open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc)
+open import Cubical.Data.NatPlusOne
+open import Cubical.Data.Rationals as ℚ
+open import Cubical.Data.Sigma
 
+open import Cubical.HITs.SetQuotients as SetQuotients
 
--- ℚ is a field
+open import Cubical.Relation.Nullary
 
 open CommRingStr (ℚCommRing .snd)
 open Units        ℚCommRing
-open Helpers      ℤCommRing
 
-
-hasInverseℚ : (q : ℚ) → ¬ q ≡ 0 → Σ[ p ∈ ℚ ] q · p ≡ 1
-hasInverseℚ = SetQuot.elimProp (λ q → isPropΠ (λ _ → inverseUniqueness q))
-  (λ 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)
+hasInverseℚ : (x : ℚ) → ¬ x ≡ 0 → Σ[ y ∈ ℚ ] x ℚ.· y ≡ 1
+hasInverseℚ = SetQuotients.elimProp
+  (λ x → isPropΠ (λ _ → inverseUniqueness x))
+  (λ u p → r u p , q u p)
   where
-  inv-helper : (x : ℤ × ℕ₊₁) → ¬ x .fst ≡ 0 → ℚ
-  inv-helper (signed spos (suc a) , b) _ = [ ℕ₊₁→ℤ b , 1+ a ]
-  inv-helper (signed sneg (suc a) , b) _ = [ -ℤ ℕ₊₁→ℤ b , 1+ a ]
-  inv-helper (signed spos zero , _) a≢0 = Empty.rec (a≢0 refl)
-  inv-helper (signed sneg zero , _) a≢0 = Empty.rec (a≢0 (sym posneg))
-  inv-helper (posneg i , _) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))
-
-  inv·-helper : (x : ℤ × ℕ₊₁)(a≢0 : ¬ x .fst ≡ 0) → [ x ] · inv-helper x a≢0 ≡ 1
-  inv·-helper (signed spos zero , b) a≢0 = Empty.rec (a≢0 refl)
-  inv·-helper (signed sneg zero , b) a≢0 = Empty.rec (a≢0 (sym posneg))
-  inv·-helper (posneg i , b) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))
-  inv·-helper (signed spos (suc a) , b) _ = eq/ _ _ (helper1 (pos (suc a)) (ℕ₊₁→ℤ b))
-  inv·-helper (signed sneg (suc a) , b) _ = eq/ _ _ (helper2 (pos (suc a)) (ℕ₊₁→ℤ b))
+  r : (u : ℤ × ℕ₊₁) → ¬ [ u ] ≡ 0 → ℚ
+  r (ℤ.pos zero , b) p =
+    Empty.rec (p (numerator0→0 ((ℤ.pos zero , b)) refl))
+  r (ℤ.pos (suc n) , b) _ = [ (ℕ₊₁→ℤ b , (1+ n)) ]
+  r (ℤ.negsuc n , b) _ = [ (ℤ.- ℕ₊₁→ℤ b , (1+ n)) ]
+
+  q : (u : ℤ × ℕ₊₁) (p : ¬ [ u ] ≡ 0) → [ u ] ℚ.· (r u p) ≡ 1
+  q (ℤ.pos zero , b) p =
+    Empty.rec (p (numerator0→0 ((ℤ.pos zero , b)) refl))
+  q (ℤ.pos (suc n) , (1+ m)) _ =
+    eq/ ((ℤ.pos (suc n) ℤ.· (ℕ₊₁→ℤ (1+ m)) , (1+ m) ·₊₁ (1+ n))) ((1 , 1)) q'
+    where
+    q' = (ℤ.pos (suc n) ℤ.· (ℕ₊₁→ℤ (1+ m))) ℤ.· 1
+           ≡⟨ ℤ.·IdR _ ⟩
+         ℤ.pos (suc n) ℤ.· ℤ.pos (suc m)
+           ≡⟨ sym $ ℤ.pos·pos (suc n) (suc m) ⟩
+         ℤ.pos ((suc n) ℕ.· (suc m))
+           ≡⟨ cong ℤ.pos (ℕ.·-comm (suc n) (suc m)) ⟩
+         ℤ.pos ((suc m) ℕ.· (suc n))
+           ≡⟨ refl ⟩
+         ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))
+           ≡⟨ sym (ℤ.·IdL _) ⟩
+         1 ℤ.· (ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))) ∎
+  q (ℤ.negsuc n , (1+ m)) _ =
+    eq/ ((ℤ.negsuc n ℤ.· ℤ.negsuc m) , ((1+ m) ·₊₁ (1+ n))) ((1 , 1)) q'
+    where
+    q' : (ℤ.negsuc n ℤ.· ℤ.negsuc m , (1+ m) ·₊₁ (1+ n)) ∼ (1 , 1)
+    q' = (ℤ.negsuc n ℤ.· ℤ.negsuc m) ℤ.· 1
+           ≡⟨ ℤ.·IdR _ ⟩
+         (ℤ.negsuc n ℤ.· ℤ.negsuc m)
+           ≡⟨ negsuc·negsuc n m ⟩
+         (ℤ.pos (suc n) ℤ.· ℤ.pos (suc m))
+           ≡⟨ sym $ ℤ.pos·pos (suc n) (suc m) ⟩
+         ℤ.pos ((suc n) ℕ.· (suc m))
+           ≡⟨ cong ℤ.pos (ℕ.·-comm (suc n) (suc m)) ⟩
+         ℤ.pos ((suc m) ℕ.· (suc n))
+           ≡⟨ refl ⟩
+         ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))
+           ≡⟨ sym (ℤ.·IdL _) ⟩
+         1 ℤ.· (ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))) ∎
 
 0≢1-ℚ : ¬ Path ℚ 0 1
 0≢1-ℚ p = 0≢1-ℤ (effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ p)
 
-
--- The instance
-
 ℚField : Field ℓ-zero
 ℚField = makeFieldFromCommRing ℚCommRing hasInverseℚ 0≢1-ℚ
+
+_[_]⁻¹ : (x : ℚ) → ¬ x ≡ 0 → ℚ
+_[_]⁻¹ = FieldStr._[_]⁻¹ $ snd ℚField
+
+_/_[_] : ℚ → (y : ℚ) → ¬ y ≡ 0 → ℚ
+x / y [ p ] = x ℚ.· (y [ p ]⁻¹)

Cubical/Data/Rationals/Properties.agda

@@ -483,3 +483,16 @@ x - y = x + (- y)
 
 +CancelR : ∀ x y z → x + y ≡ z + y → x ≡ z
 +CancelR x y z p = +CancelL y x z (+Comm y x ∙ p ∙ +Comm z y)
+
+numerator0→0 : (u : ℤ × ℕ₊₁) → u .fst ≡ 0 → [ u ] ≡ 0
+numerator0→0 (a , b) p = eq/ ((a , b)) ((0 , 1)) q
+  where
+  q : a ℤ.· (ℕ₊₁→ℤ 1) ≡ 0 ℤ.· (ℕ₊₁→ℤ b)
+  q =
+    a ℤ.· (ℕ₊₁→ℤ 1)
+      ≡⟨ ℤ.·IdR a ⟩
+    a
+      ≡⟨ p ⟩
+    0
+      ≡⟨ sym (ℤ.·AnnihilL (ℕ₊₁→ℤ b)) ⟩
+    0 ℤ.· (ℕ₊₁→ℤ b) ∎