Changeset 14 for C-semantics/extralib.ma


Ignore:
Timestamp:
Jul 21, 2010, 3:08:58 PM (10 years ago)
Author:
campbell
Message:

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/extralib.ma

    r11 r14  
    649649    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
    650650    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
    651                 match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
     651                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
    652652    ]
    653653  | neg n ⇒
     
    655655    [ OZ ⇒ OZ
    656656    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
    657                 match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
     657                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
    658658    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
    659659    ]
     
    664664interpretation "integer division" 'divide m n = (divZ m n).
    665665interpretation "integer modulus" 'module m n = (modZ m n).
     666
     667nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
     668#x y; ncases y;
     669##[ #H; napply (False_ind … H);
     670##| #m; #_; ncases x; //; #n;
     671    nwhd in ⊢ (?%?);
     672    nlapply (pos_compare_to_Prop n m);
     673    ncases (pos_compare n m); /2/;
     674    #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/;
     675##| #m H; napply (False_ind … H);
     676##] nqed.
     677
     678nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
     679#n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);
     680##[ //;
     681##| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/;
     682##] nqed.
     683
     684ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
     685#x y; ncases y;
     686##[ #H; napply (False_ind … H);
     687##| #m; #_; ncases x;
     688  ##[ @;//;
     689  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
     690      ncases (divide n m) in ⊢ (???% → %); #dv md H;
     691      nelim (divide_ok … H); #e l; nelim l; /2/;
     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;
     695      ##[ /2/;
     696      ##| #md' m' l'; @;
     697        ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
     698            nrewrite > (pos_compare_lt … l'); //;
     699        ##| /2/;
     700        ##]
     701      ##]
     702  ##]
     703##| #m H; napply (False_ind … H);
     704##] nqed.
Note: See TracChangeset for help on using the changeset viewer.