Comm ring solver improvement

.github/workflows/ci-ubuntu.yml

@@ -42,7 +42,7 @@ on:
 ########################################################################
 
 env:
-  AGDA_BRANCH: v2.8.0
+  AGDA_BRANCH: master
   GHC_VERSION: 9.10.2
   CABAL_VERSION: 3.12.1.0
   CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'

Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda

@@ -17,7 +17,7 @@ open import Cubical.Data.Empty as ⊥
 
 open import Cubical.HITs.FreeAbGroup
 open import Cubical.HITs.FreeGroup as FG hiding (rec)
-open import Cubical.HITs.SetQuotients as SQ hiding (_/_ ; rec)
+open import Cubical.HITs.SetQuotients as SQ hiding (_/_ ; rec ; Rec ; ElimProp)
 
 open import Cubical.Algebra.AbGroup
 open import Cubical.Algebra.AbGroup.Instances.Pi

Cubical/Algebra/CommRing/Instances/Fast/Int.agda

@@ -3,8 +3,13 @@ module Cubical.Algebra.CommRing.Instances.Fast.Int where
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Algebra.CommRing
+
+open import Cubical.Algebra.Ring.Properties
 open import Cubical.Data.Fast.Int as Int renaming (_+_ to _+ℤ_; _·_ to _·ℤ_ ; -_ to -ℤ_)
 
+open import Cubical.Data.Nat hiding (_+_; _·_)
+import Cubical.Data.Nat as ℕ
+
 open CommRingStr using (0r ; 1r ; _+_ ; _·_ ; -_ ; isCommRing)
 
 ℤCommRing : CommRing ℓ-zero
@@ -21,3 +26,102 @@ isCommRing (snd ℤCommRing) = isCommRingℤ
     isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc +IdR
                                  -Cancel Int.+Comm Int.·Assoc
                                  Int.·IdR ·DistR+ Int.·Comm
