Context Navigation

source: C-semantics/extralib.ma @ 82

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

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

Download in other formats:

Original Format