Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/mul.agda @ 413:ad086c3161d7 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 18 Jun 2024 14:05:44 +0900
parents b85402051cdb
children
comparison
equal deleted inserted replaced
412:b85402051cdb 413:ad086c3161d7
8 8
9 lemmm00 : ℕ 9 lemmm00 : ℕ
10 lemmm00 = suc (suc zero) 10 lemmm00 = suc (suc zero)
11 11
12 _+_ : ℕ → ℕ → ℕ 12 _+_ : ℕ → ℕ → ℕ
13 zero + y = y 13 x + zero = x
14 suc x + y = suc (x + y) 14 x + (suc y) = suc (x + y)
15 15
16 _*_ : ℕ → ℕ → ℕ 16 _*_ : ℕ → ℕ → ℕ
17 zero * y = zero 17 x * zero = zero
18 suc x * y = y + (x * y) 18 x * (suc y) = x + (x * y)
19 19
20 lemmm01 : ℕ 20 lemmm01 : ℕ
21 lemmm01 = suc (suc zero) + suc (suc zero) 21 lemmm01 = suc (suc zero) + suc (suc zero)
22 22
23 +-comm : ∀ x y → (x + y) ≡ (y + x) 23 +-comm : ∀ x y → (x + y) ≡ (y + x)
24 +-comm zero zero = refl 24 +-comm zero zero = refl
25 +-comm zero (suc y) = cong suc (+-comm zero y) 25 +-comm zero (suc y) = cong suc (+-comm zero y)
26 +-comm (suc x) zero = cong suc (+-comm x zero) 26 +-comm (suc x) zero = cong suc (+-comm x zero)
27 +-comm (suc x) (suc y) = begin 27 +-comm (suc x) (suc y) = begin
28 suc (x + suc y) ≡⟨ (cong suc (+-comm x (suc y))) ⟩ 28 suc (suc x + y) ≡⟨ cong suc (+-comm (suc x) y) ⟩
29 suc (suc (y + x)) ≡⟨ cong suc (cong suc (+-comm y x)) ⟩ 29 suc (y + suc x) ≡⟨ refl ⟩
30 suc (suc (x + y)) ≡⟨ cong suc ( +-comm (suc x) y) ⟩ 30 suc (suc (y + x)) ≡⟨ cong suc (cong suc (+-comm y x )) ⟩
31 suc (y + suc x) ∎ where open ≡-Reasoning 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
32 34
33 +-assoc : ∀ x y z → (x + (y + z)) ≡ ((x + y) + z) 35 +-assoc : ∀ x y z → (x + (y + z)) ≡ ((x + y) + z)
34 +-assoc zero y z = refl 36 +-assoc x y zero = refl
35 +-assoc (suc x) y z = cong suc (+-assoc x y z) 37 +-assoc x y (suc z) = cong suc (+-assoc x y z)
36
37 *-distr-r : {y x z : ℕ } → (y * z) + (x * z) ≡ ((y + x) * z)
38 *-distr-r {zero} {x} {z} = refl
39 *-distr-r {suc y} {x} {z} = trans (sym (+-assoc z _ _)) (cong (λ k → z + k)(*-distr-r {y} {x} {z}))
40 38
41 *-distr-l : {y x z : ℕ } → (y * z) + (y * x) ≡ y * (z + x ) 39 *-distr-r : {x y z : ℕ } → (x * y) + (x * z) ≡ x * (y + z)
42 *-distr-l {zero} {x} = refl 40 *-distr-r {x} {y} {zero} = refl
43 *-distr-l {suc y} {x} {z} = begin 41 *-distr-r {x} {y} {suc z} = begin
44 (z + (y * z)) + (x + (y * x)) ≡⟨ +-assoc (z + (y * z)) x _ ⟩ 42 (x * y) + (x + (x * z)) ≡⟨ +-assoc (x * y) x _ ⟩
45 ((z + (y * z)) + x) + (y * x) ≡⟨ cong (λ k → k + (y * x)) (sym (+-assoc z _ _)) ⟩ 43 ((x * y) + x) + (x * z) ≡⟨ cong (λ k → k + (x * z)) (+-comm (x * y) _ ) ⟩
46 (z + ((y * z) + x)) + (y * x) ≡⟨ cong (λ k → (z + k) + (y * x) ) (+-comm _ x) ⟩ 44 (x + (x * y) ) + (x * z) ≡⟨ sym (+-assoc x (x * y) _) ⟩
47 (z + (x + (y * z))) + (y * x) ≡⟨ cong (λ k → k + (y * x)) (+-assoc z _ _) ⟩ 45 (x + ((x * y) + (x * z))) ≡⟨ cong (λ k → x + k)(*-distr-r {x} {y} {z}) ⟩
48 ((z + x) + (y * z)) + (y * x) ≡⟨ sym (+-assoc (z + x) _ _) ⟩ 46 x + (x * (y + z)) ∎ where open ≡-Reasoning
49 (z + x) + ((y * z) + (y * x)) ≡⟨ cong (λ k → (z + x) + k) (*-distr-l {y} {x} {z}) ⟩ 47
50 (z + x) + (y * (z + x)) ∎ where open ≡-Reasoning 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
51 58
52 *-comm : ∀ x y → (x * y) ≡ (y * x) 59 *-comm : ∀ x y → (x * y) ≡ (y * x)
53 *-comm zero zero = refl 60 *-comm zero zero = refl
54 *-comm zero (suc y) = *-comm zero y 61 *-comm zero (suc y) = trans (+-comm zero (zero * y)) (*-comm zero y)
55 *-comm (suc x) y = lemma2 where 62 *-comm (suc x) zero = trans (*-comm x zero) (+-comm (zero * x ) zero )
56 lemma3 : {y : ℕ}　→ y ≡ (y * suc zero) 63 *-comm (suc x) (suc y) = lemma2 where
57 lemma3 {zero} = refl 64 lemma3 : (y : ℕ) → y ≡ (suc zero * y)
58 lemma3 {suc y} = cong suc (lemma3 {y}) 65 lemma3 zero = refl
59 lemma2 : (y + (x * y)) ≡ (y * suc x) 66 lemma3 (suc y) = trans (cong suc (lemma3 y)) (+-comm _ (suc zero))
60 lemma2 = begin 67 lemma2 : (suc x * suc y) ≡ (suc y * suc x)
61 (y + (x * y)) ≡⟨ cong₂ (λ j k → j + k ) lemma3 (*-comm x y) ⟩ 68 lemma2 = begin
62 (y * suc zero) + (y * x) ≡⟨ *-distr-l {y} ⟩ 69 (suc x * suc y) ≡⟨ sym ( *-distr-l {x} {suc zero} {suc y}) ⟩
63 y * suc x ∎ where open ≡-Reasoning 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
64 77
65 *-assoc : ∀ x y z → (x * y) * z ≡ x * (y * z) 78 *-assoc : ∀ x y z → (x * (y * z)) ≡ ((x * y) * z)
66 *-assoc zero y z = refl 79 *-assoc x y zero = refl
67 *-assoc (suc x) y z = begin 80 *-assoc x y (suc z) = begin
68 ((y + (x * y)) * z) ≡⟨ sym (*-distr-r {y} ) ⟩ 81 x * (y * suc z) ≡⟨ refl ⟩
69 (y * z) + ((x * y) * z) ≡⟨ cong (λ k → (y * z) + k) (*-assoc x y z) ⟩ 82 x * (y + (y * z)) ≡⟨ sym ( *-distr-r {x} {y} {y * z}) ⟩
70 (y * z) + (x * (y * z)) ∎ where open ≡-Reasoning 83 (x * y) + (x * (y * z)) ≡⟨ cong (λ k → (x * y) + k) (*-assoc x y z) ⟩
71 84 (x * y) + ((x * y) * z) ∎ where open ≡-Reasoning
72 _+ˡ_ : ℕ → ℕ → ℕ
73 x +ˡ zero = x
74 x +ˡ suc y = suc (x +ˡ y)
75
76 theorem00 : ∀ x y → (x +ˡ y) ≡ (y + x)
77 theorem00 x zero = refl
78 theorem00 x (suc y) = cong suc (theorem00 x y)
79
80 _*ˡ_ : ℕ → ℕ → ℕ
81 x *ˡ zero = zero
82 x *ˡ (suc y) = x +ˡ (x *ˡ y)
83
84
85 open import Data.Empty
86 open import Data.Unit
87 open import Relation.Nullary
88
89 -- theorem000 : ¬ ( _*_ ≡ _*ˡ_ )
90 -- theorem000 ()
91
92 theorem01 : ∀ x y → (x *ˡ y) ≡ (y * x)
93 theorem01 x zero = refl
94 theorem01 x (suc y) = begin
95 (x *ˡ suc y) ≡⟨ refl ⟩
96 x +ˡ (x *ˡ y) ≡⟨ cong (λ k → x +ˡ k) (theorem01 x y) ⟩
97 x +ˡ (y * x) ≡⟨ theorem00 x _ ⟩
98 (y * x) + x ≡⟨ +-comm _ x ⟩
99 x + (y * x) ∎ where open ≡-Reasoning
100
101 +ˡ-assoc : ∀ x y z → (x +ˡ (y +ˡ z)) ≡ ((x +ˡ y) +ˡ z)
102 +ˡ-assoc x y zero = refl
103 +ˡ-assoc x y (suc z) = cong suc (+ˡ-assoc x y z)
104
105 -- *ˡ-distr-l : {y x z : ℕ } → (y *ˡ z) +ˡ (y *ˡ x) ≡ y *ˡ (z +ˡ x )
106 -- *ˡ-distr-l {y} {zero} {z} = refl
107 -- *ˡ-distr-l {y} {suc x} {z} = trans ? (cong (λ k → y +ˡ k)(*ˡ-distr-l {y} {x} {z}))
108
109
110 theorem02 : ∀ x y → (x *ˡ y) ≡ (x * y)
111 theorem02 x y = trans (theorem01 x y) (*-comm y x)
112
113 -- record Monad (M : Set → Set) : Set₁ where
114 -- field
115 -- return : {A : Set} → A → M A
116 -- _>>=_ : {A B : Set} → M A → (A → M B) → M B
117
118 --*-Monad : { M : Set → Set } → Monad M → ℕ → ℕ → ℕ
119 --*-Monad {M} m n n = ?
120 85
121 86
122 87