Some modular arithmetic

Cubical/Algebra/Group/Instances/IntMod.agda

@@ -0,0 +1,69 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Group.Instances.IntMod where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Algebra.Group.Instances.Int
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Monoid.Base
+open import Cubical.Algebra.Semigroup.Base
+open import Cubical.Data.Empty renaming (rec to ⊥-rec)
+open import Cubical.Data.Bool
+open import Cubical.Data.Fin
+open import Cubical.Data.Fin.Arithmetic
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Algebra.Group.Instances.Unit
+  renaming (Unit to UnitGroup)
+open import Cubical.Algebra.Group.Instances.Bool
+  renaming (Bool to BoolGroup)
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Sigma
+
+open GroupStr
+open IsGroup
+open IsMonoid
+
+ℤ/_ : ℕ → Group₀
+ℤ/ zero = UnitGroup
+fst (ℤ/ suc n) = Fin (suc n)
+1g (snd (ℤ/ suc n)) = 0
+GroupStr._·_ (snd (ℤ/ suc n)) = _+ₘ_
+inv (snd (ℤ/ suc n)) = -ₘ_
+IsSemigroup.is-set (isSemigroup (isMonoid (isGroup (snd (ℤ/ suc n))))) =
+  isSetFin
+IsSemigroup.assoc (isSemigroup (isMonoid (isGroup (snd (ℤ/ suc n))))) =
+  λ x y z → sym (+ₘ-assoc x y z)
+fst (identity (isMonoid (isGroup (snd (ℤ/ suc n)))) x) = +ₘ-rUnit x
+snd (identity (isMonoid (isGroup (snd (ℤ/ suc n)))) x) = +ₘ-lUnit x
+fst (inverse (isGroup (snd (ℤ/ suc n))) x) = +ₘ-rCancel x
+snd (inverse (isGroup (snd (ℤ/ suc n))) x) = +ₘ-lCancel x
+
+ℤ/1≅Unit : GroupIso (ℤ/ 1) UnitGroup
+ℤ/1≅Unit = contrGroupIsoUnit isContrFin1
+
+Bool≅ℤ/2 : GroupIso BoolGroup (ℤ/ 2)
+Iso.fun (fst Bool≅ℤ/2) false = 1
+Iso.fun (fst Bool≅ℤ/2) true = 0
+Iso.inv (fst Bool≅ℤ/2) (zero , p) = true
+Iso.inv (fst Bool≅ℤ/2) (suc zero , p) = false
+Iso.inv (fst Bool≅ℤ/2) (suc (suc x) , p) =
+  ⊥-rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p)))
+Iso.rightInv (fst Bool≅ℤ/2) (zero , p) =
+  Σ≡Prop (λ _ → m≤n-isProp) refl
+Iso.rightInv (fst Bool≅ℤ/2) (suc zero , p) =
+  Σ≡Prop (λ _ → m≤n-isProp) refl
+Iso.rightInv (fst Bool≅ℤ/2) (suc (suc x) , p) =
+  ⊥-rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p)))
+Iso.leftInv (fst Bool≅ℤ/2) false = refl
+Iso.leftInv (fst Bool≅ℤ/2) true = refl
+snd Bool≅ℤ/2 =
+  makeIsGroupHom λ { false false → refl
+                   ; false true → refl
+                   ; true false → refl
+                   ; true true → refl}
+
+ℤ/2≅Bool : GroupIso (ℤ/ 2) BoolGroup
+ℤ/2≅Bool = invGroupIso Bool≅ℤ/2

Cubical/Algebra/Group/MorphismProperties.agda

@@ -184,25 +184,25 @@ compGroupEquiv : GroupEquiv F G → GroupEquiv G H → GroupEquiv F H
 fst (compGroupEquiv f g) = compEquiv (fst f) (fst g)
 snd (compGroupEquiv f g) = isGroupHomComp (_ , f .snd) (_ , g .snd)
 
