Context Navigation

source: C-semantics/extralib.ma @ 350

Last change on this file since 350 was 181, checked in by campbell, 10 years ago
Sort out some axioms.
File size: 23.9 KB

Line
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	include "datatypes/sums.ma".
16	include "datatypes/list.ma".
17	include "Plogic/equality.ma".
18	include "binary/Z.ma".
19	include "binary/positive.ma".
20
21	nlemma eq_rect_Type0_r:
22	∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
23	#A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ??? p0); nassumption.
24	nqed.
25
26	nlemma eq_rect_r2:
27	∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
28	#A; #a; #x; #p; ncases p; #P; #H; nassumption.
29	nqed.
30
31	nlemma eq_rect_Type2_r:
32	∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
33	#A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
34	nqed.
35
36	nlemma eq_rect_CProp0_r:
37	∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
38	#A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
39	nqed.
40
41	nlemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.
42	#A;#x;#y;*;#H;napply nmk;#H';/2/;
43	nqed.
44
45	(* stolen from logic/connectives.ma to give Prop version. *)
46	notation > "hvbox(a break \liff b)"
47	left associative with precedence 25
48	for @{ 'iff $a $b }.
49
50	notation "hvbox(a break \leftrightarrow b)"
51	left associative with precedence 25
52	for @{ 'iff $a $b }.
53
54	interpretation "logical iff" 'iff x y = (iff x y).
55
56	(* bool *)
57
58	ndefinition xorb : bool → bool → bool ≝
59	λx,y. match x with [ false ⇒ y \| true ⇒ notb y ].
60
61
62	(* TODO: move to Z.ma *)
63
64	nlemma eqZb_z_z : ∀z.eqZb z z = true.
65	#z;ncases z;nnormalize;//;
66	nqed.
67
68	(* XXX: divides goes to arithmetics *)
69	ninductive dividesP (n,m:Pos) : Prop ≝
70	\| witness : ∀p:Pos.m = times n p → dividesP n m.
71	interpretation "positive divides" 'divides n m = (dividesP n m).
72	interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).
73
74	ndefinition dividesZ : Z → Z → Prop ≝
75	λx,y. match x with
76	[ OZ ⇒ False
77	\| pos n ⇒ match y with [ OZ ⇒ True \| pos m ⇒ dividesP n m \| neg m ⇒ dividesP n m ]
78	\| neg n ⇒ match y with [ OZ ⇒ True \| pos m ⇒ dividesP n m \| neg m ⇒ dividesP n m ]
79	].
80
81	interpretation "integer divides" 'divides n m = (dividesZ n m).
82	interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).
83
84	(* should be proved in nat.ma, but it's not! *)
85	nlemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m \| false ⇒ n ≠ m ].
86	#n; nelim n;
87	##[ #m; ncases m; //;
88	##\| #n' IH m; ncases m; ##[ /2/; ##\| #m'; nwhd in match (eqb (S n') (S m')) in ⊢ %;
89	nlapply (IH m'); ncases (eqb n' m'); /2/; ##]
90	##] nqed.
91
92	nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m \| false ⇒ n ≠ m ].
93	#n m; napply eqb_elim; //; nqed.
94
95	nlemma injective_Z_of_nat : injective ? ? Z_of_nat.
96	nnormalize;
97	#n;#m;ncases n;ncases m;nnormalize;//;
98	##[ ##1,2: #n';#H;ndestruct
99	##\| #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0); //
100	##] nqed.
101
102	nlemma reflexive_Zle : reflexive ? Zle.
103	#x; ncases x; //; nqed.
104
105	nlemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
106	#n;ncases n;nnormalize;//;nqed.
107
108	nlemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
109	#x; ncases x; //;
110	#n; ncases n; //; nqed.
111
112	nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
113	#x;#y;
114	napply pos_elim
115	##[ ##2: #n'; #IH; ##]
116	nrewrite > (Zplus_Zsucc_Zpred y ?);
117	##[ nrewrite > (Zpred_Zsucc (pos n'));
118	#H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
119	napply Zsucc_le;
120	##\| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le;
121	##] nqed.
122
123	(* XXX: Zmax must go to arithmetics *)
124	ndefinition Zmax : Z → Z → Z ≝
125	λx,y.match Z_compare x y with
126	[ LT ⇒ y
127	\| _ ⇒ x ].
128
129	nlemma Zmax_l: ∀x,y. x ≤ Zmax x y.
130	#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
131	/3/; ncases x; /3/; nqed.
132
133	nlemma Zmax_r: ∀x,y. y ≤ Zmax x y.
134	#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
135	ncases x; /3/; nqed.
136
137	ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
138	#x y; ncases x;
139	##[ ncases y;
140	##[ ##1,2: //
141	##\| #n; napply False_ind;
142	##]
143	##\| #n; ncases y;
144	##[ nnormalize; napply False_ind;
145	##\| #m; napply (pos_cases … n); /2/;
146	##\| #m; nnormalize; napply False_ind;
147	##]
148	##\| #n; ncases y; /2/;
149	##] nqed.
150
151	ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
152	#n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt;
153	napply (transitive_Zle … Hle); /2/;
154	nqed.
155
156	ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
157	#z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H;
158	##[@;//
159	##\|@2;//##]
160	nqed.
161
162	nlemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
163	#z1;#z2;nlapply (eqZb_to_Prop z1 z2); ncases (eqZb z1 z2); //;
164	#H; #H'; napply False_ind; napply (absurd ? H H');
165	nqed.
166
167	(* Z.ma *)
168
169	ndefinition Zge: Z → Z → Prop ≝
170	λn,m:Z.m ≤ n.
171
172	interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).
173
174	ndefinition Zgt: Z → Z → Prop ≝
175	λn,m:Z.m<n.
176
177	interpretation "integer 'greater than'" 'gt x y = (Zgt x y).
178
179	interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
180
181	nlet rec Zleb (x:Z) (y:Z) : bool ≝
182	match x with
183	[ OZ ⇒
184	match y with
185	[ OZ ⇒ true
186	\| pos m ⇒ true
187	\| neg m ⇒ false ]
188	\| pos n ⇒
189	match y with
190	[ OZ ⇒ false
191	\| pos m ⇒ leb n m
192	\| neg m ⇒ false ]
193	\| neg n ⇒
194	match y with
195	[ OZ ⇒ true
196	\| pos m ⇒ true
197	\| neg m ⇒ leb m n ]].
198
199	nlet rec Zltb (x:Z) (y:Z) : bool ≝
200	match x with
201	[ OZ ⇒
202	match y with
203	[ OZ ⇒ false
204	\| pos m ⇒ true
205	\| neg m ⇒ false ]
206	\| pos n ⇒
207	match y with
208	[ OZ ⇒ false
209	\| pos m ⇒ leb (succ n) m
210	\| neg m ⇒ false ]
211	\| neg n ⇒
212	match y with
213	[ OZ ⇒ true
214	\| pos m ⇒ true
215	\| neg m ⇒ leb (succ m) n ]].
216
217
218
219	ntheorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
220	#n;#m;ncases n;ncases m; //;
221	##[ ##1,2: #m'; nnormalize; #H; napply (False_ind ? H)
222	##\| ##3,5: #n';#m'; nnormalize; napply le_to_leb_true;
223	##\| ##4: #n';#m'; nnormalize; #H; napply (False_ind ? H)
224	##] nqed.
225
226	ntheorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
227	#n;#m;ncases n;ncases m; //;
228	##[ ##1,2: #m'; nnormalize; #H; ndestruct
229	##\| ##3,5: #n';#m'; nnormalize; napply leb_true_to_le;
230	##\| ##4: #n';#m'; nnormalize; #H; ndestruct
231	##] nqed.
232
233	ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
234	#n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct;
235	nqed.
236
237	ntheorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
238	#n;#m;ncases n;ncases m; //;
239	##[ nnormalize; #H; napply (False_ind ? H)
240	##\| ##2,3: #m'; nnormalize; #H; napply (False_ind ? H)
241	##\| ##4,6: #n';#m'; nnormalize; napply le_to_leb_true;
242	##\| #n';#m'; nnormalize; #H; napply (False_ind ? H)
243	##] nqed.
244
245	ntheorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
246	#n;#m;ncases n;ncases m; //;
247	##[ nnormalize; #H; ndestruct
248	##\| ##2,3: #m'; nnormalize; #H; ndestruct
249	##\| ##4,6: #n';#m'; napply leb_true_to_le;
250	##\| #n';#m'; nnormalize; #H; ndestruct
251	##] nqed.
252
253	ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
254	#n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct;
255	nqed.
256
257	ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
258	(n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
259	#n;#m;#P;#Hle;#Hnle;
260	nlapply (refl ? (Zleb n m));
261	nelim (Zleb n m) in ⊢ ((???%)→%);
262	#Hb;
263	##[ napply Hle; napply (Zleb_true_to_Zle … Hb)
264	##\| napply Hnle; napply (Zleb_false_to_not_Zle … Hb)
265	##] nqed.
266
267	ntheorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
268	(n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
269	#n;#m;#P;#Hlt;#Hnlt;
270	nlapply (refl ? (Zltb n m));
271	nelim (Zltb n m) in ⊢ ((???%)→%);
272	#Hb;
273	##[ napply Hlt; napply (Zltb_true_to_Zlt … Hb)
274	##\| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb)
275	##] nqed.
276
277	nlemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
278	#x y; ncases x; ncases y; /2/;
279	#n m; napply (pos_cases … n); napply (pos_cases … m);
280	##[ //;
281	##\| #n'; /2/;
282	##\| #m'; #H; napply False_ind; nnormalize in H; napply (absurd … (not_le_succ_one m')); /2/;
283	##\| #n' m'; #H; nnormalize in H;
284	nrewrite > (Zsucc_neg_succ n'); nrewrite > (Zsucc_neg_succ m'); /2/;
285	##] nqed.
286
287	nlemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
288	#x y; ncases x; ncases y;
289	##[ ##1,2,7,8,9: /2/;
290	##\| ##3,4: #m; nnormalize; *;
291	##\| #m n; napply (pos_cases … n); napply (pos_cases … m);
292	##[ ##1,2: /2/;
293	##\| #n'; nnormalize; #H; napply False_ind; napply (absurd … (not_le_succ_one n')); /2/;
294	##\| #n' m'; nrewrite > (Zpred_pos_succ n'); nrewrite > (Zpred_pos_succ m'); /2/;
295	##]
296	##\| #m n; nnormalize; *;
297	##] nqed.
298
299	nlemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
300	#n; ncases n; //; #n'; #a b H;
301	##[ napply (pos_elim … n');
302	##[ nrewrite < (Zsucc_Zplus_pos_O a); nrewrite < (Zsucc_Zplus_pos_O b); /2/;
303	##\| #n'' H; nrewrite > (?:pos (succ n'') = Zsucc (pos n'')); //;
304	nrewrite > (Zplus_Zsucc …); nrewrite > (Zplus_Zsucc …); /2/;
305	##]
306	##\| napply (pos_elim … n');
307	##[ nrewrite < (Zpred_Zplus_neg_O a); nrewrite < (Zpred_Zplus_neg_O b); /2/;
308	##\| #n'' H; nrewrite > (?:neg (succ n'') = Zpred (neg n'')); //;
309	nrewrite > (Zplus_Zpred …); nrewrite > (Zplus_Zpred …); /2/;
310	##]
311	##] nqed.
312
313	nlemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
314	/2/; nqed.
315
316	nlet rec Z_times (x:Z) (y:Z) : Z ≝
317	match x with
318	[ OZ ⇒ OZ
319	\| pos n ⇒
320	match y with
321	[ OZ ⇒ OZ
322	\| pos m ⇒ pos (n*m)
323	\| neg m ⇒ neg (n*m)
324	]
325	\| neg n ⇒
326	match y with
327	[ OZ ⇒ OZ
328	\| pos m ⇒ neg (n*m)
329	\| neg m ⇒ pos (n*m)
330	]
331	].
332	interpretation "integer multiplication" 'times x y = (Z_times x y).
333
334	(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
335	notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
336	notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
337	interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
338
339	(* datatypes/list.ma *)
340
341	ntheorem nil_append_nil_both:
342	∀A:Type. ∀l1,l2:list A.
343	l1 @ l2 = [] → l1 = [] ∧ l2 = [].
344	#A l1 l2; ncases l1;
345	##[ ncases l2;
346	##[ /2/
347	##\| #h t H; ndestruct;
348	##]
349	##\| ncases l2;
350	##[ nnormalize; #h t H; ndestruct;
351	##\| nnormalize; #h1 t1 h2 h3 H; ndestruct;
352	##]
353	##] nqed.
354
355	(* division *)
356
357	ninductive natp : Type ≝
358	\| pzero : natp
359	\| ppos : Pos → natp.
360
361	ndefinition natp0 ≝
362	λn. match n with [ pzero ⇒ pzero \| ppos m ⇒ ppos (p0 m) ].
363
364	ndefinition natp1 ≝
365	λn. match n with [ pzero ⇒ ppos one \| ppos m ⇒ ppos (p1 m) ].
366
367	nlet rec divide (m,n:Pos) on m ≝
368	match m with
369	[ one ⇒
370	match n with
371	[ one ⇒ 〈ppos one,pzero〉
372	\| _ ⇒ 〈pzero,ppos one〉
373	]
374	\| p0 m' ⇒
375	match divide m' n with
376	[ mk_pair q r ⇒
377	match r with
378	[ pzero ⇒ 〈natp0 q,pzero〉
379	\| ppos r' ⇒
380	match partial_minus (p0 r') n with
381	[ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
382	\| MinusZero ⇒ 〈natp1 q, pzero〉
383	\| MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
384	]
385	]
386	]
387	\| p1 m' ⇒
388	match divide m' n with
389	[ mk_pair q r ⇒
390	match r with
391	[ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 \| _ ⇒ 〈natp0 q,ppos one〉 ]
392	\| ppos r' ⇒
393	match partial_minus (p1 r') n with
394	[ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
395	\| MinusZero ⇒ 〈natp1 q, pzero〉
396	\| MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
397	]
398	]
399	]
400	].
401
402	ndefinition div ≝ λm,n. fst ?? (divide m n).
403	ndefinition mod ≝ λm,n. snd ?? (divide m n).
404
405	ndefinition pairdisc ≝
406	λA,B.λx,y:pair A B.
407	match x with
408	[(mk_pair t0 t1) ⇒
409	match y with
410	[(mk_pair u0 u1) ⇒
411	∀P: Type[1].
412	(∀e0: (eq A (R0 ? t0) u0).
413	∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].
414
415	nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
416	#A;#B;#x;#y;#e;nrewrite > e;ncases y;
417	#a;#b;nnormalize;#P;#PH;napply PH;@;
418	nqed.
419
420	nlemma pred_minus: ∀n,m. pred n - m = pred (n-m).
421	napply pos_elim; /3/;
422	nqed.
423
424	nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
425	napply pos_elim;
426	##[ //
427	##\| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/;
428	##] nqed.
429
430	ntheorem plus_minus_r:
431	∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
432	#m;#n;#p;#le;nrewrite > (symmetric_plus …);
433	nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.
434
435	nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
436	#m;#n;#p;nelim m;/2/; nqed.
437	(*
438	nlemma le_to_minus: ∀m,n. m≤n → m-n = 0.
439	#m;#n;nelim n;
440	##[ nrewrite < (minus_n_O …); /2/;
441	##\| #n'; #IH; #le; ninversion le; /2/; #n''; #A;#B;#C; ndestruct;
442	nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/
443	##] nqed.
444	*)
445	nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → pm-pn = p*(m-n).
446	#n;#m;#p;(nelim (decidable_lt n m);)#lt;
447	(##[) napply (pos_elim … p); //;#p'; #IH;
448	nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);
449	nrewrite > (minus_plus_distrib …);
450	nrewrite < (plus_minus … lt); nrewrite < IH;
451	nrewrite > (plus_minus_r …); /2/;
452	nqed.
453	(*##\|
454	nlapply (not_lt_to_le … lt); #le;
455	napply (pos_elim … p); //; #p';
456	ncut (m-n = one); ##[ /3/ ##]
457	#mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …);
458	#H; nrewrite < H in ⊢ (???%);
459	napply sym_eq; napply le_n_one_to_eq; nrewrite < H;
460	nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;
461	/2/;
462	##] nqed.
463
464	nlemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
465	#m;#n;#H;nlapply (refl ? (m-n));nelim (m-n) in ⊢ (???% → %);//;
466	#H'; nlapply (minus_to_plus … H'); /2/;
467	nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H;
468	napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
469	nqed.
470	*)
471
472	nlet rec natp_plus (n,m:natp) ≝
473	match n with
474	[ pzero ⇒ m
475	\| ppos n' ⇒ match m with [ pzero ⇒ n \| ppos m' ⇒ ppos (n'+m') ]
476	].
477
478	nlet rec natp_times (n,m:natp) ≝
479	match n with
480	[ pzero ⇒ pzero
481	\| ppos n' ⇒ match m with [ pzero ⇒ pzero \| ppos m' ⇒ ppos (n'*m') ]
482	].
483
484	ninductive natp_lt : natp → Pos → Prop ≝
485	\| plt_zero : ∀n. natp_lt pzero n
486	\| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
487
488	nlemma lt_p0: ∀n:Pos. one < p0 n.
489	#n; nnormalize; /2/; nqed.
490
491	nlemma lt_p1: ∀n:Pos. one < p1 n.
492	#n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.
493
494	nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
495	#m; nelim m;
496	##[ //;
497	##\| ##2,3: #m' IH; nnormalize; nrewrite > IH; //;
498	##] nqed.
499
500	nlemma pos_nonzero2: ∀n. ∀P:Pos→Type. ∀Q:Type. match succ n with [ one ⇒ Q \| p0 p ⇒ P (p0 p) \| p1 p ⇒ P (p1 p) ] = P (succ n).
501	#n P Q; napply succ_elim; /2/; nqed.
502
503	nlemma partial_minus_to_Prop: ∀n,m.
504	match partial_minus n m with
505	[ MinusNeg ⇒ n < m
506	\| MinusZero ⇒ n = m
507	\| MinusPos r ⇒ n = m+r
508	].
509	#n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m);
510	nnormalize; ncases (partial_minus n m); /2/; nqed.
511
512	nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
513	#n m lt; nelim lt; /2/;
514	nqed.
515
516	nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
517	#n m lt; napply (transitive_lt ? (p0 m) ?); /2/;
518	nqed.
519
520	nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
521	#n m lt; ninversion lt;
522	##[ #H; nrewrite > (succ_injective … H); //;
523	##\| #p H1 H2 H3;nrewrite > (succ_injective … H3);
524	napply (transitive_lt ? (p0 p) ?); /2/;
525	##]
526	nqed.
527
528	nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
529	#n m lt; nelim lt; /2/;
530	nqed.
531
532
533
534	nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
535	#n m lt;ninversion lt;
536	##[ #p H; ndestruct;
537	##\| #n' m' lt e1 e2; ndestruct; //;
538	##] nqed.
539
540	nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
541	#a b; /2/; nqed.
542
543	nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
544	#a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.
545
546	nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
547	/2/; nqed.
548
549	nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
550	#A B a1 a2 b1 b2 H; ndestruct; //;
551	nqed.
552
553	nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
554	#A B a1 a2 b1 b2 H; ndestruct; //;
555	nqed.
556
557	ntheorem divide_ok : ∀m,n,dv,md.
558	divide m n = 〈dv,md〉 →
559	ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
560	#m n; napply (pos_cases … n);
561	##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/;
562	##\| #n'; nelim m;
563	##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
564	##\| #m' IH dv md; nwhd in ⊢ (??%? → ?(???%)?);
565	nlapply (refl ? (divide m' (succ n')));
566	nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
567	#dv' md' DIVr; nelim (IH … DIVr);
568	nwhd in ⊢ (? → ? → ??%? → ?);
569	ncases md';
570	##[ ncases dv'; nnormalize;
571	##[ #H; ndestruct;
572	##\| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
573	##]
574	##\| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
575	nnormalize; #n md'' Hr1 Hr2;
576	nlapply (plt_lt … Hr2); #Hr2';
577	nlapply (partial_minus_to_Prop md'' n);
578	ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;
579	#lt; #e; ndestruct; @; ##[ /3/; ##\| ##*: /2/; ##] napply plt_pos;
580	##[ ##1,3,5,7: napply double_lt1; /2/;
581	##\| ##2,4: napply double_lt3; /2/;
582	##\| ##*: napply double_lt2; /2/;
583	##]
584	##]
585	##\| #m' IH dv md; nwhd in ⊢ (??%? → ?);
586	nlapply (refl ? (divide m' (succ n')));
587	nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
588	#dv' md' DIVr; nelim (IH … DIVr);
589	nwhd in ⊢ (? → ? → ??%? → ?); ncases md';
590	##[ ncases dv'; nnormalize;
591	##[ #H; ndestruct;
592	##\| #dv'' Hr1 Hr2; #H; ndestruct; /3/;
593	##]
594	##\| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
595	nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2;
596	nlapply (plt_lt … Hr2); #Hr2';
597	nwhd in ⊢ (??%? → ?);
598	nlapply (partial_minus_to_Prop (p0 md'') (succ n'));
599	ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(,6,9,12): #r'' ##]
600	ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize;
601	#Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##]
602	#lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##]
603	nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e);
604	nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos;
605	##[ ncut (succ n' + r'' < p0 (succ n')); /2/;
606	##\| ncut (succ n' + r'' < p0 (succ n')); /2/;
607	##\| /2/;
608	##\| /2/;
609	##]
610	##]
611	##]
612	##] nqed.
613
614	nlemma mod0_divides: ∀m,n,dv:Pos.
615	divide n m = 〈ppos dv,pzero〉 → m∣n.
616	#m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *;
617	nnormalize; #H; ndestruct; //;
618	nqed.
619
620	nlemma divides_mod0: ∀dv,m,n:Pos.
621	n = dv*m → divide n m = 〈ppos dv,pzero〉.
622	#dv;#m;#n;#DIV;nlapply (refl ? (divide n m));
623	nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE;
624	nlapply (divide_ok … DIVIDE); *;
625	ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]
626	ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE; nnormalize;
627	nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct;
628	##[ nlapply (plus_to_minus … e0);
629	nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …);
630	ncut (dv'' < dv); ##[ ncut (dv''m < dvm); /2/; ##] #dvlt;
631	nrewrite > (minus_times_distrib_l …); //;
632
633	(*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
634	#Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind;
635	napply (absurd ? B (lt_to_not_le … A));
636
637	##\| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/;
638
639	##\| nrewrite > DIVIDE; ncut (dv = dv''); /2/;
640	##]
641	nqed.
642
643	nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
644	#m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
645	#dv;#md; ncases md; ncases dv;
646	##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct
647	##\| #dv'; #H; @1; napply mod0_divides; /2/;
648	##\| #md'; #DIVIDES; @2; napply nmk; *; #dv';
649	nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
650	nrewrite > DIVIDES; #H';
651	ndestruct;
652	##\| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv';
653	nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
654	nrewrite > DIVIDES; #H';
655	ndestruct;
656	##] nqed.
657
658	ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
659	#p;#q;ncases p;
660	##[ ncases q; nnormalize; ##[ @2; /2/; ##\| ##*: #m; @2; /2/; ##]
661	##\| ##*: #n; ncases q; nnormalize; /2/;
662	##] nqed.
663
664	ndefinition natp_to_Z ≝
665	λn. match n with [ pzero ⇒ OZ \| ppos p ⇒ pos p ].
666
667	ndefinition natp_to_negZ ≝
668	λn. match n with [ pzero ⇒ OZ \| ppos p ⇒ neg p ].
669
670	(* TODO: check these definitions are right. They are supposed to be the same
671	as Zdiv/Zmod in Coq. *)
672	ndefinition divZ ≝ λx,y.
673	match x with
674	[ OZ ⇒ OZ
675	\| pos n ⇒
676	match y with
677	[ OZ ⇒ OZ
678	\| pos m ⇒ natp_to_Z (fst ?? (divide n m))
679	\| neg m ⇒ match divide n m with [ mk_pair q r ⇒
680	match r with [ pzero ⇒ natp_to_negZ q \| _ ⇒ Zpred (natp_to_negZ q) ] ]
681	]
682	\| neg n ⇒
683	match y with
684	[ OZ ⇒ OZ
685	\| pos m ⇒ match divide n m with [ mk_pair q r ⇒
686	match r with [ pzero ⇒ natp_to_negZ q \| _ ⇒ Zpred (natp_to_negZ q) ] ]
687	\| neg m ⇒ natp_to_Z (fst ?? (divide n m))
688	]
689	].
690
691	ndefinition modZ ≝ λx,y.
692	match x with
693	[ OZ ⇒ OZ
694	\| pos n ⇒
695	match y with
696	[ OZ ⇒ OZ
697	\| pos m ⇒ natp_to_Z (snd ?? (divide n m))
698	\| neg m ⇒ match divide n m with [ mk_pair q r ⇒
699	match r with [ pzero ⇒ OZ \| _ ⇒ y+(natp_to_Z r) ] ]
700	]
701	\| neg n ⇒
702	match y with
703	[ OZ ⇒ OZ
704	\| pos m ⇒ match divide n m with [ mk_pair q r ⇒
705	match r with [ pzero ⇒ OZ \| _ ⇒ y-(natp_to_Z r) ] ]
706	\| neg m ⇒ natp_to_Z (snd ?? (divide n m))
707	]
708	].
709
710	interpretation "natural division" 'divide m n = (div m n).
711	interpretation "natural modulus" 'module m n = (mod m n).
712	interpretation "integer division" 'divide m n = (divZ m n).
713	interpretation "integer modulus" 'module m n = (modZ m n).
714
715	nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
716	#x y; ncases y;
717	##[ #H; napply (False_ind … H);
718	##\| #m; #_; ncases x; //; #n;
719	nwhd in ⊢ (?%?);
720	nlapply (pos_compare_to_Prop n m);
721	ncases (pos_compare n m); /2/;
722	#lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/;
723	##\| #m H; napply (False_ind … H);
724	##] nqed.
725
726	nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
727	#n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);
728	##[ //;
729	##\| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/;
730	##] nqed.
731
732	ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
733	#x y; ncases y;
734	##[ #H; napply (False_ind … H);
735	##\| #m; #_; ncases x;
736	##[ @;//;
737	##\| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
738	ncases (divide n m) in ⊢ (???% → %); #dv md H;
739	nelim (divide_ok … H); #e l; nelim l; /2/;
740	##\| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
741	ncases (divide n m) in ⊢ (???% → %); #dv md H;
742	nelim (divide_ok … H); #e l; nelim l;
743	##[ /2/;
744	##\| #md' m' l'; @;
745	##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
746	nrewrite > (pos_compare_lt … l'); //;
747	##\| napply Zminus_Zlt; //;
748	##]
749	##]
750	##]
751	##\| #m H; napply (False_ind … H);
752	##] nqed.

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format