diff --git a/Cubical/Algebra/CommRing/Instances/QuoQRationals.agda b/Cubical/Algebra/CommRing/Instances/QuoQRationals.agda new file mode 100644 index 0000000000..c521da7743 --- /dev/null +++ b/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 diff --git a/Cubical/Algebra/CommRing/Instances/Rationals.agda b/Cubical/Algebra/CommRing/Instances/Rationals.agda index d2884b756b..92416ac328 100644 --- a/Cubical/Algebra/CommRing/Instances/Rationals.agda +++ b/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 + diff --git a/Cubical/Algebra/Field/Instances/QuoQRationals.agda b/Cubical/Algebra/Field/Instances/QuoQRationals.agda new file mode 100644 index 0000000000..71fcc00d80 --- /dev/null +++ b/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-ℚ diff --git a/Cubical/Algebra/Field/Instances/Rationals.agda b/Cubical/Algebra/Field/Instances/Rationals.agda index 8f16bc609a..2209eb5f03 100644 --- a/Cubical/Algebra/Field/Instances/Rationals.agda +++ b/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 ]⁻¹) diff --git a/Cubical/Data/Rationals/Properties.agda b/Cubical/Data/Rationals/Properties.agda index cf1d501e99..d12f6bcaf1 100644 --- a/Cubical/Data/Rationals/Properties.agda +++ b/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) ∎