1
------------------------------------------------------------------------
2
-- The Agda standard library
4
-- Properties related to addition of integers
5
------------------------------------------------------------------------
7
module Data.Integer.Addition.Properties where
10
import Algebra.FunctionProperties
11
open import Algebra.Structures
12
open import Data.Integer hiding (suc)
13
open import Data.Nat using (suc; zero) renaming (_+_ to _ℕ+_)
14
import Data.Nat.Properties as ℕ
15
open import Relation.Binary.PropositionalEquality
17
open Algebra.FunctionProperties (_≡_ {A = ℤ})
18
open CommutativeSemiring ℕ.commutativeSemiring
19
using (+-comm; +-assoc; +-identity)
21
------------------------------------------------------------------------
22
-- Addition and zero form a commutative monoid
26
comm : Commutative _+_
27
comm -[1+ a ] -[1+ b ] rewrite +-comm a b = refl
28
comm (+ a ) (+ b ) rewrite +-comm a b = refl
29
comm -[1+ _ ] (+ _ ) = refl
30
comm (+ _ ) -[1+ _ ] = refl
32
identityˡ : LeftIdentity (+ 0) _+_
33
identityˡ -[1+ _ ] = refl
34
identityˡ (+ _ ) = refl
36
identityʳ : RightIdentity (+ 0) _+_
37
identityʳ x rewrite comm x (+ 0) = identityˡ x
39
distribˡ-⊖-+-neg : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (suc c ℕ+ a)
40
distribˡ-⊖-+-neg _ zero zero = refl
41
distribˡ-⊖-+-neg _ zero (suc _) = refl
42
distribˡ-⊖-+-neg _ (suc _) zero = refl
43
distribˡ-⊖-+-neg a (suc b) (suc c) = distribˡ-⊖-+-neg a b c
45
distribʳ-⊖-+-neg : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (suc a ℕ+ c)
46
distribʳ-⊖-+-neg a b c
47
rewrite comm -[1+ a ] (b ⊖ c)
48
| distribˡ-⊖-+-neg a b c
52
distribˡ-⊖-+-pos : ∀ a b c → b ⊖ c + + a ≡ b ℕ+ a ⊖ c
53
distribˡ-⊖-+-pos _ zero zero = refl
54
distribˡ-⊖-+-pos _ zero (suc _) = refl
55
distribˡ-⊖-+-pos _ (suc _) zero = refl
56
distribˡ-⊖-+-pos a (suc b) (suc c) = distribˡ-⊖-+-pos a b c
58
distribʳ-⊖-+-pos : ∀ a b c → + a + (b ⊖ c) ≡ a ℕ+ b ⊖ c
59
distribʳ-⊖-+-pos a b c
60
rewrite comm (+ a) (b ⊖ c)
61
| distribˡ-⊖-+-pos a b c
65
assoc : Associative _+_
66
assoc (+ zero) y z rewrite identityˡ y | identityˡ (y + z) = refl
67
assoc x (+ zero) z rewrite identityʳ x | identityˡ z = refl
68
assoc x y (+ zero) rewrite identityʳ (x + y) | identityʳ y = refl
69
assoc -[1+ a ] -[1+ b ] (+ suc c) = sym (distribʳ-⊖-+-neg a c b)
70
assoc -[1+ a ] (+ suc b) (+ suc c) = distribˡ-⊖-+-pos (suc c) b a
71
assoc (+ suc a) -[1+ b ] -[1+ c ] = distribˡ-⊖-+-neg c a b
72
assoc (+ suc a) -[1+ b ] (+ suc c)
73
rewrite distribˡ-⊖-+-pos (suc c) a b
74
| distribʳ-⊖-+-pos (suc a) c b
78
assoc (+ suc a) (+ suc b) -[1+ c ]
79
rewrite distribʳ-⊖-+-pos (suc a) b c
83
assoc -[1+ a ] -[1+ b ] -[1+ c ]
84
rewrite sym (+-assoc a 1 (b ℕ+ c))
88
assoc -[1+ a ] (+ suc b) -[1+ c ]
89
rewrite distribʳ-⊖-+-neg a b c
90
| distribˡ-⊖-+-neg c b a
92
assoc (+ suc a) (+ suc b) (+ suc c)
93
rewrite +-assoc (suc a) (suc b) (suc c)
96
isSemigroup : IsSemigroup _≡_ _+_
98
{ isEquivalence = isEquivalence
103
isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ (+ 0)
104
isCommutativeMonoid = record
105
{ isSemigroup = isSemigroup
106
; identityˡ = identityˡ
110
commutativeMonoid : CommutativeMonoid _ _
111
commutativeMonoid = record
116
; isCommutativeMonoid = isCommutativeMonoid
added
removed
src/Data/Integer/Addition/Properties.agda
