]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly2/common/nat.ma
a wrong conjecture bypassed!
[helm.git] / matita / matita / contribs / ng_assembly2 / common / nat.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "common/comp.ma".
24 include "num/bool_lemmas.ma".
25
26 (* ******** *)
27 (* NATURALI *)
28 (* ******** *)
29
30 ninductive nat : Type ≝
31   O : nat
32 | S : nat → nat.
33
34 (*
35 interpretation "Natural numbers" 'N = nat.
36
37 default "natural numbers" cic:/matita/common/nat/nat.ind.
38
39 alias num (instance 0) = "natural number".
40 *)
41
42 nlet rec nat_it (T:Type) (f:T → T) (arg:T) (n:nat) on n ≝
43  match n with
44   [ O ⇒ arg
45   | S n' ⇒ nat_it T f (f arg) n'
46   ].
47
48 ndefinition nat1 ≝ S O.
49 ndefinition nat2 ≝ S nat1.
50 ndefinition nat3 ≝ S nat2.
51 ndefinition nat4 ≝ S nat3.
52 ndefinition nat5 ≝ S nat4.
53 ndefinition nat6 ≝ S nat5.
54 ndefinition nat7 ≝ S nat6.
55 ndefinition nat8 ≝ S nat7.
56 ndefinition nat9 ≝ S nat8.
57 ndefinition nat10 ≝ S nat9.
58 ndefinition nat11 ≝ S nat10.
59 ndefinition nat12 ≝ S nat11.
60 ndefinition nat13 ≝ S nat12.
61 ndefinition nat14 ≝ S nat13.
62 ndefinition nat15 ≝ S nat14.
63 ndefinition nat16 ≝ S nat15.
64 ndefinition nat17 ≝ S nat16.
65 ndefinition nat18 ≝ S nat17.
66 ndefinition nat19 ≝ S nat18.
67 ndefinition nat20 ≝ S nat19.
68 ndefinition nat21 ≝ S nat20.
69 ndefinition nat22 ≝ S nat21.
70 ndefinition nat23 ≝ S nat22.
71 ndefinition nat24 ≝ S nat23.
72 ndefinition nat25 ≝ S nat24.
73 ndefinition nat26 ≝ S nat25.
74 ndefinition nat27 ≝ S nat26.
75 ndefinition nat28 ≝ S nat27.
76 ndefinition nat29 ≝ S nat28.
77 ndefinition nat30 ≝ S nat29.
78 ndefinition nat31 ≝ S nat30.
79 ndefinition nat32 ≝ S nat31.
80 ndefinition nat33 ≝ S nat32.
81 ndefinition nat34 ≝ S nat33.
82 ndefinition nat35 ≝ S nat34.
83 ndefinition nat36 ≝ S nat35.
84 ndefinition nat37 ≝ S nat36.
85 ndefinition nat38 ≝ S nat37.
86 ndefinition nat39 ≝ S nat38.
87 ndefinition nat40 ≝ S nat39.
88 ndefinition nat41 ≝ S nat40.
89 ndefinition nat42 ≝ S nat41.
90 ndefinition nat43 ≝ S nat42.
91 ndefinition nat44 ≝ S nat43.
92 ndefinition nat45 ≝ S nat44.
93 ndefinition nat46 ≝ S nat45.
94 ndefinition nat47 ≝ S nat46.
95 ndefinition nat48 ≝ S nat47.
96 ndefinition nat49 ≝ S nat48.
97 ndefinition nat50 ≝ S nat49.
98 ndefinition nat51 ≝ S nat50.
99 ndefinition nat52 ≝ S nat51.
100 ndefinition nat53 ≝ S nat52.
101 ndefinition nat54 ≝ S nat53.
102 ndefinition nat55 ≝ S nat54.
103 ndefinition nat56 ≝ S nat55.
104 ndefinition nat57 ≝ S nat56.
105 ndefinition nat58 ≝ S nat57.
106 ndefinition nat59 ≝ S nat58.
107 ndefinition nat60 ≝ S nat59.
108 ndefinition nat61 ≝ S nat60.
109 ndefinition nat62 ≝ S nat61.
110 ndefinition nat63 ≝ S nat62.
111 ndefinition nat64 ≝ S nat63.
112 ndefinition nat65 ≝ S nat64.
113 ndefinition nat66 ≝ S nat65.
114 ndefinition nat67 ≝ S nat66.
115 ndefinition nat68 ≝ S nat67.
116 ndefinition nat69 ≝ S nat68.
117 ndefinition nat70 ≝ S nat69.
118 ndefinition nat71 ≝ S nat70.
119 ndefinition nat72 ≝ S nat71.
120 ndefinition nat73 ≝ S nat72.
121 ndefinition nat74 ≝ S nat73.
122 ndefinition nat75 ≝ S nat74.
123 ndefinition nat76 ≝ S nat75.
124 ndefinition nat77 ≝ S nat76.
125 ndefinition nat78 ≝ S nat77.
126 ndefinition nat79 ≝ S nat78.
127 ndefinition nat80 ≝ S nat79.
128 ndefinition nat81 ≝ S nat80.
129 ndefinition nat82 ≝ S nat81.
130 ndefinition nat83 ≝ S nat82.
131 ndefinition nat84 ≝ S nat83.
132 ndefinition nat85 ≝ S nat84.
133 ndefinition nat86 ≝ S nat85.
134 ndefinition nat87 ≝ S nat86.
135 ndefinition nat88 ≝ S nat87.
136 ndefinition nat89 ≝ S nat88.
137 ndefinition nat90 ≝ S nat89.
138 ndefinition nat91 ≝ S nat90.
139 ndefinition nat92 ≝ S nat91.
140 ndefinition nat93 ≝ S nat92.
141 ndefinition nat94 ≝ S nat93.
142 ndefinition nat95 ≝ S nat94.
143 ndefinition nat96 ≝ S nat95.
144 ndefinition nat97 ≝ S nat96.
145 ndefinition nat98 ≝ S nat97.
146 ndefinition nat99 ≝ S nat98.
147 ndefinition nat100 ≝ S nat99.
148
149 nlet rec eq_nat (n1,n2:nat) on n1 ≝
150  match n1 with
151   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
152   | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
153   ].
154
155 nlet rec le_nat n m ≝ 
156  match n with 
157   [ O ⇒ true
158   | (S p) ⇒ match m with 
159    [ O ⇒ false | (S q) ⇒ le_nat p q ]
160   ].
161
162 interpretation "natural 'less or equal to'" 'leq x y = (le_nat x y).
163
164 ndefinition lt_nat ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
165
166 interpretation "natural 'less than'" 'lt x y = (lt_nat x y).
167
168 ndefinition ge_nat ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
169
170 interpretation "natural 'greater or equal to'" 'geq x y = (ge_nat x y).
171
172 ndefinition gt_nat ≝ λn1,n2:nat.⊖ (le_nat n1 n2).
173
174 interpretation "natural 'greater than'" 'gt x y = (gt_nat x y).
175
176 nlet rec plus (n1,n2:nat) on n1 ≝ 
177  match n1 with
178   [ O ⇒ n2
179   | (S n1') ⇒ S (plus n1' n2) ].
180
181 interpretation "natural plus" 'plus x y = (plus x y).
182
183 nlet rec times (n1,n2:nat) on n1 ≝ 
184  match n1 with 
185   [ O ⇒ O
186   | (S n1') ⇒ n2 + (times n1' n2) ].
187
188 interpretation "natural times" 'times x y = (times x y).
189
190 nlet rec minus n m ≝ 
191  match n with 
192  [ O ⇒ O
193  | (S p) ⇒ 
194         match m with
195         [O ⇒ (S p)
196   | (S q) ⇒ minus p q ]].
197
198 interpretation "natural minus" 'minus x y = (minus x y).
199
200 nlet rec div_aux p m n : nat ≝
201 match (le_nat m n) with
202 [ true ⇒ O
203 | false ⇒
204   match p with
205   [ O ⇒ O
206   | (S q) ⇒ S (div_aux q (m-(S n)) n)]].
207
208 ndefinition div : nat → nat → nat ≝
209 λn,m.match m with 
210  [ O ⇒ S n
211  | (S p) ⇒ div_aux n n p]. 
212
213 interpretation "natural divide" 'divide x y = (div x y).
214
215 ndefinition pred ≝ λn.match n with [ O ⇒ O | S n ⇒ n ].
216
217 ndefinition nat128 ≝ nat64 + nat64.
218 ndefinition nat256 ≝ nat128 + nat128.
219 ndefinition nat512 ≝ nat256 + nat256.
220 ndefinition nat1024 ≝ nat512 + nat512.
221 ndefinition nat2048 ≝ nat1024 + nat1024.
222 ndefinition nat4096 ≝ nat2048 + nat2048.
223 ndefinition nat8192 ≝ nat4096 + nat4096.
224 ndefinition nat16384 ≝ nat8192 + nat8192.
225 ndefinition nat32768 ≝ nat16384 + nat16384.
226 ndefinition nat65536 ≝ nat32768 + nat32768.
227
228 nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
229  #n1; #n2; #H;
230  nchange with (match S n2 with [ O ⇒ False | S a ⇒ n1 = a ]);
231  nrewrite < H;
232  nnormalize;
233  napply refl_eq.
234 nqed.
235
236 nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
237  #n; #H;
238  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
239  nrewrite < H;
240  nnormalize;
241  napply I.
242 nqed.
243
244 nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
245  #n; #H;
246  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
247  nrewrite > H;
248  nnormalize;
249  napply I.
250 nqed.
251
252 nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
253  #n1;
254  nelim n1;
255  ##[ ##1: #n2;
256           nelim n2;
257           nnormalize;
258           ##[ ##1: #H; napply refl_eq
259           ##| ##2: #n3; #H; #H1; ndestruct (*nelim (nat_destruct_0_S ? H1)*)
260           ##]
261  ##| ##2: #n2; #H; #n3; #H1;
262           ncases n3 in H1:(%) ⊢ %;
263           nnormalize;
264           ##[ ##1: #H1; ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
265           ##| ##2: #n4; #H1;
266                    napply (H n4 (nat_destruct_S_S … H1))
267           ##]
268  ##]
269 nqed.
270
271 nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2).
272  #n1; #n2; #H;
273  napply (not_to_not (n1 = n2) (eq_nat n1 n2 = true) …);
274  ##[ ##1: napply (eq_to_eqnat n1 n2)
275  ##| ##2: napply (eqfalse_to_neqtrue … H)
276  ##]
277 nqed.
278
279 nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
280  #n1;
281  nelim n1;
282  ##[ ##1: #n2;
283           nelim n2;
284           nnormalize;
285           ##[ ##1: #H; napply refl_eq
286           ##| ##2: #n3; #H; #H1; ndestruct (*napply (bool_destruct … (O = S n3) H1)*)
287           ##]
288  ##| ##2: #n2; #H; #n3; #H1;
289           ncases n3 in H1:(%) ⊢ %;
290           nnormalize;
291           ##[ ##1: #H1; ndestruct (*napply (bool_destruct … (S n2 = O) H1)*)
292           ##| ##2: #n4; #H1;
293                    nrewrite > (H n4 H1);
294                    napply refl_eq
295           ##]
296  ##]
297 nqed.
298
299 nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false.
300  #n1; #n2; #H;
301  napply (neqtrue_to_eqfalse (eq_nat n1 n2));
302  napply (not_to_not (eq_nat n1 n2 = true) (n1 = n2) ? H);
303  napply (eqnat_to_eq n1 n2).
304 nqed.
305
306 nlemma decidable_nat : ∀x,y:nat.decidable (x = y).
307  #x; #y; nnormalize;
308  napply (or2_elim (eq_nat x y = true) (eq_nat x y = false) ? (decidable_bexpr ?));
309  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqnat_to_eq … H))
310  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqnat_to_neq … H))
311  ##]
312 nqed.
313
314 nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
315  #n1; #n2;
316  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2));
317  ##[ ##1: #H; nrewrite > H; napply refl_eq
318  ##| ##2: #H; nrewrite > (neq_to_neqnat n1 n2 H);
319           napply (symmetric_eq ? (eq_nat n2 n1) false);
320           napply (neq_to_neqnat n2 n1 (symmetric_neq ? n1 n2 H))
321  ##]
322 nqed.
323
324 nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
325  #n1;
326  nelim n1;
327  ##[ ##1: nnormalize; #n2; napply refl_eq
328  ##| ##2: #n; #H; #n2; nrewrite > (H n2);
329           ncases n in H:(%) ⊢ %;
330           ##[ ##1: nnormalize; #H; napply refl_eq
331           ##| ##2: #n3; nnormalize; #H; napply refl_eq
332           ##]
333  ##]
334 nqed.
335
336 nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2).
337  #n1;
338  nelim n1;
339  ##[ ##1: nnormalize; #n2; napply refl_eq
340  ##| ##2: #n; #H; #n2;
341           nrewrite > (Sn_p_n_to_S_npn n (S n2));
342           nrewrite > (H n2);
343           napply refl_eq
344  ##]
345 nqed.
346
347 nlemma Opn_to_n : ∀n.O + n = n.
348  #n; nnormalize; napply refl_eq.
349 nqed.
350
351 nlemma npO_to_n : ∀n.n + O = n.
352  #n;
353  nelim n;
354  ##[ ##1: nnormalize; napply refl_eq
355  ##| ##2: #n1; #H;
356           nrewrite > (Sn_p_n_to_S_npn n1 O); 
357           nrewrite > H;
358           napply refl_eq
359  ##]
360 nqed.
361
362 nlemma symmetric_plusnat : symmetricT nat nat plus.
363  #n1;
364  nelim n1;
365  ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply refl_eq
366  ##| ##2: #n2; #H; #n3;
367           nrewrite > (Sn_p_n_to_S_npn n2 n3);
368           nrewrite > (n_p_Sn_to_S_npn n3 n2);
369           nrewrite > (H n3);
370           napply refl_eq
371  ##]
372 nqed.
373
374 nlemma nat_is_comparable : comparable.
375  napply (mk_comparable nat);
376  ##[ napply O
377  ##| napply (λx.false)
378  ##| napply eq_nat
379  ##| napply eqnat_to_eq
380  ##| napply eq_to_eqnat
381  ##| napply neqnat_to_neq
382  ##| napply neq_to_neqnat
383  ##| napply decidable_nat
384  ##| napply symmetric_eqnat
385  ##]
386 nqed.
387
388 unification hint 0 ≔ ⊢ carr nat_is_comparable ≡ nat.