Context Navigation

source: C-semantics/extralib.ma @ 11

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

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

Download in other formats:

Original Format