From 1054d17b0e19120c59f67145c2733b3eba8edf87 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 25 Jan 2024 08:19:11 +0000 Subject: [PATCH 01/29] sketch of arithmetic mod n, based on `Data.Nat.Bounded` --- src/Data/Integer/Modulo.agda | 102 ++++++++++++++++++++++++++ src/Data/Integer/Modulo/Literals.agda | 17 +++++ 2 files changed, 119 insertions(+) create mode 100644 src/Data/Integer/Modulo.agda create mode 100644 src/Data/Integer/Modulo/Literals.agda diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda new file mode 100644 index 0000000000..94089f4e14 --- /dev/null +++ b/src/Data/Integer/Modulo.agda @@ -0,0 +1,102 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Integers mod n, type and basic operations +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Data.Nat.Base as ℕ + using (ℕ; zero; suc; NonZero; NonTrivial; _<_; _∸_) + +module Data.Integer.Modulo (n : ℕ) .{{_ : NonTrivial n}} where + +open import Algebra.Bundles.Raw + using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring) +open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) +open import Data.Nat.Bounded as Bounded hiding (π; module Literals) +open import Data.Nat.DivMod as ℕ using (_%_) +open import Data.Nat.Properties as ℕ +import Data.Sign.Base as Sign +open import Data.Unit.Base using (⊤) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) + +private + variable + m o p : ℕ + i j : ℕ< n + + instance + _ = ℕ.nonTrivial⇒nonZero n + + m∸n Date: Thu, 25 Jan 2024 12:20:40 +0000 Subject: [PATCH 02/29] `RawRing`, not only `RawSemiring` --- src/Data/Integer/Modulo.agda | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index 94089f4e14..c0695e3f1b 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -12,7 +12,7 @@ open import Data.Nat.Base as ℕ module Data.Integer.Modulo (n : ℕ) .{{_ : NonTrivial n}} where open import Algebra.Bundles.Raw - using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring) + using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) open import Data.Nat.Bounded as Bounded hiding (π; module Literals) open import Data.Nat.DivMod as ℕ using (_%_) @@ -23,8 +23,8 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_) private variable - m o p : ℕ - i j : ℕ< n + m o : ℕ + i j : ℕ< n instance _ = ℕ.nonTrivial⇒nonZero n @@ -51,11 +51,11 @@ infixl 6 _+_ -- Addition _+_ : ℤmod → ℤmod → ℤmod -⟦ o ⟧< _ + ⟦ p ⟧< _ = Bounded.π (o ℕ.+ p) +i + j = Bounded.π (⟦ i ⟧ ℕ.+ ⟦ j ⟧) -- Multiplication _*_ : ℤmod → ℤmod → ℤmod -⟦ o ⟧< _ * ⟦ p ⟧< _ = Bounded.π (o ℕ.* p) +i * j = Bounded.π (⟦ i ⟧ ℕ.* ⟦ j ⟧) ------------------------------------------------------------------------ -- Projection from ℤ @@ -73,20 +73,22 @@ syntax Mod {n = n} i = i mod n ------------------------------------------------------------------------ -- Raw bundles -+-*-rawSemiring : RawSemiring _ _ -+-*-rawSemiring = record ++-*-rawRing : RawRing _ _ ++-*-rawRing = record { _≈_ = _≡_ ; _+_ = _+_ ; _*_ = _*_ + ; -_ = -_ ; 0# = ⟦0⟧< ; 1# = ⟦1⟧< } -open RawSemiring +-*-rawSemiring public +open RawRing +-*-rawRing public using (+-rawMagma; *-rawMagma) renaming ( +-rawMonoid to +-0-rawMonoid ; *-rawMonoid to *-1-rawMonoid ; rawNearSemiring to +-*-rawNearSemiring + ; rawSemiring to +-*-rawSemiring ) ------------------------------------------------------------------------ From edfe8173b48fad2db556922469d9802b4320d9d1 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 25 Jan 2024 15:13:01 +0000 Subject: [PATCH 03/29] tweaks --- src/Data/Integer/Modulo.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index c0695e3f1b..1c2ee39925 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -14,7 +14,7 @@ module Data.Integer.Modulo (n : ℕ) .{{_ : NonTrivial n}} where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.Bounded as Bounded hiding (π; module Literals) +open import Data.Nat.Bounded as ℕ< hiding (π; module Literals) open import Data.Nat.DivMod as ℕ using (_%_) open import Data.Nat.Properties as ℕ import Data.Sign.Base as Sign @@ -51,16 +51,16 @@ infixl 6 _+_ -- Addition _+_ : ℤmod → ℤmod → ℤmod -i + j = Bounded.π (⟦ i ⟧ ℕ.+ ⟦ j ⟧) +i + j = ℕ<.π (⟦ i ⟧ ℕ.+ ⟦ j ⟧) -- Multiplication _*_ : ℤmod → ℤmod → ℤmod -i * j = Bounded.π (⟦ i ⟧ ℕ.* ⟦ j ⟧) +i * j = ℕ<.π (⟦ i ⟧ ℕ.* ⟦ j ⟧) ------------------------------------------------------------------------ -- Projection from ℤ π : ℤ → ℤmod -π i with s ◂ ∣i∣ ← signAbs i with j ← Bounded.π ∣i∣ | s +π i with s ◂ ∣i∣ ← signAbs i with j ← ℕ<.π ∣i∣ | s ... | Sign.+ = j ... | Sign.- = - j @@ -100,5 +100,5 @@ module Literals where Constraint _ = ⊤ fromNat : ∀ m → {{Constraint m}} → ℤmod - fromNat m = Bounded.π m + fromNat m = ℕ<.π m From 5808442a5706eafd37e0a42965a973db9dbd8da1 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 1 Feb 2024 07:17:36 +0000 Subject: [PATCH 04/29] streamline the quotient map --- src/Data/Integer/Modulo.agda | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index 1c2ee39925..01f7409f88 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -58,11 +58,14 @@ _*_ : ℤmod → ℤmod → ℤmod i * j = ℕ<.π (⟦ i ⟧ ℕ.* ⟦ j ⟧) ------------------------------------------------------------------------ --- Projection from ℤ +-- Quotient map from ℤ + +_◃_ : Sign → ℤmod → ℤmod +Sign.+ ◃ j = j +Sign.- ◃ j = - j + π : ℤ → ℤmod -π i with s ◂ ∣i∣ ← signAbs i with j ← ℕ<.π ∣i∣ | s -... | Sign.+ = j -... | Sign.- = - j +π i with s ◂ ∣i∣ ← signAbs i = s ◃ ℕ<.π ∣i∣ -- the _mod_ syntax Mod : ℤ → ℤmod From 7fbcb465755a322848171e43299083baac53781f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 1 Feb 2024 09:31:23 +0000 Subject: [PATCH 05/29] start of proving the `IsRing` property --- src/Data/Integer/Modulo.agda | 28 ++++++----- src/Data/Integer/Modulo/Properties.agda | 65 +++++++++++++++++++++++++ 2 files changed, 82 insertions(+), 11 deletions(-) create mode 100644 src/Data/Integer/Modulo/Properties.agda diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index 01f7409f88..b066efda1f 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -17,7 +17,7 @@ open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) open import Data.Nat.Bounded as ℕ< hiding (π; module Literals) open import Data.Nat.DivMod as ℕ using (_%_) open import Data.Nat.Properties as ℕ -import Data.Sign.Base as Sign +open import Data.Sign.Base as Sign using (Sign) open import Data.Unit.Base using (⊤) open import Relation.Binary.PropositionalEquality.Core using (_≡_) @@ -41,34 +41,34 @@ infixl 7 _*_ infixl 6 _+_ -- Type definition -ℤmod : Set -ℤmod = ℕ< n +ℤmod_ : Set +ℤmod_ = ℕ< n -- Negation --_ : ℤmod → ℤmod +-_ : ℤmod_ → ℤmod_ - ⟦ m@zero ⟧< _ = ⟦0⟧< - ⟦ m@(suc _) ⟧< _ = ⟦ n ∸ m ⟧< m∸n Date: Sun, 4 Feb 2024 11:29:02 +0000 Subject: [PATCH 06/29] rename projections --- src/Data/Integer/Modulo.agda | 14 +++++++------- src/Data/Integer/Modulo/Literals.agda | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index b066efda1f..e24a7990b2 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -14,7 +14,7 @@ module Data.Integer.Modulo (n : ℕ) .{{_ : NonTrivial n}} where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.Bounded as ℕ< hiding (π; module Literals) +open import Data.Nat.Bounded as ℕ< hiding (module Literals) open import Data.Nat.DivMod as ℕ using (_%_) open import Data.Nat.Properties as ℕ open import Data.Sign.Base as Sign using (Sign) @@ -51,11 +51,11 @@ infixl 6 _+_ -- Addition _+_ : ℤmod_ → ℤmod_ → ℤmod_ -i + j = ℕ<.π (⟦ i ⟧ ℕ.+ ⟦ j ⟧) +i + j = fromℕ (⟦ i ⟧ ℕ.+ ⟦ j ⟧) -- Multiplication _*_ : ℤmod_ → ℤmod_ → ℤmod_ -i * j = ℕ<.π (⟦ i ⟧ ℕ.* ⟦ j ⟧) +i * j = fromℕ (⟦ i ⟧ ℕ.* ⟦ j ⟧) ------------------------------------------------------------------------ -- Quotient map from ℤ @@ -64,12 +64,12 @@ _◃_ : Sign → ℤmod_ → ℤmod_ Sign.+ ◃ j = j Sign.- ◃ j = - j -π : ℤ → ℤmod_ -π i with s ◂ ∣i∣ ← signAbs i = s ◃ ℕ<.π ∣i∣ +fromℤ : ℤ → ℤmod_ +fromℤ i with s ◂ ∣i∣ ← signAbs i = s ◃ fromℕ ∣i∣ -- the _mod_ syntax Mod : ℤ → ℤmod_ -Mod = π +Mod = fromℤ syntax Mod {n = n} i = i mod n @@ -103,7 +103,7 @@ module Literals where Constraint _ = ⊤ fromNat : ∀ m → {{Constraint m}} → ℤmod_ - fromNat m = ℕ<.π m + fromNat m = fromℕ m ------------------------------------------------------------------------ -- -- Postfix notation for when opening the module unparameterised diff --git a/src/Data/Integer/Modulo/Literals.agda b/src/Data/Integer/Modulo/Literals.agda index d36b4e97a1..fb8402efa8 100644 --- a/src/Data/Integer/Modulo/Literals.agda +++ b/src/Data/Integer/Modulo/Literals.agda @@ -11,7 +11,7 @@ open import Data.Nat.Base using (ℕ; NonTrivial) module Data.Integer.Modulo.Literals (n : ℕ) .{{_ : NonTrivial n}} where open import Agda.Builtin.FromNat using (Number) -open import Data.Integer.Modulo using (ℤmod; module Literals) +open import Data.Integer.Modulo using (ℤmod_; module Literals) number : Number (ℤmod n) number = record { Literals n } From aa7b2bf447100176c1ca957792cf60b6204ad7ca Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 5 Feb 2024 05:28:33 +0000 Subject: [PATCH 07/29] more properties --- src/Data/Integer/Modulo/Properties.agda | 77 +++++++++++++++++++++++-- 1 file changed, 71 insertions(+), 6 deletions(-) diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index b3059c7477..af40b8c0d4 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -18,17 +18,22 @@ open import Algebra.Bundles import Algebra.Definitions as Definitions import Algebra.Structures as Structures open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) ---open import Data.Nat.Bounded as ℕ< hiding (π; module Literals) +open import Data.Nat.Bounded as ℕ< hiding (module Literals) import Data.Nat.DivMod as ℕ import Data.Nat.Properties as ℕ +open import Data.Product.Base as Product using (_,_) open import Data.Sign.Base as Sign using (Sign) open import Data.Unit.Base using (⊤) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong₂) +open import Relation.Binary.PropositionalEquality + using (_≡_; cong; cong₂; isEquivalence; module ≡-Reasoning) open import Data.Integer.Modulo n as Modulo using (ℤmod_; +-*-rawRing) open Definitions (_≡_ {A = ℤmod_}) open Structures (_≡_ {A = ℤmod_}) - using (IsMagma; IsMonoid; IsAbelianGroup; IsNearSemiring; IsSemiring; IsRing) + using ( IsMagma; IsSemigroup; IsMonoid + ; IsGroup; IsAbelianGroup + ; IsNearSemiring; IsSemiring + ; IsRing) private variable @@ -39,18 +44,78 @@ private _ = ℕ.nonTrivial⇒nonZero n open RawRing +-*-rawRing +open ≡-Reasoning + ++-cong₂ : Congruent₂ _+_ ++-cong₂ = cong₂ _+_ + ++-isMagma : IsMagma _+_ ++-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = +-cong₂ } + ++-assoc : Associative _+_ ++-assoc x y z = begin + x + y + z ≡⟨⟩ + fromℕ (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) ≡⟨ {!!} ⟩ + {!!} ≡⟨ {!!} ⟩ + {!!} ≡⟨ {!!} ⟩ + {!!} ≡⟨ {!!} ⟩ + fromℕ (⟦ x ⟧ ℕ.+ ((⟦ y ⟧ ℕ.+ ⟦ z ⟧) ℕ.% n)) ≡⟨⟩ + x + (y + z) ∎ + ++-isSemigroup : IsSemigroup _+_ ++-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc } + ++-identityˡ : LeftIdentity 0# _+_ ++-identityˡ = {!!} + ++-identityʳ : RightIdentity 0# _+_ ++-identityʳ = {!!} + ++-identity : Identity 0# _+_ ++-identity = +-identityˡ , +-identityʳ + ++-isMonoid : IsMonoid _+_ 0# ++-isMonoid = record { isSemigroup = +-isSemigroup ; identity = +-identity } + ++-inverseˡ : LeftInverse 0# -_ _+_ ++-inverseˡ = {!!} + ++-inverseʳ : RightInverse 0# -_ _+_ ++-inverseʳ = {!!} + ++-inverse : Inverse 0# -_ _+_ ++-inverse = +-inverseˡ , +-inverseʳ + ++-0-isGroup : IsGroup _+_ 0# -_ ++-0-isGroup = record { isMonoid = +-isMonoid ; inverse = {!+-inverse!} ; ⁻¹-cong = cong -_ } + ++-comm : Commutative _+_ ++-comm x y = cong fromℕ (ℕ.+-comm ⟦ x ⟧ ⟦ y ⟧) +-0-isAbelianGroup : IsAbelianGroup _+_ 0# -_ -+-0-isAbelianGroup = {!!} ++-0-isAbelianGroup = record { isGroup = +-0-isGroup ; comm = +-comm } *-cong₂ : Congruent₂ _*_ *-cong₂ = cong₂ _*_ *-assoc : Associative _*_ -*-assoc x y z = {!!} +*-assoc x y z = begin + x * y * z ≡⟨⟩ + fromℕ (((⟦ x ⟧ ℕ.* ⟦ y ⟧) ℕ.% n) ℕ.* ⟦ z ⟧) ≡⟨ {!!} ⟩ + {!!} ≡⟨ {!!} ⟩ + {!!} ≡⟨ {!!} ⟩ + {!!} ≡⟨ {!!} ⟩ + fromℕ (⟦ x ⟧ ℕ.* ((⟦ y ⟧ ℕ.* ⟦ z ⟧) ℕ.% n)) ≡⟨⟩ + x * (y * z) ∎ + +*-identityˡ : LeftIdentity 1# _*_ +*-identityˡ = {!!} + +*-identityʳ : RightIdentity 1# _*_ +*-identityʳ = {!!} *-identity : Identity 1# _*_ -*-identity = {!!} +*-identity = *-identityˡ , *-identityʳ *-distrib-+ : _*_ DistributesOver _+_ *-distrib-+ = {!!} From 9d855cb0f574de986bbf2dda2e1aadd70d78e1e3 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 5 Feb 2024 08:51:02 +0000 Subject: [PATCH 08/29] progress --- src/Data/Integer/Modulo/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index af40b8c0d4..23a2c1ab21 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -25,7 +25,7 @@ open import Data.Product.Base as Product using (_,_) open import Data.Sign.Base as Sign using (Sign) open import Data.Unit.Base using (⊤) open import Relation.Binary.PropositionalEquality - using (_≡_; cong; cong₂; isEquivalence; module ≡-Reasoning) + using (_≡_; refl; cong; cong₂; isEquivalence; module ≡-Reasoning) open import Data.Integer.Modulo n as Modulo using (ℤmod_; +-*-rawRing) open Definitions (_≡_ {A = ℤmod_}) @@ -66,10 +66,10 @@ open ≡-Reasoning +-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc } +-identityˡ : LeftIdentity 0# _+_ -+-identityˡ = {!!} ++-identityˡ x = {!!} +-identityʳ : RightIdentity 0# _+_ -+-identityʳ = {!!} ++-identityʳ x = {!!} +-identity : Identity 0# _+_ +-identity = +-identityˡ , +-identityʳ @@ -87,7 +87,7 @@ open ≡-Reasoning +-inverse = +-inverseˡ , +-inverseʳ +-0-isGroup : IsGroup _+_ 0# -_ -+-0-isGroup = record { isMonoid = +-isMonoid ; inverse = {!+-inverse!} ; ⁻¹-cong = cong -_ } ++-0-isGroup = record { isMonoid = +-isMonoid ; inverse = +-inverse ; ⁻¹-cong = cong -_ } +-comm : Commutative _+_ +-comm x y = cong fromℕ (ℕ.+-comm ⟦ x ⟧ ⟦ y ⟧) From 0c9eed6e929935975a6d4194b31b37b9f8263694 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 9 Feb 2024 16:33:19 +0000 Subject: [PATCH 09/29] shim for `Data.Nat.Bounded` --- src/Data/Integer/Modulo.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index e24a7990b2..d71cc18744 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -14,8 +14,7 @@ module Data.Integer.Modulo (n : ℕ) .{{_ : NonTrivial n}} where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.Bounded as ℕ< hiding (module Literals) -open import Data.Nat.DivMod as ℕ using (_%_) +open import Data.Nat.BoundedORIG as ℕ< hiding (module Literals) open import Data.Nat.Properties as ℕ open import Data.Sign.Base as Sign using (Sign) open import Data.Unit.Base using (⊤) From d5bed3af65b97ed952f721edfff5944b1e46d7f6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 9 Feb 2024 18:32:55 +0000 Subject: [PATCH 10/29] local change to `Bounded` shim --- src/Data/Integer/Modulo/Properties.agda | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index 23a2c1ab21..e888e1710f 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -18,14 +18,14 @@ open import Algebra.Bundles import Algebra.Definitions as Definitions import Algebra.Structures as Structures open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.Bounded as ℕ< hiding (module Literals) +open import Data.Nat.BoundedORIG as ℕ< hiding (module Literals) import Data.Nat.DivMod as ℕ import Data.Nat.Properties as ℕ open import Data.Product.Base as Product using (_,_) open import Data.Sign.Base as Sign using (Sign) -open import Data.Unit.Base using (⊤) +open import Function.Base using (_$_) open import Relation.Binary.PropositionalEquality - using (_≡_; refl; cong; cong₂; isEquivalence; module ≡-Reasoning) + using (_≡_; refl; sym; trans; cong; cong₂; isEquivalence; module ≡-Reasoning) open import Data.Integer.Modulo n as Modulo using (ℤmod_; +-*-rawRing) open Definitions (_≡_ {A = ℤmod_}) @@ -66,10 +66,11 @@ open ≡-Reasoning +-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc } +-identityˡ : LeftIdentity 0# _+_ -+-identityˡ x = {!!} ++-identityˡ x = ⟦⟧≡⟦⟧⇒bounded≡ (ℕ.m Date: Fri, 9 Feb 2024 19:11:16 +0000 Subject: [PATCH 11/29] incremental progress --- src/Data/Integer/Modulo/Properties.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index e888e1710f..0e1a1d0f42 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -66,10 +66,10 @@ open ≡-Reasoning +-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc } +-identityˡ : LeftIdentity 0# _+_ -+-identityˡ x = ⟦⟧≡⟦⟧⇒bounded≡ (ℕ.m Date: Sat, 10 Feb 2024 13:56:34 +0000 Subject: [PATCH 12/29] =?UTF-8?q?revised=20to=20reflect=20improvements=20t?= =?UTF-8?q?o=20`=E2=84=95<`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Integer/Modulo.agda | 62 +++++++++++++++------------ src/Data/Integer/Modulo/Literals.agda | 18 ++++++-- 2 files changed, 48 insertions(+), 32 deletions(-) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index d71cc18744..ba453704c9 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -7,17 +7,19 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Data.Nat.Base as ℕ - using (ℕ; zero; suc; NonZero; NonTrivial; _<_; _∸_) + using (ℕ; zero; suc; NonZero; NonTrivial; nonTrivial⇒nonZero; _<_; _∸_) -module Data.Integer.Modulo (n : ℕ) .{{_ : NonTrivial n}} where +module Data.Integer.Modulo n .{{_ : NonTrivial n}} where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.BoundedORIG as ℕ< hiding (module Literals) -open import Data.Nat.Properties as ℕ +open import Data.Nat.BoundedORIG as ℕ< hiding (fromℕ; _∼_; ≡-Mod) +import Data.Nat.Properties as ℕ open import Data.Sign.Base as Sign using (Sign) open import Data.Unit.Base using (⊤) +open import Function.Base using (id; _∘_; _$_; _on_) +open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_) private @@ -26,10 +28,10 @@ private i j : ℕ< n instance - _ = ℕ.nonTrivial⇒nonZero n + _ = nonTrivial⇒nonZero n m∸n Date: Sat, 10 Feb 2024 14:38:12 +0000 Subject: [PATCH 13/29] remove shim dependency --- src/Data/Integer/Modulo.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index ba453704c9..9f602eee02 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -14,7 +14,7 @@ module Data.Integer.Modulo n .{{_ : NonTrivial n}} where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.BoundedORIG as ℕ< hiding (fromℕ; _∼_; ≡-Mod) +open import Data.Nat.Bounded.Base as ℕ< hiding (fromℕ; _∼_; ≡-Mod) import Data.Nat.Properties as ℕ open import Data.Sign.Base as Sign using (Sign) open import Data.Unit.Base using (⊤) From b29985611a31f42691dfc1a58af13cec5a001aba Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 10 Feb 2024 14:39:10 +0000 Subject: [PATCH 14/29] remove shim dependency --- src/Data/Integer/Modulo/Properties.agda | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index 0e1a1d0f42..64a3c6904f 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -9,7 +9,7 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; NonTrivial; _<_; _∸_) -module Data.Integer.Modulo.Properties (n : ℕ) .{{_ : NonTrivial n}} where +module Data.Integer.Modulo.Properties n .{{_ : NonTrivial n}} where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) @@ -18,7 +18,8 @@ open import Algebra.Bundles import Algebra.Definitions as Definitions import Algebra.Structures as Structures open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.BoundedORIG as ℕ< hiding (module Literals) +open import Data.Nat.Bounded.Base as ℕ< hiding (fromℕ; _∼_; ≡-Mod) +import Data.Nat.Bounded.Properties as ℕ< hiding () import Data.Nat.DivMod as ℕ import Data.Nat.Properties as ℕ open import Data.Product.Base as Product using (_,_) @@ -27,9 +28,11 @@ open import Function.Base using (_$_) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; isEquivalence; module ≡-Reasoning) -open import Data.Integer.Modulo n as Modulo using (ℤmod_; +-*-rawRing) -open Definitions (_≡_ {A = ℤmod_}) -open Structures (_≡_ {A = ℤmod_}) +open import Data.Integer.Modulo n as Modulo + using (ℤmod; fromℕ; fromℤ; _∼_; ≡-Mod; +-*-rawRing) + +open Definitions (_≡_ {A = ℤmod}) +open Structures (_≡_ {A = ℤmod}) using ( IsMagma; IsSemigroup; IsMonoid ; IsGroup; IsAbelianGroup ; IsNearSemiring; IsSemiring @@ -38,7 +41,7 @@ open Structures (_≡_ {A = ℤmod_}) private variable m o : ℕ - i j k : ℤmod_ + i j k : ℤmod instance _ = ℕ.nonTrivial⇒nonZero n @@ -66,10 +69,10 @@ open ≡-Reasoning +-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc } +-identityˡ : LeftIdentity 0# _+_ -+-identityˡ x = ⟦⟧≡⟦⟧⇒≡ (ℕ.m Date: Sun, 11 Feb 2024 04:28:22 +0000 Subject: [PATCH 15/29] =?UTF-8?q?further=20revised=20to=20reflect=20improv?= =?UTF-8?q?ements=20to=20`=E2=84=95<`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Integer/Modulo.agda | 6 +++--- src/Data/Integer/Modulo/Properties.agda | 10 ++++++---- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index 9f602eee02..e6ed60bb1b 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -73,6 +73,7 @@ fromℤ : ℤ → ℤmod fromℤ i with s ◂ ∣i∣ ← signAbs i = s ◃ fromℕ ∣i∣ -- the _mod_ syntax + Mod : ℤ → ℤmod Mod = fromℤ @@ -83,12 +84,11 @@ syntax Mod {n = n} i = i mod n _∼_ : Rel ℤ _ _∼_ = _≡_ on fromℤ -≡-Mod : ∀ n .{{_ : NonTrivial n}} → Rel ℤ _ -≡-Mod n i j = i ∼ j +≡-Mod : Rel ℤ _ +≡-Mod i j = i ∼ j syntax ≡-Mod n i j = i ≡ j mod n - ------------------------------------------------------------------------ -- Raw bundles diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index 64a3c6904f..36799a80e7 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -19,7 +19,7 @@ import Algebra.Definitions as Definitions import Algebra.Structures as Structures open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) open import Data.Nat.Bounded.Base as ℕ< hiding (fromℕ; _∼_; ≡-Mod) -import Data.Nat.Bounded.Properties as ℕ< hiding () +import Data.Nat.Bounded.Properties as ℕ< import Data.Nat.DivMod as ℕ import Data.Nat.Properties as ℕ open import Data.Product.Base as Product using (_,_) @@ -69,7 +69,7 @@ open ≡-Reasoning +-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc } +-identityˡ : LeftIdentity 0# _+_ -+-identityˡ x = ℕ<.⟦⟧≡⟦⟧⇒≡ (ℕ.m Date: Mon, 12 Feb 2024 12:42:04 +0000 Subject: [PATCH 16/29] committed `Data.Nat.Bounded.*` against subsequent PR --- src/Data/Nat/Bounded/Base.agda | 93 +++++++++++++++ src/Data/Nat/Bounded/Properties.agda | 163 +++++++++++++++++++++++++++ 2 files changed, 256 insertions(+) create mode 100644 src/Data/Nat/Bounded/Base.agda create mode 100644 src/Data/Nat/Bounded/Properties.agda diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda new file mode 100644 index 0000000000..74989456a1 --- /dev/null +++ b/src/Data/Nat/Bounded/Base.agda @@ -0,0 +1,93 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bounded natural numbers, and their equivalence to `Fin` +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Nat.Bounded.Base where + +open import Data.Nat.Base as ℕ +import Data.Nat.DivMod as ℕ +import Data.Nat.Properties as ℕ +open import Data.Fin.Base as Fin using (Fin) +import Data.Fin.Properties as Fin +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions +open import Relation.Nullary.Decidable.Core using (recompute) +open import Relation.Nullary.Negation.Core using (¬_) + +private + variable + m n : ℕ + +------------------------------------------------------------------------ +-- Definition + +record ℕ< (n : ℕ) : Set where + constructor ⟦_⟧<_ + field + ⟦_⟧ : ℕ + .bounded : ⟦_⟧ < n + +open ℕ< public using (⟦_⟧) + +-- Constructors: 'n-1 mod n', '0 mod n', '1 mod n' + +⟦-1⟧< ⟦0⟧< ⟦1⟧< : .{{ NonZero n }} → ℕ< n +⟦-1⟧< {n = suc m} = ⟦ m ⟧< ℕ.n<1+n m +⟦0⟧< = ⟦ 0 ⟧< >-nonZero⁻¹ _ +⟦1⟧< {n = 1} = ⟦0⟧< +⟦1⟧< {n = 2+ _} = ⟦ 1 ⟧< nonTrivial⇒n>1 _ + +-- Projection from ℕ + +fromℕ : .{{ NonZero n }} → ℕ → ℕ< n +fromℕ {n} m = ⟦ m % n ⟧< ℕ.m%n-nonZero (ℕ.m-nonZero (ℕ.m-nonZero (ℕ.m-nonZero (ℕ.m Date: Mon, 12 Feb 2024 14:31:31 +0000 Subject: [PATCH 17/29] tweak syntax to distinguish from `Data.Integer.Modulo` --- src/Data/Nat/Bounded/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda index 74989456a1..5d6b2af269 100644 --- a/src/Data/Nat/Bounded/Base.agda +++ b/src/Data/Nat/Bounded/Base.agda @@ -90,4 +90,4 @@ record _∼_ {n} (lhs rhs : ℕ) : Set where ≡-Mod : ℕ → Rel ℕ _ ≡-Mod n i j = _∼_ {n} i j -syntax ≡-Mod n i j = i ≡ j mod n +syntax ≡-Mod n i j = i ≡ j modℕ n From cccf3a8f5a9f964d95ddb709fc48a9bd01054e9e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 12 Feb 2024 14:48:02 +0000 Subject: [PATCH 18/29] tweaks --- src/Data/Nat/Bounded/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index bca4611b67..7940f32229 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -109,7 +109,7 @@ module _ {m} {i : ℕ< n} where ------------------------------------------------------------------------ -- Properties of the quotient on ℕ induced by `fromℕ` -n≡0-mod : .{{_ : NonZero n}} → n ≡ 0 mod n +n≡0-mod : .{{_ : NonZero n}} → n ≡ 0 modℕ n n≡0-mod = let r = fromℕ[n]≡0 /∼≡fromℕ in r , ‵fromℕ 0 ⟦0⟧< ≡-mod-refl : .{{NonZero n}} → Reflexive (≡-Mod n) @@ -138,12 +138,12 @@ isEquivalence {n} = record setoid : .{{NonZero n}} → Setoid _ _ setoid = record { isEquivalence = isEquivalence } -≡-mod⇒fromℕ≡fromℕ : (eq : m ≡ o mod n) → +≡-mod⇒fromℕ≡fromℕ : (eq : m ≡ o modℕ n) → let _,_ {k} _ _ = eq ; instance _ = nonZeroIndex k in fromℕ {n} m ≡ fromℕ o ≡-mod⇒fromℕ≡fromℕ (lhs/∼≡ , rhs/∼≡) = trans (lhs/∼≡ /∼≡fromℕ⁻¹) (sym (rhs/∼≡ /∼≡fromℕ⁻¹)) -≡-mod⇒≡ : m ≡ o mod n → m < n → o < n → m ≡ o +≡-mod⇒≡ : m ≡ o modℕ n → m < n → o < n → m ≡ o ≡-mod⇒≡ {m} {o} eq m Date: Mon, 12 Feb 2024 14:49:23 +0000 Subject: [PATCH 19/29] refactoring `Data.Integer.Modulo.Properties` via revised `Data.Nat.Bounded.Properties` --- src/Data/Integer/Modulo/Properties.agda | 48 ++++++++++++++----------- 1 file changed, 28 insertions(+), 20 deletions(-) diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index 36799a80e7..715b2f8d49 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -18,7 +18,8 @@ open import Algebra.Bundles import Algebra.Definitions as Definitions import Algebra.Structures as Structures open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.Bounded.Base as ℕ< hiding (fromℕ; _∼_; ≡-Mod) +open import Data.Nat.Bounded.Base as ℕ< + renaming (≡-Mod to ≡-Modℕ) hiding (fromℕ; _∼_) import Data.Nat.Bounded.Properties as ℕ< import Data.Nat.DivMod as ℕ import Data.Nat.Properties as ℕ @@ -58,12 +59,12 @@ open ≡-Reasoning +-assoc : Associative _+_ +-assoc x y z = begin x + y + z ≡⟨⟩ - fromℕ (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) ≡⟨ {!!} ⟩ - {!!} ≡⟨ {!!} ⟩ - {!!} ≡⟨ {!!} ⟩ - {!!} ≡⟨ {!!} ⟩ + fromℕ (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ eq ⟩ fromℕ (⟦ x ⟧ ℕ.+ ((⟦ y ⟧ ℕ.+ ⟦ z ⟧) ℕ.% n)) ≡⟨⟩ x + (y + z) ∎ + where + eq : (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) ≡ (⟦ x ⟧ ℕ.+ ((⟦ y ⟧ ℕ.+ ⟦ z ⟧) ℕ.% n)) modℕ n + eq = {!!} +-isSemigroup : IsSemigroup _+_ +-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc } @@ -72,8 +73,7 @@ open ≡-Reasoning +-identityˡ = ℕ<.fromℕ∘toℕ≐id +-identityʳ : RightIdentity 0# _+_ -+-identityʳ x = ℕ<.⟦⟧≡⟦⟧⇒≡ $ - trans (cong (ℕ._% n) (ℕ.+-identityʳ _)) (ℕ.m Date: Mon, 12 Feb 2024 17:07:29 +0000 Subject: [PATCH 20/29] `nonZeroModulus` --- src/Data/Nat/Bounded/Base.agda | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda index 5d6b2af269..a2a5493888 100644 --- a/src/Data/Nat/Bounded/Base.agda +++ b/src/Data/Nat/Bounded/Base.agda @@ -20,7 +20,7 @@ open import Relation.Nullary.Negation.Core using (¬_) private variable - m n : ℕ + m n o : ℕ ------------------------------------------------------------------------ -- Definition @@ -88,6 +88,9 @@ record _∼_ {n} (lhs rhs : ℕ) : Set where rhs/∼≡ : rhs /∼≡ k ≡-Mod : ℕ → Rel ℕ _ -≡-Mod n i j = _∼_ {n} i j +≡-Mod n = _∼_ {n} -syntax ≡-Mod n i j = i ≡ j modℕ n +syntax ≡-Mod n m o = m ≡ o modℕ n + +nonZeroModulus : (m ≡ o modℕ n) → NonZero n +nonZeroModulus eq = nonZeroIndex k where open _∼_ eq From 4e9921ae9da7c7987adb507ec9e6cdf0968a9f41 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 12 Feb 2024 17:08:59 +0000 Subject: [PATCH 21/29] using `nonZeroModulus` --- src/Data/Nat/Bounded/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index 7940f32229..b8623d30c5 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -139,8 +139,8 @@ setoid : .{{NonZero n}} → Setoid _ _ setoid = record { isEquivalence = isEquivalence } ≡-mod⇒fromℕ≡fromℕ : (eq : m ≡ o modℕ n) → - let _,_ {k} _ _ = eq ; instance _ = nonZeroIndex k - in fromℕ {n} m ≡ fromℕ o + let instance _ = nonZeroModulus eq + in fromℕ m ≡ fromℕ o ≡-mod⇒fromℕ≡fromℕ (lhs/∼≡ , rhs/∼≡) = trans (lhs/∼≡ /∼≡fromℕ⁻¹) (sym (rhs/∼≡ /∼≡fromℕ⁻¹)) ≡-mod⇒≡ : m ≡ o modℕ n → m < n → o < n → m ≡ o From fbcec66b0ce9bd8726f63bf21c2daa5e2f72d6a4 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 12 Feb 2024 18:31:06 +0000 Subject: [PATCH 22/29] refactoring --- src/Data/Integer/Modulo/Properties.agda | 60 +++++++++++++++++-------- src/Data/Nat/Bounded/Properties.agda | 20 ++++++--- 2 files changed, 55 insertions(+), 25 deletions(-) diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index 715b2f8d49..f8ee362c9a 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -58,13 +58,19 @@ open ≡-Reasoning +-assoc : Associative _+_ +-assoc x y z = begin - x + y + z ≡⟨⟩ - fromℕ (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ eq ⟩ - fromℕ (⟦ x ⟧ ℕ.+ ((⟦ y ⟧ ℕ.+ ⟦ z ⟧) ℕ.% n)) ≡⟨⟩ + x + y + z + ≡⟨⟩ + fromℕ (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) + ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod ⟩ + fromℕ (⟦ x ⟧ ℕ.+ ((⟦ y ⟧ ℕ.+ ⟦ z ⟧) ℕ.% n)) + ≡⟨⟩ x + (y + z) ∎ where - eq : (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) ≡ (⟦ x ⟧ ℕ.+ ((⟦ y ⟧ ℕ.+ ⟦ z ⟧) ℕ.% n)) modℕ n - eq = {!!} + ≡-mod : (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) + ≡ + (⟦ x ⟧ ℕ.+ ((⟦ y ⟧ ℕ.+ ⟦ z ⟧) ℕ.% n)) + modℕ n + ≡-mod = {!%-distribˡ-+!} +-isSemigroup : IsSemigroup _+_ +-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc } @@ -82,14 +88,12 @@ open ≡-Reasoning +-isMonoid = record { isSemigroup = +-isSemigroup ; identity = +-identity } +-inverseˡ : LeftInverse 0# -_ _+_ -+-inverseˡ (⟦ zero ⟧< _) = +-identityˡ 0# -+-inverseˡ i@(⟦ m@(suc _) ⟧< _) - = trans (cong fromℕ (ℕ.m∸n+n≡m (ℕ.<⇒≤ (ℕ<.isBounded i)))) ℕ<.fromℕ[n]≡0 ++-inverseˡ (⟦ zero ⟧< _) = +-identityˡ 0# ++-inverseˡ i@(⟦ suc _ ⟧< _) = ℕ<.+-inverseˡ (ℕ<.isBounded i) +-inverseʳ : RightInverse 0# -_ _+_ +-inverseʳ (⟦ zero ⟧< _) = +-identityʳ 0# -+-inverseʳ i@(⟦ m@(suc _) ⟧< _) - = trans (cong fromℕ (ℕ.m+[n∸m]≡n (ℕ.<⇒≤ (ℕ<.isBounded i)))) ℕ<.fromℕ[n]≡0 ++-inverseʳ i@(⟦ m@(suc _) ⟧< _) = ℕ<.+-inverseʳ (ℕ<.isBounded i) +-inverse : Inverse 0# -_ _+_ +-inverse = +-inverseˡ , +-inverseʳ @@ -107,14 +111,20 @@ open ≡-Reasoning *-cong₂ = cong₂ _*_ *-assoc : Associative _*_ -*-assoc x y z = begin - x * y * z ≡⟨⟩ - fromℕ (((⟦ x ⟧ ℕ.* ⟦ y ⟧) ℕ.% n) ℕ.* ⟦ z ⟧) ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ eq ⟩ - fromℕ (⟦ x ⟧ ℕ.* ((⟦ y ⟧ ℕ.* ⟦ z ⟧) ℕ.% n)) ≡⟨⟩ - x * (y * z) ∎ +*-assoc i j k = begin + i * j * k + ≡⟨⟩ + fromℕ (((⟦ i ⟧ ℕ.* ⟦ j ⟧) ℕ.% n) ℕ.* ⟦ k ⟧) + ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod ⟩ + fromℕ (⟦ i ⟧ ℕ.* ((⟦ j ⟧ ℕ.* ⟦ k ⟧) ℕ.% n)) + ≡⟨⟩ + i * (j * k) ∎ where - eq : (((⟦ x ⟧ ℕ.* ⟦ y ⟧) ℕ.% n) ℕ.* ⟦ z ⟧) ≡ (⟦ x ⟧ ℕ.* ((⟦ y ⟧ ℕ.* ⟦ z ⟧) ℕ.% n)) modℕ n - eq = {!!} + ≡-mod : (((⟦ i ⟧ ℕ.* ⟦ j ⟧) ℕ.% n) ℕ.* ⟦ k ⟧) + ≡ + (⟦ i ⟧ ℕ.* ((⟦ j ⟧ ℕ.* ⟦ k ⟧) ℕ.% n)) + modℕ n + ≡-mod = {!!} *-identityˡ : LeftIdentity 1# _*_ *-identityˡ i with eq ← ℕ<.⟦1⟧≡1 {n = n} rewrite eq @@ -128,10 +138,22 @@ open ≡-Reasoning *-identity = *-identityˡ , *-identityʳ *-distribˡ-+ : _*_ DistributesOverˡ _+_ -*-distribˡ-+ i j k = {!!} +*-distribˡ-+ i j k = ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod + where + ≡-mod : (⟦ i ⟧ ℕ.* ⟦ j + k ⟧) + ≡ + (⟦ i * j ⟧ ℕ.+ ⟦ i * k ⟧) + modℕ n + ≡-mod = {!ℕ.%-distribˡ-*!} *-distribʳ-+ : _*_ DistributesOverʳ _+_ -*-distribʳ-+ i j k = {!!} +*-distribʳ-+ i j k = ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod + where + ≡-mod : (⟦ j + k ⟧ ℕ.* ⟦ i ⟧) + ≡ + (⟦ j * i ⟧ ℕ.+ ⟦ k * i ⟧) + modℕ n + ≡-mod = {!ℕ.%-distribʳ-*!} *-distrib-+ : _*_ DistributesOver _+_ *-distrib-+ = *-distribˡ-+ , *-distribʳ-+ diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index b8623d30c5..2dcccd6e06 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -8,6 +8,7 @@ module Data.Nat.Bounded.Properties where +import Algebra.Definitions as Definitions open import Data.Fin.Base as Fin using (Fin) import Data.Fin.Properties as Fin open import Data.Nat.Base as ℕ @@ -51,13 +52,20 @@ private ⟦⟧≡⟦⟧⇒≡ refl = refl fromℕ[n]≡0 : .{{_ : NonZero n}} → fromℕ n ≡ ⟦0⟧< -fromℕ[n]≡0 {n = n@(suc _)} = ⟦⟧≡⟦⟧⇒≡ (ℕ.n%n≡0 n) +fromℕ[n]≡0 {n} = ⟦⟧≡⟦⟧⇒≡ (ℕ.n%n≡0 n) -fromℕ≐⟦⟧< : (m-nonZero (ℕ.m-nonZero (ℕ.m-nonZero (ℕ.m Date: Mon, 12 Feb 2024 20:17:04 +0000 Subject: [PATCH 23/29] refactoring lemmas --- src/Data/Integer/Modulo.agda | 2 +- src/Data/Integer/Modulo/Properties.agda | 17 ++++--- src/Data/Nat/Bounded/Base.agda | 6 +-- src/Data/Nat/Bounded/Properties.agda | 59 ++++++++++++++++--------- 4 files changed, 51 insertions(+), 33 deletions(-) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo.agda index e6ed60bb1b..199d542ac1 100644 --- a/src/Data/Integer/Modulo.agda +++ b/src/Data/Integer/Modulo.agda @@ -14,7 +14,7 @@ module Data.Integer.Modulo n .{{_ : NonTrivial n}} where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.Bounded.Base as ℕ< hiding (fromℕ; _∼_; ≡-Mod) +open import Data.Nat.Bounded.Base as ℕ< hiding (fromℕ; _∼_; ≡-Modℕ) import Data.Nat.Properties as ℕ open import Data.Sign.Base as Sign using (Sign) open import Data.Unit.Base using (⊤) diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index f8ee362c9a..679dc74c50 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -18,8 +18,7 @@ open import Algebra.Bundles import Algebra.Definitions as Definitions import Algebra.Structures as Structures open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs) -open import Data.Nat.Bounded.Base as ℕ< - renaming (≡-Mod to ≡-Modℕ) hiding (fromℕ; _∼_) +open import Data.Nat.Bounded.Base as ℕ< hiding (fromℕ; _∼_) import Data.Nat.Bounded.Properties as ℕ< import Data.Nat.DivMod as ℕ import Data.Nat.Properties as ℕ @@ -57,18 +56,18 @@ open ≡-Reasoning +-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = +-cong₂ } +-assoc : Associative _+_ -+-assoc x y z = begin - x + y + z ++-assoc i j k = begin + i + j + k ≡⟨⟩ - fromℕ (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) + fromℕ (((⟦ i ⟧ ℕ.+ ⟦ j ⟧) ℕ.% n) ℕ.+ ⟦ k ⟧) ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod ⟩ - fromℕ (⟦ x ⟧ ℕ.+ ((⟦ y ⟧ ℕ.+ ⟦ z ⟧) ℕ.% n)) + fromℕ (⟦ i ⟧ ℕ.+ ((⟦ j ⟧ ℕ.+ ⟦ k ⟧) ℕ.% n)) ≡⟨⟩ - x + (y + z) ∎ + i + (j + k) ∎ where - ≡-mod : (((⟦ x ⟧ ℕ.+ ⟦ y ⟧) ℕ.% n) ℕ.+ ⟦ z ⟧) + ≡-mod : (((⟦ i ⟧ ℕ.+ ⟦ j ⟧) ℕ.% n) ℕ.+ ⟦ k ⟧) ≡ - (⟦ x ⟧ ℕ.+ ((⟦ y ⟧ ℕ.+ ⟦ z ⟧) ℕ.% n)) + (⟦ i ⟧ ℕ.+ ((⟦ j ⟧ ℕ.+ ⟦ k ⟧) ℕ.% n)) modℕ n ≡-mod = {!%-distribˡ-+!} diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda index a2a5493888..a230b09b06 100644 --- a/src/Data/Nat/Bounded/Base.agda +++ b/src/Data/Nat/Bounded/Base.agda @@ -87,10 +87,10 @@ record _∼_ {n} (lhs rhs : ℕ) : Set where lhs/∼≡ : lhs /∼≡ k rhs/∼≡ : rhs /∼≡ k -≡-Mod : ℕ → Rel ℕ _ -≡-Mod n = _∼_ {n} +≡-Modℕ : ℕ → Rel ℕ _ +≡-Modℕ n = _∼_ {n} -syntax ≡-Mod n m o = m ≡ o modℕ n +syntax ≡-Modℕ n m o = m ≡ o modℕ n nonZeroModulus : (m ≡ o modℕ n) → NonZero n nonZeroModulus eq = nonZeroIndex k where open _∼_ eq diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index 2dcccd6e06..de9bdbc4b2 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -60,7 +60,7 @@ module _ (m-nonZero (ℕ.m-nonZero (ℕ.m-nonZero (ℕ.m-nonZero (ℕ.m Date: Mon, 12 Feb 2024 22:02:13 +0000 Subject: [PATCH 24/29] arithmetic `mod n` lemmas --- src/Data/Nat/Bounded/Properties.agda | 49 +++++++++++++++++++++------- 1 file changed, 38 insertions(+), 11 deletions(-) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index de9bdbc4b2..cedf8471b1 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -151,9 +151,17 @@ setoid = record { isEquivalence = isEquivalence } in fromℕ m ≡ fromℕ o ≡-mod⇒fromℕ≡fromℕ (lhs/∼≡ , rhs/∼≡) = trans (lhs/∼≡ /∼≡fromℕ⁻¹) (sym (rhs/∼≡ /∼≡fromℕ⁻¹)) -fromℕ≡fromℕ⇒≡-mod : .{{_ : NonZero n}} → (_≡_ on fromℕ {n}) ⇒ ≡-Modℕ n +≡-mod⇒%≡% : (eq : m ≡ o modℕ n) → + let instance _ = nonZeroModulus eq + in m % n ≡ o % n +≡-mod⇒%≡% = ≡⇒⟦⟧≡⟦⟧ ∘ ≡-mod⇒fromℕ≡fromℕ + +fromℕ≡fromℕ⇒≡-mod : .{{_ : NonZero n}} → (_≡_ on fromℕ) ⇒ ≡-Modℕ n fromℕ≡fromℕ⇒≡-mod eq = eq /∼≡fromℕ , refl /∼≡fromℕ +%≡%⇒≡-mod : .{{_ : NonZero n}} → (_≡_ on _% n) ⇒ ≡-Modℕ n +%≡%⇒≡-mod eq = fromℕ≡fromℕ⇒≡-mod (⟦⟧≡⟦⟧⇒≡ eq) + toℕ∘fromℕ≐id : .{{_ : NonZero n}} → (m : ℕ) → ⟦ fromℕ m ⟧ ≡ m modℕ n toℕ∘fromℕ≐id m = fromℕ≡fromℕ⇒≡-mod (fromℕ∘toℕ≐id (fromℕ m)) @@ -175,16 +183,35 @@ module _ (m Date: Mon, 12 Feb 2024 22:51:13 +0000 Subject: [PATCH 25/29] additional arithmetic --- src/Data/Nat/Bounded/Properties.agda | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index cedf8471b1..c7e8231a9f 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -120,9 +120,6 @@ module _ {m} {i : ℕ< n} where n≡0-mod : .{{_ : NonZero n}} → n ≡ 0 modℕ n n≡0-mod = let r = fromℕ[n]≡0 /∼≡fromℕ in r , ‵fromℕ 0 ⟦0⟧< -≡-mod-refl : .{{NonZero n}} → Reflexive (≡-Modℕ n) -≡-mod-refl {n} {m} = let r = erefl (fromℕ m) /∼≡fromℕ in r , r - ≡-mod-sym : Symmetric (≡-Modℕ n) ≡-mod-sym (lhs , rhs) = rhs , lhs @@ -136,6 +133,9 @@ isPartialEquivalence = record { sym = ≡-mod-sym ; trans = ≡-mod-trans } partialSetoid : ℕ → PartialSetoid _ _ partialSetoid n = record { _≈_ = ≡-Modℕ n ; isPartialEquivalence = isPartialEquivalence } +≡-mod-refl : .{{NonZero n}} → Reflexive (≡-Modℕ n) +≡-mod-refl {n} {m} = let r = erefl (fromℕ m) /∼≡fromℕ in r , r + isEquivalence : .{{NonZero n}} → IsEquivalence (≡-Modℕ n) isEquivalence {n} = record { refl = ≡-mod-refl @@ -146,6 +146,9 @@ isEquivalence {n} = record setoid : .{{NonZero n}} → Setoid _ _ setoid = record { isEquivalence = isEquivalence } +≡-mod-reflexive : .{{NonZero n}} → _≡_ {A = ℕ} ⇒ (≡-Modℕ n) +≡-mod-reflexive = reflexive where open IsEquivalence isEquivalence + ≡-mod⇒fromℕ≡fromℕ : (eq : m ≡ o modℕ n) → let instance _ = nonZeroModulus eq in fromℕ m ≡ fromℕ o @@ -202,6 +205,11 @@ module _ .{{_ : NonZero n}} (m o : ℕ) where (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ (m + o) % n ∎ + +-distrib-% : ((m % n) + (o % n)) ≡ (m + o) modℕ n + +-distrib-% = %≡%⇒≡-mod $ begin + (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ + (m + o) % n ∎ + *-distribˡ-% : ((m % n) * o) ≡ (m * o) modℕ n *-distribˡ-% = %≡%⇒≡-mod $ begin (m % n * o) % n ≡⟨ ℕ.%-distribˡ-* (m % n) o n ⟩ From 0f6f0cecc65fdbacd0bc4d85359283f74e5c57e0 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 12 Feb 2024 22:53:27 +0000 Subject: [PATCH 26/29] integers `mod n` form a `Ring` --- src/Data/Integer/Modulo/Properties.agda | 37 ++++++++++++++++--------- 1 file changed, 24 insertions(+), 13 deletions(-) diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index 679dc74c50..353367401b 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -7,7 +7,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Data.Nat.Base as ℕ - using (ℕ; zero; suc; NonZero; NonTrivial; _<_; _∸_) + using (ℕ; zero; suc; NonZero; NonTrivial; _<_; _∸_; _%_) module Data.Integer.Modulo.Properties n .{{_ : NonTrivial n}} where @@ -59,17 +59,19 @@ open ≡-Reasoning +-assoc i j k = begin i + j + k ≡⟨⟩ - fromℕ (((⟦ i ⟧ ℕ.+ ⟦ j ⟧) ℕ.% n) ℕ.+ ⟦ k ⟧) + fromℕ (((⟦ i ⟧ ℕ.+ ⟦ j ⟧) % n) ℕ.+ ⟦ k ⟧) ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod ⟩ - fromℕ (⟦ i ⟧ ℕ.+ ((⟦ j ⟧ ℕ.+ ⟦ k ⟧) ℕ.% n)) + fromℕ (⟦ i ⟧ ℕ.+ ((⟦ j ⟧ ℕ.+ ⟦ k ⟧) % n)) ≡⟨⟩ i + (j + k) ∎ where - ≡-mod : (((⟦ i ⟧ ℕ.+ ⟦ j ⟧) ℕ.% n) ℕ.+ ⟦ k ⟧) + ≡-mod : (((⟦ i ⟧ ℕ.+ ⟦ j ⟧) % n) ℕ.+ ⟦ k ⟧) ≡ - (⟦ i ⟧ ℕ.+ ((⟦ j ⟧ ℕ.+ ⟦ k ⟧) ℕ.% n)) + (⟦ i ⟧ ℕ.+ ((⟦ j ⟧ ℕ.+ ⟦ k ⟧) % n)) modℕ n - ≡-mod = {!%-distribˡ-+!} + ≡-mod = ℕ<.≡-mod-trans (ℕ<.+-distribˡ-% (⟦ i ⟧ ℕ.+ ⟦ j ⟧) ⟦ k ⟧) + (ℕ<.≡-mod-trans (ℕ<.≡-mod-reflexive (ℕ.+-assoc ⟦ i ⟧ ⟦ j ⟧ ⟦ k ⟧)) + (ℕ<.≡-mod-sym (ℕ<.+-distribʳ-% ⟦ i ⟧ (⟦ j ⟧ ℕ.+ ⟦ k ⟧)))) +-isSemigroup : IsSemigroup _+_ +-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc } @@ -113,17 +115,19 @@ open ≡-Reasoning *-assoc i j k = begin i * j * k ≡⟨⟩ - fromℕ (((⟦ i ⟧ ℕ.* ⟦ j ⟧) ℕ.% n) ℕ.* ⟦ k ⟧) + fromℕ (((⟦ i ⟧ ℕ.* ⟦ j ⟧) % n) ℕ.* ⟦ k ⟧) ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod ⟩ - fromℕ (⟦ i ⟧ ℕ.* ((⟦ j ⟧ ℕ.* ⟦ k ⟧) ℕ.% n)) + fromℕ (⟦ i ⟧ ℕ.* ((⟦ j ⟧ ℕ.* ⟦ k ⟧) % n)) ≡⟨⟩ i * (j * k) ∎ where - ≡-mod : (((⟦ i ⟧ ℕ.* ⟦ j ⟧) ℕ.% n) ℕ.* ⟦ k ⟧) + ≡-mod : (((⟦ i ⟧ ℕ.* ⟦ j ⟧) % n) ℕ.* ⟦ k ⟧) ≡ - (⟦ i ⟧ ℕ.* ((⟦ j ⟧ ℕ.* ⟦ k ⟧) ℕ.% n)) + (⟦ i ⟧ ℕ.* ((⟦ j ⟧ ℕ.* ⟦ k ⟧) % n)) modℕ n - ≡-mod = {!!} + ≡-mod = ℕ<.≡-mod-trans (ℕ<.*-distribˡ-% (⟦ i ⟧ ℕ.* ⟦ j ⟧) ⟦ k ⟧) + (ℕ<.≡-mod-trans (ℕ<.≡-mod-reflexive (ℕ.*-assoc ⟦ i ⟧ ⟦ j ⟧ ⟦ k ⟧)) + (ℕ<.≡-mod-sym (ℕ<.*-distribʳ-% ⟦ i ⟧ (⟦ j ⟧ ℕ.* ⟦ k ⟧)))) *-identityˡ : LeftIdentity 1# _*_ *-identityˡ i with eq ← ℕ<.⟦1⟧≡1 {n = n} rewrite eq @@ -143,7 +147,9 @@ open ≡-Reasoning ≡ (⟦ i * j ⟧ ℕ.+ ⟦ i * k ⟧) modℕ n - ≡-mod = {!ℕ.%-distribˡ-*!} + ≡-mod = ℕ<.≡-mod-trans (ℕ<.*-distribʳ-% ⟦ i ⟧ (⟦ j ⟧ ℕ.+ ⟦ k ⟧)) + (ℕ<.≡-mod-trans (ℕ<.≡-mod-reflexive (ℕ.*-distribˡ-+ ⟦ i ⟧ ⟦ j ⟧ ⟦ k ⟧)) + (ℕ<.≡-mod-sym (ℕ<.+-distrib-% (⟦ i ⟧ ℕ.* ⟦ j ⟧) (⟦ i ⟧ ℕ.* ⟦ k ⟧)))) *-distribʳ-+ : _*_ DistributesOverʳ _+_ *-distribʳ-+ i j k = ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod @@ -152,7 +158,9 @@ open ≡-Reasoning ≡ (⟦ j * i ⟧ ℕ.+ ⟦ k * i ⟧) modℕ n - ≡-mod = {!ℕ.%-distribʳ-*!} + ≡-mod = ℕ<.≡-mod-trans (ℕ<.*-distribˡ-% (⟦ j ⟧ ℕ.+ ⟦ k ⟧) ⟦ i ⟧) + (ℕ<.≡-mod-trans (ℕ<.≡-mod-reflexive (ℕ.*-distribʳ-+ ⟦ i ⟧ ⟦ j ⟧ ⟦ k ⟧)) + (ℕ<.≡-mod-sym (ℕ<.+-distrib-% (⟦ j ⟧ ℕ.* ⟦ i ⟧) (⟦ k ⟧ ℕ.* ⟦ i ⟧)))) *-distrib-+ : _*_ DistributesOver _+_ *-distrib-+ = *-distribˡ-+ , *-distribʳ-+ @@ -165,3 +173,6 @@ open ≡-Reasoning ; *-identity = *-identity ; distrib = *-distrib-+ } + +ring : Ring _ _ +ring = record { isRing = +-*-isRing } From 8cf05cba712cc3e3ffa169f41420da72daf67a03 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 12 Feb 2024 22:55:44 +0000 Subject: [PATCH 27/29] moved `Modulo` to `Modulo.Base` --- src/Data/Integer/{Modulo.agda => Modulo/Base.agda} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/Data/Integer/{Modulo.agda => Modulo/Base.agda} (100%) diff --git a/src/Data/Integer/Modulo.agda b/src/Data/Integer/Modulo/Base.agda similarity index 100% rename from src/Data/Integer/Modulo.agda rename to src/Data/Integer/Modulo/Base.agda From b78f4077212f192f5bec6b0e4d5d2e94bf574813 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 12 Feb 2024 23:00:48 +0000 Subject: [PATCH 28/29] knock-on from moving `Modulo` to `Modulo.Base`; `CHANGELOG` --- CHANGELOG.md | 7 +++++++ src/Data/Integer/Modulo/Base.agda | 2 +- src/Data/Integer/Modulo/Literals.agda | 2 +- src/Data/Integer/Modulo/Properties.agda | 2 +- 4 files changed, 10 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c690740a1e..907f8c5be2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -33,6 +33,13 @@ Deprecated names New modules ----------- +* Integer arithmetic modulo `n`, based on `Data.Nat.Bounded.*`: + ```agda + Data.Integer.Modulo.Base + Data.Integer.Modulo.Literals + Data.Integer.Modulo.Properties + ``` + Additions to existing modules ----------------------------- diff --git a/src/Data/Integer/Modulo/Base.agda b/src/Data/Integer/Modulo/Base.agda index 199d542ac1..0cef16ca1c 100644 --- a/src/Data/Integer/Modulo/Base.agda +++ b/src/Data/Integer/Modulo/Base.agda @@ -9,7 +9,7 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; NonTrivial; nonTrivial⇒nonZero; _<_; _∸_) -module Data.Integer.Modulo n .{{_ : NonTrivial n}} where +module Data.Integer.Modulo.Base n .{{_ : NonTrivial n}} where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) diff --git a/src/Data/Integer/Modulo/Literals.agda b/src/Data/Integer/Modulo/Literals.agda index 55dcd198cb..481fe9e2e5 100644 --- a/src/Data/Integer/Modulo/Literals.agda +++ b/src/Data/Integer/Modulo/Literals.agda @@ -12,7 +12,7 @@ module Data.Integer.Modulo.Literals n .{{_ : NonTrivial n}} where open import Agda.Builtin.FromNat using (Number) open import Data.Unit.Base using (⊤) -open import Data.Integer.Modulo using (ℤmod; fromℕ) +open import Data.Integer.Modulo.Base using (ℤmod; fromℕ) ------------------------------------------------------------------------ -- Definitions diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda index 353367401b..5dc33eebc4 100644 --- a/src/Data/Integer/Modulo/Properties.agda +++ b/src/Data/Integer/Modulo/Properties.agda @@ -28,7 +28,7 @@ open import Function.Base using (_$_) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; isEquivalence; module ≡-Reasoning) -open import Data.Integer.Modulo n as Modulo +open import Data.Integer.Modulo.Base n as Modulo using (ℤmod; fromℕ; fromℤ; _∼_; ≡-Mod; +-*-rawRing) open Definitions (_≡_ {A = ℤmod}) From 4ab04f176475f633e731b97501eb628c2da374cb Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 13 Feb 2024 12:18:28 +0000 Subject: [PATCH 29/29] 'rebasing' against revised /updated #2257 --- src/Data/Nat/Bounded/Properties.agda | 33 ++++++++++++++-------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index c7e8231a9f..739b8bb8d4 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -191,35 +191,36 @@ module _ .{{_ : NonZero n}} (m o : ℕ) where open ≡-Reasoning + +-distrib-% : ((m % n) + (o % n)) ≡ (m + o) modℕ n + +-distrib-% = %≡%⇒≡-mod $ begin + (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ + (m + o) % n ∎ + +-distribˡ-% : ((m % n) + o) ≡ (m + o) modℕ n - +-distribˡ-% = %≡%⇒≡-mod $ begin + +-distribˡ-% = ≡-mod-trans (%≡%⇒≡-mod $ (begin (m % n + o) % n ≡⟨ ℕ.%-distribˡ-+ (m % n) o n ⟩ (m % n % n + o % n) % n ≡⟨ cong ((_% n) ∘ (_+ o % n)) (ℕ.m%n%n≡m%n m n) ⟩ - (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ - (m + o) % n ∎ + (m % n + o % n) % n ∎)) +-distrib-% +-distribʳ-% : (m + (o % n)) ≡ (m + o) modℕ n - +-distribʳ-% = %≡%⇒≡-mod $ begin + +-distribʳ-% = ≡-mod-trans (%≡%⇒≡-mod $ begin (m + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m (o % n) n ⟩ (m % n + o % n % n) % n ≡⟨ cong ((_% n) ∘ (m % n +_)) (ℕ.m%n%n≡m%n o n) ⟩ - (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ - (m + o) % n ∎ + (m % n + o % n) % n ∎) +-distrib-% - +-distrib-% : ((m % n) + (o % n)) ≡ (m + o) modℕ n - +-distrib-% = %≡%⇒≡-mod $ begin - (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ - (m + o) % n ∎ + *-distrib-% : ((m % n) * (o % n)) ≡ (m * o) modℕ n + *-distrib-% = %≡%⇒≡-mod $ begin + ((m % n) * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m o n ⟨ + (m * o) % n ∎ *-distribˡ-% : ((m % n) * o) ≡ (m * o) modℕ n - *-distribˡ-% = %≡%⇒≡-mod $ begin + *-distribˡ-% = ≡-mod-trans (%≡%⇒≡-mod $ begin (m % n * o) % n ≡⟨ ℕ.%-distribˡ-* (m % n) o n ⟩ (m % n % n * (o % n)) % n ≡⟨ cong ((_% n) ∘ (_* (o % n))) (ℕ.m%n%n≡m%n m n) ⟩ - (m % n * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m o n ⟨ - (m * o) % n ∎ + (m % n * (o % n)) % n ∎) *-distrib-% *-distribʳ-% : (m * (o % n)) ≡ (m * o) modℕ n - *-distribʳ-% = %≡%⇒≡-mod $ begin + *-distribʳ-% = ≡-mod-trans (%≡%⇒≡-mod $ begin (m * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m (o % n) n ⟩ (m % n * (o % n % n)) % n ≡⟨ cong ((_% n) ∘ (m % n *_)) (ℕ.m%n%n≡m%n o n) ⟩ - (m % n * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m o n ⟨ - (m * o) % n ∎ + (m % n * (o % n)) % n ∎) *-distrib-%