source: C-semantics/extralib.ma @ 3

Last change on this file since 3 was 3, checked in by campbell, 10 years ago

Import work-in-progress port of the CompCert? C semantics to matita.

File size: 15.0 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
15include "arithmetics/Z.ma".
16include "datatypes/sums.ma".
17include "datatypes/list.ma".
18include "Plogic/equality.ma".
19
20nlemma eq_rect_Type0_r:
21 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
22 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ??? p0); nassumption.
23nqed.
24
25nlemma eq_rect_r2:
26 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
27 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
28nqed.
29
30nlemma eq_rect_Type2_r:
31 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
32 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
33nqed.
34
35nlemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.
36#A;#x;#y;*;#H;napply nmk;#H';/2/;
37nqed.
38
39(* stolen from logic/connectives.ma to give Prop version. *)
40notation > "hvbox(a break \liff b)"
41  left associative with precedence 25
42for @{ 'iff $a $b }.
43
44notation "hvbox(a break \leftrightarrow b)"
45  left associative with precedence 25
46for @{ 'iff $a $b }.
47
48interpretation "logical iff" 'iff x y = (iff x y).
49
50(* bool *)
51
52ndefinition xorb : bool → bool → bool ≝
53  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
54 
55
56(* TODO: move to Z.ma *)
57
58nlemma eqZb_z_z : ∀z.eqZb z z = true.
59#z;ncases z;nnormalize;//;
60nqed.
61
62(* XXX: divides goes to arithmetics *)
63ninductive divides (n,m:nat) : Prop ≝
64| witness : ∀p:nat.m = times n p → divides n m.
65interpretation "divides" 'divides n m = (divides n m).
66interpretation "not divides" 'ndivides n m = (Not (divides n m)).
67
68ndefinition dividesZ ≝ λx,y:Z. abs x ∣ abs y.
69interpretation "integer divides" 'divides n m = (dividesZ n m).
70interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).
71
72(* should be proved in nat.ma, but it's not! *)
73naxiom eqb_to_Prop : ∀n,m.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
74
75nlemma injective_Z_of_nat : injective ? ? Z_of_nat.
76nnormalize;
77#n;#m;ncases n;ncases m;nnormalize;//;
78##[ ##1,2: #n';#H;ndestruct
79##| #n';#m'; #H; ndestruct; //
80##] nqed.
81
82nlemma reflexive_Zle : reflexive ? Zle.
83#x; ncases x; //; nqed.
84
85nlemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
86#n;ncases n;nnormalize;//;nqed.
87
88nlemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
89#x; ncases x; //;
90#n; ncases n; //; nqed.
91
92nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
93#x;#y;
94#n;
95nelim n; ##[ ##2: #n'; #IH; ##]
96nrewrite > (Zplus_Zsucc_Zpred y ?);
97nwhd in ⊢ (?→??(??%));
98##[ #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
99    napply Zsucc_le;
100##| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le;
101##] nqed.
102
103(* XXX: Zmax must go to arithmetics *)
104ndefinition Zmax : Z → Z → Z ≝
105  λx,y.match Z_compare x y with
106  [ LT ⇒ y
107  | _ ⇒ x ].
108
109nlemma Zmax_l: ∀x,y. x ≤ Zmax x y.
110#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
111/3/; nqed.
112
113nlemma Zmax_r: ∀x,y. y ≤ Zmax x y.
114#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
115/3/; #H; nrewrite > H; //; nqed.
116
117ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
118#n;#m;#p; nlapply (Z_compare_to_Prop n p); nelim (Z_compare n p);
119##[ //;
120##| #H; nrewrite > H; #A;#B; napply False_ind; nlapply (Zlt_to_Zle … A);
121    #C; nlapply (transitive_Zle … C B); nelim p; /2/; #n';nelim n'; /2/;
122##| #A; #B; #C; nlapply (transitive_Zlt … A B); #D;
123    napply False_ind; nlapply (Zlt_to_Zle … D);
124    #E; nlapply (transitive_Zle … E C); nelim p; /2/; #n';nelim n'; /2/;
125##] nqed.
126
127nlemma decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
128#z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H;
129##[@;//
130##|@2;//##]
131nqed.
132
133nlemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
134#z1;#z2;nlapply (eqZb_to_Prop z1 z2); ncases (eqZb z1 z2); //;
135#H; #H'; napply False_ind; napply (absurd ? H H');
136nqed.
137
138(* Z.ma *)
139
140ndefinition Zge: Z → Z → Prop ≝
141λn,m:Z.m ≤ n.
142
143interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).
144
145ndefinition Zgt: Z → Z → Prop ≝
146λn,m:Z.m<n.
147
148interpretation "integer 'greater than'" 'gt x y = (Zgt x y).
149
150interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
151
152ndefinition Zleb : Z → Z → bool ≝
153λx,y:Z.
154  match x with
155  [ OZ ⇒
156    match y with
157    [ OZ ⇒ true
158    | pos m ⇒ true
159    | neg m ⇒ false ]
160  | pos n ⇒
161    match y with
162    [ OZ ⇒ false
163    | pos m ⇒ leb n m
164    | neg m ⇒ false ]
165  | neg n ⇒
166    match y with
167    [ OZ ⇒ true
168    | pos m ⇒ true
169    | neg m ⇒ leb m n ]].
170   
171ndefinition Zltb : Z → Z → bool ≝
172λx,y:Z.
173  match x with
174  [ OZ ⇒
175    match y with
176    [ OZ ⇒ false
177    | pos m ⇒ true
178    | neg m ⇒ false ]
179  | pos n ⇒
180    match y with
181    [ OZ ⇒ false
182    | pos m ⇒ leb (S n) m
183    | neg m ⇒ false ]
184  | neg n ⇒
185    match y with
186    [ OZ ⇒ true
187    | pos m ⇒ true
188    | neg m ⇒ leb (S m) n ]].
189
190
191
192ntheorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
193#n;#m;ncases n;ncases m; //;
194##[ ##1,2: #m'; nnormalize; #H; napply (False_ind ? H)
195##| ##3,5: #n';#m'; nnormalize; napply le_to_leb_true;
196##| ##4: #n';#m'; nnormalize; #H; napply (False_ind ? H)
197##] nqed.
198
199ntheorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
200#n;#m;ncases n;ncases m; //;
201##[ ##1,2: #m'; nnormalize; #H; ndestruct
202##| ##3,5: #n';#m'; nnormalize; napply leb_true_to_le;
203##| ##4: #n';#m'; nnormalize; #H; ndestruct
204##] nqed.
205
206ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
207#n;#m;ncases n;ncases m; nnormalize; /2/;
208nqed.
209
210ntheorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
211#n;#m;ncases n;ncases m; //;
212##[ nnormalize; #H; napply (False_ind ? H)
213##| ##2,3: #m'; nnormalize; #H; napply (False_ind ? H)
214##| ##4,6: #n';#m'; nnormalize; napply le_to_leb_true;
215##| #n';#m'; nnormalize; #H; napply (False_ind ? H)
216##] nqed.
217
218ntheorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
219#n;#m;ncases n;ncases m; //;
220##[ nnormalize; #H; ndestruct
221##| ##2,3: #m'; nnormalize; #H; ndestruct
222##| ##4,6: #n';#m'; napply leb_true_to_le;
223##| #n';#m'; nnormalize; #H; ndestruct
224##] nqed.
225
226ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
227#n;#m;ncases n;ncases m; nnormalize; /2/;
228##[ #n';#m';ncases n';nnormalize;
229  ##[ ##2: #n';#H; napply not_le_to_not_le_S_S; napply leb_false_to_not_le; ##]
230  //;
231##| #n';#m';ncases m';nnormalize;
232  ##[ ##2: #m';#H; napply not_le_to_not_le_S_S; napply leb_false_to_not_le; ##]
233  //;
234##] nqed.
235
236ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
237(n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
238#n;#m;#P;#Hle;#Hnle;
239nlapply (refl ? (Zleb n m));
240nelim (Zleb n m) in ⊢ ((???%)→%);
241#Hb;
242##[ napply Hle; napply (Zleb_true_to_Zle … Hb)
243##| napply Hnle; napply (Zleb_false_to_not_Zle … Hb)
244##] nqed.
245
246ntheorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
247(n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
248#n;#m;#P;#Hlt;#Hnlt;
249nlapply (refl ? (Zltb n m));
250nelim (Zltb n m) in ⊢ ((???%)→%);
251#Hb;
252##[ napply Hlt; napply (Zltb_true_to_Zlt … Hb)
253##| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb)
254##] nqed.
255
256naxiom Z_times : Z → Z → Z.
257interpretation "integer multiplication" 'times x y = (Z_times x y).
258
259(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
260notation > "'if' term 19 e 'then' term 19 t 'else' term 68 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
261notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 68 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
262interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
263
264(* datatypes/list.ma *)
265
266ntheorem nil_append_nil_both:
267  ∀A:Type. ∀l1,l2:list A.
268    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
269#A l1 l2; ncases l1;
270##[ ncases l2;
271  ##[ /2/
272  ##| #h t H; ndestruct;
273  ##]
274##| ncases l2;
275  ##[ nnormalize; #h t H; ndestruct;
276  ##| nnormalize; #h1 t1 h2 h3 H; ndestruct;
277  ##]
278##] nqed.
279
280(* division *)
281
282nlet rec divide_aux (b,m,n,p:nat) on b ≝
283  if leb (S m) n then 〈p,m〉 else
284  match b with
285  [ O ⇒ 〈p,m〉
286  | S b' ⇒ divide_aux b' (m-n) n (S p)
287  ].
288
289ndefinition divide ≝ λm,n. divide_aux m m n O.
290ndefinition div ≝ λm,n. fst ?? (divide m n).
291ndefinition mod ≝ λm,n. snd ?? (divide m n).
292
293ndefinition pairdisc ≝
294λA,B.λx,y:pair A B.
295match x with
296[(mk_pair t0 t1) ⇒
297match y with
298[(mk_pair u0 u1) ⇒
299  ∀P: Type[1].
300  (∀e0: (eq A (R0 ? t0) u0).
301   ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].
302
303nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
304#A;#B;#x;#y;#e;nrewrite > e;ncases y;
305#a;#b;nnormalize;#P;#PH;napply PH;@;
306nqed.
307
308nlemma minus_plus_distrib: ∀n,m,p. m-(n+p) = m-n-p.
309#n;nelim n; //; #n';#IH;#m;#p;nnormalize;
310nelim m; //; nqed.
311
312ntheorem plus_minus_r:
313∀m,n,p:nat. m ≤ n → p+(n-m) = (p+n)-m.
314#m;#n;#p;#le;nrewrite > (symmetric_plus …);
315nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.
316
317nlemma plus_minus_le: ∀m,n,p. m≤n → m+p-n≤p.
318#m;#n;#p;nelim m;/2/; nqed.
319
320nlemma le_to_minus: ∀m,n. m≤n → m-n = 0.
321#m;#n;nelim n;
322##[ nrewrite < (minus_n_O …); /2/;
323##| #n'; #IH; #le; ninversion le; /2/; #n''; #A;#B;#C; ndestruct;
324    nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/
325##] nqed.
326
327nlemma minus_times_distrib_l: ∀n,m,p:nat. p*m-p*n = p*(m-n).
328#n;#m;#p;nelim (decidable_le n m);#le;
329##[ nelim p; //;#p'; #IH; nnormalize; nrewrite > (minus_plus_distrib …);
330    nrewrite < (plus_minus … le); nrewrite < IH;
331    nrewrite > (plus_minus_r …); /2/;
332##|
333nlapply (not_le_to_lt … le); #lt;
334nelim p; //; #p';
335 ncut (m-n = 0); ##[ /3/ ##]
336  #mn; nrewrite > mn; nrewrite < (times_n_O …); #H;
337  nnormalize; napply sym_eq; napply  le_n_O_to_eq; nrewrite < H;
338  nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;
339  /2/;
340##] nqed.
341
342nlemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
343#m;#n;#H;nlapply (refl ? (m-n));nelim (m-n) in ⊢ (???% → %);//;
344#H'; nlapply (minus_to_plus … H'); /2/;
345nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H;
346napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
347nqed.
348
349nlemma divide_aux_ok : ∀b,m,n,p,dv,md:nat.
350 n > 0 → b ≥ m →
351 divide_aux b m n p = 〈dv,md〉 →
352 m + p*n = dv*n + md ∧ md < n.
353#b;nelim b;
354##[ #m;#n;#p;#dv;#md;#npos;#bound;
355    nwhd in ⊢ (??%% → ?); nelim (leb (S m) n); nwhd in ⊢ (??%% → ?); #H;
356    ndestruct;
357    @; /2/
358##| #b';#IH;#m;#n;#p;#dv;#md;
359 #npos; #bound; nwhd in ⊢ (??%? → ?); napply leb_elim;
360  ##[ #Hlt; nwhd in ⊢ (??%? → ?); #H;
361    ndestruct;
362    /2/;
363  ##| #Hnlt; ncut (n≤m); ##[ nlapply (not_le_to_lt … Hnlt); /2/; ##]
364      #Hnm; nwhd in ⊢ (??%? → ?); #H;
365      nlapply (IH … H); ##[ napply le_S_S_to_le; napply (transitive_le ? m);  //;
366                            nrewrite < (minus_Sn_m …); //; napply (lt_O_n_elim …npos); #n';
367                            nrewrite > (minus_S_S …); /2/;
368                        ##| //
369                        ##| nnormalize; nrewrite < (associative_plus …); nrewrite < (plus_minus_m_m …); //;
370                        ##]
371  ##] nqed.
372
373ntheorem divide_divides: ∀m,n,dv,md:nat.
374 n > 0 → divide m n = 〈dv,md〉 → m = dv * n + md ∧ md < n.
375#m;#n;#dv;#md;#npos; nwhd in ⊢ (??%? → ?); #DIVIDE;
376nlapply (divide_aux_ok … DIVIDE); //; nqed.
377
378nlemma mod0_divides: ∀m,n,dv:nat.
379  m>0 → divide n m = 〈dv,O〉 → m∣n.
380#m;#n;#dv;#mpos;#DIVIDE;@ dv; nlapply (divide_divides … DIVIDE); //; *; //;
381nqed.
382
383nlemma divides_mod0: ∀dv,m,n:nat.
384  m>0 → n = dv*m → divide n m = 〈dv,O〉.
385#dv;#m;#n;#mpos;#DIV;nlapply (refl ? (divide n m));
386nelim (divide n m) in ⊢ (???% → ?); #dv';#md'; #DIVIDE;
387nlapply (divide_divides … mpos DIVIDE); *;
388nrewrite > DIV in ⊢ (% → ?); #H; nlapply (plus_to_minus … H);
389nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv' …);
390nrewrite > (minus_times_distrib_l …);
391nelim (decidable_le dv dv');
392##[ #le; ncut (dv-dv' = 0); ##[ /2/ ##]
393    #eq; nrewrite > eq; nrewrite < (times_n_O …); #md0; #_;
394    nrewrite > DIVIDE; nrewrite < md0 in H ⊢ %; nrewrite < (plus_n_O …);
395    #H; ncut (dv = dv');  ##[ napply le_to_le_to_eq; //;
396    napply (le_times_to_le m); //; ##]
397     //;
398##| #nle; ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
399    #Hdv; #H; ncut (md' ≥ m); /2/; #A;#B; napply False_ind;
400    napply (absurd ? A (lt_to_not_le … B));
401##] nqed.
402
403nlemma dec_divides_1: ∀m,n:nat. m>0 → (m∣n) + ¬(m∣n).
404#m;#n;#mpos; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
405#dv;#md; ncases md;
406##[ #H; @1; napply mod0_divides; //;
407##| #md'; #DIVIDES; @2; napply nmk; *; #dv';
408    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); //;
409    nrewrite > DIVIDES; #H';
410    ndestruct;
411##] nqed.
412
413nlemma dec_divides: ∀m,n:nat. (m∣n) + ¬(m∣n).
414#m;#n; ncases m; /2/;
415ncases n;
416##[ @1; @ O; //;
417##| #n'; @ 2; @; *; /2/
418##] nqed.
419
420ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
421#p;#q;napply dec_divides; nqed.
422
423
424(* TODO: check these definitions are right.  They are supposed to be the same
425   as Zdiv/Zmod in Coq. *)
426ndefinition divZ ≝ λx,y.
427  match divide (abs x) (abs y) with
428  [ mk_pair q r ⇒
429    match x with
430    [ OZ ⇒ OZ
431    | pos m ⇒
432      match y with
433      [ OZ ⇒ OZ
434      | pos n ⇒ q
435      | neg n ⇒ match r with [ O ⇒ -q | _ ⇒ -(S q) ]
436      ]
437    | neg m ⇒
438      match y return λ_.Z with
439      [ OZ ⇒ OZ
440      | pos n ⇒ match r with [ O ⇒ -q | _ ⇒ -(S q) ]
441      | neg n ⇒ q
442      ]
443    ]
444  ].
445
446ndefinition modZ ≝ λx,y.
447  match divide (abs x) (abs y) with
448  [ mk_pair q r ⇒
449    match x with
450    [ OZ ⇒ OZ
451    | pos m ⇒
452      match y return λ_.Z with
453      [ OZ ⇒ OZ
454      | pos n ⇒ r
455      | neg n ⇒ match r with [ O ⇒ O | _ ⇒ y-r ]
456      ]
457    | neg m ⇒
458      match y return λ_.Z with
459      [ OZ ⇒ OZ
460      | pos n ⇒ match r with [ O ⇒ O | _ ⇒ y+r ]
461      | neg n ⇒ r
462      ]
463    ]
464  ].
465
466interpretation "natural division" 'divide m n = (div m n).
467interpretation "natural modulus" 'module m n = (mod m n).
468interpretation "integer division" 'divide m n = (divZ m n).
469interpretation "integer modulus" 'module m n = (modZ m n).
Note: See TracBrowser for help on using the repository browser.