Mercurial > hg > Members > atton > agda > systemT

comparison int.agda @ 8:e191792472f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Try proof mult-sym. but not completed.
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 21 May 2014 21:11:34 +0900
parents f922e687f3a1
children 8ad92d830679
comparison
equal deleted inserted replaced
7:f922e687f3a1 8:e191792472f8
11 11
12 infixl 30 _+_ 12 infixl 30 _+_
13 _+_ : Int -> Int -> Int 13 _+_ : Int -> Int -> Int
14 n + O = n 14 n + O = n
15 n + (S m) = S (n + m) 15 n + (S m) = S (n + m)
16
17 left-add-zero : (n : Int) -> O + n ≡ n
18 left-add-zero O = refl
19 left-add-zero (S n) = cong S (left-add-zero n)
20
16 21
17 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m) 22 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m)
18 left-increment n O = refl 23 left-increment n O = refl
19 left-increment n (S m) = cong S (left-increment n m) 24 left-increment n (S m) = cong S (left-increment n m)
20 25
50 infixl 40 _*_ 55 infixl 40 _*_
51 _*_ : Int -> Int -> Int 56 _*_ : Int -> Int -> Int
52 n * O = O 57 n * O = O
53 n * (S O) = n 58 n * (S O) = n
54 n * (S m) = n + (n * m) 59 n * (S m) = n + (n * m)
60
61 right-mult-zero : (n : Int) -> n * O ≡ O
62 right-mult-zero n = refl
63
64 right-mult-one : (n : Int) -> n * (S O) ≡ n
65 right-mult-one n = refl
66
67 right-mult-distr-one : (n m : Int) -> n * (S m) ≡ n + (n * m)
68 right-mult-distr-one O O = refl
69 right-mult-distr-one O (S m) = refl
70 right-mult-distr-one (S n) O = refl
71 right-mult-distr-one (S n) (S m) = refl
72
73
74 left-mult-zero : (n : Int) -> O * n ≡ O
75 left-mult-zero O = refl
76 left-mult-zero (S n) = begin
77 O * (S n)
78 ≡⟨ right-mult-distr-one O n ⟩
79 O + (O * n)
80 ≡⟨ sum-sym O (O * n) ⟩
81 (O * n) + O
82 ≡⟨ refl ⟩
83 (O * n)
84 ≡⟨ left-mult-zero n ⟩
85 O
86 ∎
87
88 left-mult-one : (n : Int) -> (S O) * n ≡ n
89 left-mult-one O = refl
90 left-mult-one (S n) = begin
91 (S O) * S n
92 ≡⟨ right-mult-distr-one (S O) n ⟩
93 (S O) + ((S O) * n)
94 ≡⟨ cong (_+_ (S O)) (left-mult-one n) ⟩
95 (S O) + n
96 ≡⟨ sum-sym (S O) n ⟩
97 n + (S O)
98 ≡⟨ refl ⟩
99 S n
100 ∎
101
102
103 left-mult-distr-one : (n m : Int) -> (S n) * m ≡ m + (n * m)
104 left-mult-distr-one O O = refl
105 left-mult-distr-one O (S m) = begin
106 (S O) * S m
107 ≡⟨ left-mult-one (S m) ⟩
108 S m
109 ≡⟨ refl ⟩
110 S m + O
111 ≡⟨ cong (_+_ (S m)) (sym (left-mult-zero (S m))) ⟩
112 S m + (O * S m)
113 ∎
114 left-mult-distr-one (S n) O = refl
115 left-mult-distr-one (S n) (S m) = begin
116 S (S n) * S m
117 ≡⟨ right-mult-distr-one (S (S n)) m ⟩
118 (S (S n)) + ((S (S n)) * m)
119 ≡⟨ cong (\x -> (S (S n)) + x) (left-mult-distr-one (S n) m) ⟩
120 S (S n) + (m + S n * m)
121 ≡⟨ {!!} ⟩
122 S m + S n * S m
123 ∎
124
125
126
127 mult-sym : (n m : Int) -> n * m ≡ m * n
128 mult-sym n O = begin
129 n * O
130 ≡⟨ refl ⟩
131 O
132 ≡⟨ sym (left-mult-zero n) ⟩
133 O * n
134 ∎
135 mult-sym n (S m) = begin
136 n * (S m)
137 ≡⟨ right-mult-distr-one n m ⟩
138 n + (n * m)
139 ≡⟨ cong (\x -> n + x ) (mult-sym n m) ⟩
140 n + (m * n)
141 ≡⟨ sym (left-mult-distr-one m n) ⟩
142 (S m) * n
143 ∎