|
412
|
1 module mul where
|
|
|
2
|
|
|
3 open import Relation.Binary.PropositionalEquality
|
|
|
4
|
|
|
5 data ℕ : Set where
|
|
|
6 zero : ℕ
|
|
|
7 suc : ℕ → ℕ
|
|
|
8
|
|
|
9 lemmm00 : ℕ
|
|
|
10 lemmm00 = suc (suc zero)
|
|
|
11
|
|
|
12 _+_ : ℕ → ℕ → ℕ
|
|
413
|
13 x + zero = x
|
|
|
14 x + (suc y) = suc (x + y)
|
|
412
|
15
|
|
|
16 _*_ : ℕ → ℕ → ℕ
|
|
413
|
17 x * zero = zero
|
|
|
18 x * (suc y) = x + (x * y)
|
|
412
|
19
|
|
|
20 lemmm01 : ℕ
|
|
|
21 lemmm01 = suc (suc zero) + suc (suc zero)
|
|
|
22
|
|
|
23 +-comm : ∀ x y → (x + y) ≡ (y + x)
|
|
|
24 +-comm zero zero = refl
|
|
|
25 +-comm zero (suc y) = cong suc (+-comm zero y)
|
|
|
26 +-comm (suc x) zero = cong suc (+-comm x zero)
|
|
|
27 +-comm (suc x) (suc y) = begin
|
|
413
|
28 suc (suc x + y) ≡⟨ cong suc (+-comm (suc x) y) ⟩
|
|
|
29 suc (y + suc x) ≡⟨ refl ⟩
|
|
|
30 suc (suc (y + x)) ≡⟨ cong suc (cong suc (+-comm y x )) ⟩
|
|
|
31 suc (suc (x + y)) ≡⟨ refl ⟩
|
|
|
32 suc (x + suc y) ≡⟨ cong suc (+-comm x (suc y) ) ⟩
|
|
|
33 suc (suc y + x) ∎ where open ≡-Reasoning
|
|
412
|
34
|
|
|
35 +-assoc : ∀ x y z → (x + (y + z)) ≡ ((x + y) + z)
|
|
413
|
36 +-assoc x y zero = refl
|
|
|
37 +-assoc x y (suc z) = cong suc (+-assoc x y z)
|
|
412
|
38
|
|
413
|
39 *-distr-r : {x y z : ℕ } → (x * y) + (x * z) ≡ x * (y + z)
|
|
|
40 *-distr-r {x} {y} {zero} = refl
|
|
|
41 *-distr-r {x} {y} {suc z} = begin
|
|
|
42 (x * y) + (x + (x * z)) ≡⟨ +-assoc (x * y) x _ ⟩
|
|
|
43 ((x * y) + x) + (x * z) ≡⟨ cong (λ k → k + (x * z)) (+-comm (x * y) _ ) ⟩
|
|
|
44 (x + (x * y) ) + (x * z) ≡⟨ sym (+-assoc x (x * y) _) ⟩
|
|
|
45 (x + ((x * y) + (x * z))) ≡⟨ cong (λ k → x + k)(*-distr-r {x} {y} {z}) ⟩
|
|
|
46 x + (x * (y + z)) ∎ where open ≡-Reasoning
|
|
|
47
|
|
|
48 *-distr-l : {x y z : ℕ } → (x * z) + (y * z) ≡ (x + y) * z
|
|
|
49 *-distr-l {x} {y} {zero} = refl
|
|
|
50 *-distr-l {x} {y} {suc z} = begin
|
|
|
51 (x + (x * z)) + (y + (y * z)) ≡⟨ +-assoc (x + (x * z)) y (y * z) ⟩
|
|
|
52 ((x + (x * z)) + y) + (y * z) ≡⟨ cong (λ k → k + (y * z)) (sym (+-assoc x (x * z) y)) ⟩
|
|
|
53 (x + ((x * z) + y)) + (y * z) ≡⟨ cong (λ k → (x + k) + (y * z) ) (+-comm _ y) ⟩
|
|
|
54 (x + (y + (x * z) )) + (y * z) ≡⟨ cong (λ k → k + (y * z)) (+-assoc x y (x * z)) ⟩
|
|
|
55 ((x + y) + (x * z) ) + (y * z) ≡⟨ sym (+-assoc (x + y) (x * z) (y * z)) ⟩
|
|
|
56 (x + y) + ((x * z) + (y * z)) ≡⟨ cong (λ k → (x + y) + k) (*-distr-l {x} {y} {z}) ⟩
|
|
|
57 (x + y) + ((x + y) * z) ∎ where open ≡-Reasoning
|
|
412
|
58
|
|
|
59 *-comm : ∀ x y → (x * y) ≡ (y * x)
|
|
|
60 *-comm zero zero = refl
|
|
413
|
61 *-comm zero (suc y) = trans (+-comm zero (zero * y)) (*-comm zero y)
|
|
|
62 *-comm (suc x) zero = trans (*-comm x zero) (+-comm (zero * x ) zero )
|
|
|
63 *-comm (suc x) (suc y) = lemma2 where
|
|
|
64 lemma3 : (y : ℕ) → y ≡ (suc zero * y)
|
|
|
65 lemma3 zero = refl
|
|
|
66 lemma3 (suc y) = trans (cong suc (lemma3 y)) (+-comm _ (suc zero))
|
|
|
67 lemma2 : (suc x * suc y) ≡ (suc y * suc x)
|
|
|
68 lemma2 = begin
|
|
|
69 (suc x * suc y) ≡⟨ sym ( *-distr-l {x} {suc zero} {suc y}) ⟩
|
|
|
70 (x + (x * y)) + (suc zero + (suc zero * y)) ≡⟨ cong (λ k → (x + (x * y)) + k) (+-comm (suc zero) (suc zero * y)) ⟩
|
|
|
71 (x + (x * y)) + suc (suc zero * y) ≡⟨ cong (λ k → (x + (x * y)) + k ) (cong suc (sym (lemma3 y))) ⟩
|
|
|
72 (x + (x * y)) + suc y ≡⟨ refl ⟩
|
|
|
73 (x * suc y) + suc y ≡⟨ +-comm _ (suc y) ⟩
|
|
|
74 suc y + (x * suc y ) ≡⟨ cong (λ k → suc y + k) (*-comm x (suc y)) ⟩
|
|
|
75 suc y + (suc y * x) ≡⟨ refl ⟩
|
|
|
76 suc y * suc x ∎ where open ≡-Reasoning
|
|
412
|
77
|
|
413
|
78 *-assoc : ∀ x y z → (x * (y * z)) ≡ ((x * y) * z)
|
|
|
79 *-assoc x y zero = refl
|
|
|
80 *-assoc x y (suc z) = begin
|
|
|
81 x * (y * suc z) ≡⟨ refl ⟩
|
|
|
82 x * (y + (y * z)) ≡⟨ sym ( *-distr-r {x} {y} {y * z}) ⟩
|
|
|
83 (x * y) + (x * (y * z)) ≡⟨ cong (λ k → (x * y) + k) (*-assoc x y z) ⟩
|
|
|
84 (x * y) + ((x * y) * z) ∎ where open ≡-Reasoning
|
|
412
|
85
|
|
|
86
|
|
|
87
|
