-
Notifications
You must be signed in to change notification settings - Fork 134
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #550 from aljungstrom/modular
Some modular arithmetic
- Loading branch information
Showing
4 changed files
with
326 additions
and
33 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |