Changeset 10 for C-semantics/extralib.ma


Ignore:
Timestamp:
Jul 6, 2010, 11:53:23 AM (10 years ago)
Author:
campbell
Message:

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/extralib.ma

    r3 r10  
    1313(**************************************************************************)
    1414
    15 include "arithmetics/Z.ma".
    1615include "datatypes/sums.ma".
    1716include "datatypes/list.ma".
    1817include "Plogic/equality.ma".
     18include "binary/Z.ma".
     19include "binary/positive.ma".
    1920
    2021nlemma eq_rect_Type0_r:
     
    6162
    6263(* XXX: divides goes to arithmetics *)
    63 ninductive divides (n,m:nat) : Prop ≝
    64 | witness : ∀p:nat.m = times n p → divides n m.
    65 interpretation "divides" 'divides n m = (divides n m).
    66 interpretation "not divides" 'ndivides n m = (Not (divides n m)).
    67 
    68 ndefinition dividesZ ≝ λx,y:Z. abs x ∣ abs y.
     64ninductive dividesP (n,m:Pos) : Prop ≝
     65| witness : ∀p:Pos.m = times n p → dividesP n m.
     66interpretation "positive divides" 'divides n m = (dividesP n m).
     67interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).
     68
     69ndefinition 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
    6976interpretation "integer divides" 'divides n m = (dividesZ n m).
    7077interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).
    7178
    7279(* should be proved in nat.ma, but it's not! *)
    73 naxiom eqb_to_Prop : ∀n,m.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     80naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     81
     82nlemma 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.
    7484
    7585nlemma injective_Z_of_nat : injective ? ? Z_of_nat.
     
    7787#n;#m;ncases n;ncases m;nnormalize;//;
    7888##[ ##1,2: #n';#H;ndestruct
    79 ##| #n';#m'; #H; ndestruct; //
     89##| #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0); //
    8090##] nqed.
    8191
     
    92102nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
    93103#x;#y;
    94 #n;
    95 nelim n; ##[ ##2: #n'; #IH; ##]
     104napply pos_elim
     105 ##[ ##2: #n'; #IH; ##]
    96106nrewrite > (Zplus_Zsucc_Zpred y ?);
    97 nwhd in ⊢ (?→??(??%));
    98 ##[ #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
     107##[ nrewrite > (Zpred_Zsucc (pos n'));
     108 #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
    99109    napply Zsucc_le;
    100110##| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le;
     
    115125/3/; #H; nrewrite > H; //; nqed.
    116126
     127ntheorem 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   
    117141ntheorem 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 
    127 nlemma decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
     142#n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt;
     143napply (transitive_Zle … Hle); /2/;
     144nqed.
     145
     146ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
    128147#z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H;
    129148##[@;//
     
    180199    match y with
    181200    [ OZ ⇒ false
    182     | pos m ⇒ leb (S n) m
     201    | pos m ⇒ leb (succ n) m
    183202    | neg m ⇒ false ]
    184203  | neg n ⇒
     
    186205    [ OZ ⇒ true
    187206    | pos m ⇒ true
    188     | neg m ⇒ leb (S m) n ]].
     207    | neg m ⇒ leb (succ m) n ]].
    189208
    190209
     
    205224
    206225ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
    207 #n;#m;ncases n;ncases m; nnormalize; /2/;
     226#n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct;
    208227nqed.
    209228
     
    225244
    226245ntheorem 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.
     246#n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct;
     247nqed.
    235248
    236249ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
     
    258271
    259272(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
    260 notation > "'if' term 19 e 'then' term 19 t 'else' term 68 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
    261 notation < "'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 }.
     273notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
     274notation < "'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 }.
    262275interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
    263276
     
    280293(* division *)
    281294
    282 nlet 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 
    289 ndefinition divide ≝ λm,n. divide_aux m m n O.
     295ninductive natp : Type ≝
     296| pzero : natp
     297| ppos  : Pos → natp.
     298
     299ndefinition natp0 ≝
     300λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
     301
     302ndefinition natp1 ≝
     303λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
     304
     305nlet rec divide (m,n:Pos) on m ≝
     306match m with
     307[ one ⇒
     308  match n with
     309  [ one ⇒ 〈ppos one,pzero〉
     310  | _ ⇒ 〈pzero,ppos one〉
     311  ]
     312| p0 m' ⇒
     313  match divide m' n with
     314  [ mk_pair q r ⇒
     315    match r with
     316    [ pzero ⇒ 〈natp0 q,pzero〉
     317    | ppos r' ⇒
     318      match partial_minus (p0 r') n with
     319      [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
     320      | MinusZero ⇒ 〈natp1 q, pzero〉
     321      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
     322      ]
     323    ]
     324  ]
     325| p1 m' ⇒
     326  match divide m' n with
     327  [ mk_pair q r ⇒
     328    match r with
     329    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
     330    | ppos r' ⇒
     331      match partial_minus (p1 r') n with
     332      [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
     333      | MinusZero ⇒ 〈natp1 q, pzero〉
     334      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
     335      ]
     336    ]
     337  ]
     338].
     339
    290340ndefinition div ≝ λm,n. fst ?? (divide m n).
    291341ndefinition mod ≝ λm,n. snd ?? (divide m n).
     
    306356nqed.
    307357
    308 nlemma minus_plus_distrib: ∀n,m,p. m-(n+p) = m-n-p.
    309 #n;nelim n; //; #n';#IH;#m;#p;nnormalize;
    310 nelim m; //; nqed.
     358nlemma pred_minus: ∀n,m. pred n - m = pred (n-m).
     359napply pos_elim; /3/;
     360nqed.
     361
     362nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
     363napply pos_elim;
     364##[ //
     365##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/;
     366##] nqed.
    311367
    312368ntheorem plus_minus_r:
    313 ∀m,n,p:nat. m ≤ n → p+(n-m) = (p+n)-m.
     369∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
    314370#m;#n;#p;#le;nrewrite > (symmetric_plus …);
    315371nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.
    316372
    317 nlemma plus_minus_le: ∀m,n,p. m≤n → m+p-n≤p.
     373nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
    318374#m;#n;#p;nelim m;/2/; nqed.
    319 
     375(*
    320376nlemma le_to_minus: ∀m,n. m≤n → m-n = 0.
    321377#m;#n;nelim n;
     
    324380    nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/
    325381##] nqed.
    326 
    327 nlemma 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;
     382*)
     383nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
     384#n;#m;#p;(*nelim (decidable_lt n m);*)#lt;
     385(*##[*) napply (pos_elim … p); //;#p'; #IH;
     386    nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);
     387    nrewrite > (minus_plus_distrib …);
     388    nrewrite < (plus_minus … lt); nrewrite < IH;
    331389    nrewrite > (plus_minus_r …); /2/;
    332 ##|
    333 nlapply (not_le_to_lt … le); #lt;
    334 nelim 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;
     390nqed.
     391(*##|
     392nlapply (not_lt_to_le … lt); #le;
     393napply (pos_elim … p); //; #p';
     394 ncut (m-n = one); ##[ /3/ ##]
     395  #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …);
     396  #H; nrewrite < H in ⊢ (???%);
     397  napply sym_eq; napply  le_n_one_to_eq; nrewrite < H;
    338398  nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;
    339399  /2/;
     
    346406napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
    347407nqed.
    348 
    349 nlemma 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 
    373 ntheorem 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;
    376 nlapply (divide_aux_ok … DIVIDE); //; nqed.
    377 
    378 nlemma 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); //; *; //;
    381 nqed.
    382 
    383 nlemma 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));
    386 nelim (divide n m) in ⊢ (???% → ?); #dv';#md'; #DIVIDE;
    387 nlapply (divide_divides … mpos DIVIDE); *;
    388 nrewrite > DIV in ⊢ (% → ?); #H; nlapply (plus_to_minus … H);
    389 nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv' …);
    390 nrewrite > (minus_times_distrib_l …);
    391 nelim (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 
    403 nlemma 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; //;
     408*)
     409
     410nlet rec natp_plus (n,m:natp) ≝
     411match n with
     412[ pzero ⇒ m
     413| ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
     414].
     415
     416nlet rec natp_times (n,m:natp) ≝
     417match n with
     418[ pzero ⇒ pzero
     419| ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
     420].
     421
     422ninductive natp_lt : natp → Pos → Prop ≝
     423| plt_zero : ∀n. natp_lt pzero n
     424| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
     425
     426nlemma lt_p0: ∀n:Pos. one < p0 n.
     427#n; nnormalize; /2/; nqed.
     428
     429nlemma lt_p1: ∀n:Pos. one < p1 n.
     430#n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.
     431
     432nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
     433#m; nelim m;
     434##[ //;
     435##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //;
     436##] nqed.
     437
     438nlemma 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).
     439#n P Q; napply succ_elim; /2/; nqed.
     440
     441nlemma partial_minus_to_Prop: ∀n,m.
     442  match partial_minus n m with
     443  [ MinusNeg ⇒ n < m
     444  | MinusZero ⇒ n = m
     445  | MinusPos r ⇒ n = m+r
     446  ].
     447#n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m);
     448nnormalize; ncases (partial_minus n m); /2/; nqed.
     449
     450nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
     451#n m lt; nelim lt; /2/;
     452nqed.
     453
     454nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
     455#n m lt; napply (transitive_lt ? (p0 m) ?); /2/;
     456nqed.
     457
     458nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
     459#n m lt; ninversion lt;
     460##[ #H; nrewrite > (succ_injective … H); //;
     461##| #p H1 H2 H3;nrewrite > (succ_injective … H3);
     462    napply (transitive_lt ? (p0 p) ?); /2/;
     463##]
     464nqed.
     465
     466nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
     467#n m lt; nelim lt; /2/;
     468nqed.
     469
     470
     471
     472nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
     473#n m lt;ninversion lt;
     474##[ #p H; ndestruct;
     475##| #n' m' lt e1 e2; ndestruct; //;
     476##] nqed.
     477
     478nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
     479#a b; /2/; nqed.
     480
     481nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
     482#a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.
     483
     484nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
     485/2/; nqed.
     486
     487nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
     488#A B a1 a2 b1 b2 H; ndestruct; //;
     489nqed.
     490
     491nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
     492#A B a1 a2 b1 b2 H; ndestruct; //;
     493nqed.
     494
     495ntheorem divide_ok : ∀m,n,dv,md.
     496 divide m n = 〈dv,md〉 →
     497 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
     498#m n; napply (pos_cases … n);
     499##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/;
     500##| #n'; nelim m;
     501  ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
     502  ##| #m' IH dv md; nnormalize;
     503      nlapply (refl ? (divide m' (succ n')));
     504      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
     505      #dv' md' DIVr; nelim (IH … DIVr);
     506      nnormalize; ncases md';
     507      ##[ ncases dv'; nnormalize;
     508        ##[ #H; ndestruct;
     509        ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
     510        ##]
     511      ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
     512          nnormalize; #n md'' Hr1 Hr2;
     513          nlapply (plt_lt … Hr2); #Hr2';
     514          nlapply (partial_minus_to_Prop md'' n);
     515          ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;
     516          #lt; #e; ndestruct; @; /2/; napply plt_pos;
     517          ##[ ##1,3,5,7: napply double_lt1; /2/;
     518          ##| ##2,4: napply double_lt3; /2/;
     519          ##| ##*: napply double_lt2; /2/;
     520          ##]
     521      ##]
     522  ##| #m' IH dv md; nwhd in ⊢ (??%? → ?);
     523      nlapply (refl ? (divide m' (succ n')));
     524      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
     525      #dv' md' DIVr; nelim (IH … DIVr);
     526      nwhd in ⊢ (? → ? → ??%? → ?); ncases md';
     527      ##[ ncases dv'; nnormalize;
     528        ##[ #H; ndestruct;
     529        ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/;
     530        ##]
     531      ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
     532          nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2;
     533          nlapply (plt_lt … Hr2); #Hr2';
     534          nwhd in ⊢ (??%? → ?);
     535          nlapply (partial_minus_to_Prop (p0 md'') (succ n'));
     536          ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##]
     537          ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize;
     538          #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##]
     539          #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##]
     540          nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e);
     541          nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos;
     542          ##[ ncut (succ n' + r'' < p0 (succ n')); /2/;
     543          ##| ncut (succ n' + r'' < p0 (succ n')); /2/;
     544          ##| /2/;
     545          ##| /2/;
     546          ##]
     547      ##]
     548  ##]
     549##] nqed.
     550
     551nlemma mod0_divides: ∀m,n,dv:Pos.
     552  divide n m = 〈ppos dv,pzero〉 → m∣n.
     553#m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *;
     554nnormalize; #H; ndestruct; //;
     555nqed.
     556
     557nlemma divides_mod0: ∀dv,m,n:Pos.
     558  n = dv*m → divide n m = 〈ppos dv,pzero〉.
     559#dv;#m;#n;#DIV;nlapply (refl ? (divide n m));
     560nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE;
     561nlapply (divide_ok … DIVIDE); *;
     562ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]
     563ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE;  nnormalize;
     564nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct;
     565##[ nlapply (plus_to_minus … e0);
     566    nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …);
     567    ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt;
     568    nrewrite > (minus_times_distrib_l …); //;
     569
     570 (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
     571    #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind;
     572    napply (absurd ? B (lt_to_not_le … A));
     573
     574##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/;
     575
     576##| nrewrite > DIVIDE; ncut (dv = dv''); /2/;
     577##]
     578nqed.
     579
     580nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
     581#m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
     582#dv;#md; ncases md; ncases dv;
     583##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct
     584##| #dv'; #H; @1; napply mod0_divides; /2/;
    407585##| #md'; #DIVIDES; @2; napply nmk; *; #dv';
    408     nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); //;
     586    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
    409587    nrewrite > DIVIDES; #H';
    410588    ndestruct;
    411 ##] nqed.
    412 
    413 nlemma dec_divides: ∀m,n:nat. (m∣n) + ¬(m∣n).
    414 #m;#n; ncases m; /2/;
    415 ncases n;
    416 ##[ @1; @ O; //;
    417 ##| #n'; @ 2; @; *; /2/
     589##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv';
     590    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
     591    nrewrite > DIVIDES; #H';
     592    ndestruct;
    418593##] nqed.
    419594
    420595ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
    421 #p;#q;napply dec_divides; nqed.
    422 
     596#p;#q;ncases p;
     597##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##]
     598##| ##*: #n; ncases q; nnormalize; /2/;
     599##] nqed.
     600
     601ndefinition natp_to_Z ≝
     602λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
     603
     604ndefinition natp_to_negZ ≝
     605λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].
    423606
    424607(* TODO: check these definitions are right.  They are supposed to be the same
    425608   as Zdiv/Zmod in Coq. *)
    426609ndefinition divZ ≝ λx,y.
    427   match divide (abs x) (abs y) with
    428   [ mk_pair q r ⇒
    429     match x with
     610  match x with
     611  [ OZ ⇒ OZ
     612  | pos n ⇒
     613    match y with
    430614    [ 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       ]
     615    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
     616    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
     617                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
     618    ]
     619  | neg n ⇒
     620    match y with
     621    [ OZ ⇒ OZ
     622    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
     623                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
     624    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
    443625    ]
    444626  ].
    445627
    446628ndefinition modZ ≝ λx,y.
    447   match divide (abs x) (abs y) with
    448   [ mk_pair q r ⇒
    449     match x with
     629  match x with
     630  [ OZ ⇒ OZ
     631  | pos n ⇒
     632    match y with
    450633    [ 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       ]
     634    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
     635    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
     636                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
     637    ]
     638  | neg n ⇒
     639    match y with
     640    [ OZ ⇒ OZ
     641    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
     642                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
     643    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
    463644    ]
    464645  ].
Note: See TracChangeset for help on using the changeset viewer.