source: Deliverables/D4.1/Matita/Nat.ma @ 231

Last change on this file since 231 was 231, checked in by mulligan, 9 years ago

BitVector? stuff from this morning: need further development of Nat
theory before I can write any interesting functions on BitVectors?.

File size: 4.0 KB
Line 
1include "Cartesian.ma".
2include "Maybe.ma".
3include "Bool.ma".
4
5include "logic/pts.ma".
6include "Plogic/equality.ma".
7
8ninductive Nat: Type[0] ≝
9  Z: Nat
10| S: Nat → Nat.
11
12nlet rec plus (n: Nat) (o: Nat) on n ≝
13  match n with
14    [ Z ⇒ o
15    | S p ⇒ S (plus p o)
16    ].
17   
18notation "n break + m"
19  right associative with precedence 52
20  for @{ 'plus $n $m }.
21 
22interpretation "Nat plus" 'plus n m = (plus n m).
23   
24nlet rec minus (n: Nat) (o: Nat) on n ≝
25  match n with
26    [ Z ⇒ Z
27    | S p ⇒
28      match o with
29        [ Z ⇒ S p
30        | S q ⇒ minus p q
31        ]
32    ].
33   
34notation "n break - m"
35  right associative with precedence 47
36  for @{ 'minus $n $m }.
37 
38interpretation "Nat minus" 'minus n m = (minus n m).
39   
40nlet rec multiplication (n: Nat) (o: Nat) on n ≝
41  match n with
42    [ Z ⇒ Z
43    | S p ⇒ o + (multiplication p o)
44    ].
45   
46notation "n break * m"
47  right associative with precedence 47
48  for @{ 'multiplication $n $m }.
49 
50interpretation "Nat multiplication" 'times n m = (multiplication n m).
51
52nlet rec less_than_or_equal (n: Nat) (m: Nat) ≝
53  match n with
54    [ Z ⇒ True
55    | S o ⇒
56      match m with
57        [ Z ⇒ False
58        | S p ⇒ less_than_or_equal o p
59        ]
60    ].
61   
62notation "n break ≤ m"
63  non associative with precedence 47
64  for @{ 'less_than_or_equal $n $m }.
65 
66interpretation "Nat less than or equal" 'less_than_or_equal n m = (less_than_or_equal n m).
67
68nlemma plus_zero:
69  ∀n: Nat.
70    n + Z = n.
71  #n.
72  nelim n.
73  nnormalize.
74  @.
75  #N H.
76  nnormalize.
77  nrewrite > H.
78  @.
79nqed.
80
81nlemma plus_associative:
82  ∀m, n, o: Nat.
83    (m + n) + o = m + (n + o).
84  #m n o.
85  nelim m.
86  nnormalize.
87  @.
88  #N H.
89  nnormalize.
90  nrewrite > H.
91  @.
92nqed.
93
94nlemma succ_plus:
95  ∀m, n: Nat.
96    S(m + n) = m + S(n).
97  #m n.
98  nelim m.
99  nnormalize.
100  @.
101  #N H.
102  nnormalize.
103  nrewrite > H.
104  @.
105nqed.
106
107nlemma plus_symmetrical:
108  ∀m, n: Nat.
109    m + n = n + m.
110  #m n.
111  nelim m.
112  nnormalize.
113  nelim n.
114  nnormalize.
115  @.
116  #N H.
117  nnormalize.
118  nrewrite < H.
119  @.
120  #N H.
121  nnormalize.
122  nrewrite > H.
123  napplyS succ_plus.
124nqed.
125
126nlemma multiplication_zero_right_neutral:
127  ∀m: Nat.
128    m * Z = Z.
129  #m.
130  nelim m.
131  nnormalize.
132  @.
133  #N H.
134  nnormalize.
135  nrewrite > H.
136  @.
137nqed.
138
139nlemma multiplication_succ:
140  ∀m, n: Nat.
141    m * S(n) = m + (m * n).
142  #m n.
143  nelim m.
144  nnormalize.
145  @.
146  #N H.
147  nnormalize.
148  napplyS plus_symmetrical.
149nqed.
150
151nlemma multiplication_symmetrical:
152  ∀m, n: Nat.
153    m * n = n * m.
154  #m n.
155  nelim m.
156  nnormalize.
157  nelim n.
158  nnormalize.
159  @.
160  #N H.
161  nnormalize.
162  nrewrite < H.
163  @.
164  #N H.
165  nnormalize.
166  nrewrite > H.
167  napplyS multiplication_succ.
168nqed.
169
170nlemma multiplication_succ_zero_left_neutral:
171  ∀m: Nat.
172    (S Z) * m = m.
173  #m.
174  nelim m.
175  nnormalize.
176  @.
177  #N H.
178  nnormalize.
179  napplyS succ_plus.
180nqed.
181
182nlemma multiplication_succ_zero_right_neutral:
183  ∀m: Nat.
184    m * (S Z) = m.
185  #m.
186  nelim m.
187  nnormalize.
188  @.
189  #N H.
190  nnormalize.
191  nrewrite > H.
192  @.
193nqed.
194
195nlemma multiplication_distributes_right_plus:
196  ∀m, n, o: Nat.
197    (m + n) * o = m * o + n * o.
198  #m n o.
199  nelim m.
200  nnormalize.
201  @.
202  #N H.
203  nnormalize.
204  nrewrite > H.
205  napplyS plus_associative.
206nqed.
207
208nlemma multiplication_distributes_left_plus:
209  ∀m, n, o: Nat.
210    o * (m + n) = o * m + o * n.
211  #m n o.
212  napplyS multiplication_symmetrical.
213nqed.
214
215nlemma mutliplication_associative:
216  ∀m, n, o: Nat.
217    m * (n * o) = (m * n) * o.
218  #m n o.
219  nelim m.
220  nnormalize.
221  @.
222  #N H.
223  nnormalize.
224  nrewrite > H.
225  napplyS multiplication_distributes_right_plus.
226nqed.
227
228nlemma minus_minus:
229  ∀n: Nat.
230    n - n = Z.
231  #n.
232  nelim n.
233  nnormalize.
234  @.
235  #N H.
236  nnormalize.
237  nrewrite > H.
238  @.
239nqed.
240
241(*
242nlemma succ_injective:
243  ∀m, n: Nat.
244    S m = S n → m = n.
245  #m n.
246  nelim m.
247  #H.
248  ninversion H.
249  #H.
250  ndestruct
251
252nlemma plus_minus_associate:
253  ∀m, n, o: Nat.
254    (m + n) - o = m + (n - o).
255  #m n o.
256  nelim m.
257  nnormalize.
258  @.
259  #N H.
260 
261
262nlemma plus_minus_inverses:
263  ∀m, n: Nat.
264    (m + n) - n = m.
265  #m n.
266  nelim m.
267  nnormalize.
268  napply minus_minus.
269  #N H.
270*)
Note: See TracBrowser for help on using the repository browser.