From 144ae6eb368f9dbe6b69590742b39c0c0b733495 Mon Sep 17 00:00:00 2001 From: Matthew Daggitt Date: Wed, 28 Jun 2017 15:23:34 +0100 Subject: [PATCH 1/3] Moved properties from `Data.Integer.Addition.Properties` and `Data.Integer.Multiplication.Properties` to `Data.Integer.Properties` and deprivatised `Data.Integer.Properties` --- CHANGELOG.md | 64 ++- src/Data/Integer/Addition/Properties.agda | 122 +----- .../Integer/Multiplication/Properties.agda | 92 +--- src/Data/Integer/Properties.agda | 396 +++++++++++++----- src/Data/Sign/Properties.agda | 30 +- 5 files changed, 397 insertions(+), 307 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b218cb17f1..227d63d5c1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -44,9 +44,8 @@ Non-backwards compatible changes * Changed the implementation of `All₂` in `Data.Vec.All` to a native datatype which allows better pattern matching. - The new version (and the associated - proofs in `Data.Vec.All.Properties`) are also more generic with respect to - types and levels. + The new version (and the associated proofs in `Data.Vec.All.Properties`) + are also more generic with respect to types and levels. * Changed the implementation of `downFrom` in `Data.List` to a native (pattern-matching) definition. @@ -64,6 +63,24 @@ but they may be removed in some future release of the library. have been deprecated in favour of `+-mono-≤` and `*-mono-≤` which better follow the library's naming conventions. +* The module `Data.Nat.Properties.Simple` is now deprecated. All proofs + have been moved to `Data.Nat.Properties` where they should be used directly. + The `Simple` file still exists for backwards compatability reasons and + re-exports the proofs from `Data.Nat.Properties` but will be removed in some + future release. + +* The module `Data.Integer.Addition.Properties` is now deprecated. All proofs + have been moved to `Data.Integer.Properties` where they should be used + directly. The `Addition.Properties` file still exists for backwards + compatability reasons and re-exports the proofs from `Data.Integer.Properties` + but will be removed in some future release. + +* The module `Data.Integer.Multiplication.Properties` is now deprecated. All + proofs have been moved to `Data.Integer.Properties` where they should be used + directly. The `Multiplication.Properties` file still exists for backwards + compatability reasons and re-exports the proofs from `Data.Integer.Properties` + but will be removed in some future release. + Backwards compatible changes ---------------------------- @@ -71,12 +88,6 @@ Backwards compatible changes * Added `Category.Functor.Morphism` and module `Category.Functor.Identity`. -* The module `Data.Nat.Properties.Simple` is now deprecated. All proofs - have been moved to `Data.Nat.Properties` where they should be used directly. - The `Simple` file still exists for backwards compatability reasons and - re-exports the proofs from `Data.Nat.Properties` but will be removed in some - future release. - * `Data.Container` and `Data.Container.Indexed` now allow for different levels in the container and in the data it contains. @@ -205,7 +216,29 @@ Backwards compatible changes ∩⇔× : x ∈ p ∩ q ⇔ (x ∈ p × x ∈ q) ``` -* Added additional proofs to `Data.Nat.Properties`: +* Added proofs to `Data.Integer.Properties` + ```agda + +◃n≡+n : Sign.+ ◃ n ≡ + n + -◃n≡-n : Sign.- ◃ n ≡ - + n + signₙ◃∣n∣≡n : sign n ◃ ∣ n ∣ ≡ n + + ⊖-≰ : n ≰ m → m ⊖ n ≡ - + (n ∸ m) + ∣⊖∣-≰ : n ≰ m → ∣ m ⊖ n ∣ ≡ n ∸ m + sign-⊖-≰ : n ≰ m → sign (m ⊖ n) ≡ Sign.- + + +-identity : Identity (+ 0) _+_ + +-0-isMonoid : IsMonoid _≡_ _+_ (+ 0) + +-0-isGroup : IsGroup _≡_ _+_ (+ 0) (-_) + + *-identityʳ : RightIdentity (+ 1) _*_ + *-identity : Identity (+ 1) _*_ + *-1-isMonoid : IsMonoid _≡_ _*_ (+ 1) + + +-*-isRing : IsRing _≡_ _+_ _*_ -_ (+ 0) (+ 1) + +-*-isCommutativeRing : IsCommutativeRing _≡_ _+_ _*_ -_ (+ 0) (+ 1) + ``` + +* Added proofs to `Data.Nat.Properties`: ```agda suc-injective : suc m ≡ suc n → m ≡ n ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ}) @@ -358,6 +391,17 @@ Backwards compatible changes zipWith-map₂ : zipWith _⊕_ xs (map f ys) ≡ zipWith (λ x y → x ⊕ f y) xs ys ``` +* Added proofs to `Data.Sign.Properties`: + ```agda + opposite-cong : opposite s ≡ opposite t → s ≡ t + + *-identityˡ : LeftIdentity + _*_ + *-identityʳ : RightIdentity + _*_ + *-identity : Identity + _*_ + cancel-*-left : LeftCancellative _*_ + *-cancellative : Cancellative _*_ + ``` + * Added proofs to `Data.Vec.All.Properties` ```agda All-++⁺ : All P xs → All P ys → All P (xs ++ ys) diff --git a/src/Data/Integer/Addition/Properties.agda b/src/Data/Integer/Addition/Properties.agda index 422524d46a..2da1bdf5ba 100644 --- a/src/Data/Integer/Addition/Properties.agda +++ b/src/Data/Integer/Addition/Properties.agda @@ -2,110 +2,26 @@ -- The Agda standard library -- -- Properties related to addition of integers +-- +-- This module is DEPRECATED. Please use the corresponding properties in +-- Data.Integer.Properties directly. ------------------------------------------------------------------------ module Data.Integer.Addition.Properties where -open import Algebra -open import Algebra.Structures -open import Data.Integer hiding (suc) -open import Data.Nat.Base using (suc; zero) renaming (_+_ to _ℕ+_) -import Data.Nat.Properties as ℕ -open import Relation.Binary.PropositionalEquality -open import Algebra.FunctionProperties (_≡_ {A = ℤ}) - ------------------------------------------------------------------------- --- Addition and zero form a commutative monoid - -comm : Commutative _+_ -comm -[1+ a ] -[1+ b ] rewrite ℕ.+-comm a b = refl -comm (+ a ) (+ b ) rewrite ℕ.+-comm a b = refl -comm -[1+ _ ] (+ _ ) = refl -comm (+ _ ) -[1+ _ ] = refl - -identityˡ : LeftIdentity (+ 0) _+_ -identityˡ -[1+ _ ] = refl -identityˡ (+ _ ) = refl - -identityʳ : RightIdentity (+ 0) _+_ -identityʳ x rewrite comm x (+ 0) = identityˡ x - -distribˡ-⊖-+-neg : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (suc c ℕ+ a) -distribˡ-⊖-+-neg _ zero zero = refl -distribˡ-⊖-+-neg _ zero (suc _) = refl -distribˡ-⊖-+-neg _ (suc _) zero = refl -distribˡ-⊖-+-neg a (suc b) (suc c) = distribˡ-⊖-+-neg a b c - -distribʳ-⊖-+-neg : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (suc a ℕ+ c) -distribʳ-⊖-+-neg a b c - rewrite comm -[1+ a ] (b ⊖ c) - | distribˡ-⊖-+-neg a b c - | ℕ.+-comm a c - = refl - -distribˡ-⊖-+-pos : ∀ a b c → b ⊖ c + + a ≡ b ℕ+ a ⊖ c -distribˡ-⊖-+-pos _ zero zero = refl -distribˡ-⊖-+-pos _ zero (suc _) = refl -distribˡ-⊖-+-pos _ (suc _) zero = refl -distribˡ-⊖-+-pos a (suc b) (suc c) = distribˡ-⊖-+-pos a b c - -distribʳ-⊖-+-pos : ∀ a b c → + a + (b ⊖ c) ≡ a ℕ+ b ⊖ c -distribʳ-⊖-+-pos a b c - rewrite comm (+ a) (b ⊖ c) - | distribˡ-⊖-+-pos a b c - | ℕ.+-comm a b - = refl - -assoc : Associative _+_ -assoc (+ zero) y z rewrite identityˡ y | identityˡ (y + z) = refl -assoc x (+ zero) z rewrite identityʳ x | identityˡ z = refl -assoc x y (+ zero) rewrite identityʳ (x + y) | identityʳ y = refl -assoc -[1+ a ] -[1+ b ] (+ suc c) = sym (distribʳ-⊖-+-neg a c b) -assoc -[1+ a ] (+ suc b) (+ suc c) = distribˡ-⊖-+-pos (suc c) b a -assoc (+ suc a) -[1+ b ] -[1+ c ] = distribˡ-⊖-+-neg c a b -assoc (+ suc a) -[1+ b ] (+ suc c) - rewrite distribˡ-⊖-+-pos (suc c) a b - | distribʳ-⊖-+-pos (suc a) c b - | sym (ℕ.+-assoc a 1 c) - | ℕ.+-comm a 1 - = refl -assoc (+ suc a) (+ suc b) -[1+ c ] - rewrite distribʳ-⊖-+-pos (suc a) b c - | sym (ℕ.+-assoc a 1 b) - | ℕ.+-comm a 1 - = refl -assoc -[1+ a ] -[1+ b ] -[1+ c ] - rewrite sym (ℕ.+-assoc a 1 (b ℕ+ c)) - | ℕ.+-comm a 1 - | ℕ.+-assoc a b c - = refl -assoc -[1+ a ] (+ suc b) -[1+ c ] - rewrite distribʳ-⊖-+-neg a b c - | distribˡ-⊖-+-neg c b a - = refl -assoc (+ suc a) (+ suc b) (+ suc c) - rewrite ℕ.+-assoc (suc a) (suc b) (suc c) - = refl - -isSemigroup : IsSemigroup _≡_ _+_ -isSemigroup = record - { isEquivalence = isEquivalence - ; assoc = assoc - ; ∙-cong = cong₂ _+_ - } - -isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ (+ 0) -isCommutativeMonoid = record - { isSemigroup = isSemigroup - ; identityˡ = identityˡ - ; comm = comm - } - -commutativeMonoid : CommutativeMonoid _ _ -commutativeMonoid = record - { Carrier = ℤ - ; _≈_ = _≡_ - ; _∙_ = _+_ - ; ε = + 0 - ; isCommutativeMonoid = isCommutativeMonoid - } +open import Data.Integer.Properties public + using + ( distribˡ-⊖-+-neg + ; distribʳ-⊖-+-neg + ; distribˡ-⊖-+-pos + ; distribʳ-⊖-+-pos + ) + renaming + ( +-comm to comm + ; +-identityˡ to identityˡ + ; +-identityʳ to identityʳ + ; +-assoc to assoc + ; +-isSemigroup to isSemigroup + ; +-0-isCommutativeMonoid to isCommutativeMonoid + ; +-0-commutativeMonoid to commutativeMonoid + ) diff --git a/src/Data/Integer/Multiplication/Properties.agda b/src/Data/Integer/Multiplication/Properties.agda index 5fcf11c5f9..f2bfc9a9d9 100644 --- a/src/Data/Integer/Multiplication/Properties.agda +++ b/src/Data/Integer/Multiplication/Properties.agda @@ -2,86 +2,20 @@ -- The Agda standard library -- -- Properties related to multiplication of integers +-- +-- This module is DEPRECATED. Please use the corresponding properties in +-- Data.Integer.Properties directly. ------------------------------------------------------------------------ module Data.Integer.Multiplication.Properties where -open import Algebra using (CommutativeMonoid) -open import Algebra.Structures using (IsSemigroup; IsCommutativeMonoid) -open import Data.Integer - using (ℤ; -[1+_]; +_; ∣_∣; sign; _◃_) renaming (_*_ to ℤ*) -open import Data.Nat - using (suc; zero) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_) -open import Data.Product using (proj₂) -import Data.Nat.Properties as ℕ -open import Data.Sign using () renaming (_*_ to _S*_) -open import Function using (_∘_) -open import Relation.Binary.PropositionalEquality - using (_≡_; refl; cong; cong₂; isEquivalence) - -open import Algebra.FunctionProperties (_≡_ {A = ℤ}) - ------------------------------------------------------------------------- --- Multiplication and one form a commutative monoid - -private - lemma : ∀ a b c → c ℕ+ (b ℕ+ a ℕ* suc b) ℕ* suc c - ≡ c ℕ+ b ℕ* suc c ℕ+ a ℕ* suc (c ℕ+ b ℕ* suc c) - lemma = - solve 3 (λ a b c → c :+ (b :+ a :* (con 1 :+ b)) :* (con 1 :+ c) - := c :+ b :* (con 1 :+ c) :+ - a :* (con 1 :+ (c :+ b :* (con 1 :+ c)))) - refl - where open ℕ.SemiringSolver - - -identityˡ : LeftIdentity (+ 1) ℤ* -identityˡ (+ zero ) = refl -identityˡ -[1+ n ] rewrite ℕ.+-right-identity n = refl -identityˡ (+ suc n) rewrite ℕ.+-right-identity n = refl - -comm : Commutative ℤ* -comm -[1+ a ] -[1+ b ] rewrite ℕ.*-comm (suc a) (suc b) = refl -comm -[1+ a ] (+ b ) rewrite ℕ.*-comm (suc a) b = refl -comm (+ a ) -[1+ b ] rewrite ℕ.*-comm a (suc b) = refl -comm (+ a ) (+ b ) rewrite ℕ.*-comm a b = refl - -assoc : Associative ℤ* -assoc (+ zero) _ _ = refl -assoc x (+ zero) _ rewrite ℕ.*-right-zero ∣ x ∣ = refl -assoc x y (+ zero) rewrite - ℕ.*-right-zero ∣ y ∣ - | ℕ.*-right-zero ∣ x ∣ - | ℕ.*-right-zero ∣ sign x S* sign y ◃ ∣ x ∣ ℕ* ∣ y ∣ ∣ - = refl -assoc -[1+ a ] -[1+ b ] (+ suc c) = cong (+_ ∘ suc) (lemma a b c) -assoc -[1+ a ] (+ suc b) -[1+ c ] = cong (+_ ∘ suc) (lemma a b c) -assoc (+ suc a) (+ suc b) (+ suc c) = cong (+_ ∘ suc) (lemma a b c) -assoc (+ suc a) -[1+ b ] -[1+ c ] = cong (+_ ∘ suc) (lemma a b c) -assoc -[1+ a ] -[1+ b ] -[1+ c ] = cong -[1+_] (lemma a b c) -assoc -[1+ a ] (+ suc b) (+ suc c) = cong -[1+_] (lemma a b c) -assoc (+ suc a) -[1+ b ] (+ suc c) = cong -[1+_] (lemma a b c) -assoc (+ suc a) (+ suc b) -[1+ c ] = cong -[1+_] (lemma a b c) - -isSemigroup : IsSemigroup _ _ -isSemigroup = record - { isEquivalence = isEquivalence - ; assoc = assoc - ; ∙-cong = cong₂ ℤ* - } - -isCommutativeMonoid : IsCommutativeMonoid _≡_ ℤ* (+ 1) -isCommutativeMonoid = record - { isSemigroup = isSemigroup - ; identityˡ = identityˡ - ; comm = comm - } - -commutativeMonoid : CommutativeMonoid _ _ -commutativeMonoid = record - { Carrier = ℤ - ; _≈_ = _≡_ - ; _∙_ = ℤ* - ; ε = + 1 - ; isCommutativeMonoid = isCommutativeMonoid - } +open import Data.Integer.Properties public + using () + renaming + ( *-comm to comm + ; *-identityˡ to identityˡ + ; *-assoc to assoc + ; *-isSemigroup to isSemigroup + ; *-1-isCommutativeMonoid to isCommutativeMonoid + ; *-1-commutativeMonoid to commutativeMonoid + ) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 52cf18cb95..96c523c799 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -12,16 +12,14 @@ import Algebra.Morphism as Morphism import Algebra.Properties.AbelianGroup open import Algebra.Structures open import Data.Integer hiding (suc; _≤?_) -import Data.Integer.Addition.Properties as Add -import Data.Integer.Multiplication.Properties as Mul open import Data.Nat - using (ℕ; suc; zero; _∸_; _≤?_; _<_; _≥_; _≱_; s≤s; z≤n; ≤-pred) + using (ℕ; suc; zero; _∸_; _≤?_; _<_; _≥_; _≰_; s≤s; z≤n; ≤-pred) hiding (module ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_) -open import Data.Nat.Properties as ℕ using (_*-mono_; ≤-refl) +open import Data.Nat.Properties as ℕ using (≤-refl) open import Data.Product using (proj₁; proj₂; _,_) -open import Data.Sign as Sign using () renaming (_*_ to _S*_) -import Data.Sign.Properties as SignProp +open import Data.Sign as Sign using () renaming (_*_ to _𝕊*_) +import Data.Sign.Properties as 𝕊 open import Function using (_∘_; _$_) open import Relation.Binary open import Relation.Binary.PropositionalEquality @@ -29,33 +27,34 @@ open import Relation.Nullary using (yes; no) open import Relation.Nullary.Negation using (contradiction) open Algebra.FunctionProperties (_≡_ {A = ℤ}) -open CommutativeMonoid Add.commutativeMonoid - using () - renaming ( assoc to +-assoc; comm to +-comm; identity to +-identity - ; isCommutativeMonoid to +-isCommutativeMonoid - ; isMonoid to +-isMonoid - ) -open CommutativeMonoid Mul.commutativeMonoid - using () - renaming ( assoc to *-assoc; comm to *-comm; identity to *-identity - ; isCommutativeMonoid to *-isCommutativeMonoid - ; isMonoid to *-isMonoid - ) -open CommutativeSemiring ℕ.commutativeSemiring - using () renaming (zero to *-zero; distrib to *-distrib) open Morphism.Definitions ℤ ℕ _≡_ open ℕ.SemiringSolver open ≡-Reasoning ------------------------------------------------------------------------ --- Miscellaneous properties +-- Properties of sign and _◃_ --- Some properties relating sign and ∣_∣ to _◃_. ++◃n≡+n : ∀ n → Sign.+ ◃ n ≡ + n ++◃n≡+n zero = refl ++◃n≡+n (suc _) = refl + +-◃n≡-n : ∀ n → Sign.- ◃ n ≡ - + n +-◃n≡-n zero = refl +-◃n≡-n (suc _) = refl sign-◃ : ∀ s n → sign (s ◃ suc n) ≡ s sign-◃ Sign.- _ = refl sign-◃ Sign.+ _ = refl +abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n +abs-◃ _ zero = refl +abs-◃ Sign.- (suc n) = refl +abs-◃ Sign.+ (suc n) = refl + +signₙ◃∣n∣≡n : ∀ n → sign n ◃ ∣ n ∣ ≡ n +signₙ◃∣n∣≡n (+ n) = +◃n≡+n n +signₙ◃∣n∣≡n (-[1+ n ]) = refl + sign-cong : ∀ {s₁ s₂ n₁ n₂} → s₁ ◃ suc n₁ ≡ s₂ ◃ suc n₂ → s₁ ≡ s₂ sign-cong {s₁} {s₂} {n₁} {n₂} eq = begin @@ -64,11 +63,6 @@ sign-cong {s₁} {s₂} {n₁} {n₂} eq = begin sign (s₂ ◃ suc n₂) ≡⟨ sign-◃ s₂ n₂ ⟩ s₂ ∎ -abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n -abs-◃ _ zero = refl -abs-◃ Sign.- (suc n) = refl -abs-◃ Sign.+ (suc n) = refl - abs-cong : ∀ {s₁ s₂ n₁ n₂} → s₁ ◃ n₁ ≡ s₂ ◃ n₂ → n₁ ≡ n₂ abs-cong {s₁} {s₂} {n₁} {n₂} eq = begin @@ -77,25 +71,13 @@ abs-cong {s₁} {s₂} {n₁} {n₂} eq = begin ∣ s₂ ◃ n₂ ∣ ≡⟨ abs-◃ s₂ n₂ ⟩ n₂ ∎ --- ∣_∣ commutes with multiplication. - -abs-*-commute : Homomorphic₂ ∣_∣ _*_ _ℕ*_ -abs-*-commute i j = abs-◃ _ _ - --- Subtraction properties +------------------------------------------------------------------------ +-- Properties of _⊖_ n⊖n≡0 : ∀ n → n ⊖ n ≡ + 0 n⊖n≡0 zero = refl n⊖n≡0 (suc n) = n⊖n≡0 n -sign-⊖-< : ∀ {m n} → m < n → sign (m ⊖ n) ≡ Sign.- -sign-⊖-< {zero} (s≤s z≤n) = refl -sign-⊖-< {suc n} (s≤s m + ∣⊖∣-< : ∀ {m n} → m < n → ∣ m ⊖ n ∣ ≡ n ∸ m ∣⊖∣-< {zero} (s≤s z≤n) = refl ∣⊖∣-< {suc n} (s≤s m + +sign-⊖-< : ∀ {m n} → m < n → sign (m ⊖ n) ≡ Sign.- +sign-⊖-< {zero} (s≤s z≤n) = refl +sign-⊖-< {suc n} (s≤s m + ++-⊖-left-cancel : ∀ a b c → (a ℕ+ b) ⊖ (a ℕ+ c) ≡ b ⊖ c ++-⊖-left-cancel zero b c = refl ++-⊖-left-cancel (suc a) b c = +-⊖-left-cancel a b c ------------------------------------------------------------------------ --- The integers form a commutative ring +-- Properties of _+_ + ++-comm : Commutative _+_ ++-comm -[1+ a ] -[1+ b ] rewrite ℕ.+-comm a b = refl ++-comm (+ a ) (+ b ) rewrite ℕ.+-comm a b = refl ++-comm -[1+ _ ] (+ _ ) = refl ++-comm (+ _ ) -[1+ _ ] = refl + ++-identityˡ : LeftIdentity (+ 0) _+_ ++-identityˡ -[1+ _ ] = refl ++-identityˡ (+ _ ) = refl + ++-identityʳ : RightIdentity (+ 0) _+_ ++-identityʳ x rewrite +-comm x (+ 0) = +-identityˡ x + ++-identity : Identity (+ 0) _+_ ++-identity = +-identityˡ , +-identityʳ + +distribˡ-⊖-+-neg : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (suc c ℕ+ a) +distribˡ-⊖-+-neg _ zero zero = refl +distribˡ-⊖-+-neg _ zero (suc _) = refl +distribˡ-⊖-+-neg _ (suc _) zero = refl +distribˡ-⊖-+-neg a (suc b) (suc c) = distribˡ-⊖-+-neg a b c + +distribʳ-⊖-+-neg : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (suc a ℕ+ c) +distribʳ-⊖-+-neg a b c + rewrite +-comm -[1+ a ] (b ⊖ c) + | distribˡ-⊖-+-neg a b c + | ℕ.+-comm a c + = refl + +distribˡ-⊖-+-pos : ∀ a b c → b ⊖ c + + a ≡ b ℕ+ a ⊖ c +distribˡ-⊖-+-pos _ zero zero = refl +distribˡ-⊖-+-pos _ zero (suc _) = refl +distribˡ-⊖-+-pos _ (suc _) zero = refl +distribˡ-⊖-+-pos a (suc b) (suc c) = distribˡ-⊖-+-pos a b c + +distribʳ-⊖-+-pos : ∀ a b c → + a + (b ⊖ c) ≡ a ℕ+ b ⊖ c +distribʳ-⊖-+-pos a b c + rewrite +-comm (+ a) (b ⊖ c) + | distribˡ-⊖-+-pos a b c + | ℕ.+-comm a b + = refl --- Additive abelian group. ++-assoc : Associative _+_ ++-assoc (+ zero) y z rewrite +-identityˡ y | +-identityˡ (y + z) = refl ++-assoc x (+ zero) z rewrite +-identityʳ x | +-identityˡ z = refl ++-assoc x y (+ zero) rewrite +-identityʳ (x + y) | +-identityʳ y = refl ++-assoc -[1+ a ] -[1+ b ] (+ suc c) = sym (distribʳ-⊖-+-neg a c b) ++-assoc -[1+ a ] (+ suc b) (+ suc c) = distribˡ-⊖-+-pos (suc c) b a ++-assoc (+ suc a) -[1+ b ] -[1+ c ] = distribˡ-⊖-+-neg c a b ++-assoc (+ suc a) -[1+ b ] (+ suc c) + rewrite distribˡ-⊖-+-pos (suc c) a b + | distribʳ-⊖-+-pos (suc a) c b + | sym (ℕ.+-assoc a 1 c) + | ℕ.+-comm a 1 + = refl ++-assoc (+ suc a) (+ suc b) -[1+ c ] + rewrite distribʳ-⊖-+-pos (suc a) b c + | sym (ℕ.+-assoc a 1 b) + | ℕ.+-comm a 1 + = refl ++-assoc -[1+ a ] -[1+ b ] -[1+ c ] + rewrite sym (ℕ.+-assoc a 1 (b ℕ+ c)) + | ℕ.+-comm a 1 + | ℕ.+-assoc a b c + = refl ++-assoc -[1+ a ] (+ suc b) -[1+ c ] + rewrite distribʳ-⊖-+-neg a b c + | distribˡ-⊖-+-neg c b a + = refl ++-assoc (+ suc a) (+ suc b) (+ suc c) + rewrite ℕ.+-assoc (suc a) (suc b) (suc c) + = refl inverseˡ : LeftInverse (+ 0) -_ _+_ inverseˡ -[1+ n ] = n⊖n≡0 n @@ -131,46 +200,140 @@ inverseʳ i = begin - i + i ≡⟨ inverseˡ i ⟩ + 0 ∎ ++-isSemigroup : IsSemigroup _≡_ _+_ ++-isSemigroup = record + { isEquivalence = isEquivalence + ; assoc = +-assoc + ; ∙-cong = cong₂ _+_ + } + ++-0-isMonoid : IsMonoid _≡_ _+_ (+ 0) ++-0-isMonoid = record + { isSemigroup = +-isSemigroup + ; identity = +-identity + } + ++-0-isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ (+ 0) ++-0-isCommutativeMonoid = record + { isSemigroup = +-isSemigroup + ; identityˡ = +-identityˡ + ; comm = +-comm + } + ++-0-commutativeMonoid : CommutativeMonoid _ _ ++-0-commutativeMonoid = record + { Carrier = ℤ + ; _≈_ = _≡_ + ; _∙_ = _+_ + ; ε = + 0 + ; isCommutativeMonoid = +-0-isCommutativeMonoid + } + ++-0-isGroup : IsGroup _≡_ _+_ (+ 0) (-_) ++-0-isGroup = record + { isMonoid = +-0-isMonoid + ; inverse = inverseˡ , inverseʳ + ; ⁻¹-cong = cong (-_) + } + +-isAbelianGroup : IsAbelianGroup _≡_ _+_ (+ 0) (-_) +-isAbelianGroup = record - { isGroup = record - { isMonoid = +-isMonoid - ; inverse = inverseˡ , inverseʳ - ; ⁻¹-cong = cong (-_) - } - ; comm = +-comm + { isGroup = +-0-isGroup + ; comm = +-comm } open Algebra.Properties.AbelianGroup (record { isAbelianGroup = +-isAbelianGroup }) using () renaming (⁻¹-involutive to -‿involutive) +------------------------------------------------------------------------ +-- Properties of _*_ --- Distributivity +*-comm : Commutative _*_ +*-comm -[1+ a ] -[1+ b ] rewrite ℕ.*-comm (suc a) (suc b) = refl +*-comm -[1+ a ] (+ b ) rewrite ℕ.*-comm (suc a) b = refl +*-comm (+ a ) -[1+ b ] rewrite ℕ.*-comm a (suc b) = refl +*-comm (+ a ) (+ b ) rewrite ℕ.*-comm a b = refl + +*-identityˡ : LeftIdentity (+ 1) _*_ +*-identityˡ (+ zero ) = refl +*-identityˡ -[1+ n ] rewrite ℕ.+-right-identity n = refl +*-identityˡ (+ suc n) rewrite ℕ.+-right-identity n = refl + +*-identityʳ : RightIdentity (+ 1) _*_ +*-identityʳ x rewrite + 𝕊.*-identityʳ (sign x) + | ℕ.*-right-identity ∣ x ∣ + | signₙ◃∣n∣≡n x + = refl + +*-identity : Identity (+ 1) _*_ +*-identity = *-identityˡ , *-identityʳ private + lemma : ∀ a b c → c ℕ+ (b ℕ+ a ℕ* suc b) ℕ* suc c + ≡ c ℕ+ b ℕ* suc c ℕ+ a ℕ* suc (c ℕ+ b ℕ* suc c) + lemma = + solve 3 (λ a b c → c :+ (b :+ a :* (con 1 :+ b)) :* (con 1 :+ c) + := c :+ b :* (con 1 :+ c) :+ + a :* (con 1 :+ (c :+ b :* (con 1 :+ c)))) + refl + where open ℕ.SemiringSolver + +*-assoc : Associative _*_ +*-assoc (+ zero) _ _ = refl +*-assoc x (+ zero) _ rewrite ℕ.*-right-zero ∣ x ∣ = refl +*-assoc x y (+ zero) rewrite + ℕ.*-right-zero ∣ y ∣ + | ℕ.*-right-zero ∣ x ∣ + | ℕ.*-right-zero ∣ sign x 𝕊* sign y ◃ ∣ x ∣ ℕ* ∣ y ∣ ∣ + = refl +*-assoc -[1+ a ] -[1+ b ] (+ suc c) = cong (+_ ∘ suc) (lemma a b c) +*-assoc -[1+ a ] (+ suc b) -[1+ c ] = cong (+_ ∘ suc) (lemma a b c) +*-assoc (+ suc a) (+ suc b) (+ suc c) = cong (+_ ∘ suc) (lemma a b c) +*-assoc (+ suc a) -[1+ b ] -[1+ c ] = cong (+_ ∘ suc) (lemma a b c) +*-assoc -[1+ a ] -[1+ b ] -[1+ c ] = cong -[1+_] (lemma a b c) +*-assoc -[1+ a ] (+ suc b) (+ suc c) = cong -[1+_] (lemma a b c) +*-assoc (+ suc a) -[1+ b ] (+ suc c) = cong -[1+_] (lemma a b c) +*-assoc (+ suc a) (+ suc b) -[1+ c ] = cong -[1+_] (lemma a b c) + +*-isSemigroup : IsSemigroup _ _ +*-isSemigroup = record + { isEquivalence = isEquivalence + ; assoc = *-assoc + ; ∙-cong = cong₂ _*_ + } - -- Various lemmas used to prove distributivity. +*-1-isMonoid : IsMonoid _≡_ _*_ (+ 1) +*-1-isMonoid = record + { isSemigroup = *-isSemigroup + ; identity = *-identity + } - sign-⊖-≱ : ∀ {m n} → m ≱ n → sign (m ⊖ n) ≡ Sign.- - sign-⊖-≱ = sign-⊖-< ∘ ℕ.≰⇒> +*-1-isCommutativeMonoid : IsCommutativeMonoid _≡_ _*_ (+ 1) +*-1-isCommutativeMonoid = record + { isSemigroup = *-isSemigroup + ; identityˡ = *-identityˡ + ; comm = *-comm + } - ∣⊖∣-≱ : ∀ {m n} → m ≱ n → ∣ m ⊖ n ∣ ≡ n ∸ m - ∣⊖∣-≱ = ∣⊖∣-< ∘ ℕ.≰⇒> +*-1-commutativeMonoid : CommutativeMonoid _ _ +*-1-commutativeMonoid = record + { Carrier = ℤ + ; _≈_ = _≡_ + ; _∙_ = _*_ + ; ε = + 1 + ; isCommutativeMonoid = *-1-isCommutativeMonoid + } - ⊖-≱ : ∀ {m n} → m ≱ n → m ⊖ n ≡ - + (n ∸ m) - ⊖-≱ = ⊖-< ∘ ℕ.≰⇒> +------------------------------------------------------------------------ +-- The integers form a commutative ring - -- Lemmas working around the fact that _◃_ pattern matches on its - -- second argument before its first. +-- Distributivity - +‿◃ : ∀ n → Sign.+ ◃ n ≡ + n - +‿◃ zero = refl - +‿◃ (suc _) = refl +private - -‿◃ : ∀ n → Sign.- ◃ n ≡ - + n - -‿◃ zero = refl - -‿◃ (suc _) = refl + -- lemma used to prove distributivity. distrib-lemma : ∀ a b c → (c ⊖ b) * -[1+ a ] ≡ a ℕ+ b ℕ* suc a ⊖ (a ℕ+ c ℕ* suc a) @@ -180,15 +343,15 @@ private with b ≤? c ... | yes b≤c rewrite ⊖-≥ b≤c - | ⊖-≥ (b≤c *-mono (≤-refl {x = suc a})) - | -‿◃ ((c ∸ b) ℕ* suc a) + | ⊖-≥ (ℕ.*-mono-≤ b≤c (≤-refl {x = suc a})) + | -◃n≡-n ((c ∸ b) ℕ* suc a) | ℕ.*-distrib-∸ʳ (suc a) c b = refl ... | no b≰c - rewrite sign-⊖-≱ b≰c - | ∣⊖∣-≱ b≰c - | +‿◃ ((b ∸ c) ℕ* suc a) - | ⊖-≱ (b≰c ∘ ℕ.cancel-*-right-≤ b c a) + rewrite sign-⊖-≰ b≰c + | ∣⊖∣-≰ b≰c + | +◃n≡+n ((b ∸ c) ℕ* suc a) + | ⊖-≰ (b≰c ∘ ℕ.cancel-*-right-≤ b c a) | -‿involutive (+ (b ℕ* suc a ∸ c ℕ* suc a)) | ℕ.*-distrib-∸ʳ (suc a) b c = refl @@ -196,19 +359,19 @@ private distribʳ : _*_ DistributesOverʳ _+_ distribʳ (+ zero) y z - rewrite proj₂ *-zero ∣ y ∣ - | proj₂ *-zero ∣ z ∣ - | proj₂ *-zero ∣ y + z ∣ + rewrite ℕ.*-right-zero ∣ y ∣ + | ℕ.*-right-zero ∣ z ∣ + | ℕ.*-right-zero ∣ y + z ∣ = refl distribʳ x (+ zero) z - rewrite proj₁ +-identity z - | proj₁ +-identity (sign z S* sign x ◃ ∣ z ∣ ℕ* ∣ x ∣) + rewrite +-identityˡ z + | +-identityˡ (sign z 𝕊* sign x ◃ ∣ z ∣ ℕ* ∣ x ∣) = refl distribʳ x y (+ zero) - rewrite proj₂ +-identity y - | proj₂ +-identity (sign y S* sign x ◃ ∣ y ∣ ℕ* ∣ x ∣) + rewrite +-identityʳ y + | +-identityʳ (sign y 𝕊* sign x ◃ ∣ y ∣ ℕ* ∣ x ∣) = refl distribʳ -[1+ a ] -[1+ b ] -[1+ c ] = cong (+_) $ @@ -245,15 +408,15 @@ distribʳ (+ suc a) -[1+ b ] (+ suc c) ... | yes b≤c rewrite ⊖-≥ b≤c | +-comm (- (+ (a ℕ+ b ℕ* suc a))) (+ (a ℕ+ c ℕ* suc a)) - | ⊖-≥ (b≤c *-mono ≤-refl {x = suc a}) + | ⊖-≥ (ℕ.*-mono-≤ b≤c (≤-refl {x = suc a})) | ℕ.*-distrib-∸ʳ (suc a) c b - | +‿◃ (c ℕ* suc a ∸ b ℕ* suc a) + | +◃n≡+n (c ℕ* suc a ∸ b ℕ* suc a) = refl ... | no b≰c - rewrite sign-⊖-≱ b≰c - | ∣⊖∣-≱ b≰c - | -‿◃ ((b ∸ c) ℕ* suc a) - | ⊖-≱ (b≰c ∘ ℕ.cancel-*-right-≤ b c a) + rewrite sign-⊖-≰ b≰c + | ∣⊖∣-≰ b≰c + | -◃n≡-n ((b ∸ c) ℕ* suc a) + | ⊖-≰ (b≰c ∘ ℕ.cancel-*-right-≤ b c a) | ℕ.*-distrib-∸ʳ (suc a) b c = refl @@ -262,29 +425,40 @@ distribʳ (+ suc c) (+ suc a) -[1+ b ] with b ≤? a ... | yes b≤a rewrite ⊖-≥ b≤a - | ⊖-≥ (b≤a *-mono ≤-refl {x = suc c}) - | +‿◃ ((a ∸ b) ℕ* suc c) + | ⊖-≥ (ℕ.*-mono-≤ b≤a (≤-refl {x = suc c})) + | +◃n≡+n ((a ∸ b) ℕ* suc c) | ℕ.*-distrib-∸ʳ (suc c) a b = refl ... | no b≰a - rewrite sign-⊖-≱ b≰a - | ∣⊖∣-≱ b≰a - | ⊖-≱ (b≰a ∘ ℕ.cancel-*-right-≤ b a c) - | -‿◃ ((b ∸ a) ℕ* suc c) + rewrite sign-⊖-≰ b≰a + | ∣⊖∣-≰ b≰a + | ⊖-≰ (b≰a ∘ ℕ.cancel-*-right-≤ b a c) + | -◃n≡-n ((b ∸ a) ℕ* suc c) | ℕ.*-distrib-∸ʳ (suc c) b a = refl --- The IsCommutativeSemiring module contains a proof of --- distributivity which is used below. - isCommutativeSemiring : IsCommutativeSemiring _≡_ _+_ _*_ (+ 0) (+ 1) isCommutativeSemiring = record - { +-isCommutativeMonoid = +-isCommutativeMonoid - ; *-isCommutativeMonoid = *-isCommutativeMonoid + { +-isCommutativeMonoid = +-0-isCommutativeMonoid + ; *-isCommutativeMonoid = *-1-isCommutativeMonoid ; distribʳ = distribʳ ; zeroˡ = λ _ → refl } ++-*-isRing : IsRing _≡_ _+_ _*_ -_ (+ 0) (+ 1) ++-*-isRing = record + { +-isAbelianGroup = +-isAbelianGroup + ; *-isMonoid = *-1-isMonoid + ; distrib = IsCommutativeSemiring.distrib + isCommutativeSemiring + } + ++-*-isCommutativeRing : IsCommutativeRing _≡_ _+_ _*_ -_ (+ 0) (+ 1) ++-*-isCommutativeRing = record + { isRing = +-*-isRing + ; *-comm = *-comm + } + commutativeRing : CommutativeRing _ _ commutativeRing = record { Carrier = ℤ @@ -294,15 +468,7 @@ commutativeRing = record ; -_ = -_ ; 0# = + 0 ; 1# = + 1 - ; isCommutativeRing = record - { isRing = record - { +-isAbelianGroup = +-isAbelianGroup - ; *-isMonoid = *-isMonoid - ; distrib = IsCommutativeSemiring.distrib - isCommutativeSemiring - } - ; *-comm = *-comm - } + ; isCommutativeRing = +-*-isCommutativeRing } import Algebra.RingSolver.Simple as Solver @@ -313,10 +479,14 @@ module RingSolver = ------------------------------------------------------------------------ -- More properties +-- ∣_∣ commutes with multiplication. + +abs-*-commute : Homomorphic₂ ∣_∣ _*_ _ℕ*_ +abs-*-commute i j = abs-◃ _ _ + -- Multiplication is right cancellative for non-zero integers. -cancel-*-right : ∀ i j k → - k ≢ + 0 → i * k ≡ j * k → i ≡ j +cancel-*-right : ∀ i j k → k ≢ + 0 → i * k ≡ j * k → i ≡ j cancel-*-right i j k ≢0 eq with signAbs k cancel-*-right i j .(+ 0) ≢0 eq | s ◂ zero = contradiction refl ≢0 cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n @@ -326,20 +496,20 @@ cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n ℕ.cancel-*-right ∣ i ∣ ∣ j ∣ $ abs-cong eq where sign-i≡sign-j : ∀ i j → - sign i S* s ◃ ∣ i ∣ ℕ* suc n ≡ - sign j S* s ◃ ∣ j ∣ ℕ* suc n → + sign i 𝕊* s ◃ ∣ i ∣ ℕ* suc n ≡ + sign j 𝕊* s ◃ ∣ j ∣ ℕ* suc n → sign i ≡ sign j sign-i≡sign-j i j eq with signAbs i | signAbs j sign-i≡sign-j .(+ 0) .(+ 0) eq | s₁ ◂ zero | s₂ ◂ zero = refl sign-i≡sign-j .(+ 0) .(s₂ ◃ suc n₂) eq | s₁ ◂ zero | s₂ ◂ suc n₂ with ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂) ... | .(suc n₂) | refl - with abs-cong {s₁} {sign (s₂ ◃ suc n₂) S* s} {0} {suc n₂ ℕ* suc n} eq + with abs-cong {s₁} {sign (s₂ ◃ suc n₂) 𝕊* s} {0} {suc n₂ ℕ* suc n} eq ... | () sign-i≡sign-j .(s₁ ◃ suc n₁) .(+ 0) eq | s₁ ◂ suc n₁ | s₂ ◂ zero with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁) ... | .(suc n₁) | refl - with abs-cong {sign (s₁ ◃ suc n₁) S* s} {s₁} {suc n₁ ℕ* suc n} {0} eq + with abs-cong {sign (s₁ ◃ suc n₁) 𝕊* s} {s₁} {suc n₁ ℕ* suc n} {0} eq ... | () sign-i≡sign-j .(s₁ ◃ suc n₁) .(s₂ ◃ suc n₂) eq | s₁ ◂ suc n₁ | s₂ ◂ suc n₂ with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁) @@ -347,7 +517,7 @@ cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n | ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂) | sign (s₂ ◃ suc n₂) | sign-◃ s₂ n₂ ... | .(suc n₁) | refl | .s₁ | refl | .(suc n₂) | refl | .s₂ | refl = - SignProp.cancel-*-right s₁ s₂ (sign-cong eq) + 𝕊.cancel-*-right s₁ s₂ (sign-cong eq) -- Multiplication with a positive number is right cancellative (for -- _≤_). @@ -370,9 +540,9 @@ cancel-*-+-right-≤ (+ suc m) (+ suc n) o (+≤+ m≤n) = *-+-right-mono _ (-≤+ {n = 0}) = -≤+ *-+-right-mono _ (-≤+ {n = suc _}) = -≤+ *-+-right-mono x (-≤- n≤m) = - -≤- (≤-pred (s≤s n≤m *-mono ≤-refl {x = suc x})) + -≤- (≤-pred (ℕ.*-mono-≤ (s≤s n≤m) (≤-refl {x = suc x}))) *-+-right-mono _ (+≤+ {m = 0} {n = 0} m≤n) = +≤+ m≤n *-+-right-mono _ (+≤+ {m = 0} {n = suc _} m≤n) = +≤+ z≤n *-+-right-mono _ (+≤+ {m = suc _} {n = 0} ()) *-+-right-mono x (+≤+ {m = suc _} {n = suc _} m≤n) = - +≤+ (m≤n *-mono ≤-refl {x = suc x}) + +≤+ ((ℕ.*-mono-≤ m≤n (≤-refl {x = suc x}))) diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda index 55f6278319..3f60dae982 100644 --- a/src/Data/Sign/Properties.agda +++ b/src/Data/Sign/Properties.agda @@ -9,7 +9,9 @@ module Data.Sign.Properties where open import Data.Empty open import Function open import Data.Sign +open import Data.Product using (_,_) open import Relation.Binary.PropositionalEquality +open import Algebra.FunctionProperties (_≡_ {A = Sign}) -- The opposite of a sign is not equal to the sign. @@ -17,10 +19,34 @@ opposite-not-equal : ∀ s → s ≢ opposite s opposite-not-equal - () opposite-not-equal + () --- Sign multiplication is right cancellative. +opposite-cong : ∀ {s t} → opposite s ≡ opposite t → s ≡ t +opposite-cong { - } { - } refl = refl +opposite-cong { - } { + } () +opposite-cong { + } { - } () +opposite-cong { + } { + } refl = refl -cancel-*-right : ∀ s₁ s₂ {s} → s₁ * s ≡ s₂ * s → s₁ ≡ s₂ +------------------------------------------------------------------------ +-- _*_ + +*-identityˡ : LeftIdentity + _*_ +*-identityˡ _ = refl + +*-identityʳ : RightIdentity + _*_ +*-identityʳ - = refl +*-identityʳ + = refl + +*-identity : Identity + _*_ +*-identity = *-identityˡ , *-identityʳ + +cancel-*-right : RightCancellative _*_ cancel-*-right - - _ = refl cancel-*-right - + eq = ⊥-elim (opposite-not-equal _ $ sym eq) cancel-*-right + - eq = ⊥-elim (opposite-not-equal _ eq) cancel-*-right + + _ = refl + +cancel-*-left : LeftCancellative _*_ +cancel-*-left - eq = opposite-cong eq +cancel-*-left + eq = eq + +*-cancellative : Cancellative _*_ +*-cancellative = cancel-*-left , cancel-*-right From d56ec0e4338aee1adc5811722a4164cf4957b923 Mon Sep 17 00:00:00 2001 From: Matthew Daggitt Date: Wed, 28 Jun 2017 17:37:03 +0100 Subject: [PATCH 2/3] Added some additional properties from mechvel to Data.Integer.Properties --- CHANGELOG.md | 20 +++++++ src/Data/Integer/Base.agda | 4 +- src/Data/Integer/Properties.agda | 99 ++++++++++++++++++++++++++++---- src/Data/Sign/Properties.agda | 17 ++++++ 4 files changed, 126 insertions(+), 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 227d63d5c1..ec29d8b681 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -218,6 +218,15 @@ Backwards compatible changes * Added proofs to `Data.Integer.Properties` ```agda + +-injective : + m ≡ + n → m ≡ n + -[1+-injective : -[1+ m ] ≡ -[1+ n ] → m ≡ n + + doubleNeg : - - n ≡ n + neg-injective : - m ≡ - n → m ≡ n + + ∣n∣≡0⇒n≡0 : ∀ {n} → ∣ n ∣ ≡ 0 → n ≡ + 0 + ∣-n∣≡∣n∣ : ∀ n → ∣ - n ∣ ≡ ∣ n ∣ + +◃n≡+n : Sign.+ ◃ n ≡ + n -◃n≡-n : Sign.- ◃ n ≡ - + n signₙ◃∣n∣≡n : sign n ◃ ∣ n ∣ ≡ n @@ -225,14 +234,22 @@ Backwards compatible changes ⊖-≰ : n ≰ m → m ⊖ n ≡ - + (n ∸ m) ∣⊖∣-≰ : n ≰ m → ∣ m ⊖ n ∣ ≡ n ∸ m sign-⊖-≰ : n ≰ m → sign (m ⊖ n) ≡ Sign.- + -[n⊖m]≡-m+n : - (m ⊖ n) ≡ (- (+ m)) + (+ n) +-identity : Identity (+ 0) _+_ + +-inverse : Inverse (+ 0) -_ _+_ +-0-isMonoid : IsMonoid _≡_ _+_ (+ 0) +-0-isGroup : IsGroup _≡_ _+_ (+ 0) (-_) + neg-distrib-+ : - (m + n) ≡ (- m) + (- n) + ◃-distrib-+ : s ◃ (m + n) ≡ (s ◃ m) + (s ◃ n) *-identityʳ : RightIdentity (+ 1) _*_ *-identity : Identity (+ 1) _*_ + *-zeroˡ : LeftZero (+ 0) _*_ + *-zeroʳ : RightZero (+ 0) _*_ + *-zero : Zero (+ 0) _*_ *-1-isMonoid : IsMonoid _≡_ _*_ (+ 1) + -1*n≡-n : -[1+ 0 ] * n ≡ - n +-*-isRing : IsRing _≡_ _+_ _*_ -_ (+ 0) (+ 1) +-*-isCommutativeRing : IsCommutativeRing _≡_ _+_ _*_ -_ (+ 0) (+ 1) @@ -398,8 +415,11 @@ Backwards compatible changes *-identityˡ : LeftIdentity + _*_ *-identityʳ : RightIdentity + _*_ *-identity : Identity + _*_ + *-comm : Commutative _*_ + *-assoc : Associative _*_ cancel-*-left : LeftCancellative _*_ *-cancellative : Cancellative _*_ + s*s≡+ : s * s ≡ + ``` * Added proofs to `Data.Vec.All.Properties` diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda index 8894f16ae2..a227013728 100644 --- a/src/Data/Integer/Base.agda +++ b/src/Data/Integer/Base.agda @@ -146,8 +146,8 @@ _⊓_ : ℤ → ℤ → ℤ data _≤_ : ℤ → ℤ → Set where -≤+ : ∀ {m n} → -[1+ m ] ≤ + n - -≤- : ∀ {m n} → (n≤m : ℕ._≤_ n m) → -[1+ m ] ≤ -[1+ n ] - +≤+ : ∀ {m n} → (m≤n : ℕ._≤_ m n) → + m ≤ + n + -≤- : ∀ {m n} → (n≤m : n ℕ.≤ m) → -[1+ m ] ≤ -[1+ n ] + +≤+ : ∀ {m n} → (m≤n : m ℕ.≤ n) → + m ≤ + n drop‿+≤+ : ∀ {m n} → + m ≤ + n → ℕ._≤_ m n drop‿+≤+ (+≤+ m≤n) = m≤n diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 96c523c799..f0cffc9dbf 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -31,6 +31,42 @@ open Morphism.Definitions ℤ ℕ _≡_ open ℕ.SemiringSolver open ≡-Reasoning +------------------------------------------------------------------------ +-- Equality + ++-injective : ∀ {m n} → + m ≡ + n → m ≡ n ++-injective refl = refl + +-[1+-injective : ∀ {m n} → -[1+ m ] ≡ -[1+ n ] → m ≡ n +-[1+-injective refl = refl + +------------------------------------------------------------------------ +-- Properties of -_ + +doubleNeg : ∀ n → - - n ≡ n +doubleNeg (+ zero) = refl +doubleNeg (+ suc n) = refl +doubleNeg (-[1+ n ]) = refl + +neg-injective : ∀ {m n} → - m ≡ - n → m ≡ n +neg-injective {m} {n} -m≡-n = begin + m ≡⟨ sym (doubleNeg m) ⟩ + - - m ≡⟨ cong -_ -m≡-n ⟩ + - - n ≡⟨ doubleNeg n ⟩ + n ∎ + +------------------------------------------------------------------------ +-- Properties of ∣_∣ + +∣n∣≡0⇒n≡0 : ∀ {n} → ∣ n ∣ ≡ 0 → n ≡ + 0 +∣n∣≡0⇒n≡0 {+ .zero} refl = refl +∣n∣≡0⇒n≡0 { -[1+_] n} () + +∣-n∣≡∣n∣ : ∀ n → ∣ - n ∣ ≡ ∣ n ∣ +∣-n∣≡∣n∣ (+ zero) = refl +∣-n∣≡∣n∣ (+ suc n) = refl +∣-n∣≡∣n∣ (-[1+ n ]) = refl + ------------------------------------------------------------------------ -- Properties of sign and _◃_ @@ -109,6 +145,12 @@ sign-⊖-< {suc n} (s≤s m +-[n⊖m]≡-m+n : ∀ m n → - (m ⊖ n) ≡ (- (+ m)) + (+ n) +-[n⊖m]≡-m+n zero zero = refl +-[n⊖m]≡-m+n zero (suc n) = refl +-[n⊖m]≡-m+n (suc m) zero = refl +-[n⊖m]≡-m+n (suc m) (suc n) = sym (⊖-swap n m) + +-⊖-left-cancel : ∀ a b c → (a ℕ+ b) ⊖ (a ℕ+ c) ≡ b ⊖ c +-⊖-left-cancel zero b c = refl +-⊖-left-cancel (suc a) b c = +-⊖-left-cancel a b c @@ -200,6 +242,9 @@ inverseʳ i = begin - i + i ≡⟨ inverseˡ i ⟩ + 0 ∎ ++-inverse : Inverse (+ 0) -_ _+_ ++-inverse = inverseˡ , inverseʳ + +-isSemigroup : IsSemigroup _≡_ _+_ +-isSemigroup = record { isEquivalence = isEquivalence @@ -232,7 +277,7 @@ inverseʳ i = begin +-0-isGroup : IsGroup _≡_ _+_ (+ 0) (-_) +-0-isGroup = record { isMonoid = +-0-isMonoid - ; inverse = inverseˡ , inverseʳ + ; inverse = +-inverse ; ⁻¹-cong = cong (-_) } @@ -246,6 +291,32 @@ open Algebra.Properties.AbelianGroup (record { isAbelianGroup = +-isAbelianGroup }) using () renaming (⁻¹-involutive to -‿involutive) +-- Other properties of _+_ + +neg-distrib-+ : ∀ m n → - (m + n) ≡ (- m) + (- n) +neg-distrib-+ (+ zero) (+ zero) = refl +neg-distrib-+ (+ zero) (+ suc n) = refl +neg-distrib-+ (+ suc m) (+ zero) = cong -[1+_] (ℕ.+-right-identity m) +neg-distrib-+ (+ suc m) (+ suc n) = cong -[1+_] (ℕ.+-suc m n) +neg-distrib-+ -[1+ m ] -[1+ n ] = cong (λ v → + suc v) (sym (ℕ.+-suc m n)) +neg-distrib-+ (+ m) -[1+ n ] = -[n⊖m]≡-m+n m (suc n) +neg-distrib-+ -[1+ m ] (+ n) = + trans (-[n⊖m]≡-m+n n (suc m)) (+-comm (- + n) (+ suc m)) + +◃-distrib-+ : ∀ s m n → s ◃ (m ℕ+ n) ≡ (s ◃ m) + (s ◃ n) +◃-distrib-+ Sign.- m n = begin + Sign.- ◃ (m ℕ+ n) ≡⟨ -◃n≡-n (m ℕ+ n) ⟩ + - (+ (m ℕ+ n)) ≡⟨⟩ + - ((+ m) + (+ n)) ≡⟨ neg-distrib-+ (+ m) (+ n) ⟩ + (- (+ m)) + (- (+ n)) ≡⟨ sym (cong₂ _+_ (-◃n≡-n m) (-◃n≡-n n)) ⟩ + (Sign.- ◃ m) + (Sign.- ◃ n) ∎ +◃-distrib-+ Sign.+ m n = begin + Sign.+ ◃ (m ℕ+ n) ≡⟨ +◃n≡+n (m ℕ+ n) ⟩ + + (m ℕ+ n) ≡⟨⟩ + (+ m) + (+ n) ≡⟨ sym (cong₂ _+_ (+◃n≡+n m) (+◃n≡+n n)) ⟩ + (Sign.+ ◃ m) + (Sign.+ ◃ n) ∎ + + ------------------------------------------------------------------------ -- Properties of _*_ @@ -270,6 +341,15 @@ open Algebra.Properties.AbelianGroup *-identity : Identity (+ 1) _*_ *-identity = *-identityˡ , *-identityʳ +*-zeroˡ : LeftZero (+ 0) _*_ +*-zeroˡ n = refl + +*-zeroʳ : RightZero (+ 0) _*_ +*-zeroʳ n rewrite *-comm n (+ 0) = refl + +*-zero : Zero (+ 0) _*_ +*-zero = *-zeroˡ , *-zeroʳ + private lemma : ∀ a b c → c ℕ+ (b ℕ+ a ℕ* suc b) ℕ* suc c ≡ c ℕ+ b ℕ* suc c ℕ+ a ℕ* suc (c ℕ+ b ℕ* suc c) @@ -476,16 +556,11 @@ import Algebra.RingSolver.AlmostCommutativeRing as ACR module RingSolver = Solver (ACR.fromCommutativeRing commutativeRing) _≟_ ------------------------------------------------------------------------- --- More properties - --- ∣_∣ commutes with multiplication. +-- Other properties of _*_ abs-*-commute : Homomorphic₂ ∣_∣ _*_ _ℕ*_ abs-*-commute i j = abs-◃ _ _ --- Multiplication is right cancellative for non-zero integers. - cancel-*-right : ∀ i j k → k ≢ + 0 → i * k ≡ j * k → i ≡ j cancel-*-right i j k ≢0 eq with signAbs k cancel-*-right i j .(+ 0) ≢0 eq | s ◂ zero = contradiction refl ≢0 @@ -519,9 +594,6 @@ cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n ... | .(suc n₁) | refl | .s₁ | refl | .(suc n₂) | refl | .s₂ | refl = 𝕊.cancel-*-right s₁ s₂ (sign-cong eq) --- Multiplication with a positive number is right cancellative (for --- _≤_). - cancel-*-+-right-≤ : ∀ m n o → m * + suc o ≤ n * + suc o → m ≤ n cancel-*-+-right-≤ (-[1+ m ]) (-[1+ n ]) o (-≤- n≤m) = -≤- (≤-pred (ℕ.cancel-*-right-≤ (suc n) (suc m) o (s≤s n≤m))) @@ -534,8 +606,6 @@ cancel-*-+-right-≤ (+ suc _) (+ 0) _ (+≤+ ()) cancel-*-+-right-≤ (+ suc m) (+ suc n) o (+≤+ m≤n) = +≤+ (ℕ.cancel-*-right-≤ (suc m) (suc n) o m≤n) --- Multiplication with a positive number is monotone. - *-+-right-mono : ∀ n → (λ x → x * + suc n) Preserves _≤_ ⟶ _≤_ *-+-right-mono _ (-≤+ {n = 0}) = -≤+ *-+-right-mono _ (-≤+ {n = suc _}) = -≤+ @@ -546,3 +616,8 @@ cancel-*-+-right-≤ (+ suc m) (+ suc n) o (+≤+ m≤n) = *-+-right-mono _ (+≤+ {m = suc _} {n = 0} ()) *-+-right-mono x (+≤+ {m = suc _} {n = suc _} m≤n) = +≤+ ((ℕ.*-mono-≤ m≤n (≤-refl {x = suc x}))) + +-1*n≡-n : ∀ n → -[1+ 0 ] * n ≡ - n +-1*n≡-n (+ zero) = refl +-1*n≡-n (+ suc n) = cong -[1+_] (ℕ.+-right-identity n) +-1*n≡-n -[1+ n ] = cong (λ v → + suc v) (ℕ.+-right-identity n) diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda index 3f60dae982..8ac8bc48e2 100644 --- a/src/Data/Sign/Properties.agda +++ b/src/Data/Sign/Properties.agda @@ -38,6 +38,19 @@ opposite-cong { + } { + } refl = refl *-identity : Identity + _*_ *-identity = *-identityˡ , *-identityʳ +*-comm : Commutative _*_ +*-comm + + = refl +*-comm + - = refl +*-comm - + = refl +*-comm - - = refl + +*-assoc : Associative _*_ +*-assoc + + _ = refl +*-assoc + - _ = refl +*-assoc - + _ = refl +*-assoc - - + = refl +*-assoc - - - = refl + cancel-*-right : RightCancellative _*_ cancel-*-right - - _ = refl cancel-*-right - + eq = ⊥-elim (opposite-not-equal _ $ sym eq) @@ -50,3 +63,7 @@ cancel-*-left + eq = eq *-cancellative : Cancellative _*_ *-cancellative = cancel-*-left , cancel-*-right + +s*s≡+ : ∀ s → s * s ≡ + +s*s≡+ + = refl +s*s≡+ - = refl From 1426a27ce7f581a7c46a23ee4429c069ce7ebd84 Mon Sep 17 00:00:00 2001 From: Matthew Daggitt Date: Thu, 29 Jun 2017 10:49:15 +0100 Subject: [PATCH 3/3] Added Sergei Meshveliani to README.agda --- README.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README.agda b/README.agda index 731ff7e805..9322fd7a87 100644 --- a/README.agda +++ b/README.agda @@ -8,10 +8,10 @@ module README where -- Joachim Breitner, Samuel Bronson, Daniel Brown, James Chapman, -- Liang-Ting Chen, Matthew Daggitt, Dominique Devriese, Dan Doel, -- Érdi Gergő, Helmut Grohne, Simon Foster, Liyang Hu, Patrik Jansson, --- Alan Jeffrey, Pepijn Kokke, Evgeny Kotelnikov, Eric Mertens, Darin --- Morrison, Guilhem Moulin, Shin-Cheng Mu, Ulf Norell, Noriyuki --- OHKAWA, Nicolas Pouillard, Andrés Sicard-Ramírez, Noam Zeilberger --- and some anonymous contributors. +-- Alan Jeffrey, Pepijn Kokke, Evgeny Kotelnikov, Sergei Meshveliani +-- Eric Mertens, Darin Morrison, Guilhem Moulin, Shin-Cheng Mu, +-- Ulf Norell, Noriyuki OHKAWA, Nicolas Pouillard, Andrés Sicard-Ramírez, +-- Noam Zeilberger and some anonymous contributors. -- ---------------------------------------------------------------------- -- The development version of the library often requires the latest