+isGroupHomInv : (f : GroupEquiv G H) → IsGroupHom (H .snd) (invEq (fst f)) (G .snd)
+isGroupHomInv {G = G} {H = H} f = makeIsGroupHom λ h h' →
+  isInj-f _ _
+    (f' (g (h ⋆² h'))        ≡⟨ secEq (fst f) _ ⟩
+     (h ⋆² h')               ≡⟨ sym (cong₂ _⋆²_ (secEq (fst f) h) (secEq (fst f) h')) ⟩
+     (f' (g h) ⋆² f' (g h')) ≡⟨ sym (pres· (snd f) _ _) ⟩
+     f' (g h ⋆¹ g h') ∎)
+  where
+  f' = fst (fst f)
+  _⋆¹_ = _·_ (snd G)
+  _⋆²_ = _·_ (snd H)
+  g = invEq (fst f)
+
+  isInj-f : (x y : ⟨ G ⟩) → f' x ≡ f' y → x ≡ y
+  isInj-f x y = invEq (_ , isEquiv→isEmbedding (snd (fst f)) x y)
+
 invGroupEquiv : GroupEquiv G H → GroupEquiv H G
 fst (invGroupEquiv f) = invEquiv (fst f)
 snd (invGroupEquiv f) = isGroupHomInv f
-  where
-  isGroupHomInv : (f : GroupEquiv G H) → IsGroupHom (H .snd) (invEq (fst f)) (G .snd)
-  isGroupHomInv {G = G} {H = H} f = makeIsGroupHom λ h h' →
-    isInj-f _ _
-      (f' (g (h ⋆² h'))        ≡⟨ secEq (fst f) _ ⟩
-       (h ⋆² h')               ≡⟨ sym (cong₂ _⋆²_ (secEq (fst f) h) (secEq (fst f) h')) ⟩
-       (f' (g h) ⋆² f' (g h')) ≡⟨ sym (pres· (snd f) _ _) ⟩
-       f' (g h ⋆¹ g h') ∎)
-    where
-    f' = fst (fst f)
-    _⋆¹_ = _·_ (snd G)
-    _⋆²_ = _·_ (snd H)
-    g = invEq (fst f)
-
-    isInj-f : (x y : ⟨ G ⟩) → f' x ≡ f' y → x ≡ y
-    isInj-f x y = invEq (_ , isEquiv→isEmbedding (snd (fst f)) x y)
 
 GroupEquivDirProd : {A : Group ℓ} {B : Group ℓ'} {C : Group ℓ''} {D : Group ℓ'''}
                   → GroupEquiv A C → GroupEquiv B D
@@ -229,23 +229,7 @@ snd (compGroupIso iso1 iso2) = isGroupHomComp (_ , snd iso1) (_ , snd iso2)
 
 invGroupIso : GroupIso G H → GroupIso H G
 fst (invGroupIso iso1) = invIso (fst iso1)
-snd (invGroupIso iso1) = isGroupHomInv iso1
-  where
-  isGroupHomInv : (f : GroupIso G H) → IsGroupHom (H .snd) (inv (fst f)) (G .snd)
-  isGroupHomInv {G = G} {H = H}  f = makeIsGroupHom λ h h' →
-    isInj-f _ _
-      (f' (g (h ⋆² h')) ≡⟨ (rightInv (fst f)) _ ⟩
-       (h ⋆² h') ≡⟨ sym (cong₂ _⋆²_ (rightInv (fst f) h) (rightInv (fst f) h')) ⟩
-       (f' (g h) ⋆² f' (g h')) ≡⟨ sym (f .snd .pres· _ _) ⟩
-       f' (g h ⋆¹ g h') ∎)
-    where
-    f' = fun (fst f)
-    _⋆¹_ = GroupStr._·_ (snd G)
-    _⋆²_ = GroupStr._·_ (snd H)
-    g = inv (fst f)
-
-    isInj-f : (x y : ⟨ G ⟩) → f' x ≡ f' y → x ≡ y
-    isInj-f x y p = sym (leftInv (fst f) _) ∙∙ cong g p ∙∙ leftInv (fst f) _
+snd (invGroupIso iso1) = isGroupHomInv (isoToEquiv (fst iso1) , snd iso1)
 
 GroupIsoDirProd : {G : Group ℓ} {H : Group ℓ'} {A : Group ℓ''} {B : Group ℓ'''}
                 → GroupIso G H → GroupIso A B → GroupIso (DirProd G A) (DirProd H B)

Cubical/Data/Fin/Arithmetic.agda

