Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/extralib.ma

    r400 r487  
    1313(**************************************************************************)
    1414
    15 include "datatypes/sums.ma".
    16 include "datatypes/list.ma".
    17 include "Plogic/equality.ma".
     15include "basics/types.ma".
     16include "basics/list.ma".
     17include "basics/logic.ma".
    1818include "binary/Z.ma".
    1919include "binary/positive.ma".
    2020
    21 nlemma eq_rect_Type0_r:
     21lemma eq_rect_Type0_r:
    2222 ∀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:
     23 #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption.
     24qed.
     25
     26lemma eq_rect_r2:
    2727 ∀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:
     28 #A #a #x #p cases p; #P #H assumption.
     29qed.
     30
     31lemma eq_rect_Type2_r:
    3232 ∀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:
     33 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption.
     34qed.
     35
     36lemma eq_rect_CProp0_r:
    3737 ∀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.
     38 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption.
     39qed.
     40
     41lemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.
     42#A #x #y *;#H @nmk #H' /2/;
     43qed.
    4444
    4545(* stolen from logic/connectives.ma to give Prop version. *)
     
    5656(* bool *)
    5757
    58 ndefinition xorb : bool → bool → bool ≝
     58definition xorb : bool → bool → bool ≝
    5959  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
    6060 
     
    6262(* TODO: move to Z.ma *)
    6363
    64 nlemma eqZb_z_z : ∀z.eqZb z z = true.
    65 #z;ncases z;nnormalize;//;
    66 nqed.
     64lemma eqZb_z_z : ∀z.eqZb z z = true.
     65#z cases z;normalize;//;
     66qed.
    6767
    6868(* XXX: divides goes to arithmetics *)
    69 ninductive dividesP (n,m:Pos) : Prop ≝
     69inductive dividesP (n,m:Pos) : Prop ≝
    7070| witness : ∀p:Pos.m = times n p → dividesP n m.
    7171interpretation "positive divides" 'divides n m = (dividesP n m).
    7272interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).
    7373
    74 ndefinition dividesZ : Z → Z → Prop ≝
     74definition dividesZ : Z → Z → Prop ≝
    7575λx,y. match x with
    7676[ OZ ⇒ False
     
    8383
    8484(* should be proved in nat.ma, but it's not! *)
    85 nlemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
    86 #n; nelim n;
    87 ##[ #m; ncases m; //;
    88 ##| #n' IH m; ncases m; ##[ /2/; ##| #m'; nwhd in match (eqb (S n') (S m')) in ⊢ %;
    89   nlapply (IH m'); ncases (eqb n' m'); /2/; ##]
    90 ##] nqed.
    91 
    92 nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
    93 #n m; napply eqb_elim; //; nqed.
    94 
    95 nlemma injective_Z_of_nat : injective ? ? Z_of_nat.
    96 nnormalize;
    97 #n;#m;ncases n;ncases m;nnormalize;//;
    98 ##[ ##1,2: #n';#H;ndestruct
    99 ##| #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0); //
    100 ##] nqed.
    101 
    102 nlemma reflexive_Zle : reflexive ? Zle.
    103 #x; ncases x; //; nqed.
    104 
    105 nlemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
    106 #n;ncases n;nnormalize;//;nqed.
    107 
    108 nlemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
    109 #x; ncases x; //;
    110 #n; ncases n; //; nqed.
    111 
    112 nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
    113 #x;#y;
    114 napply pos_elim
    115  ##[ ##2: #n'; #IH; ##]
    116 nrewrite > (Zplus_Zsucc_Zpred y ?);
    117 ##[ nrewrite > (Zpred_Zsucc (pos n'));
    118  #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
    119     napply Zsucc_le;
    120 ##| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le;
    121 ##] nqed.
     85lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     86#n elim n;
     87[ #m cases m; //;
     88| #n' #IH #m cases m; [ /2/; | #m' whd in match (eqb (S n') (S m')) in ⊢ %;
     89  lapply (IH m'); cases (eqb n' m'); /2/; ]
     90] qed.
     91
     92lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     93#n #m @eqb_elim //; qed.
     94
     95lemma injective_Z_of_nat : injective ? ? Z_of_nat.
     96normalize;
     97#n #m cases n;cases m;normalize;//;
     98[ 1,2: #n' #H destruct
     99| #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) //
     100] qed.
     101
     102lemma reflexive_Zle : reflexive ? Zle.
     103#x cases x; //; qed.
     104
     105lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
     106#n cases n;normalize;//;qed.
     107
     108lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
     109#x cases x; //;
     110#n cases n; //; qed.
     111
     112lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
     113#x #y
     114@pos_elim
     115 [ 2: #n' #IH ]
     116>(Zplus_Zsucc_Zpred y ?)
     117[ >(Zpred_Zsucc (pos n'))
     118 #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??)
     119    @Zsucc_le
     120| #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le
     121] qed.
    122122
    123123(* XXX: Zmax must go to arithmetics *)
    124 ndefinition Zmax : Z → Z → Z ≝
     124definition Zmax : Z → Z → Z ≝
    125125  λx,y.match Z_compare x y with
    126126  [ LT ⇒ y
    127127  | _ ⇒ x ].
    128128
    129 nlemma Zmax_l: ∀x,y. x ≤ Zmax x y.
    130 #x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
    131 /3/; ncases x; /3/; nqed.
    132 
    133 nlemma Zmax_r: ∀x,y. y ≤ Zmax x y.
    134 #x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
    135 ncases x; /3/; nqed.
    136 
    137 ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
    138 #x y; ncases x;
    139 ##[ ncases y;
    140   ##[ ##1,2: //
    141   ##| #n; napply False_ind;
    142   ##]
    143 ##| #n; ncases y;
    144   ##[ nnormalize; napply False_ind;
    145   ##| #m; napply (pos_cases … n); /2/;
    146   ##| #m; nnormalize; napply False_ind;
    147   ##]
    148 ##| #n; ncases y; /2/;
    149 ##] nqed.
     129lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
     130#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y);
     131/3/; cases x; /3/; qed.
     132
     133lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
     134#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y);
     135cases x; /3/; qed.
     136
     137theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
     138#x #y cases x;
     139[ cases y;
     140  [ 1,2: //
     141  | #n @False_ind
     142  ]
     143| #n cases y;
     144  [ normalize; @False_ind
     145  | #m @(pos_cases … n) /2/;
     146  | #m normalize; @False_ind
     147  ]
     148| #n cases y; /2/;
     149] qed.
    150150   
    151 ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
    152 #n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt;
    153 napply (transitive_Zle … Hle); /2/;
    154 nqed.
    155 
    156 ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
    157 #z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H;
    158 ##[@;//
    159 ##|@2;//##]
    160 nqed.
    161 
    162 nlemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
    163 #z1;#z2;nlapply (eqZb_to_Prop z1 z2); ncases (eqZb z1 z2); //;
    164 #H; #H'; napply False_ind; napply (absurd ? H H');
    165 nqed.
     151theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
     152#n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt
     153@(transitive_Zle … Hle) /2/;
     154qed.
     155
     156definition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
     157#z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H
     158[% //
     159|%2 //]
     160qed.
     161
     162lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
     163#z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //;
     164#H #H' @False_ind @(absurd ? H H')
     165qed.
    166166
    167167(* Z.ma *)
    168168
    169 ndefinition Zge: Z → Z → Prop ≝
     169definition Zge: Z → Z → Prop ≝
    170170λn,m:Z.m ≤ n.
    171171
    172172interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).
    173173
    174 ndefinition Zgt: Z → Z → Prop ≝
     174definition Zgt: Z → Z → Prop ≝
    175175λn,m:Z.m<n.
    176176
     
    179179interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
    180180
    181 nlet rec Zleb (x:Z) (y:Z) : bool ≝
     181let rec Zleb (x:Z) (y:Z) : bool ≝
    182182  match x with
    183183  [ OZ ⇒
     
    197197    | neg m ⇒ leb m n ]].
    198198   
    199 nlet rec Zltb (x:Z) (y:Z) : bool ≝
     199let rec Zltb (x:Z) (y:Z) : bool ≝
    200200  match x with
    201201  [ OZ ⇒
     
    217217
    218218
    219 ntheorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
    220 #n;#m;ncases n;ncases m; //;
    221 ##[ ##1,2: #m'; nnormalize; #H; napply (False_ind ? H)
    222 ##| ##3,5: #n';#m'; nnormalize; napply le_to_leb_true;
    223 ##| ##4: #n';#m'; nnormalize; #H; napply (False_ind ? H)
    224 ##] nqed.
    225 
    226 ntheorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
    227 #n;#m;ncases n;ncases m; //;
    228 ##[ ##1,2: #m'; nnormalize; #H; ndestruct
    229 ##| ##3,5: #n';#m'; nnormalize; napply leb_true_to_le;
    230 ##| ##4: #n';#m'; nnormalize; #H; ndestruct
    231 ##] nqed.
    232 
    233 ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
    234 #n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct;
    235 nqed.
    236 
    237 ntheorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
    238 #n;#m;ncases n;ncases m; //;
    239 ##[ nnormalize; #H; napply (False_ind ? H)
    240 ##| ##2,3: #m'; nnormalize; #H; napply (False_ind ? H)
    241 ##| ##4,6: #n';#m'; nnormalize; napply le_to_leb_true;
    242 ##| #n';#m'; nnormalize; #H; napply (False_ind ? H)
    243 ##] nqed.
    244 
    245 ntheorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
    246 #n;#m;ncases n;ncases m; //;
    247 ##[ nnormalize; #H; ndestruct
    248 ##| ##2,3: #m'; nnormalize; #H; ndestruct
    249 ##| ##4,6: #n';#m'; napply leb_true_to_le;
    250 ##| #n';#m'; nnormalize; #H; ndestruct
    251 ##] nqed.
    252 
    253 ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
    254 #n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct;
    255 nqed.
    256 
    257 ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
     219theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
     220#n #m cases n;cases m; //;
     221[ 1,2: #m' normalize; #H @(False_ind ? H)
     222| 3,5: #n' #m' normalize; @le_to_leb_true
     223| 4: #n' #m' normalize; #H @(False_ind ? H)
     224] qed.
     225
     226theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
     227#n #m cases n;cases m; //;
     228[ 1,2: #m' normalize; #H destruct
     229| 3,5: #n' #m' normalize; @leb_true_to_le
     230| 4: #n' #m' normalize; #H destruct
     231] qed.
     232
     233theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
     234#n #m #H % #H' >(Zle_to_Zleb_true … H') in H #H destruct;
     235qed.
     236
     237theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
     238#n #m cases n;cases m; //;
     239[ normalize; #H @(False_ind ? H)
     240| 2,3: #m' normalize; #H @(False_ind ? H)
     241| 4,6: #n' #m' normalize; @le_to_leb_true
     242| #n' #m' normalize; #H @(False_ind ? H)
     243] qed.
     244
     245theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
     246#n #m cases n;cases m; //;
     247[ normalize; #H destruct
     248| 2,3: #m' normalize; #H destruct
     249| 4,6: #n' #m' @leb_true_to_le
     250| #n' #m' normalize; #H destruct
     251] qed.
     252
     253theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
     254#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H #H destruct;
     255qed.
     256
     257theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
    258258(n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
    259 #n;#m;#P;#Hle;#Hnle;
    260 nlapply (refl ? (Zleb n m));
    261 nelim (Zleb n m) in ⊢ ((???%)→%);
    262 #Hb;
    263 ##[ napply Hle; napply (Zleb_true_to_Zle … Hb)
    264 ##| napply Hnle; napply (Zleb_false_to_not_Zle … Hb)
    265 ##] nqed.
    266 
    267 ntheorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
     259#n #m #P #Hle #Hnle
     260lapply (refl ? (Zleb n m));
     261elim (Zleb n m) in ⊢ ((???%)→%);
     262#Hb
     263[ @Hle @(Zleb_true_to_Zle … Hb)
     264| @Hnle @(Zleb_false_to_not_Zle … Hb)
     265] qed.
     266
     267theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
    268268(n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
    269 #n;#m;#P;#Hlt;#Hnlt;
    270 nlapply (refl ? (Zltb n m));
    271 nelim (Zltb n m) in ⊢ ((???%)→%);
    272 #Hb;
    273 ##[ napply Hlt; napply (Zltb_true_to_Zlt … Hb)
    274 ##| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb)
    275 ##] nqed.
    276 
    277 nlemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
    278 #x y; ncases x; ncases y; /2/;
    279 #n m; napply (pos_cases … n); napply (pos_cases … m);
    280 ##[ //;
    281 ##| #n'; /2/;
    282 ##| #m'; #H; napply False_ind; nnormalize in H; napply (absurd … (not_le_succ_one m')); /2/;
    283 ##| #n' m'; #H; nnormalize in H;
    284     nrewrite > (Zsucc_neg_succ n'); nrewrite > (Zsucc_neg_succ m'); /2/;
    285 ##] nqed.
    286 
    287 nlemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
    288 #x y; ncases x; ncases y;
    289 ##[ ##1,2,7,8,9: /2/;
    290 ##| ##3,4: #m; nnormalize; *;
    291 ##| #m n; napply (pos_cases … n); napply (pos_cases … m);
    292   ##[ ##1,2: /2/;
    293   ##| #n'; nnormalize; #H; napply False_ind; napply (absurd … (not_le_succ_one n')); /2/;
    294   ##| #n' m'; nrewrite > (Zpred_pos_succ n'); nrewrite > (Zpred_pos_succ m'); /2/;
    295   ##]
    296 ##| #m n; nnormalize; *;
    297 ##] nqed.
    298 
    299 nlemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
    300 #n; ncases n; //; #n'; #a b H;
    301 ##[ napply (pos_elim … n');
    302   ##[ nrewrite < (Zsucc_Zplus_pos_O a); nrewrite < (Zsucc_Zplus_pos_O b); /2/;
    303   ##| #n'' H; nrewrite > (?:pos (succ n'') = Zsucc (pos n'')); //;
    304       nrewrite > (Zplus_Zsucc …); nrewrite > (Zplus_Zsucc …); /2/;
    305   ##]
    306 ##| napply (pos_elim … n');
    307   ##[ nrewrite < (Zpred_Zplus_neg_O a); nrewrite < (Zpred_Zplus_neg_O b); /2/;
    308   ##| #n'' H; nrewrite > (?:neg (succ n'') = Zpred (neg n'')); //;
    309       nrewrite > (Zplus_Zpred …); nrewrite > (Zplus_Zpred …); /2/;
    310   ##]
    311 ##] nqed.
    312 
    313 nlemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
    314 /2/; nqed.
    315 
    316 nlet rec Z_times (x:Z) (y:Z) : Z ≝
     269#n #m #P #Hlt #Hnlt
     270lapply (refl ? (Zltb n m));
     271elim (Zltb n m) in ⊢ ((???%)→%);
     272#Hb
     273[ @Hlt @(Zltb_true_to_Zlt … Hb)
     274| @Hnlt @(Zltb_false_to_not_Zlt … Hb)
     275] qed.
     276
     277lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
     278#x #y cases x; cases y; /2/;
     279#n #m @(pos_cases … n) @(pos_cases … m)
     280[ //;
     281| #n' /2/;
     282| #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/;
     283| #n' #m' #H normalize in H;
     284    >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/;
     285] qed.
     286
     287lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
     288#x #y cases x; cases y;
     289[ 1,2,7,8,9: /2/;
     290| 3,4: #m normalize; *;
     291| #m #n @(pos_cases … n) @(pos_cases … m)
     292  [ 1,2: /2/;
     293  | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/;
     294  | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/;
     295  ]
     296| #m #n normalize; *;
     297] qed.
     298
     299lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
     300#n cases n; //; #n' #a #b #H
     301[ @(pos_elim … n')
     302  [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/;
     303  | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //;
     304      >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/;
     305  ]
     306| @(pos_elim … n')
     307  [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;
     308  | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //;
     309      >(Zplus_Zpred …) >(Zplus_Zpred …) /2/;
     310  ]
     311] qed.
     312
     313lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
     314/2/; qed.
     315
     316let rec Z_times (x:Z) (y:Z) : Z ≝
    317317match x with
    318318[ OZ ⇒ OZ
     
    339339(* datatypes/list.ma *)
    340340
    341 ntheorem nil_append_nil_both:
    342   ∀A:Type. ∀l1,l2:list A.
     341theorem nil_append_nil_both:
     342  ∀A:Type[0]. ∀l1,l2:list A.
    343343    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
    344 #A l1 l2; ncases l1;
    345 ##[ ncases l2;
    346   ##[ /2/
    347   ##| #h t H; ndestruct;
    348   ##]
    349 ##| ncases l2;
    350   ##[ nnormalize; #h t H; ndestruct;
    351   ##| nnormalize; #h1 t1 h2 h3 H; ndestruct;
    352   ##]
    353 ##] nqed.
     344#A #l1 #l2 cases l1;
     345[ cases l2;
     346  [ /2/
     347  | #h #t #H destruct;
     348  ]
     349| cases l2;
     350  [ normalize; #h #t #H destruct;
     351  | normalize; #h1 #t1 #h2 #h3 #H destruct;
     352  ]
     353] qed.
    354354
    355355(* division *)
    356356
    357 ninductive natp : Type
     357inductive natp : Type[0]
    358358| pzero : natp
    359359| ppos  : Pos → natp.
    360360
    361 ndefinition natp0 ≝
     361definition natp0 ≝
    362362λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
    363363
    364 ndefinition natp1 ≝
     364definition natp1 ≝
    365365λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
    366366
    367 nlet rec divide (m,n:Pos) on m ≝
     367let rec divide (m,n:Pos) on m ≝
    368368match m with
    369369[ one ⇒
     
    374374| p0 m' ⇒
    375375  match divide m' n with
    376   [ mk_pair q r ⇒
     376  [ pair q r ⇒
    377377    match r with
    378378    [ pzero ⇒ 〈natp0 q,pzero〉
     
    387387| p1 m' ⇒
    388388  match divide m' n with
    389   [ mk_pair q r ⇒
     389  [ pair q r ⇒
    390390    match r with
    391391    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
     
    400400].
    401401
    402 ndefinition div ≝ λm,n. fst ?? (divide m n).
    403 ndefinition mod ≝ λm,n. snd ?? (divide m n).
    404 
    405 ndefinition pairdisc ≝
    406 λA,B.λx,y:pair A B.
     402definition div ≝ λm,n. fst ?? (divide m n).
     403definition mod ≝ λm,n. snd ?? (divide m n).
     404
     405definition pairdisc ≝
     406λA,B.λx,y:Prod A B.
    407407match x with
    408 [(mk_pair t0 t1) ⇒
     408[(pair t0 t1) ⇒
    409409match y with
    410 [(mk_pair u0 u1) ⇒
     410[(pair u0 u1) ⇒
    411411  ∀P: Type[1].
    412412  (∀e0: (eq A (R0 ? t0) u0).
    413413   ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].
    414414
    415 nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
    416 #A;#B;#x;#y;#e;nrewrite > e;ncases y;
    417 #a;#b;nnormalize;#P;#PH;napply PH;@;
    418 nqed.
    419 
    420 nlemma pred_minus: ∀n,m. pred n - m = pred (n-m).
    421 napply pos_elim; /3/;
    422 nqed.
    423 
    424 nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
    425 napply pos_elim;
    426 ##[ //
    427 ##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/;
    428 ##] nqed.
    429 
    430 ntheorem plus_minus_r:
     415lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
     416#A #B #x #y #e >e cases y;
     417#a #b normalize;#P #PH @PH %
     418qed.
     419
     420lemma pred_minus: ∀n,m. pred n - m = pred (n-m).
     421@pos_elim /3/;
     422qed.
     423
     424lemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
     425@pos_elim
     426[ //
     427| #n #IH #m #p >(succ_plus_one …) >(IH m one) /2/;
     428] qed.
     429
     430theorem plus_minus_r:
    431431∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
    432 #m;#n;#p;#le;nrewrite > (symmetric_plus …);
    433 nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.
    434 
    435 nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
    436 #m;#n;#p;nelim m;/2/; nqed.
     432#m #n #p #le >(commutative_plus …)
     433>(commutative_plus p ?) @plus_minus //; qed.
     434
     435lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
     436#m #n #p elim m;/2/; qed.
    437437(*
    438 nlemma le_to_minus: ∀m,n. m≤n → m-n = 0.
    439 #m;#n;nelim n;
    440 ##[ nrewrite < (minus_n_O …); /2/;
    441 ##| #n'; #IH; #le; ninversion le; /2/; #n''; #A;#B;#C; ndestruct;
    442     nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/
    443 ##] nqed.
     438lemma le_to_minus: ∀m,n. m≤n → m-n = 0.
     439#m #n elim n;
     440[ <(minus_n_O …) /2/;
     441| #n' #IH #le inversion le; /2/; #n'' #A #B #C destruct;
     442    >(eq_minus_S_pred …) >(IH A) /2/
     443] qed.
    444444*)
    445 nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
    446 #n;#m;#p;(*nelim (decidable_lt n m);*)#lt;
    447 (*##[*) napply (pos_elim … p); //;#p'; #IH;
    448     nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);
    449     nrewrite > (minus_plus_distrib …);
    450     nrewrite < (plus_minus … lt); nrewrite < IH;
    451     nrewrite > (plus_minus_r …); /2/;
    452 nqed.
    453 (*##|
    454 nlapply (not_lt_to_le … lt); #le;
    455 napply (pos_elim … p); //; #p';
    456  ncut (m-n = one); ##[ /3/ ##]
    457   #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …);
    458   #H; nrewrite < H in ⊢ (???%);
    459   napply sym_eq; napply  le_n_one_to_eq; nrewrite < H;
    460   nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;
     445lemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
     446#n #m #p (*elim (decidable_lt n m);*)#lt
     447(*[*) @(pos_elim … p) //;#p' #IH
     448    <(times_succn_m …) <(times_succn_m …) <(times_succn_m …)
     449    >(minus_plus_distrib …)
     450    <(plus_minus … lt) <IH
     451    >(plus_minus_r …) /2/;
     452qed.
     453(*|
     454lapply (not_lt_to_le … lt); #le
     455@(pos_elim … p) //; #p'
     456 cut (m-n = one); [ /3/ ]
     457  #mn >mn >(times_n_one …) >(times_n_one …)
     458  #H <H in ⊢ (???%)
     459  @sym_eq @le_n_one_to_eq <H
     460  >(minus_plus_distrib …) @monotonic_le_minus_l
    461461  /2/;
    462 ##] nqed.
    463 
    464 nlemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
    465 #m;#n;#H;nlapply (refl ? (m-n));nelim (m-n) in ⊢ (???% → %);//;
    466 #H'; nlapply (minus_to_plus … H'); /2/;
    467 nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H;
    468 napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
    469 nqed.
     462] qed.
     463
     464lemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
     465#m #n #H lapply (refl ? (m-n));elim (m-n) in ⊢ (???% → %);//;
     466#H' lapply (minus_to_plus … H'); /2/;
     467<(plus_n_O …) #H'' >H'' in H #H
     468@False_ind @(absurd ? H ( not_le_Sn_n n))
     469qed.
    470470*)
    471471
    472 nlet rec natp_plus (n,m:natp) ≝
     472let rec natp_plus (n,m:natp) ≝
    473473match n with
    474474[ pzero ⇒ m
     
    476476].
    477477
    478 nlet rec natp_times (n,m:natp) ≝
     478let rec natp_times (n,m:natp) ≝
    479479match n with
    480480[ pzero ⇒ pzero
     
    482482].
    483483
    484 ninductive natp_lt : natp → Pos → Prop ≝
     484inductive natp_lt : natp → Pos → Prop ≝
    485485| plt_zero : ∀n. natp_lt pzero n
    486486| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
    487487
    488 nlemma lt_p0: ∀n:Pos. one < p0 n.
    489 #n; nnormalize; /2/; nqed.
    490 
    491 nlemma lt_p1: ∀n:Pos. one < p1 n.
    492 #n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.
    493 
    494 nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
    495 #m; nelim m;
    496 ##[ //;
    497 ##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //;
    498 ##] nqed.
    499 
    500 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).
    501 #n P Q; napply succ_elim; /2/; nqed.
    502 
    503 nlemma partial_minus_to_Prop: ∀n,m.
     488lemma lt_p0: ∀n:Pos. one < p0 n.
     489#n normalize; /2/; qed.
     490
     491lemma lt_p1: ∀n:Pos. one < p1 n.
     492#n' normalize; >(?:p1 n' = succ (p0 n')) //; qed.
     493
     494lemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
     495#m elim m;
     496[ //;
     497| 2,3: #m' #IH normalize; >IH //;
     498] qed.
     499
     500lemma pos_nonzero2: ∀n. ∀P:Pos→Type[0]. ∀Q:Type[0]. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n).
     501#n #P #Q @succ_elim /2/; qed.
     502
     503lemma partial_minus_to_Prop: ∀n,m.
    504504  match partial_minus n m with
    505505  [ MinusNeg ⇒ n < m
     
    507507  | MinusPos r ⇒ n = m+r
    508508  ].
    509 #n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m);
    510 nnormalize; ncases (partial_minus n m); /2/; nqed.
    511 
    512 nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
    513 #n m lt; nelim lt; /2/;
    514 nqed.
    515 
    516 nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
    517 #n m lt; napply (transitive_lt ? (p0 m) ?); /2/;
    518 nqed.
    519 
    520 nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
    521 #n m lt; ninversion lt;
    522 ##[ #H; nrewrite > (succ_injective … H); //;
    523 ##| #p H1 H2 H3;nrewrite > (succ_injective … H3);
    524     napply (transitive_lt ? (p0 p) ?); /2/;
    525 ##]
    526 nqed.
    527 
    528 nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
    529 #n m lt; nelim lt; /2/;
    530 nqed.
    531 
    532 
    533 
    534 nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
    535 #n m lt;ninversion lt;
    536 ##[ #p H; ndestruct;
    537 ##| #n' m' lt e1 e2; ndestruct; //;
    538 ##] nqed.
    539 
    540 nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
    541 #a b; /2/; nqed.
    542 
    543 nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
    544 #a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.
    545 
    546 nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
    547 /2/; nqed.
    548 
    549 nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
    550 #A B a1 a2 b1 b2 H; ndestruct; //;
    551 nqed.
    552 
    553 nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
    554 #A B a1 a2 b1 b2 H; ndestruct; //;
    555 nqed.
    556 
    557 ntheorem divide_ok : ∀m,n,dv,md.
     509#n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m);
     510normalize; cases (partial_minus n m); /2/; qed.
     511
     512lemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
     513#n #m #lt elim lt; /2/;
     514qed.
     515
     516lemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
     517#n #m #lt @(transitive_lt ? (p0 m) ?) /2/;
     518qed.
     519
     520lemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
     521#n #m #lt inversion lt;
     522[ #H >(succ_injective … H) //;
     523| #p #H1 #H2 #H3 >(succ_injective … H3)
     524    @(transitive_lt ? (p0 p) ?) /2/;
     525]
     526qed.
     527
     528lemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
     529#n #m #lt elim lt; /2/;
     530qed.
     531
     532
     533
     534lemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
     535#n #m #lt inversion lt;
     536[ #p #H destruct;
     537| #n' #m' #lt #e1 #e2 destruct @lt
     538] qed.
     539
     540lemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
     541#a #b /2/; qed.
     542
     543lemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
     544#a #b >(?:p1 b = succ (p0 b)) /2/; qed.
     545
     546lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
     547/2/; qed.
     548
     549lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
     550#A #B #a1 #a2 #b1 #b2 #H destruct //
     551qed.
     552
     553lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
     554#A #B #a1 #a2 #b1 #b2 #H destruct //
     555qed.
     556
     557theorem divide_ok : ∀m,n,dv,md.
    558558 divide m n = 〈dv,md〉 →
    559559 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
    560 #m n; napply (pos_cases … n);
    561 ##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/;
    562 ##| #n'; nelim m;
    563   ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
    564   ##| #m' IH dv md; nwhd in ⊢ (??%? → ?(???%)?);
    565       nlapply (refl ? (divide m' (succ n')));
    566       nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
    567       #dv' md' DIVr; nelim (IH … DIVr);
    568       nwhd in ⊢ (? → ? → ??%? → ?);
    569       ncases md';
    570       ##[ ncases dv'; nnormalize;
    571         ##[ #H; ndestruct;
    572         ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
    573         ##]
    574       ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
    575           nnormalize; #n md'' Hr1 Hr2;
    576           nlapply (plt_lt … Hr2); #Hr2';
    577           nlapply (partial_minus_to_Prop md'' n);
    578           ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;
    579           #lt; #e; ndestruct; @; ##[ /3/; ##| ##*: /2/; ##] napply plt_pos;
    580           ##[ ##1,3,5,7: napply double_lt1; /2/;
    581           ##| ##2,4: napply double_lt3; /2/;
    582           ##| ##*: napply double_lt2; /2/;
    583           ##]
    584       ##]
    585   ##| #m' IH dv md; nwhd in ⊢ (??%? → ?);
    586       nlapply (refl ? (divide m' (succ n')));
    587       nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
    588       #dv' md' DIVr; nelim (IH … DIVr);
    589       nwhd in ⊢ (? → ? → ??%? → ?); ncases md';
    590       ##[ ncases dv'; nnormalize;
    591         ##[ #H; ndestruct;
    592         ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/;
    593         ##]
    594       ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
    595           nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2;
    596           nlapply (plt_lt … Hr2); #Hr2';
    597           nwhd in ⊢ (??%? → ?);
    598           nlapply (partial_minus_to_Prop (p0 md'') (succ n'));
    599           ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##]
    600           ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize;
    601           #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##]
    602           #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##]
    603           nrewrite < (pair_eq1 ?????? e); nrewrite < (pair_eq2 ?????? e);
    604           nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos;
    605           ##[ ncut (succ n' + r'' < p0 (succ n')); /2/;
    606           ##| ncut (succ n' + r'' < p0 (succ n')); /2/;
    607           ##| /2/;
    608           ##| /2/;
    609           ##]
    610       ##]
    611   ##]
    612 ##] nqed.
    613 
    614 nlemma mod0_divides: ∀m,n,dv:Pos.
     560#m #n @(pos_cases … n)
     561[ >(divide_by_one m) #dv #md #H destruct /2/
     562| #n' elim m;
     563  [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/
     564  | #m' #IH #dv #md whd in ⊢ (??%? → ?(???%)?);
     565      lapply (refl ? (divide m' (succ n')));
     566      elim (divide m' (succ n')) in ⊢ (???% → % → ?);
     567      #dv' #md' #DIVr elim (IH … DIVr);
     568      whd in ⊢ (? → ? → ??%? → ?);
     569      cases md';
     570      [ cases dv'; normalize;
     571        [ #H destruct
     572        | #dv'' #Hr1 #Hr2 >(pos_nonzero …) #H destruct % /2/
     573        ]
     574      | cases dv'; [ 2: #dv'' ] @succ_elim
     575          normalize; #n #md'' #Hr1 #Hr2
     576          lapply (plt_lt … Hr2); #Hr2'
     577          lapply (partial_minus_to_Prop md'' n);
     578          cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
     579          #lt #e destruct % [ /3/ | *: /2/ ] @plt_pos
     580          [ 1,3,5,7: @double_lt1 /2/;
     581          | 2,4: @double_lt3 /2/;
     582          | *: @double_lt2 /2/;
     583          ]
     584      ]
     585  | #m' #IH #dv #md whd in ⊢ (??%? → ?);
     586      lapply (refl ? (divide m' (succ n')));
     587      elim (divide m' (succ n')) in ⊢ (???% → % → ?);
     588      #dv' #md' #DIVr elim (IH … DIVr);
     589      whd in ⊢ (? → ? → ??%? → ?); cases md';
     590      [ cases dv'; normalize;
     591        [ #H destruct;
     592        | #dv'' #Hr1 #Hr2 #H destruct; /3/;
     593        ]
     594      | (*cases dv'; [ 2: #dv'' ] @succ_elim
     595          normalize; #n #md'' #Hr1 #Hr2 *) #md'' #Hr1 #Hr2
     596          lapply (plt_lt … Hr2); #Hr2'
     597          whd in ⊢ (??%? → ?);
     598          lapply (partial_minus_to_Prop (p0 md'') (succ n'));
     599          cases (partial_minus (p0 md'') (succ n')); [ 3(*,6,9,12*): #r'' ]
     600          cases dv' in Hr1 ⊢ %; [ 2,4,6: #dv'' ] normalize
     601          #Hr1 destruct [ 1,2,3: >(p0_plus ? md'') ]
     602          #lt #e [ 1,3,4,6: >lt ]
     603          <(pair_eq1 ?????? e) <(pair_eq2 ?????? e)
     604          normalize in ⊢ (?(???%)?); % /2/; @plt_pos
     605          [ cut (succ n' + r'' < p0 (succ n')); /2/;
     606          | cut (succ n' + r'' < p0 (succ n')); /2/;
     607          | /2/;
     608          | /2/;
     609          ]
     610      ]
     611  ]
     612] qed.
     613
     614lemma mod0_divides: ∀m,n,dv:Pos.
    615615  divide n m = 〈ppos dv,pzero〉 → m∣n.
    616 #m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *;
    617 nnormalize; #H; ndestruct; //;
    618 nqed.
    619 
    620 nlemma divides_mod0: ∀dv,m,n:Pos.
     616#m #n #dv #DIVIDE %{dv} lapply (divide_ok … DIVIDE) *; (* XXX: need ; or it eats normalize *)
     617normalize #H destruct //
     618qed.
     619
     620lemma divides_mod0: ∀dv,m,n:Pos.
    621621  n = dv*m → divide n m = 〈ppos dv,pzero〉.
    622 #dv;#m;#n;#DIV;nlapply (refl ? (divide n m));
    623 nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE;
    624 nlapply (divide_ok … DIVIDE); *;
    625 ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]
    626 ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE;  nnormalize;
    627 nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct;
    628 ##[ nlapply (plus_to_minus … e0);
    629     nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …);
    630     ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt;
    631     nrewrite > (minus_times_distrib_l …); //;
    632 
    633  (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
    634     #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind;
    635     napply (absurd ? B (lt_to_not_le … A));
    636 
    637 ##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/;
    638 
    639 ##| nrewrite > DIVIDE; ncut (dv = dv''); /2/;
    640 ##]
    641 nqed.
    642 
    643 nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
    644 #m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
    645 #dv;#md; ncases md; ncases dv;
    646 ##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct
    647 ##| #dv'; #H; @1; napply mod0_divides; /2/;
    648 ##| #md'; #DIVIDES; @2; napply nmk; *; #dv';
    649     nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
    650     nrewrite > DIVIDES; #H';
    651     ndestruct;
    652 ##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv';
    653     nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
    654     nrewrite > DIVIDES; #H';
    655     ndestruct;
    656 ##] nqed.
    657 
    658 ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
    659 #p;#q;ncases p;
    660 ##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##]
    661 ##| ##*: #n; ncases q; nnormalize; /2/;
    662 ##] nqed.
    663 
    664 ndefinition natp_to_Z ≝
     622#dv #m #n #DIV lapply (refl ? (divide n m));
     623elim (divide n m) in ⊢ (???% → ?); #dv' #md' #DIVIDE
     624lapply (divide_ok … DIVIDE); *;
     625cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ]
     626cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
     627>DIV in ⊢ (% → ?) #H #lt destruct;
     628[ lapply (plus_to_minus … e0);
     629    >(commutative_times …) >(commutative_times dv'' …)
     630    cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt
     631    >(minus_times_distrib_l …) //;
     632
     633 (*cut (0 < dv-dv'); [ lapply (not_le_to_lt … nle); /2/ ]
     634    #Hdv *) #H' cut (md'' ≥ m); /2/; lapply (plt_lt … lt); #A #B @False_ind
     635    @(absurd ? B (lt_to_not_le … A))
     636
     637| @False_ind @(absurd ? (plt_lt … lt) ?) /2/;
     638
     639| >DIVIDE cut (dv = dv''); /2/;
     640]
     641qed.
     642
     643lemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
     644#m #n lapply (refl ? (divide n m)); elim (divide n m) in ⊢ (???% → %);
     645#dv #md cases md; cases dv;
     646[ #DIVIDES lapply (divide_ok … DIVIDES); *; normalize; #H destruct
     647| #dv' #H %1 @mod0_divides /2/;
     648| #md' #DIVIDES %2 @nmk *; #dv'
     649    >(commutative_times …) #H lapply (divides_mod0 … H);
     650    >DIVIDES #H'
     651    destruct;
     652| #md' #dv' #DIVIDES %2 @nmk *; #dv'
     653    >(commutative_times …) #H lapply (divides_mod0 … H);
     654    >DIVIDES #H'
     655    destruct;
     656] qed.
     657
     658theorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
     659#p #q cases p;
     660[ cases q; normalize; [ %2 /2/; | *: #m %2 /2/; ]
     661| *: #n cases q; normalize; /2/;
     662] qed.
     663
     664definition natp_to_Z ≝
    665665λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
    666666
    667 ndefinition natp_to_negZ ≝
     667definition natp_to_negZ ≝
    668668λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].
    669669
    670670(* TODO: check these definitions are right.  They are supposed to be the same
    671671   as Zdiv/Zmod in Coq. *)
    672 ndefinition divZ ≝ λx,y.
     672definition divZ ≝ λx,y.
    673673  match x with
    674674  [ OZ ⇒ OZ
     
    677677    [ OZ ⇒ OZ
    678678    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
    679     | neg m ⇒ match divide n m with [ mk_pair q r ⇒
     679    | neg m ⇒ match divide n m with [ pair q r ⇒
    680680                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
    681681    ]
     
    683683    match y with
    684684    [ OZ ⇒ OZ
    685     | pos m ⇒ match divide n m with [ mk_pair q r ⇒
     685    | pos m ⇒ match divide n m with [ pair q r ⇒
    686686                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
    687687    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
     
    689689  ].
    690690
    691 ndefinition modZ ≝ λx,y.
     691definition modZ ≝ λx,y.
    692692  match x with
    693693  [ OZ ⇒ OZ
     
    696696    [ OZ ⇒ OZ
    697697    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
    698     | neg m ⇒ match divide n m with [ mk_pair q r ⇒
     698    | neg m ⇒ match divide n m with [ pair q r ⇒
    699699                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
    700700    ]
     
    702702    match y with
    703703    [ OZ ⇒ OZ
    704     | pos m ⇒ match divide n m with [ mk_pair q r ⇒
     704    | pos m ⇒ match divide n m with [ pair q r ⇒
    705705                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
    706706    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
     
    713713interpretation "integer modulus" 'module m n = (modZ m n).
    714714
    715 nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
    716 #x y; ncases y;
    717 ##[ #H; napply (False_ind … H);
    718 ##| #m; #_; ncases x; //; #n;
    719     nwhd in ⊢ (?%?);
    720     nlapply (pos_compare_to_Prop n m);
    721     ncases (pos_compare n m); /2/;
    722     #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/;
    723 ##| #m H; napply (False_ind … H);
    724 ##] nqed.
    725 
    726 nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
    727 #n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);
    728 ##[ //;
    729 ##| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/;
    730 ##] nqed.
    731 
    732 ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
    733 #x y; ncases y;
    734 ##[ #H; napply (False_ind … H);
    735 ##| #m; #_; ncases x;
    736   ##[ @;//;
    737   ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
    738       ncases (divide n m) in ⊢ (???% → %); #dv md H;
    739       nelim (divide_ok … H); #e l; nelim l; /2/;
    740   ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
    741       ncases (divide n m) in ⊢ (???% → %); #dv md H;
    742       nelim (divide_ok … H); #e l; nelim l;
    743       ##[ /2/;
    744       ##| #md' m' l'; @;
    745         ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
    746             nrewrite > (pos_compare_lt … l'); //;
    747         ##| napply Zminus_Zlt; //;
    748         ##]
    749       ##]
    750   ##]
    751 ##| #m H; napply (False_ind … H);
    752 ##] nqed.
     715lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
     716#x #y cases y;
     717[ #H @(False_ind … H)
     718| #m #_ cases x; //; #n
     719    whd in ⊢ (?%?);
     720    lapply (pos_compare_to_Prop n m);
     721    cases (pos_compare n m); /2/
     722    #lt whd <(minus_Sn_m … lt) /2/;
     723| #m #H @(False_ind … H)
     724] qed.
     725
     726lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
     727#n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m);
     728[ //;
     729| 2,3: #H @False_ind @(absurd ? lt ?) /3/;
     730] qed.
     731
     732theorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
     733#x #y cases y;
     734[ #H @(False_ind … H)
     735| #m #_ cases x;
     736  [ % //;
     737  | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
     738      cases (divide n m) in ⊢ (???% → %); #dv #md #H
     739      elim (divide_ok … H); #e #l elim l; /2/;
     740  | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
     741      cases (divide n m) in ⊢ (???% → %); #dv #md #H
     742      elim (divide_ok … H); #e #l elim l;
     743      [ /2/;
     744      | #md' #m' #l' %
     745        [ whd in ⊢ (??%); >(pos_compare_n_m_m_n …)
     746            >(pos_compare_lt … l') //;
     747        | @Zminus_Zlt //;
     748        ]
     749      ]
     750  ]
     751| #m #H @(False_ind … H)
     752] qed.
Note: See TracChangeset for help on using the changeset viewer.