Mercurial > hg > Members > atton > agda-proofs
comparison systemT/int.agda @ 1:fe247f476ecb
Migrate systemT from atton/agda/systemT (13:5a81867278af)
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 02 Nov 2014 09:40:54 +0900 |
parents | |
children |
comparison
equal
deleted
inserted
replaced
0:8a5f4ebdd34d | 1:fe247f476ecb |
---|---|
1 open import systemT | |
2 open import Relation.Binary.PropositionalEquality | |
3 open ≡-Reasoning | |
4 | |
5 module int where | |
6 | |
7 double : Int -> Int | |
8 double O = O | |
9 double (S n) = S (S (double n)) | |
10 | |
11 | |
12 infixl 30 _+_ | |
13 _+_ : Int -> Int -> Int | |
14 n + O = n | |
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 | |
21 left-add-one : (n : Int) -> (S n) ≡ S O + n | |
22 left-add-one O = refl | |
23 left-add-one (S n) = cong S (left-add-one n) | |
24 | |
25 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m) | |
26 left-increment n O = refl | |
27 left-increment n (S m) = cong S (left-increment n m) | |
28 | |
29 sum-sym : (x : Int) (y : Int) -> x + y ≡ y + x | |
30 sum-sym O O = refl | |
31 sum-sym O (S y) = cong S (sum-sym O y) | |
32 sum-sym (S x) O = cong S (sum-sym x O) | |
33 sum-sym (S x) (S y) = begin | |
34 (S x) + (S y) | |
35 ≡⟨ refl ⟩ | |
36 S ((S x) + y) | |
37 ≡⟨ cong S (sum-sym (S x) y) ⟩ | |
38 S (y + (S x)) | |
39 ≡⟨ (sym (left-increment y (S x))) ⟩ | |
40 (S y) + (S x) | |
41 ∎ | |
42 | |
43 sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z | |
44 sum-assoc O O O = refl | |
45 sum-assoc O O (S z) = cong S (sum-assoc O O z) | |
46 sum-assoc O (S y) O = refl | |
47 sum-assoc O (S y) (S z) = cong S (sum-assoc O (S y) z) | |
48 sum-assoc (S x) O O = refl | |
49 sum-assoc (S x) O (S z) = cong S (sum-assoc (S x) O z) | |
50 sum-assoc (S x) (S y) O = refl | |
51 sum-assoc (S x) (S y) (S z) = cong S (sum-assoc (S x) (S y) z) | |
52 | |
53 | |
54 infixl 40 _*_ | |
55 _*_ : Int -> Int -> Int | |
56 n * O = O | |
57 n * (S O) = n | |
58 n * (S m) = n + (n * m) | |
59 | |
60 right-mult-zero : (n : Int) -> n * O ≡ O | |
61 right-mult-zero n = refl | |
62 | |
63 right-mult-one : (n : Int) -> n * (S O) ≡ n | |
64 right-mult-one n = refl | |
65 | |
66 right-mult-distr-one : (n m : Int) -> n * (S m) ≡ n + (n * m) | |
67 right-mult-distr-one O O = refl | |
68 right-mult-distr-one O (S m) = refl | |
69 right-mult-distr-one (S n) O = refl | |
70 right-mult-distr-one (S n) (S m) = refl | |
71 | |
72 | |
73 left-mult-zero : (n : Int) -> O * n ≡ O | |
74 left-mult-zero O = refl | |
75 left-mult-zero (S n) = begin | |
76 O * (S n) | |
77 ≡⟨ right-mult-distr-one O n ⟩ | |
78 O + (O * n) | |
79 ≡⟨ sum-sym O (O * n) ⟩ | |
80 (O * n) + O | |
81 ≡⟨ refl ⟩ | |
82 (O * n) | |
83 ≡⟨ left-mult-zero n ⟩ | |
84 O | |
85 ∎ | |
86 | |
87 left-mult-one : (n : Int) -> (S O) * n ≡ n | |
88 left-mult-one O = refl | |
89 left-mult-one (S n) = begin | |
90 (S O) * S n | |
91 ≡⟨ right-mult-distr-one (S O) n ⟩ | |
92 (S O) + ((S O) * n) | |
93 ≡⟨ cong (_+_ (S O)) (left-mult-one n) ⟩ | |
94 (S O) + n | |
95 ≡⟨ sum-sym (S O) n ⟩ | |
96 n + (S O) | |
97 ≡⟨ refl ⟩ | |
98 S n | |
99 ∎ | |
100 | |
101 | |
102 left-mult-distr-one : (n m : Int) -> (S n) * m ≡ m + (n * m) | |
103 left-mult-distr-one O O = refl | |
104 left-mult-distr-one O (S m) = begin | |
105 (S O) * S m | |
106 ≡⟨ left-mult-one (S m) ⟩ | |
107 S m | |
108 ≡⟨ refl ⟩ | |
109 S m + O | |
110 ≡⟨ cong (_+_ (S m)) (sym (left-mult-zero (S m))) ⟩ | |
111 S m + (O * S m) | |
112 ∎ | |
113 left-mult-distr-one (S n) O = refl | |
114 left-mult-distr-one (S n) (S m) = begin | |
115 S (S n) * S m | |
116 ≡⟨ right-mult-distr-one (S (S n)) m ⟩ | |
117 (S (S n)) + ((S (S n)) * m) | |
118 ≡⟨ cong (\x -> (S (S n)) + x) (left-mult-distr-one (S n) m) ⟩ | |
119 S (S n) + (m + S n * m) | |
120 ≡⟨ cong (\x -> x + (m + S n * m)) (left-add-one (S n)) ⟩ | |
121 (S O) + (S n) + (m + S n * m) | |
122 ≡⟨ sum-assoc ((S O) + (S n)) m (S n * m) ⟩ | |
123 (S O) + (S n) + m + S n * m | |
124 ≡⟨ cong (\x -> x + m + S n * m) (sum-sym (S O) (S n)) ⟩ | |
125 ((((S n) + (S O)) + m) + S n * m) | |
126 ≡⟨ cong (\x -> x + (S n * m)) (sym (sum-assoc (S n) (S O) m))⟩ | |
127 (((S n) + ((S O) + m)) + S n * m) | |
128 ≡⟨ cong (\x -> (S n + x + S n * m)) (sym (left-add-one m)) ⟩ | |
129 ((S n) + (S m) + S n * m) | |
130 ≡⟨ cong (\x -> x + (S n * m)) (sum-sym (S n) (S m)) ⟩ | |
131 (S m) + (S n) + (S n * m) | |
132 ≡⟨ sym (sum-assoc (S m) (S n) (S n * m)) ⟩ | |
133 (S m) + ((S n) + ((S n) * m)) | |
134 ≡⟨ cong (\x -> (S m) + x ) (sym (right-mult-distr-one (S n) m )) ⟩ | |
135 S m + S n * S m | |
136 ∎ | |
137 | |
138 | |
139 mult-sym : (n m : Int) -> n * m ≡ m * n | |
140 mult-sym n O = begin | |
141 n * O | |
142 ≡⟨ refl ⟩ | |
143 O | |
144 ≡⟨ sym (left-mult-zero n) ⟩ | |
145 O * n | |
146 ∎ | |
147 mult-sym n (S m) = begin | |
148 n * (S m) | |
149 ≡⟨ right-mult-distr-one n m ⟩ | |
150 n + (n * m) | |
151 ≡⟨ cong (\x -> n + x ) (mult-sym n m) ⟩ | |
152 n + (m * n) | |
153 ≡⟨ sym (left-mult-distr-one m n) ⟩ | |
154 (S m) * n | |
155 ∎ |