@@ -0,0 +1,87 @@
+{-# OPTIONS --cubical --safe #-}
+module Cubical.Data.Fin.Arithmetic where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Mod
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Fin
+open import Cubical.Data.Sigma
+
+infixl 6 _+ₘ_ _-ₘ_ _·ₘ_
+infix 7 -ₘ_
+
+-- Addition, subtraction and multiplication
+_+ₘ_ : {n : ℕ} → Fin (suc n) → Fin (suc n) → Fin (suc n)
+fst (_+ₘ_ {n = n} x y) = ((fst x) + (fst y)) mod (suc n)
+snd (_+ₘ_ {n = n} x y) = mod< _ ((fst x) + (fst y))
+
+-ₘ_ : {n : ℕ} → (x : Fin (suc n)) → Fin (suc n)
+fst (-ₘ_ {n = n} x) =
+  (+induction n _ (λ x _ → ((suc n) ∸ x) mod (suc n)) λ _ x → x) (fst x)
+snd (-ₘ_ {n = n} x) = lem (fst x)
+  where
+  ≡<-trans : {x y z : ℕ} → x < y → x ≡ z → z < y
+  ≡<-trans (k , p) q = k , cong (λ x → k + suc x) (sym q) ∙ p
+
+  lem : {n : ℕ} (x : ℕ)
+     → (+induction n _ _ _) x < suc n
+  lem {n = n} =
+    +induction n _
+      (λ x p → ≡<-trans (mod< n (suc n ∸ x))
+                 (sym (+inductionBase n _ _ _ x p)))
+       λ x p → ≡<-trans p
+                 (sym (+inductionStep n _ _ _ x))
+
+_-ₘ_ : {n : ℕ} → (x y : Fin (suc n)) → Fin (suc n)
+_-ₘ_ x y = x +ₘ (-ₘ y)
+
+_·ₘ_ : {n : ℕ} → (x y : Fin (suc n)) → Fin (suc n)
+fst (_·ₘ_ {n = n} x y) = (fst x · fst y) mod (suc n)
+snd (_·ₘ_ {n = n} x y) = mod< n (fst x · fst y)
+
+-- Group laws
++ₘ-assoc : {n : ℕ} (x y z : Fin (suc n))
+  → (x +ₘ y) +ₘ z ≡ (x +ₘ (y +ₘ z))
++ₘ-assoc {n = n} x y z =
+  Σ≡Prop (λ _ → m≤n-isProp)
+       ((mod-rCancel (suc n) ((fst x + fst y) mod (suc n)) (fst z))
+    ∙∙ sym (mod+mod≡mod (suc n) (fst x + fst y) (fst z))
+    ∙∙ cong (_mod suc n) (sym (+-assoc (fst x) (fst y) (fst z)))
+    ∙∙ mod+mod≡mod (suc n) (fst x) (fst y + fst z)
+    ∙∙ sym (mod-lCancel (suc n) (fst x) ((fst y + fst z) mod suc n)))
+
++ₘ-comm : {n : ℕ} (x y : Fin (suc n)) → (x +ₘ y) ≡ (y +ₘ x)
++ₘ-comm {n = n} x y =
+  Σ≡Prop (λ _ → m≤n-isProp)
+    (cong (_mod suc n) (+-comm (fst x) (fst y)))
+
++ₘ-lUnit : {n : ℕ} (x : Fin (suc n)) → 0 +ₘ x ≡ x
++ₘ-lUnit {n = n} (x , p) =
+  Σ≡Prop (λ _ → m≤n-isProp)
+    (+inductionBase n _ _ _ x p)
+
++ₘ-rUnit : {n : ℕ} (x : Fin (suc n)) → x +ₘ 0 ≡ x
++ₘ-rUnit x = +ₘ-comm x 0 ∙ (+ₘ-lUnit x)
+
++ₘ-rCancel : {n : ℕ} (x : Fin (suc n)) → x -ₘ x ≡ 0
++ₘ-rCancel {n = n} x =
+  Σ≡Prop (λ _ → m≤n-isProp)
+      (cong (λ z → (fst x + z) mod (suc n))
+            (+inductionBase n _ _ _ (fst x) (snd x))
+    ∙∙ sym (mod-rCancel (suc n) (fst x) ((suc n) ∸ (fst x)))
+    ∙∙ cong (_mod (suc n)) (+-comm (fst x) ((suc n) ∸ (fst x)))
+    ∙∙ cong (_mod (suc n)) (≤-∸-+-cancel (<-weaken (snd x)))
+    ∙∙ zero-charac (suc n))
+
++ₘ-lCancel : {n : ℕ} (x : Fin (suc n)) → (-ₘ x) +ₘ x ≡ 0
++ₘ-lCancel {n = n} x = +ₘ-comm (-ₘ x) x ∙ +ₘ-rCancel x
+
+-- TODO : Ring laws
+
+private
+  test₁ : Path (Fin 11) (5 +ₘ 10) 4
+  test₁ = refl
+
+  test₂ : Path (Fin 11) (-ₘ 7 +ₘ 5 +ₘ 10) 8
+  test₂ = refl

Cubical/Data/Nat/Mod.agda

@@ -0,0 +1,153 @@
+{-# OPTIONS --cubical --safe #-}
+module Cubical.Data.Nat.Mod where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+
+-- Defining x mod 0 to be 0. This way all the theorems below are true
+-- for n : ℕ instead of n : ℕ₊₁.
+
+------ Preliminary definitions ------
+modInd : (n : ℕ) → ℕ → ℕ
+modInd n = +induction n (λ _ → ℕ) (λ x _ → x) λ _ x → x
+
+modIndBase : (n m : ℕ) → m < suc n → modInd n m ≡ m
+modIndBase n = +inductionBase n (λ _ → ℕ) (λ x _ → x) (λ _ x → x)
+
+modIndStep : (n m : ℕ) → modInd n (suc n + m) ≡ modInd n m
+modIndStep n = +inductionStep n (λ _ → ℕ) (λ x _ → x) (λ _ x → x)
+-------------------------------------
+
+_mod_ : (x n : ℕ) → ℕ
+x mod zero = 0
+x mod (suc n) = modInd n x
+
+mod< : (n x : ℕ) → x mod (suc n) < (suc n)
+mod< n =
+  +induction n
+    (λ x → x mod (suc n) < suc n)
+    (λ x base → fst base
+               , (cong (λ x → fst base + suc x)
+                       (modIndBase n x base)
+                ∙ snd base))
+     λ x ind → fst ind
+              , cong (λ x → fst ind + suc x)
+                     (modIndStep n x) ∙ snd ind
+
+mod-rUnit : (n x : ℕ) → x mod n ≡ ((x + n) mod n)
+mod-rUnit zero x = refl
+mod-rUnit (suc n) x =
+    sym (modIndStep n x)
+  ∙ cong (modInd n) (+-comm (suc n) x)
+
+mod-lUnit : (n x : ℕ) → x mod n ≡ ((n + x) mod n)
+mod-lUnit zero _ = refl
+mod-lUnit (suc n) x = sym (modIndStep n x)
+
+mod+mod≡mod : (n x y : ℕ)
+  → (x + y) mod n ≡ (((x mod n) + (y mod n)) mod n)
+mod+mod≡mod zero _ _ = refl
+mod+mod≡mod (suc n) =
+  +induction n
+    (λ z → (x : ℕ)
+         → ((z + x) mod (suc n))
+         ≡ (((z mod (suc n)) + (x mod (suc n))) mod (suc n)))
+    (λ x p →
+      +induction n _
+        (λ y q → cong (modInd n)
+                       (sym (cong₂  _+_ (modIndBase n x p)
+                       (modIndBase n y q))))
+        λ y ind → cong (modInd n)
+                        (cong (x +_) (+-comm (suc n) y)
+                                   ∙ (+-assoc x y (suc n)))
+                     ∙∙ sym (mod-rUnit (suc n) (x + y))
+                     ∙∙ ind
+                      ∙ cong (λ z → modInd n
+                                    ((modInd n x + z)))
+                             (mod-rUnit (suc n) y
+                             ∙ cong (modInd n) (+-comm y (suc n))))
+    λ x p y →
+      cong (modInd n) (cong suc (sym (+-assoc n x y)))
+        ∙∙ sym (mod-lUnit (suc n) (x + y))
+        ∙∙ p y
+         ∙ sym (cong (modInd n)
+                (cong (_+ modInd n y)
+                 (cong (modInd n)
+                  (+-comm (suc n) x) ∙ sym (mod-rUnit (suc n) x))))
+
+mod-idempotent : {n : ℕ} (x : ℕ) → (x mod n) mod n ≡ x mod n
+mod-idempotent {n = zero} _ = refl
+mod-idempotent {n = suc n} =
+  +induction n (λ x → (x mod suc n) mod (suc n) ≡ x mod (suc n))
+             (λ x p → cong (_mod (suc n))
+                            (modIndBase n x p))
+              λ x p → cong (_mod (suc n))
+                            (modIndStep n x)
+                          ∙∙ p
+                          ∙∙ mod-rUnit (suc n) x
+                           ∙ (cong (_mod (suc n)) (+-comm x (suc n)))
+
+mod-rCancel : (n x y : ℕ) → (x + y) mod n ≡ (x + y mod n) mod n
+mod-rCancel zero x y = refl
+mod-rCancel (suc n) x =
+  +induction n _
+    (λ y p → cong (λ z → (x + z) mod (suc n))
+                   (sym (modIndBase n y p)))
+     λ y p → cong (_mod suc n) (+-assoc x (suc n) y
+                             ∙∙ (cong (_+ y) (+-comm x (suc n)))
+                             ∙∙ sym (+-assoc (suc n) x y))
+          ∙∙ sym (mod-lUnit (suc n) (x + y))
+          ∙∙ (p ∙ cong (λ z → (x + z) mod suc n) (mod-lUnit (suc n) y))
+
+mod-lCancel : (n x y : ℕ) → (x + y) mod n ≡ (x mod n + y) mod n
+mod-lCancel n x y =
+     cong (_mod n) (+-comm x y)
+  ∙∙ mod-rCancel n y x
+  ∙∙ cong (_mod n) (+-comm y (x mod n))
+
+zero-charac : (n : ℕ) → n mod n ≡ 0
+zero-charac zero = refl
+zero-charac (suc n) = cong (_mod suc n) (+-comm 0 (suc n))
+                  ∙∙ modIndStep n 0
+                  ∙∙ modIndBase n 0 (n , (+-comm n 1))
+
+-- remainder and quotient after division by n
+-- Again, allowing for 0-division to get nicer syntax
+remainder_/_ : (x n : ℕ) → ℕ
+remainder x / zero = x
+remainder x / suc n = x mod (suc n)
+
+quotient_/_ : (x n : ℕ) → ℕ
+quotient x / zero = 0
+quotient x / suc n =
+  +induction n (λ _ → ℕ) (λ _ _ → 0) (λ _ → suc) x
+
+≡remainder+quotient : (n x : ℕ)
+  → (remainder x / n) + n · (quotient x / n) ≡ x
+≡remainder+quotient zero x = +-comm x 0
+≡remainder+quotient (suc n) =
+  +induction n
+    (λ x → (remainder x / (suc n)) + (suc n)
+          · (quotient x / (suc n)) ≡ x)
+    (λ x base → cong₂ _+_ (modIndBase n x base)
+                           (cong ((suc n) ·_)
+                           (+inductionBase n _ _ _ x base))
+              ∙∙ cong (x +_) (·-comm n 0)
+              ∙∙ +-comm x 0)
+     λ x ind → cong₂ _+_ (modIndStep n x)
+                        (cong ((suc n) ·_) (+inductionStep n _ _ _ x))
+          ∙∙ cong (modInd n x +_)
+                  (·-suc (suc n) (+induction n _ _ _ x))
+          ∙∙ cong (modInd n x +_)
+                  (+-comm (suc n) ((suc n) · (+induction n _ _ _ x)))
+          ∙∙ +-assoc (modInd n x) ((suc n) · +induction n _ _ _ x) (suc n)
+          ∙∙ cong (_+ suc n) ind
+           ∙ +-comm x (suc n)
+
+private
+  test₀ : 100 mod 81 ≡ 19
+  test₀ = refl
+
+  test₁ : ((11 + (10 mod 3)) mod 3) ≡ 0
+  test₁ = refl