+
+private
+ variable
+  ℓ : Level
+
+module CanonicalHomFromℤ (ring : CommRing ℓ) where
+
+ module R where
+  open CommRingStr (snd ring) public
+  open RingTheory (CommRing→Ring ring) public
+
+ module 𝐙 = CommRingStr (snd ℤCommRing)
+
+ suc-fromℕ : ∀ x → R.fromℕ (suc x) ≡ R.1r R.+ R.fromℕ x
+ suc-fromℕ zero = sym (R.+IdR R.1r)
+ suc-fromℕ (suc x) = refl
+
+
+ fromℕ-pres-+ : (x y : ℕ) → R.fromℕ (x ℕ.+ y) ≡ R.fromℕ x R.+ R.fromℕ y
+ fromℕ-pres-+ zero y = sym (R.+IdL _)
+ fromℕ-pres-+ (suc zero) y = suc-fromℕ y
+ fromℕ-pres-+ (suc (suc x)) y =  cong (R.1r R.+_) (fromℕ-pres-+ (suc x) y) ∙ R.+Assoc _ _ _
+
+
+ fromℤ-pres-minus : (x : ℤ) → R.fromℤ (-ℤ x) ≡ R.- R.fromℤ x
+ fromℤ-pres-minus (pos zero) = sym R.0Selfinverse
+ fromℤ-pres-minus (pos (suc n)) = refl
+ fromℤ-pres-minus (negsuc n) = sym (R.-Idempotent _)
+
+
+ suc-fromℤ : ∀ z → R.fromℤ (1 +ℤ z) ≡ R.1r R.+ R.fromℤ (z)
+ suc-fromℤ (pos n) = suc-fromℕ n
+ suc-fromℤ (negsuc zero) = sym (R.+InvR R.1r)
+
+ suc-fromℤ (negsuc (suc n)) =
+      sym (R.+IdL' _ _ (R.+InvR _))
+   ∙∙ sym (R.+Assoc _ _ _)
+   ∙∙ cong (R.1r R.+_) (R.-Dist _ _)
+
+ fromℤ-pres-+' : (n n₁ : ℕ) →
+      R.fromℤ (pos n +ℤ negsuc n₁) ≡
+      R.fromℤ (pos n) R.+ R.fromℤ (negsuc n₁)
+ fromℤ-pres-+' zero n₁ = sym (R.+IdL _)
+ fromℤ-pres-+' (suc n) n₁ =
+    (cong R.fromℤ (sym (𝐙.+Assoc 1 (pos n) (negsuc n₁)))
+     ∙ suc-fromℤ (pos n +ℤ negsuc n₁))
+    ∙∙ cong (R.1r R.+_) (fromℤ-pres-+' n n₁)
+    ∙∙ R.+Assoc _ _ _
+    ∙ cong (R._+ R.fromℤ (negsuc n₁))
+     (sym (suc-fromℕ n))
+
+ fromℤ-pres-+ : (x y : ℤ) → R.fromℤ (x +ℤ y) ≡ R.fromℤ x R.+ R.fromℤ y
+ fromℤ-pres-+ (pos n) (pos n₁) = fromℕ-pres-+ n n₁
+ fromℤ-pres-+ (pos n) (negsuc n₁) = fromℤ-pres-+' n n₁
+ fromℤ-pres-+ (negsuc n) (pos n₁) =
+       fromℤ-pres-+' n₁ n
+     ∙ R.+Comm _ _
+
+ fromℤ-pres-+ (negsuc n) (negsuc n₁) =
+    cong (R.-_)
+       (cong (R.1r R.+_) (cong R.fromℕ (sym (ℕ.+-suc n n₁)))
+        ∙ sym (suc-fromℕ (n ℕ.+ suc n₁))
+          ∙ fromℕ-pres-+ (suc n) (suc n₁))
+   ∙ sym (R.-Dist _ _)
+
+
+ fromℕ-pres-· : (x y : ℕ) → R.fromℕ (x ℕ.· y) ≡ R.fromℕ x R.· R.fromℕ y
+ fromℕ-pres-· zero y = sym (R.0LeftAnnihilates _)
+ fromℕ-pres-· (suc x) y =
+    fromℕ-pres-+ y (x ℕ.· y)
+   ∙∙ cong₂ (R._+_) (sym (R.·IdL _)) (fromℕ-pres-· x y)
+   ∙∙ sym (R.·DistL+ _ _ _)
+   ∙ cong (R._· R.fromℕ y) (sym (suc-fromℕ x))
+
+ fromℤ-pres-· : (x y : ℤ) → R.fromℤ (x ·ℤ y) ≡ R.fromℤ x R.· R.fromℤ y
+ fromℤ-pres-· (pos n) (pos n₁) = fromℕ-pres-· n n₁
+ fromℤ-pres-· (pos n) (negsuc n₁) =
+        cong R.fromℤ (sym (-DistR· (pos n) (pos (suc n₁))))
+     ∙∙ (fromℤ-pres-minus (pos (n ℕ.· suc n₁))
+        ∙ cong R.-_ (fromℕ-pres-· n (suc n₁)))
+     ∙∙ sym (R.-DistR· _ _)
+
+ fromℤ-pres-· (negsuc n) (pos n₁) =
+           cong R.fromℤ (sym (-DistL· (pos (suc n)) (pos n₁)))
+     ∙∙ (fromℤ-pres-minus (pos ((suc n) ℕ.· n₁))
+        ∙ cong R.-_ (fromℕ-pres-· (suc n) n₁))
+     ∙∙ sym (R.-DistL· _ _)
+
+ fromℤ-pres-· (negsuc n) (negsuc n₁) =
+        fromℕ-pres-· (suc n) (suc n₁)
+    ∙∙ cong₂ R._·_ (sym (R.-Idempotent _)) refl
+    ∙∙ R.-Swap· _ _
+
+ isHomFromℤ : IsCommRingHom (ℤCommRing .snd) R.fromℤ (ring .snd)
+ isHomFromℤ .IsCommRingHom.pres0 = refl
+ isHomFromℤ .IsCommRingHom.pres1 = refl
+ isHomFromℤ .IsCommRingHom.pres+ = fromℤ-pres-+
+ isHomFromℤ .IsCommRingHom.pres· = fromℤ-pres-·
+ isHomFromℤ .IsCommRingHom.pres- = fromℤ-pres-minus

Cubical/Algebra/CommRing/Instances/Rationals.agda

@@ -6,8 +6,11 @@
 module Cubical.Algebra.CommRing.Instances.Rationals where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Algebra.CommRing
 open import Cubical.Data.Rationals as ℚ
+open import Cubical.Data.Empty
+import Cubical.Data.Int as ℤ
 
 ℚCommRing : CommRing ℓ-zero
 ℚCommRing .fst = ℚ
@@ -21,3 +24,5 @@ open import Cubical.Data.Rationals as ℚ
   p : IsCommRing 0 1 _+_ _·_ (-_)
   p = makeIsCommRing isSetℚ +Assoc +IdR +InvR +Comm ·Assoc ·IdR ·DistL+ ·Comm
 
+ℚCommRingIsNotZeroRing : ℚCommRing .snd .CommRingStr.1r ≡ ℚCommRing .snd .CommRingStr.0r → ⊥
+ℚCommRingIsNotZeroRing = ℤ.0≢1-ℤ ∘S sym ∘S eq/⁻¹ _ _

Cubical/Algebra/CommRing/Instances/Unit.agda

@@ -7,11 +7,14 @@ open import Cubical.Data.Unit
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
 
+open import Cubical.Algebra.Ring.Properties
+
 private
   variable
     ℓ ℓ' : Level
 
 open CommRingStr
+open RingStr
 
 UnitCommRing : CommRing ℓ
 fst UnitCommRing = Unit*
@@ -33,5 +36,9 @@ mapToUnitCommRing R .snd .IsCommRingHom.pres+ = λ _ _ → refl
 mapToUnitCommRing R .snd .IsCommRingHom.pres· = λ _ _ → refl
 mapToUnitCommRing R .snd .IsCommRingHom.pres- = λ _ → refl
 
-isPropMapToUnitCommRing : {ℓ : Level} (R : CommRing ℓ') → isProp (CommRingHom R (UnitCommRing {ℓ = ℓ}))
+isPropMapToUnitCommRing : (R : CommRing ℓ') → isProp (CommRingHom R (UnitCommRing {ℓ = ℓ}))
 isPropMapToUnitCommRing R f g = CommRingHom≡ (funExt λ _ → refl)
+
+[1=0]→≃UnitCommRing : (R : Ring ℓ') → (1r (snd R) ≡ 0r (snd R)) → RingEquiv R (CommRing→Ring (UnitCommRing {ℓ}))
+[1=0]→≃UnitCommRing R 1=0 = isContr→≃Unit* (RingTheory.zeroRing.isContrR R 1=0) ,
+  makeIsRingHom (λ _ → _) (λ _ _ _ → _) λ _ _ _ → _

Cubical/Algebra/CommRing/Properties.agda

@@ -15,6 +15,7 @@ open import Cubical.Foundations.Powerset
 open import Cubical.Foundations.Path
 
 open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
 open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_
                                       ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)
 
@@ -145,7 +146,6 @@ module Units (R' : CommRing ℓ) where
                                   ∙ congR _·_ (·-rinv _)
                                   ∙ ·IdR _
 
-
 -- some convenient notation
 _ˣ : (R' : CommRing ℓ) → ℙ (R' .fst)
 R' ˣ = Units.Rˣ R'
@@ -223,6 +223,7 @@ module _ where
 
 module Exponentiation (R' : CommRing ℓ) where
  open CommRingStr (snd R')
+ open RingTheory (CommRing→Ring R')
  private R = fst R'
 
  -- introduce exponentiation
@@ -260,13 +261,28 @@ module Exponentiation (R' : CommRing ℓ) where
                         ∙∙ cong (f ^ m ·_) (^-rdist-·ℕ f n m)
                         ∙∙ sym  (^-ldist-· f (f ^ n) m)
 
+ 0^ˢⁿ≡0 : ∀ n → 0r ^ (suc n) ≡ 0r
+ 0^ˢⁿ≡0 _ = 0LeftAnnihilates _
+
  -- interaction of exponentiation and units
  open Units R'
 
  ^-presUnit : ∀ (f : R) (n : ℕ) → f ∈ Rˣ → f ^ n ∈ Rˣ
  ^-presUnit f zero f∈Rˣ = RˣContainsOne
  ^-presUnit f (suc n) f∈Rˣ = RˣMultClosed f (f ^ n) ⦃ f∈Rˣ ⦄ ⦃ ^-presUnit f n f∈Rˣ ⦄
 
+ module IntegralDomain (isIntDom : (c m : R) → c · m ≡ 0r → (c ≡ 0r → ⊥) → m ≡ 0r) where
+
+  x≢0→x^sn≢0 : ∀ x n → (x ≡ 0r → ⊥) → (x ^ (suc n) ≡ 0r → ⊥)
+  x≢0→x^sn≢0 x zero x≢0 p = x≢0 (sym (·IdR x) ∙ p )
+  x≢0→x^sn≢0 x (suc n) x≢0 p =
+    x≢0→x^sn≢0 x n x≢0 (isIntDom x (x ^ (suc n)) p x≢0)
+
+  x≢0≃x^sn≢0 : ∀ x n → (x ≡ 0r → ⊥) ≃ (x ^ (suc n) ≡ 0r → ⊥)
+  x≢0≃x^sn≢0 x n = propBiimpl→Equiv (isPropΠ λ _ → isProp⊥) (isPropΠ λ _ → isProp⊥)
+    (x≢0→x^sn≢0 x n) (_∘ λ x≡0 → cong (_^ (suc n)) x≡0 ∙ 0^ˢⁿ≡0 n)
+
+
 module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where
  open Units A' renaming (Rˣ to Aˣ ; _⁻¹ to _⁻¹ᵃ ; ·-rinv to ·A-rinv ; ·-linv to ·A-linv)
  open Units B' renaming (Rˣ to Bˣ ; _⁻¹ to _⁻¹ᵇ ; ·-rinv to ·B-rinv)

Cubical/Algebra/Field/Instances/Rationals.agda

@@ -18,6 +18,7 @@ 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.Rationals.Order.Properties
 open import Cubical.Data.Sigma
 
 open import Cubical.HITs.SetQuotients as SetQuotients
@@ -27,52 +28,6 @@ open import Cubical.Relation.Nullary
 open CommRingStr (ℚCommRing .snd)
 open Units        ℚCommRing
 
-hasInverseℚ : (x : ℚ) → ¬ x ≡ 0 → Σ[ y ∈ ℚ ] x ℚ.· y ≡ 1
-hasInverseℚ = SetQuotients.elimProp
-  (λ x → isPropΠ (λ _ → inverseUniqueness x))
-  (λ u p → r u p , q u p)
-  where
-  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)