26
26
open import Data.Sum
28
28
------------------------------------------------------------------------
30
-- basic lemmas about (ℕ, +, *, 0, 1):
31
open import Data.Nat.Properties.Simple
29
33
-- (ℕ, +, *, 0, 1) is a commutative semiring
33
+-assoc : Associative _+_
34
+-assoc zero _ _ = refl
35
+-assoc (suc m) n o = cong suc $ +-assoc m n o
37
+-identity : Identity 0 _+_
38
+-identity = (λ _ → refl) , n+0≡n
40
n+0≡n : RightIdentity 0 _+_
42
n+0≡n (suc n) = cong suc $ n+0≡n n
44
m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
45
m+1+n≡1+m+n zero n = refl
46
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)
48
+-comm : Commutative _+_
49
+-comm zero n = sym $ proj₂ +-identity n
55
≡⟨ cong suc (+-comm m n) ⟩
57
≡⟨ sym (m+1+n≡1+m+n n m) ⟩
61
m*1+n≡m+mn : ∀ m n → m * suc n ≡ m + m * n
62
m*1+n≡m+mn zero n = refl
63
m*1+n≡m+mn (suc m) n =
68
≡⟨ cong (λ x → suc n + x) (m*1+n≡m+mn m n) ⟩
72
≡⟨ cong suc (sym $ +-assoc n m (m * n)) ⟩
74
≡⟨ cong (λ x → suc (x + m * n)) (+-comm n m) ⟩
76
≡⟨ cong suc (+-assoc m n (m * n)) ⟩
83
*-zero = (λ _ → refl) , n*0≡0
85
n*0≡0 : RightZero 0 _*_
87
n*0≡0 (suc n) = n*0≡0 n
89
*-comm : Commutative _*_
90
*-comm zero n = sym $ proj₂ *-zero n
96
≡⟨ cong (λ x → n + x) (*-comm m n) ⟩
98
≡⟨ sym (m*1+n≡m+mn n m) ⟩
102
distribʳ-*-+ : _*_ DistributesOverʳ _+_
103
distribʳ-*-+ m zero o = refl
104
distribʳ-*-+ m (suc n) o =
109
≡⟨ cong (_+_ m) $ distribʳ-*-+ m n o ⟩
111
≡⟨ sym $ +-assoc m (n * m) (o * m) ⟩
117
*-assoc : Associative _*_
118
*-assoc zero n o = refl
119
*-assoc (suc m) n o =
124
≡⟨ distribʳ-*-+ o n (m * n) ⟩
126
≡⟨ cong (λ x → n * o + x) $ *-assoc m n o ⟩
132
34
isCommutativeSemiring : IsCommutativeSemiring _≡_ _+_ _*_ 0 1
133
35
isCommutativeSemiring = record
134
36
{ +-isCommutativeMonoid = record
477
379
n∸n≡0 (suc n) = n∸n≡0 n
479
381
∸-+-assoc : ∀ m n o → (m ∸ n) ∸ o ≡ m ∸ (n + o)
480
∸-+-assoc m n zero = cong (_∸_ m) (sym $ proj₂ +-identity n)
382
∸-+-assoc m n zero = cong (_∸_ m) (sym $ +-right-identity n)
481
383
∸-+-assoc zero zero (suc o) = refl
482
384
∸-+-assoc zero (suc n) (suc o) = refl
483
385
∸-+-assoc (suc m) zero (suc o) = refl
486
388
+-∸-assoc : ∀ m {n o} → o ≤ n → (m + n) ∸ o ≡ m + (n ∸ o)
487
389
+-∸-assoc m (z≤n {n = n}) = begin m + n ∎
488
390
+-∸-assoc m (s≤s {m = o} {n = n} o≤n) = begin
489
(m + suc n) ∸ suc o ≡⟨ cong (λ n → n ∸ suc o) (m+1+n≡1+m+n m n) ⟩
391
(m + suc n) ∸ suc o ≡⟨ cong (λ n → n ∸ suc o) (+-suc m n) ⟩
490
392
suc (m + n) ∸ suc o ≡⟨ refl ⟩
491
393
(m + n) ∸ o ≡⟨ +-∸-assoc m o≤n ⟩
495
397
m+n∸n≡m m n = begin
496
398
(m + n) ∸ n ≡⟨ +-∸-assoc m (≤-refl {x = n}) ⟩
497
399
m + (n ∸ n) ≡⟨ cong (_+_ m) (n∸n≡0 n) ⟩
498
m + 0 ≡⟨ proj₂ +-identity m ⟩
400
m + 0 ≡⟨ +-right-identity m ⟩
501
403
m+n∸m≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
added
removed
src/Data/Nat/Properties.agda
