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

Port Clight semantics to the new-new matita syntax.

Location:
Deliverables/D3.1/C-semantics/binary
Files:
2 edited

Legend:

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

    r400 r487  
    1616   comments may no longer be applicable. *)
    1717
    18 include "arithmetics/compare.ma".
     18(*include "arithmetics/compare.ma".*)
    1919include "binary/positive.ma".
    2020
    21 ninductive Z : Type
     21inductive Z : Type[0]
    2222  OZ  : Z
    2323| pos : Pos → Z
    2424| neg : Pos → Z.
    2525
    26 interpretation "Integers" 'Z = Z.
    27 
    28 ndefinition Z_of_nat ≝
     26(*interpretation "Integers" 'D = Z.*)
     27
     28definition Z_of_nat ≝
    2929λn. match n with
    3030[ O ⇒ OZ
    3131| S n ⇒ pos (succ_pos_of_nat n)].
    3232
    33 ncoercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z.
    34 
    35 ndefinition neg_Z_of_nat \def
     33coercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z.
     34
     35definition neg_Z_of_nat \def
    3636λn. match n with
    3737[ O ⇒ OZ
    3838| S n ⇒ neg (succ_pos_of_nat n)].
    3939
    40 ndefinition abs ≝
     40definition abs ≝
    4141λz.match z with
    4242[ OZ ⇒ O
     
    4444| neg n ⇒ nat_of_pos n].
    4545
    46 ndefinition OZ_test ≝
     46definition OZ_test ≝
    4747λz.match z with
    4848[ OZ ⇒ true
     
    5050| neg _ ⇒ false].
    5151
    52 ntheorem OZ_test_to_Prop : ∀z:Z.
     52theorem OZ_test_to_Prop : ∀z:Z.
    5353  match OZ_test z with
    5454  [true ⇒ z=OZ
    5555  |false ⇒ z ≠ OZ].
    56 #z;ncases z
    57 ##[napply refl
    58 ##|##*:#z1;napply nmk;#H;ndestruct]
    59 nqed.
     56#z cases z
     57[ @refl
     58|*:#z1 @nmk #H destruct]
     59qed.
    6060
    6161(* discrimination *)
    62 ntheorem injective_pos: injective Pos Z pos.
    63 #n;#m;#H;ndestruct;//;
    64 nqed.
     62theorem injective_pos: injective Pos Z pos.
     63#n #m #H destruct //
     64qed.
    6565
    6666(* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
    6767\def injective_pos. *)
    6868
    69 ntheorem injective_neg: injective Pos Z neg.
    70 #n;#m;#H;ndestruct;//;
    71 nqed.
     69theorem injective_neg: injective Pos Z neg.
     70#n #m #H destruct //
     71qed.
    7272
    7373(* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
    7474\def injective_neg. *)
    7575
    76 ntheorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n.
    77 #n;napply nmk;#H;ndestruct;
    78 nqed.
    79 
    80 ntheorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n.
    81 #n;napply nmk;#H;ndestruct;
    82 nqed.
    83 
    84 ntheorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m.
    85 #n;#m;napply nmk;#H;ndestruct;
    86 nqed.
    87 
    88 ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
    89 #x;#y;ncases x;
    90 ##[ncases y;
    91    ##[@;//
    92    ##|##*:#n;@2;napply nmk;#H;ndestruct]
    93 ##|#n;ncases y;
    94    ##[@2;napply nmk;#H;ndestruct;
    95    ##|#m;ncases (decidable_eq_pos n m);#H;
    96       ##[nrewrite > H;@;//
    97       ##|@2;napply nmk;#H2;nelim H;
    98          (* bug if you don't introduce H3 *)#H3;ndestruct;
    99          napply H3;@]
    100    ##|#m;@2;napply nmk;#H;ndestruct]
    101 ##|#n;ncases y;
    102    ##[@2;napply nmk;#H;ndestruct;
    103    ##|#m;@2;napply nmk;#H;ndestruct
    104    ##|#m;ncases (decidable_eq_pos n m);#H;
    105       ##[nrewrite > H;@;//
    106       ##|@2;napply nmk;#H2;nelim H;#H3;ndestruct;
    107          napply H3;@]##]##]
    108 nqed.
    109 
    110 ndefinition Zsucc ≝
     76theorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n.
     77#n @nmk #H destruct;
     78qed.
     79
     80theorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n.
     81#n @nmk #H destruct;
     82qed.
     83
     84theorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m.
     85#n #m @nmk #H destruct;
     86qed.
     87
     88theorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
     89#x #y cases x;
     90[cases y;
     91   [% //
     92   |*:#n %2 @nmk #H destruct]
     93|#n cases y;
     94   [%2 @nmk #H destruct;
     95   |#m cases (decidable_eq_pos n m) #H
     96      [>H % //
     97      |%2 @(not_to_not … H) #E destruct @refl
     98      ]
     99   |#m %2 @nmk #H destruct]
     100|#n cases y;
     101   [%2 @nmk #H destruct;
     102   |#m %2 @nmk #H destruct
     103   |#m cases (decidable_eq_pos n m);#H
     104      [>H % //
     105      |%2 @(not_to_not … H) #E destruct @refl
     106]]]
     107qed.
     108
     109definition Zsucc ≝
    111110λz. match z with
    112111[ OZ ⇒ pos one
     
    117116          | _ ⇒ neg (pred n)]].
    118117
    119 ndefinition Zpred ≝
     118definition Zpred ≝
    120119λz. match z with
    121120[ OZ ⇒ neg one
     
    126125| neg n ⇒ neg (succ n)].
    127126
    128 nlemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))).
    129 //; nqed.
    130 
    131 ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.
    132 #z;ncases z;
    133 ##[ //
    134 ##| #n; nnormalize; ncases n; /2/;
    135 ##| #n; ncases n; //; #n';
    136     nrewrite > (pred_succ_unfold_hack …); nrewrite < (succ_pred_n …); //;
    137     @; #H; ndestruct;
    138 nqed.
    139 
    140 nlemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))).
    141 //; nqed.
    142 
    143 ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.
    144 #z;ncases z
    145 ##[ //
    146 ##| #n; ncases n;//; #n';
    147     nrewrite > (succ_pred_unfold_hack …); nrewrite < (succ_pred_n …); //;
    148     @; #H; ndestruct;
    149 ##| #n; ncases n;/3/;
    150 ##]
    151 nqed.
    152 
    153 nlet rec Zle (x:Z) (y:Z) on x : Prop ≝
     127lemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))).
     128//; qed.
     129
     130theorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.
     131#z cases z;
     132[ //
     133| #n normalize; cases n; /2/;
     134| #n cases n; //; #n'
     135    >(pred_succ_unfold_hack …) <(succ_pred_n …) //;
     136    % #H destruct;
     137qed.
     138
     139lemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))).
     140//; qed.
     141
     142theorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.
     143#z cases z
     144[ //
     145| #n cases n;//; #n'
     146    >(succ_pred_unfold_hack …) <(succ_pred_n …) //;
     147    % #H destruct;
     148| #n cases n;/3/;
     149]
     150qed.
     151
     152let rec Zle (x:Z) (y:Z) on x : Prop ≝
    154153  match x with
    155154  [ OZ ⇒
     
    172171interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
    173172
    174 nlet rec Zlt (x:Z) (y:Z) on x : Prop ≝
     173let rec Zlt (x:Z) (y:Z) on x : Prop ≝
    175174  match x with
    176175  [ OZ ⇒
     
    193192interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
    194193
    195 ntheorem irreflexive_Zlt: irreflexive Z Zlt.
    196 #x;ncases x
    197 ##[napply nmk;//
    198 ##|##*:#n;napply (not_le_succ_n n) (* XXX: auto?? *)]
    199 nqed.
     194theorem irreflexive_Zlt: irreflexive Z Zlt.
     195#x cases x
     196[@nmk //
     197|*:#n @(not_le_succ_n n) (* XXX: auto?? *)]
     198qed.
    200199
    201200(* transitivity *)
    202 ntheorem transitive_Zle : transitive Z Zle.
    203 #x;#y;#z;ncases x
    204 ##[ncases y
    205    ##[//
    206    ##|##*:#n;ncases z;//]
    207 ##|#n;ncases y
    208    ##[#H;ncases H
    209    ##|(*##*:#m;#Hl;ncases z;//;*)
    210       #m;#Hl;ncases z;//;#p;#Hr;
    211       napply (transitive_le n m p);//; (* XXX: auto??? *)
    212    ##|#m;#Hl;ncases Hl]
    213 ##|#n;ncases y
    214    ##[#Hl;ncases z
    215       ##[##1,2://
    216       ##|#m;#Hr;ncases Hr]
    217    ##|#m;#Hl;ncases z;
    218       ##[##1,2://
    219       ##|#p;#Hr;ncases Hr]
    220    ##|#m;#Hl;ncases z;//;#p;#Hr;
    221       napply (transitive_le p m n);//; (* XXX: auto??? *) ##]
    222 nqed.
     201theorem transitive_Zle : transitive Z Zle.
     202#x #y #z cases x
     203[cases y
     204   [//
     205   |*:#n cases z;//]
     206|#n cases y
     207   [#H cases H
     208   |(**:#m #Hl cases z;//;*)
     209      #m #Hl cases z;//;#p #Hr
     210      @(transitive_le n m p) //; (* XXX: auto??? *)
     211   |#m #Hl cases Hl]
     212|#n cases y
     213   [#Hl cases z
     214      [1,2://
     215      |#m #Hr cases Hr]
     216   |#m #Hl cases z;
     217      [1,2://
     218      |#p #Hr cases Hr]
     219   |#m #Hl cases z;//;#p #Hr
     220      @(transitive_le p m n) //; (* XXX: auto??? *) ]
     221qed.
    223222
    224223(* variant trans_Zle: transitive Z Zle
    225224\def transitive_Zle.*)
    226225
    227 ntheorem transitive_Zlt: transitive Z Zlt.
    228 #x;#y;#z;ncases x
    229 ##[ncases y
    230    ##[//
    231    ##|#n;ncases z
    232       ##[#_;#Hr;ncases Hr
    233       ##|//
    234       ##|#m;#_;#Hr;ncases Hr]
    235    ##|#n;#Hl;ncases Hl]
    236 ##|#n;ncases y
    237    ##[#Hl;ncases Hl
    238    ##|#m;ncases z
    239       ##[//
    240       ##|#p;napply transitive_lt (* XXX: auto??? *)
    241       ##|//##]
    242    ##|#m;#Hl;ncases Hl]
    243 ##|#n;ncases y
    244    ##[ncases z;
    245       ##[##1,2://
    246       ##|#m;#_;#Hr;ncases Hr]
    247    ##|#m;ncases z;
    248       ##[##1,2://
    249       ##|#p;#_;#Hr;ncases Hr]
    250    ##|#m;ncases z
    251       ##[##1,2://
    252       ##|#p;#Hl;#Hr;napply (transitive_lt … Hr Hl)]
    253    ##]
    254 ##]
    255 nqed.     
     226theorem transitive_Zlt: transitive Z Zlt.
     227#x #y #z cases x
     228[cases y
     229   [//
     230   |#n cases z
     231      [#_ #Hr cases Hr
     232      |//
     233      |#m #_ #Hr cases Hr]
     234   |#n #Hl cases Hl]
     235|#n cases y
     236   [#Hl cases Hl
     237   |#m cases z
     238      [//
     239      |#p apply transitive_lt (* XXX: auto??? *)
     240      |//]
     241   |#m #Hl cases Hl]
     242|#n cases y
     243   [cases z;
     244      [1,2://
     245      |#m #_ #Hr cases Hr]
     246   |#m cases z;
     247      [1,2://
     248      |#p #_ #Hr cases Hr]
     249   |#m cases z
     250      [1,2://
     251      |#p #Hl #Hr apply (transitive_lt … Hr Hl)]
     252   ]
     253]
     254qed.     
    256255
    257256(* variant trans_Zlt: transitive Z Zlt
     
    260259\def irreflexive_Zlt.*)
    261260
    262 ntheorem Zlt_neg_neg_to_lt:
     261theorem Zlt_neg_neg_to_lt:
    263262  ∀n,m:Pos. neg n < neg m → m < n.
    264263//;
    265 nqed.
    266 
    267 ntheorem lt_to_Zlt_neg_neg: ∀n,m:Pos.m < n → neg n < neg m.
     264qed.
     265
     266theorem lt_to_Zlt_neg_neg: ∀n,m:Pos.m < n → neg n < neg m.
    268267//;
    269 nqed.
    270 
    271 ntheorem Zlt_pos_pos_to_lt:
     268qed.
     269
     270theorem Zlt_pos_pos_to_lt:
    272271  ∀n,m:Pos. pos n < pos m → n < m.
    273272//;
    274 nqed.
    275 
    276 ntheorem lt_to_Zlt_pos_pos: ∀n,m:Pos.n < m → pos n < pos m.
     273qed.
     274
     275theorem lt_to_Zlt_pos_pos: ∀n,m:Pos.n < m → pos n < pos m.
    277276//;
    278 nqed.
    279 
    280 nlemma Zsucc_neg_succ: ∀n:Pos. Zsucc (neg (succ n)) = neg n.
    281 #n; nnormalize; nrewrite < (pred_succ_n n); ncases n; //; nqed.
    282 
    283 ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
    284 #x;#y;ncases x
    285 ##[ncases y
    286    ##[#H;ncases H
    287    ##|//;
    288    ##|#p;#H;ncases H]
    289 ##|#n;ncases y
    290    ##[#H;ncases H
    291    ##|#p;nnormalize;//
    292    ##|#p;#H;ncases H]
    293 ##|#n;ncases y
    294    ##[##1,2:ncases n;//
    295    ##|#p;napply (pos_cases … n);
    296       ##[#H;nelim (not_le_succ_one p);#H2;napply H2;napply H (*//;*) (* XXX: auto? *)
    297       ##|#m;nrewrite > (Zsucc_neg_succ m);napply le_S_S_to_le; (* XXX: auto? *)
    298       ##]
    299    ##]
    300 ##]
    301 nqed.
     277qed.
     278
     279lemma Zsucc_neg_succ: ∀n:Pos. Zsucc (neg (succ n)) = neg n.
     280#n normalize; <(pred_succ_n n) cases n; //; qed.
     281
     282theorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
     283#x #y cases x
     284[cases y
     285   [#H cases H
     286   |//;
     287   |#p #H cases H]
     288|#n cases y
     289   [#H cases H
     290   |#p normalize;//
     291   |#p #H cases H]
     292|#n cases y
     293   [1,2:cases n;//
     294   |#p @(pos_cases … n)
     295      [#H elim (not_le_succ_one p);#H2 @H2 @H (*// *) (* XXX: auto? *)
     296      |#m >(Zsucc_neg_succ m) @le_S_S_to_le (* XXX: auto? *)
     297      ]
     298   ]
     299]
     300qed.
    302301
    303302(*** COMPARE ***)
    304303
    305304(* boolean equality *)
    306 nlet rec eqZb (x:Z) (y:Z) on x : bool ≝
     305let rec eqZb (x:Z) (y:Z) on x : bool ≝
    307306  match x with
    308307  [ OZ ⇒
     
    322321        | neg q ⇒ eqb p q]].
    323322
    324 ntheorem eqZb_to_Prop:
     323theorem eqZb_to_Prop:
    325324  ∀x,y:Z.
    326325    match eqZb x y with
    327326    [ true ⇒ x=y
    328327    | false ⇒ x ≠ y].
    329 #x;#y;ncases x
    330 ##[ncases y;
    331    ##[//
    332    ##|napply not_eq_OZ_pos (* XXX: auto? *)
    333    ##|napply not_eq_OZ_neg (* XXX: auto? *)]
    334 ##|#n;ncases y;
    335    ##[napply nmk;#H;nelim (not_eq_OZ_pos n);#H2;/2/;
    336    ##|#m;napply eqb_elim;
    337       ##[//
    338       ##|#H;napply nmk;#H2;nelim H;#H3;ndestruct;/2/]
    339    ##|#m;napply not_eq_pos_neg]
    340 ##|#n;ncases y
    341    ##[napply nmk;#H;nelim (not_eq_OZ_neg n);#H;/2/;
    342    ##|#m;napply nmk;#H;ndestruct
    343    ##|#m;napply eqb_elim;
    344       ##[//
    345       ##|#H;napply nmk;#H2;ndestruct;nelim H;/2/]
    346    ##]
    347 ##]
    348 nqed.
    349 
    350 ntheorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop.
     328#x #y cases x
     329[cases y;
     330   [//
     331   |@not_eq_OZ_pos (* XXX: auto? *)
     332   |@not_eq_OZ_neg (* XXX: auto? *)]
     333|#n cases y;
     334   [@nmk #H elim (not_eq_OZ_pos n);#H2 /2/;
     335   |#m @eqb_elim
     336      [//
     337      | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
     338      ]
     339   |#m @not_eq_pos_neg]
     340|#n cases y
     341   [@nmk #H elim (not_eq_OZ_neg n);#H /2/;
     342   |#m @nmk #H destruct
     343   |#m @eqb_elim
     344      [//
     345      | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
     346   ]
     347]
     348qed.
     349
     350theorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop.
    351351  (x=y → P true) → (x ≠ y → P false) → P (eqZb x y).
    352 #x;#y;#P;#HP1;#HP2;
    353 ncut
     352#x #y #P #HP1 #HP2
     353cut
    354354(match (eqZb x y) with
    355355[ true ⇒ x=y
    356356| false ⇒ x ≠ y] → P (eqZb x y))
    357 ##[ncases (eqZb x y);nnormalize; (* XXX: auto?? *)
    358    ##[napply HP1
    359    ##|napply HP2]
    360 ##|#Hcut;napply Hcut;napply eqZb_to_Prop]
    361 nqed.
    362 
    363 nlet rec Z_compare (x:Z) (y:Z) : compare ≝
     357[cases (eqZb x y);normalize; (* XXX: auto?? *)
     358   [@HP1
     359   |@HP2]
     360|#Hcut @Hcut @eqZb_to_Prop]
     361qed.
     362
     363let rec Z_compare (x:Z) (y:Z) : compare ≝
    364364  match x with
    365365  [ OZ ⇒
     
    379379    | neg m ⇒ pos_compare m n ]].
    380380
    381 ntheorem Z_compare_to_Prop :
     381theorem Z_compare_to_Prop :
    382382∀x,y:Z. match (Z_compare x y) with
    383383[ LT ⇒ x < y
    384384| EQ ⇒ x=y
    385385| GT ⇒ y < x].
    386 #x;#y;nelim x
    387 ##[nelim y;//;
    388 ##|nelim y
    389    ##[##1,3://
    390    ##|#n;#m;nnormalize;
    391       ncut (match (pos_compare m n) with
     386#x #y elim x
     387[elim y;//;
     388|elim y
     389   [1,3://
     390   |#n #m normalize;
     391      cut (match (pos_compare m n) with
    392392      [ LT ⇒ m < n
    393393      | EQ ⇒ m = n
     
    397397      | EQ ⇒ pos m = pos n
    398398      | GT ⇒ (succ n)  ≤ m])
    399       ##[ncases (pos_compare m n);//
    400       ##|#Hcut;napply Hcut;napply pos_compare_to_Prop]
    401    ##]
    402 ##|nelim y
    403    ##[#n;//
    404    ##|nnormalize;//
    405    ##|nnormalize;#n;#m;
    406       ncut (match (pos_compare n m) with
     399      [cases (pos_compare m n);//
     400      |#Hcut @Hcut @pos_compare_to_Prop]
     401   ]
     402|elim y
     403   [#n //
     404   |normalize;//
     405   |normalize;#n #m
     406      cut (match (pos_compare n m) with
    407407        [ LT ⇒ n < m
    408408        | EQ ⇒ n = m
     
    412412      | EQ ⇒ neg m = neg n
    413413      | GT ⇒ (succ m) ≤ n])
    414       ##[ncases (pos_compare n m);//
    415       ##|#Hcut;napply Hcut;napply pos_compare_to_Prop]
    416    ##]
    417 ##]
    418 nqed.
    419 
    420 nlet rec Zplus (x:Z) (y:Z) on x : Z ≝
     414      [cases (pos_compare n m);//
     415      |#Hcut @Hcut @pos_compare_to_Prop]
     416   ]
     417]
     418qed.
     419
     420let rec Zplus (x:Z) (y:Z) on x : Z ≝
    421421  match x with
    422422    [ OZ ⇒ y
     
    442442interpretation "integer plus" 'plus x y = (Zplus x y).
    443443
    444 ntheorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.
    445 #n;#m;ncases n
    446 ##[//
    447 ##|#p;ncases m
    448    ##[nnormalize;//
    449    ##|#m';nnormalize;nrewrite > (nat_plus_pos_plus …);nrewrite > (succ_nat_pos ?);/2/]
    450 nqed.
    451 
    452 ntheorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m.
    453 //; nqed.
    454 
    455 ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
    456 #z;ncases z;//;
    457 nqed.
    458 
    459 ntheorem sym_Zplus : ∀x,y:Z. x+y = y+x.
    460 #x;#y;ncases x;
    461 ##[nrewrite > (Zplus_z_OZ ?) (*XXX*);//
    462 ##|#p;ncases y
    463    ##[//
    464    ##|nnormalize;//
    465    ##|#q;nnormalize;nrewrite > (pos_compare_n_m_m_n ??) (*XXX*);
    466       ncases (pos_compare q p);//]
    467 ##|#p;ncases y
    468    ##[//;
    469    ##|#q;nnormalize;nrewrite > (pos_compare_n_m_m_n ??) (*XXX*);
    470       ncases (pos_compare q p);//
    471    ##|nnormalize;//]
    472 ##]
    473 nqed.
    474 
    475 ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z.
    476 #z;ncases z
    477 ##[//
    478 ##|##*:#n;ncases n;//]
    479 nqed.
    480 
    481 ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z.
    482 #z;ncases z
    483 ##[//
    484 ##|##*:#n;ncases n;//]
    485 nqed.
    486 
    487 nlemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n.
    488 #n; nnormalize; ncases n; /2/; nqed.
    489 
    490 ntheorem Zplus_pos_pos:
     444theorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.
     445#n #m cases n
     446[//
     447|#p cases m
     448   [normalize;//
     449   |#m' normalize;>(nat_plus_pos_plus …) >(succ_nat_pos ?) /2/]
     450qed.
     451
     452theorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m.
     453//; qed.
     454
     455theorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
     456#z cases z;//;
     457qed.
     458
     459theorem sym_Zplus : ∀x,y:Z. x+y = y+x.
     460#x #y cases x;
     461[>(Zplus_z_OZ ?) (*XXX*) //
     462|#p cases y
     463   [//
     464   |normalize;//
     465   |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*)
     466      cases (pos_compare q p);//]
     467|#p cases y
     468   [//;
     469   |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*)
     470      cases (pos_compare q p);//
     471   |normalize;//]
     472]
     473qed.
     474
     475theorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z.
     476#z cases z
     477[//
     478|*:#n cases n;//]
     479qed.
     480
     481theorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z.
     482#z cases z
     483[//
     484|*:#n cases n;//]
     485qed.
     486
     487lemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n.
     488#n normalize; cases n; /2/; qed.
     489
     490theorem Zplus_pos_pos:
    491491  ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
    492 #n;#m;napply (pos_cases … n);
    493 ##[ napply (pos_cases … m); //;
    494 ##|#p;napply (pos_cases … m);
    495    ##[nnormalize; nrewrite < (succ_plus_one …); //;
    496    ##|#q; nrewrite > (Zsucc_Zplus_pos_O …); nrewrite > (Zpred_pos_succ ?);
    497       nnormalize; /2/;
    498    ##]
    499 ##]
    500 nqed.
    501 
    502 ntheorem Zplus_pos_neg:
     492#n #m @(pos_cases … n)
     493[ @(pos_cases … m) //;
     494|#p @(pos_cases … m)
     495   [normalize; <(succ_plus_one …) //;
     496   |#q >(Zsucc_Zplus_pos_O …) >(Zpred_pos_succ ?)
     497      normalize; /2/;
     498   ]
     499]
     500qed.
     501
     502theorem Zplus_pos_neg:
    503503  ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
    504 #n m;
    505 nnormalize;
    506 nrewrite < (pos_compare_S_S …);
    507 nrewrite > (partialminus_S_S …);
    508 nrewrite > (partialminus_S_S …); //;
    509 nqed.
    510 
    511 nlemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q | p0 p ⇒ P n | p1 p ⇒ P n ] = P n.
    512 #A P Q n; napply succ_elim; //; nqed.
    513 
    514 nlemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n.
    515 #n; ncases n; //;
    516 #n'; nwhd in ⊢ (??%?); nnormalize; nrewrite < (pred_succ_n …);
    517 napply succ_elim; //; nqed.
    518 
    519 ntheorem Zplus_neg_pos :
     504#n #m
     505normalize;
     506<(pos_compare_S_S …)
     507>(partialminus_S_S …)
     508>(partialminus_S_S …) //;
     509qed.
     510
     511lemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q | p0 p ⇒ P n | p1 p ⇒ P n ] = P n.
     512#A #P #Q #n @succ_elim //; qed.
     513
     514lemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n.
     515#n cases n; //;
     516#n' whd in ⊢ (??%?); normalize; <(pred_succ_n …)
     517@succ_elim //; qed.
     518
     519theorem Zplus_neg_pos :
    520520  ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
    521 #n m; napply (pos_cases … n); napply (pos_cases … m);
    522 ##[ //;
    523 ##| #m'; nrewrite > (Zpred_pos_succ …);
    524     nrewrite > (?:pos (succ m') = Zsucc (pos m')); //;
    525 ##| #m'; nnormalize; nrewrite > (pos_compare_S_one …); nnormalize;
    526     nrewrite > (partial_minus_S_one …); nnormalize; nrewrite > (pos_nonzero …);
    527     nrewrite < (pred_succ_n …); //;
    528 ##| #m'; #n'; nnormalize; nrewrite < (pos_compare_S_S …);
    529     nrewrite > (partialminus_S_S …);
    530     nrewrite > (partialminus_S_S …);
    531     nrewrite > (pos_nonzero …);
    532     nrewrite > (pos_nonzero …);
    533     nrewrite < (pred_succ_n …);
    534     nrewrite < (pred_succ_n …);
    535     nnormalize; //;
    536 ##] nqed.
    537 
    538 ntheorem Zplus_neg_neg:
     521#n #m @(pos_cases … n) @(pos_cases … m)
     522[ //;
     523| #m' >(Zpred_pos_succ …)
     524    >(?:pos (succ m') = Zsucc (pos m')) //;
     525| #m' normalize; >(pos_compare_S_one …) normalize;
     526    >(partial_minus_S_one …) normalize; >(pos_nonzero …)
     527    <(pred_succ_n …) //;
     528| #m' #n' normalize; <(pos_compare_S_S …)
     529    >(partialminus_S_S …)
     530    >(partialminus_S_S …)
     531    >(pos_nonzero …)
     532    >(pos_nonzero …)
     533    <(pred_succ_n …)
     534    <(pred_succ_n …)
     535    normalize; //;
     536] qed.
     537
     538theorem Zplus_neg_neg:
    539539  ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
    540 #n m; napply (pos_cases … n); napply (pos_cases … m);
    541 ##[ ##1,2: //;
    542 ##| #n'; nnormalize in ⊢ (???(?%?));
    543     nrewrite > (pos_nonzero …);
    544     nrewrite < (pred_succ_n …); nnormalize; //;
    545 ##| #m';#n'; nnormalize; nrewrite > (pos_nonzero …);
    546     nrewrite < (pred_succ_n …); nnormalize; //;
    547 ##] nqed.
    548 
    549 ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
    550 #x;#y;ncases x
    551 ##[ncases y
    552    ##[//
    553    ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
    554    ##|#p;nrewrite < (Zsucc_Zplus_pos_O …); //]
    555 ##|ncases y;/2/; #p; nrewrite > (sym_Zplus ? (Zpred OZ));
    556    nrewrite < Zpred_Zplus_neg_O; //;
    557 ##|ncases y
    558    ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
    559       nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
    560    ##|##*:/2/]
    561 nqed.
    562 
    563 ntheorem Zplus_Zsucc_pos_pos :
     540#n #m @(pos_cases … n) @(pos_cases … m)
     541[ 1,2: //;
     542| #n' normalize in ⊢ (???(?%?));
     543    >(pos_nonzero …)
     544    <(pred_succ_n …) normalize; //;
     545| #m' #n' normalize; >(pos_nonzero …)
     546    <(pred_succ_n …) normalize; //;
     547] qed.
     548
     549theorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
     550#x #y cases x
     551[cases y
     552   [//
     553   |#n <(Zsucc_Zplus_pos_O ?) >(Zsucc_Zpred ?) //
     554   |#p <(Zsucc_Zplus_pos_O …) //]
     555|cases y;/2/; #p >(sym_Zplus ? (Zpred OZ))
     556   <Zpred_Zplus_neg_O //;
     557|cases y
     558   [#n <(sym_Zplus ??) <(sym_Zplus (Zpred OZ) ?)
     559      <(Zpred_Zplus_neg_O ?) >(Zpred_Zsucc ?) //
     560   |*:/2/]
     561qed.
     562
     563theorem Zplus_Zsucc_pos_pos :
    564564  ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
    565 #n m;nrewrite > (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zplus_pos_O ?);//;
    566 nqed.
    567 
    568 ntheorem Zplus_Zsucc_pos_neg:
     565#n #m >(Zsucc_Zplus_pos_O ?) >(Zsucc_Zplus_pos_O ?) //;
     566qed.
     567
     568theorem Zplus_Zsucc_pos_neg:
    569569  ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
    570 #n;#m;
    571 napply (pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
    572 ##[#n1;nelim n1
    573    ##[//
    574    ##|##*:#n2;#IH;nelim n2;//]
    575 ##|#n'; nrewrite > (sym_Zplus …); nrewrite < (Zpred_Zplus_neg_O ?);
    576    nrewrite > (sym_Zplus …); nrewrite < (Zpred_Zplus_neg_O ?);
    577    nrewrite > (Zpred_Zsucc …);  /2/
    578 ##|#n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nrewrite > IH;
    579 nrewrite < (Zplus_pos_neg …); //]
    580 nqed.
    581 
    582 ntheorem Zplus_Zsucc_neg_neg :
     570#n #m
     571@(pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
     572[#n1 elim n1
     573   [//
     574   |*:#n2 #IH elim n2;//]
     575|#n' >(sym_Zplus …) <(Zpred_Zplus_neg_O ?)
     576   >(sym_Zplus …) <(Zpred_Zplus_neg_O ?)
     577   >(Zpred_Zsucc …)  /2/
     578|#n1 #m1 #IH <(Zplus_pos_neg ? m1) >IH
     579<(Zplus_pos_neg …) //]
     580qed.
     581
     582theorem Zplus_Zsucc_neg_neg :
    583583  ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
    584 #n;#m;
    585 napply (pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
    586 ##[napply pos_elim;
    587    ##[//
    588    ##|#n2;#IH;nnormalize;nrewrite < (pred_succ_n …); nrewrite > (pos_nonzero …); //]
    589 ##| #n'; nnormalize;
    590    nrewrite > (pos_nonzero …);
    591    nrewrite < (pred_succ_n …); nnormalize;
    592    nrewrite < (succ_plus_one …);
    593    nrewrite < (succ_plus_one …); nrewrite > (pos_nonzero …); //;
    594 ##| #n' m' IH; nnormalize;
    595    nrewrite > (pos_nonzero …); nnormalize;
    596    nrewrite < (pluss_succn_m …);
    597    nrewrite > (pos_nonzero …); //;
    598 ##]
    599 nqed.
    600 
    601 nlemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
    602 #n m; nnormalize; nrewrite < (pos_compare_S_S …);
    603 nrewrite > (partialminus_S_S …);
    604 nrewrite > (partialminus_S_S …);
    605  //; nqed.
    606 
    607 
    608 ntheorem Zplus_Zsucc_neg_pos:
     584#n #m
     585@(pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
     586[@pos_elim
     587   [//
     588   |#n2 #IH normalize;<(pred_succ_n …) >(pos_nonzero …) //]
     589| #n' normalize;
     590   >(pos_nonzero …)
     591   <(pred_succ_n …) normalize;
     592   <(succ_plus_one …)
     593   <(succ_plus_one …) >(pos_nonzero …) //;
     594| #n' #m' #IH normalize;
     595   >(pos_nonzero …) normalize;
     596   <(pluss_succn_m …)
     597   >(pos_nonzero …) //;
     598]
     599qed.
     600
     601lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
     602#n #m normalize; <(pos_compare_S_S …)
     603>(partialminus_S_S …)
     604>(partialminus_S_S …)
     605 //; qed.
     606
     607
     608theorem Zplus_Zsucc_neg_pos:
    609609  ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
    610 #n;#m;
    611 napply (pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m)))
    612 ##[napply pos_elim;
    613    ##[//
    614    ##|#n2;#IH;nnormalize; nrewrite > (pos_nonzero …); nnormalize;
    615       nrewrite > (partial_minus_S_one …); //]
    616 ##| #n';
    617     nrewrite > (sym_Zplus …);
    618     nrewrite < (Zsucc_Zplus_pos_O …);
    619     nrewrite > (sym_Zplus …);
    620     nrewrite < (Zsucc_Zplus_pos_O …); //;
    621 ##|#n' m' IH;
    622    nrewrite > (neg_pos_succ …); //;
    623 ##] nqed.
    624 
    625 ntheorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).
    626 #x;#y;ncases x
    627 ##[ncases y;//;(*#n;nnormalize;ncases n;//;*)
    628 ##|##*:#n;ncases y;//;#m;napply Zplus_Zsucc_neg_pos(* XXX: // didn't work! *)]
    629 nqed.
    630 
    631 ntheorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y).
    632 #x;#y;ncut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y))
    633 ##[nrewrite > (Zsucc_Zpred ?);//
    634 ##|#Hcut;nrewrite > Hcut;nrewrite > (Zplus_Zsucc ??);//]
    635 nqed.
    636 
    637 nlemma eq_rect_Type0_r:
     610#n #m
     611@(pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m)))
     612[@pos_elim
     613   [//
     614   |#n2 #IH normalize; >(pos_nonzero …) normalize;
     615      >(partial_minus_S_one …) //]
     616| #n'
     617    >(sym_Zplus …)
     618    <(Zsucc_Zplus_pos_O …)
     619    >(sym_Zplus …)
     620    <(Zsucc_Zplus_pos_O …) //;
     621|#n' #m' #IH
     622   >(neg_pos_succ …) //;
     623] qed.
     624
     625theorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).
     626#x #y cases x
     627[cases y;//;(*#n normalize;cases n;//;*)
     628|*:#n cases y;//;#m @Zplus_Zsucc_neg_pos(* XXX: // didn't work! *)]
     629qed.
     630
     631theorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y).
     632#x #y cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y))
     633[>(Zsucc_Zpred ?) //
     634|#Hcut >Hcut >(Zplus_Zsucc ??) //]
     635qed.
     636
     637lemma eq_rect_Type0_r:
    638638 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
    639  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ??? p0); nassumption.
    640 nqed.
    641 
    642 ntheorem associative_Zplus: associative Z Zplus.
     639 #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption.
     640qed.
     641
     642theorem associative_Zplus: associative Z Zplus.
    643643(* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
    644 #x;#y;#z;ncases x
    645 ##[//
    646 ##|napply pos_elim;
    647    ##[nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite < (Zsucc_Zplus_pos_O ?);//;
    648    ##|#n1;#IH;
    649       nrewrite > (Zplus_Zsucc (pos n1) ?);nrewrite > (Zplus_Zsucc (pos n1) ?);
    650       nrewrite > (Zplus_Zsucc ((pos n1)+y) ?);//]
    651 ##|napply pos_elim;
    652    ##[nrewrite < (Zpred_Zplus_neg_O (y+z));nrewrite < (Zpred_Zplus_neg_O y);//;
    653    ##|#n1;#IH;
    654       nrewrite > (Zplus_Zpred (neg n1) ?);nrewrite > (Zplus_Zpred (neg n1) ?);
    655       nrewrite > (Zplus_Zpred ((neg n1)+y) ?);//]
    656 ##]
    657 nqed.
     644#x #y #z cases x
     645[//
     646|@pos_elim
     647   [<(Zsucc_Zplus_pos_O ?) <(Zsucc_Zplus_pos_O ?) //;
     648   |#n1 #IH
     649      >(Zplus_Zsucc (pos n1) ?) >(Zplus_Zsucc (pos n1) ?)
     650      >(Zplus_Zsucc ((pos n1)+y) ?) //]
     651|@pos_elim
     652   [<(Zpred_Zplus_neg_O (y+z)) <(Zpred_Zplus_neg_O y) //;
     653   |#n1 #IH
     654      >(Zplus_Zpred (neg n1) ?) >(Zplus_Zpred (neg n1) ?)
     655      >(Zplus_Zpred ((neg n1)+y) ?) //]
     656]
     657qed.
    658658
    659659(* variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
     
    661661
    662662(* Zopp *)
    663 ndefinition Zopp : Z → Z ≝
     663definition Zopp : Z → Z ≝
    664664  λx:Z. match x with
    665665  [ OZ ⇒ OZ
     
    669669interpretation "integer unary minus" 'uminus x = (Zopp x).
    670670
    671 ntheorem eq_OZ_Zopp_OZ : OZ = (- OZ).
     671theorem eq_OZ_Zopp_OZ : OZ = (- OZ).
    672672//;
    673 nqed.
    674 
    675 ntheorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
    676 #x;#y;ncases x
    677 ##[ncases y;//
    678 ##|##*:#n;ncases y;//;#m;nnormalize;napply pos_compare_elim;nnormalize;//]
    679 nqed.
    680 
    681 ntheorem Zopp_Zopp: ∀x:Z. --x = x.
    682 #x;ncases x;//;
    683 nqed.
    684 
    685 ntheorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
    686 #x;ncases x
    687 ##[//
    688 ##|##*:#n;nnormalize;nrewrite > (pos_compare_n_n ?);//]
    689 nqed.
    690 
    691 ntheorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
    692 #x;#z;#y;#H;
    693 nrewrite < (Zplus_z_OZ z);nrewrite < (Zplus_z_OZ y);
    694 nrewrite < (Zplus_Zopp x);
    695 nrewrite < (associative_Zplus ???);nrewrite < (associative_Zplus ???);
     673qed.
     674
     675theorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
     676#x #y cases x
     677[cases y;//
     678|*:#n cases y;//;#m normalize;@pos_compare_elim normalize;//]
     679qed.
     680
     681theorem Zopp_Zopp: ∀x:Z. --x = x.
     682#x cases x;//;
     683qed.
     684
     685theorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
     686#x cases x
     687[//
     688|*:#n normalize;>(pos_compare_n_n ?) //]
     689qed.
     690
     691theorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
     692#x #z #y #H
     693<(Zplus_z_OZ z) <(Zplus_z_OZ y)
     694<(Zplus_Zopp x)
     695<(associative_Zplus ???) <(associative_Zplus ???)
    696696//;
    697 nqed.
    698 
    699 ntheorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
    700 #x;#z;#y;#H;
    701 napply (injective_Zplus_l x);
    702 nrewrite < (sym_Zplus ??);
     697qed.
     698
     699theorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
     700#x #z #y #H
     701@(injective_Zplus_l x)
     702<(sym_Zplus ??)
    703703//;
    704 nqed.
     704qed.
    705705
    706706(* minus *)
    707 ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).
     707definition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).
    708708
    709709interpretation "integer minus" 'minus x y = (Zminus x y).
     
    711711
    712712
    713 ndefinition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n).
    714 ndefinition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n).
    715 ndefinition two_p : Z → Z ≝
     713definition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n).
     714definition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n).
     715definition two_p : Z → Z ≝
    716716λz.match z with
    717717[ OZ ⇒ pos one
  • Deliverables/D3.1/C-semantics/binary/positive.ma

    r10 r487  
    1515(* little endian positive binary numbers. *)
    1616
    17 include "basics/functions.ma".
    18 include "basics/eq.ma".
     17include "basics/logic.ma".
    1918include "arithmetics/nat.ma".
    20 include "arithmetics/compare.ma".
    21 
    22 ninductive Pos : Type ≝
     19include "oldlib/eq.ma".
     20
     21(* arithmetics/comparison.ma --> *)
     22inductive compare : Type[0] ≝
     23| LT : compare
     24| EQ : compare
     25| GT : compare.
     26
     27definition compare_invert: compare → compare ≝
     28  λc.match c with
     29      [ LT ⇒ GT
     30      | EQ ⇒ EQ
     31      | GT ⇒ LT ].
     32
     33(* <-- *)
     34
     35inductive Pos : Type[0] ≝
    2336  | one : Pos
    2437  |  p1 : Pos → Pos
    2538  |  p0 : Pos → Pos.
    2639
    27 nlet rec pred (n:Pos) ≝
     40let rec pred (n:Pos) ≝
    2841  match n with
    2942  [ one ⇒ one
     
    3245  ].
    3346
    34 nremark test : pred (p0 (p0 (p0 one))) = p1 (p1 one).
    35 //; nqed.
    36 
    37 nlet rec succ (n:Pos) ≝
     47example test : pred (p0 (p0 (p0 one))) = p1 (p1 one).
     48//; qed.
     49
     50let rec succ (n:Pos) ≝
    3851  match n with
    3952  [ one ⇒ p0 one
     
    4255  ].
    4356
    44 nlemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n).
    45 #P H0 H1 n; ncases n; nnormalize; //; nqed.
    46 
    47 ntheorem pred_succ_n : ∀n. n = pred (succ n).
    48 #n; nelim n;
    49 ##[ ##1,3: //
    50 ##| #p'; nnormalize; napply succ_elim; /2/;
    51 ##] nqed.
     57lemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n).
     58#P #H0 #H1 #n cases n; normalize; //; qed.
     59
     60theorem pred_succ_n : ∀n. n = pred (succ n).
     61#n elim n;
     62[ 1,3: //
     63| #p' normalize; @succ_elim /2/;
     64] qed.
    5265(*
    53 ntheorem succ_pred_n : ∀n. n≠one → n = succ (pred n).
    54 #n; nelim n;
    55 ##[ #H; napply False_ind; nelim H; /2/;
    56 ##| //;
    57 ##| #n'; ncases n'; /2/; #n''; #IH; #_; nrewrite < IH; nnormalize; 
     66theorem succ_pred_n : ∀n. n≠one → n = succ (pred n).
     67#n elim n;
     68[ #H @False_ind elim H; /2/;
     69| //;
     70| #n' cases n'; /2/; #n'' #IH #_ <IH normalize; 
    5871*)
    59 ntheorem succ_injective: injective Pos Pos succ.
    60 //; nqed.
    61 
    62 nlet rec nat_of_pos (p:Pos) : nat ≝
     72theorem succ_injective: injective Pos Pos succ.
     73//; qed.
     74
     75let rec nat_of_pos (p:Pos) : nat ≝
    6376  match p with
    6477  [ one ⇒ 1
     
    6780  ].
    6881
    69 nlet rec succ_pos_of_nat (n:nat) : Pos ≝
     82let rec succ_pos_of_nat (n:nat) : Pos ≝
    7083  match n with
    7184  [ O ⇒ one
     
    7386  ].
    7487
    75 ntheorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n).
    76 //; nqed.
    77 
    78 ntheorem succ_pos_of_nat_inj: injective ?? succ_pos_of_nat.
    79 #n; nelim n;
    80 ##[ #m; ncases m;
    81   ##[ //
    82   ##| #m'; nnormalize; napply succ_elim; #p H; ndestruct
    83   ##]
    84 ##| #n' IH m; ncases m;
    85   ##[ nnormalize; napply succ_elim; #p H; ndestruct;
    86   ##| nnormalize; #m' H; nrewrite > (IH m' ?); //;
    87   ##]
    88 ##] nqed.
    89 
    90 nremark test2 : nat_of_pos (p0 (p1 one)) = 6. //; nqed.
     88theorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n).
     89//; qed.
     90
     91theorem succ_pos_of_nat_inj: injective ?? succ_pos_of_nat.
     92#n elim n;
     93[ #m cases m;
     94  [ //
     95  | #m' normalize; @succ_elim #p #H destruct
     96  ]
     97| #n' #IH #m cases m;
     98  [ normalize; @succ_elim #p #H destruct;
     99  | normalize; #m' #H >(IH m' ?) //;
     100  ]
     101] qed.
     102
     103example test2 : nat_of_pos (p0 (p1 one)) = 6. //; qed.
    91104
    92105(* Usual induction principle; proof roughly following Coq's,
    93106   apparently due to Conor McBride. *)
    94107
    95 ninductive possucc : Pos → Prop ≝
     108inductive possucc : Pos → Prop ≝
    96109  | psone  : possucc one
    97110  | pssucc : ∀n. possucc n → possucc (succ n).
    98111
    99 nlet rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝
     112let rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝
    100113  match p return λn',p'.possucc (p0 n') with
    101114  [ psone ⇒ pssucc ? psone
     
    103116  ].
    104117
    105 nlet rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝
     118let rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝
    106119  match p return λn',p'. possucc (p1 n') with
    107120  [ psone ⇒ pssucc ? (pssucc ? psone)
     
    109122  ].
    110123
    111 nlet rec possuccinj (n:Pos) : possucc n ≝
     124let rec possuccinj (n:Pos) : possucc n ≝
    112125  match n with
    113126  [ one ⇒ psone
     
    116129  ].
    117130
    118 nlet rec possucc_elim
     131let rec possucc_elim
    119132  (P : Pos → Prop)
    120133  (Pone : P one)
     
    127140  ].
    128141
    129 ndefinition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n.
    130 #P Pone Psucc n; napply (possucc_elim … (possuccinj n)); /2/; nqed.
    131 
    132 nlet rec possucc_cases
     142definition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n.
     143#P #Pone #Psucc #n @(possucc_elim … (possuccinj n)) /2/; qed.
     144
     145let rec possucc_cases
    133146  (P : Pos → Prop)
    134147  (Pone : P one)
     
    141154  ].
    142155
    143 ndefinition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n.
    144 #P Pone Psucc n; napply (possucc_cases … (possuccinj n)); /2/; nqed.
    145 
    146 ntheorem succ_pred_n : ∀n. n≠one → n = succ (pred n).
    147 napply pos_elim;
    148 ##[ #H; napply False_ind; nelim H; /2/;
    149 ##| //;
    150 ##] nqed.
    151 
    152 ntheorem not_eq_one_succ : ∀n:Pos. one ≠ succ n.
    153 #n; nelim n; nnormalize;
    154 ##[ @; #H; ndestruct;
    155 ##| ##2,3: #n' H; @; #H'; ndestruct;
    156 ##] nqed.
    157 
    158 ntheorem not_eq_n_succn: ∀n:Pos. n ≠ succ n.
    159 #n; nelim n;
    160 ##[ //;
    161 ##| ##*: #n' IH; nnormalize; @; #H; ndestruct
    162 ##] nqed.
    163 
    164 ntheorem pos_elim2:
     156definition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n.
     157#P #Pone #Psucc #n @(possucc_cases … (possuccinj n)) /2/; qed.
     158
     159theorem succ_pred_n : ∀n. n≠one → n = succ (pred n).
     160@pos_elim
     161[ #H @False_ind elim H; /2/;
     162| //;
     163] qed.
     164
     165theorem not_eq_one_succ : ∀n:Pos. one ≠ succ n.
     166#n elim n; normalize;
     167[ % #H destruct;
     168| 2,3: #n' #H % #H' destruct;
     169] qed.
     170
     171theorem not_eq_n_succn: ∀n:Pos. n ≠ succ n.
     172#n elim n;
     173[ //;
     174| *: #n' #IH normalize; % #H destruct
     175] qed.
     176
     177theorem pos_elim2:
    165178 ∀R:Pos → Pos → Prop.
    166179  (∀n:Pos. R one n)
     
    168181  → (∀n,m:Pos. R n m → R (succ n) (succ m))
    169182  → ∀n,m:Pos. R n m.
    170 #R ROn RSO RSS; napply pos_elim; //;
    171 #n0 Rn0m; napply pos_elim; /2/; nqed.
    172 
    173 
    174 ntheorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m).
    175 napply pos_elim2; #n;
    176 ##[ napply (pos_elim ??? n); /2/;
    177 ##| /3/;
    178 ##| #m Hind; ncases Hind; /3/;
    179 ##] nqed.
    180 
    181 nlet rec plus n m ≝
     183#R #ROn #RSO #RSS @pos_elim //;
     184#n0 #Rn0m @pos_elim /2/; qed.
     185
     186
     187theorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m).
     188@pos_elim2 #n
     189[ @(pos_elim ??? n) /2/;
     190| /3/;
     191| #m #Hind cases Hind; /3/;
     192] qed.
     193
     194let rec plus n m ≝
    182195  match n with
    183196  [ one ⇒ succ m
     
    198211interpretation "positive plus" 'plus x y = (plus x y).
    199212
    200 ntheorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m).
    201 #n; nelim n; nnormalize;
    202 ##[ //
    203 ##| ##2,3: #n' IH m; ncases m; /3/;
    204     nnormalize; ncases n'; //;
    205 ##] nqed.
    206 
    207 ntheorem symmetric_plus : symmetric ? plus.
    208 #n; nelim n;
    209 ##[ #y; ncases y; nnormalize; //;
    210 ##| ##2,3: #n' IH y; ncases y; nnormalize; //;
    211 ##] nqed.
    212 
    213 ntheorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m.
    214 #n m; nrewrite > (symmetric_plus (succ n) m);
    215 nrewrite < (plus_n_succm …); //; nqed.
    216 
    217 ntheorem associative_plus : associative Pos plus.
    218 napply pos_elim;
    219 ##[ nnormalize; //;
    220 ##| #x' IHx; napply pos_elim;
    221   ##[ #z; nrewrite < (pluss_succn_m …); nrewrite < (pluss_succn_m …);
    222       nrewrite < (pluss_succn_m …); //;
    223   ##| #y' IHy' z;
    224       nrewrite < (pluss_succn_m y' …);
    225       nrewrite < (plus_n_succm …);
    226       nrewrite < (plus_n_succm …);
    227       nrewrite < (pluss_succn_m ? z); nrewrite > (IHy' …); //;
    228   ##]
    229 ##] nqed.
    230 
    231 ntheorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m).
    232 napply pos_elim; nnormalize; /3/; nqed.
    233 
    234 ntheorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n).
    235 /2/; nqed.
    236 
    237 ntheorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m).
    238 #n; nelim n;
    239 ##[ nnormalize; //;
    240 ##| #n' IH m; nnormalize; nrewrite > (IH m); nrewrite < (pluss_succn_m …);
    241     nrewrite < (pred_succ_n ?); nrewrite < (succ_pred_n …); //;
    242     nelim n'; nnormalize; /2/;
    243 ##] nqed.
    244 
    245 nlet rec times n m ≝
     213theorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m).
     214#n elim n; normalize;
     215[ //
     216| 2,3: #n' #IH #m cases m; /3/;
     217    normalize; cases n'; //;
     218] qed.
     219
     220theorem commutative_plus : commutative ? plus.
     221#n elim n;
     222[ #y cases y; normalize; //;
     223| 2,3: #n' #IH #y cases y; normalize; //;
     224] qed.
     225
     226theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m.
     227#n #m >(commutative_plus (succ n) m)
     228<(plus_n_succm …) //; qed.
     229
     230theorem associative_plus : associative Pos plus.
     231@pos_elim
     232[ normalize; //;
     233| #x' #IHx @pos_elim
     234  [ #z <(pluss_succn_m …) <(pluss_succn_m …)
     235      <(pluss_succn_m …) //;
     236  | #y' #IHy' #z
     237      <(pluss_succn_m y' …)
     238      <(plus_n_succm …)
     239      <(plus_n_succm …)
     240      <(pluss_succn_m ? z) >(IHy' …) //;
     241  ]
     242] qed.
     243
     244theorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m).
     245@pos_elim normalize; /3/; qed.
     246
     247theorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n).
     248/2/; qed.
     249
     250theorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m).
     251#n elim n;
     252[ normalize; //;
     253| #n' #IH #m normalize; >(IH m) <(pluss_succn_m …)
     254    <(pred_succ_n ?) <(succ_pred_n …) //;
     255    elim n'; normalize; /2/;
     256] qed.
     257
     258let rec times n m ≝
    246259match n with
    247260[ one ⇒ m
     
    252265interpretation "positive times" 'times x y = (times x y).
    253266
    254 nlemma p0_times2: ∀n. p0 n = (succ one) * n.
    255 //; nqed.
    256 
    257 nlemma plus_times2: ∀n. n + n = (succ one) * n.
    258 #n; nelim n;
    259 ##[ //;
    260 ##| ##2,3: #n' IH; nnormalize; nrewrite > IH; //;
    261 ##] nqed.
    262 
    263 
    264 ntheorem times_succn_m: ∀n,m. m+n*m = (succ n)*m.
    265 #n; nelim n;
    266 ##[ /2/
    267 ##| #n' IH; nnormalize; #m; nrewrite < (IH m); //;
    268 ##| /2/
    269 ##] nqed.
    270 
    271 ntheorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m).
    272 napply pos_elim;
    273 ##[ //
    274 ##| #n IH m; nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); /3/;
    275 ##] nqed.
    276 
    277 ntheorem times_n_one: ∀n:Pos. n * one = n.
    278 #n; nelim n; /3/; nqed.
    279 
    280 ntheorem symmetric_times: symmetric Pos times.
    281 napply pos_elim; /2/; nqed.
    282 
    283 ntheorem distributive_times_plus : distributive Pos times plus.
    284 napply pos_elim; /2/; nqed.
    285 
    286 ntheorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a.
    287 //; nqed.
    288 
    289 ntheorem associative_times: associative Pos times.
    290 napply pos_elim;
    291 ##[ //;
    292 ##| #x IH y z; nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); //;
    293 ##] nqed.
    294 
    295 nlemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z).
    296 //; nqed.
     267lemma p0_times2: ∀n. p0 n = (succ one) * n.
     268//; qed.
     269
     270lemma plus_times2: ∀n. n + n = (succ one) * n.
     271#n elim n;
     272[ //;
     273| 2,3: #n' #IH normalize; >IH //;
     274] qed.
     275
     276
     277theorem times_succn_m: ∀n,m. m+n*m = (succ n)*m.
     278#n elim n;
     279[ /2/
     280| #n' #IH normalize; #m <(IH m) //;
     281| /2/
     282] qed.
     283
     284theorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m).
     285@pos_elim
     286[ //
     287| #n #IH #m <(times_succn_m …) <(times_succn_m …) /3/;
     288] qed.
     289
     290theorem times_n_one: ∀n:Pos. n * one = n.
     291#n elim n; /3/; qed.
     292
     293theorem commutative_times: commutative Pos times.
     294@pos_elim /2/; qed.
     295
     296theorem distributive_times_plus : distributive Pos times plus.
     297@pos_elim /2/; qed.
     298
     299theorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a.
     300//; qed.
     301
     302theorem associative_times: associative Pos times.
     303@pos_elim
     304[ //;
     305| #x #IH #y #z <(times_succn_m …) <(times_succn_m …) //;
     306] qed.
     307
     308lemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z).
     309//; qed.
    297310
    298311(*** ordering relations ***)
     
    301314   but it means the proofs are much the same. *)
    302315
    303 ninductive le (n:Pos) : Pos → Prop ≝
     316inductive le (n:Pos) : Pos → Prop ≝
    304317  | le_n : le n n
    305318  | le_S : ∀m:Pos. le n m → le n (succ m).
     
    308321interpretation "positive 'neither less than or equal to'" 'nleq x y = (Not (le x y)).
    309322
    310 ndefinition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m.
     323definition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m.
    311324
    312325interpretation "positive 'less than'" 'lt x y = (lt x y).
    313326interpretation "positive 'not less than'" 'nless x y = (Not (lt x y)).
    314327
    315 ndefinition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n.
     328definition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n.
    316329
    317330interpretation "positive 'greater than or equal to'" 'geq x y = (ge x y).
    318331interpretation "positive 'neither greater than or equal to'" 'ngeq x y = (Not (ge x y)).
    319332
    320 ndefinition gt: Pos → Pos → Prop ≝ λn,m. m<n.
     333definition gt: Pos → Pos → Prop ≝ λn,m. m<n.
    321334
    322335interpretation "positive 'greater than'" 'gt x y = (gt x y).
    323336interpretation "positive 'not greater than'" 'ngtr x y = (Not (gt x y)).
    324337
    325 ntheorem transitive_le: transitive Pos le.
    326 #a b c leab lebc; nelim lebc; /2/; nqed.
    327 
    328 ntheorem transitive_lt: transitive Pos lt.
    329 #a b c ltab ltbc; nelim ltbc; /2/; nqed.
    330 
    331 ntheorem le_succ_succ: ∀n,m:Pos. n ≤ m → succ n ≤ succ m.
    332 #n m lenm; nelim lenm; /2/; nqed.
    333 
    334 ntheorem le_one_n : ∀n:Pos. one ≤ n.
    335 napply pos_elim; /2/; nqed.
    336 
    337 ntheorem le_n_succn : ∀n:Pos. n ≤ succ n.
    338 /2/; nqed.
    339 
    340 ntheorem le_pred_n : ∀n:Pos. pred n ≤ n.
    341 napply pos_elim; //; nqed.
    342 
    343 ntheorem monotonic_pred: monotonic Pos le pred.
    344 #n m lenm; nelim lenm; /2/;nqed.
    345 
    346 ntheorem le_S_S_to_le: ∀n,m:Pos. succ n ≤ succ m → n ≤ m.
    347 /2/; nqed.
     338theorem transitive_le: transitive Pos le.
     339#a #b #c #leab #lebc elim lebc; /2/; qed.
     340
     341theorem transitive_lt: transitive Pos lt.
     342#a #b #c #ltab #ltbc elim ltbc; /2/; qed.
     343
     344theorem le_succ_succ: ∀n,m:Pos. n ≤ m → succ n ≤ succ m.
     345#n #m #lenm elim lenm; /2/; qed.
     346
     347theorem le_one_n : ∀n:Pos. one ≤ n.
     348@pos_elim /2/; qed.
     349
     350theorem le_n_succn : ∀n:Pos. n ≤ succ n.
     351/2/; qed.
     352
     353theorem le_pred_n : ∀n:Pos. pred n ≤ n.
     354@pos_elim //; qed.
     355
     356theorem monotonic_pred: monotonic Pos le pred.
     357#n #m #lenm elim lenm; /2/;qed.
     358
     359theorem le_S_S_to_le: ∀n,m:Pos. succ n ≤ succ m → n ≤ m.
     360/2/; qed.
    348361
    349362(* lt vs. le *)
    350 ntheorem not_le_succ_one: ∀ n:Pos. succ n ≰ one.
    351 #n; @; #H; ninversion H; /2/; nqed.
    352 
    353 ntheorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m.
    354 /3/; nqed.
    355 
    356 ntheorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m.
    357 /3/; nqed.
    358 
    359 ntheorem decidable_le: ∀n,m:Pos. decidable (n≤m).
    360 napply pos_elim2; #n; /2/;
    361 #m; *; /3/; nqed.
    362 
    363 ntheorem decidable_lt: ∀n,m:Pos. decidable (n < m).
    364 #n; #m; napply decidable_le ; nqed.
    365 
    366 ntheorem not_le_succ_n: ∀n:Pos. succ n ≰ n.
    367 napply pos_elim; //;
    368 #m IH; napply not_le_to_not_le_succ_succ; //;
    369 nqed.
    370 
    371 ntheorem not_le_to_lt: ∀n,m:Pos. n ≰ m → m < n.
    372 napply pos_elim2; #n;
    373  ##[#abs; napply False_ind;/2/;
    374  ##|/2/;
    375  ##|#m;#Hind;#HnotleSS; napply le_succ_succ;/3/;
    376  ##]
    377 nqed.
    378 
    379 ntheorem lt_to_not_le: ∀n,m:Pos. n < m → m ≰ n.
    380 #n m Hltnm; nelim Hltnm;
    381 ##[ //
    382 ##| #p H; napply not_to_not; /2/;
    383 ##] nqed.
    384 
    385 ntheorem not_lt_to_le: ∀n,m:Pos. n ≮ m → m ≤ n.
    386 /4/; nqed.
    387 
    388 
    389 ntheorem le_to_not_lt: ∀n,m:Pos. n ≤ m → m ≮ n.
    390 #n; #m; #H;napply lt_to_not_le; /2/;nqed.
     363theorem not_le_succ_one: ∀ n:Pos. succ n ≰ one.
     364#n % #H inversion H /2/; qed.
     365
     366theorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m.
     367/3/; qed.
     368
     369theorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m.
     370/3/; qed.
     371
     372theorem decidable_le: ∀n,m:Pos. decidable (n≤m).
     373@pos_elim2 #n /2/;
     374#m *; /3/; qed.
     375
     376theorem decidable_lt: ∀n,m:Pos. decidable (n < m).
     377#n #m @decidable_le  qed.
     378
     379theorem not_le_succ_n: ∀n:Pos. succ n ≰ n.
     380@pos_elim //;
     381#m #IH @not_le_to_not_le_succ_succ //;
     382qed.
     383
     384theorem not_le_to_lt: ∀n,m:Pos. n ≰ m → m < n.
     385@pos_elim2 #n
     386 [#abs @False_ind /2/;
     387 |/2/;
     388 |#m #Hind #HnotleSS @le_succ_succ /3/;
     389 ]
     390qed.
     391
     392theorem lt_to_not_le: ∀n,m:Pos. n < m → m ≰ n.
     393#n #m #Hltnm elim Hltnm;
     394[ //
     395| #p #H @not_to_not /2/;
     396] qed.
     397
     398theorem not_lt_to_le: ∀n,m:Pos. n ≮ m → m ≤ n.
     399/4/; qed.
     400
     401
     402theorem le_to_not_lt: ∀n,m:Pos. n ≤ m → m ≮ n.
     403#n #m #H @lt_to_not_le /2/;qed.
    391404
    392405(* lt and le trans *)
    393406
    394 ntheorem lt_to_le_to_lt: ∀n,m,p:Pos. n < m → m ≤ p → n < p.
    395 #n; #m; #p; #H; #H1; nelim H1; /2/; nqed.
    396 
    397 ntheorem le_to_lt_to_lt: ∀n,m,p:Pos. n ≤ m → m < p → n < p.
    398 #n; #m; #p; #H; nelim H; /3/; nqed.
    399 
    400 ntheorem lt_succ_to_lt: ∀n,m:Pos. succ n < m → n < m.
    401 /2/; nqed.
    402 
    403 ntheorem ltn_to_lt_one: ∀n,m:Pos. n < m → one < m.
    404 /2/; nqed.
    405 
    406 ntheorem lt_one_n_elim: ∀n:Pos. one < n →
     407theorem lt_to_le_to_lt: ∀n,m,p:Pos. n < m → m ≤ p → n < p.
     408#n #m #p #H #H1 elim H1; /2/; qed.
     409
     410theorem le_to_lt_to_lt: ∀n,m,p:Pos. n ≤ m → m < p → n < p.
     411#n #m #p #H elim H; /3/; qed.
     412
     413theorem lt_succ_to_lt: ∀n,m:Pos. succ n < m → n < m.
     414/2/; qed.
     415
     416theorem ltn_to_lt_one: ∀n,m:Pos. n < m → one < m.
     417/2/; qed.
     418
     419theorem lt_one_n_elim: ∀n:Pos. one < n →
    407420  ∀P:Pos → Prop.(∀m:Pos.P (succ m)) → P n.
    408 napply pos_elim; //; #abs; napply False_ind;/2/;
    409 nqed.
     421@pos_elim //; #abs @False_ind /2/;
     422qed.
    410423
    411424(* le to lt or eq *)
    412 ntheorem le_to_or_lt_eq: ∀n,m:Pos. n ≤ m → n < m ∨ n = m.
    413 #n; #m; #lenm; nelim lenm; /3/; nqed.
     425theorem le_to_or_lt_eq: ∀n,m:Pos. n ≤ m → n < m ∨ n = m.
     426#n #m #lenm elim lenm; /3/; qed.
    414427
    415428(* not eq *)
    416 ntheorem lt_to_not_eq : ∀n,m:Pos. n < m → n ≠ m.
    417 #n; #m; #H; napply not_to_not;/2/; nqed.
    418 
    419 ntheorem not_eq_to_le_to_lt: ∀n,m:Pos. n≠m → n≤m → n<m.
    420 #n; #m; #Hneq; #Hle; ncases (le_to_or_lt_eq ?? Hle); //;
    421 #Heq; /3/; nqed.
     429theorem lt_to_not_eq : ∀n,m:Pos. n < m → n ≠ m.
     430#n #m #H @not_to_not /2/; qed.
     431
     432theorem not_eq_to_le_to_lt: ∀n,m:Pos. n≠m → n≤m → n<m.
     433#n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle); //;
     434#Heq /3/; qed.
    422435
    423436(* le elimination *)
    424 ntheorem le_n_one_to_eq : ∀n:Pos. n ≤ one → one=n.
    425 napply pos_cases; //; #a ; #abs;
    426 napply False_ind; /2/;nqed.
    427 
    428 ntheorem le_n_one_elim: ∀n:Pos. n ≤ one → ∀P: Pos →Prop. P one → P n.
    429 napply pos_cases; //; #a; #abs;
    430 napply False_ind; /2/; nqed.
    431 
    432 ntheorem le_n_Sm_elim : ∀n,m:Pos.n ≤ succ m →
     437theorem le_n_one_to_eq : ∀n:Pos. n ≤ one → one=n.
     438@pos_cases //; #a ; #abs
     439@False_ind /2/;qed.
     440
     441theorem le_n_one_elim: ∀n:Pos. n ≤ one → ∀P: Pos →Prop. P one → P n.
     442@pos_cases //; #a #abs
     443@False_ind /2/; qed.
     444
     445theorem le_n_Sm_elim : ∀n,m:Pos.n ≤ succ m →
    433446∀P:Prop. (succ n ≤ succ m → P) → (n=succ m → P) → P.
    434 #n; #m; #Hle; #P; nelim Hle; /3/; nqed.
     447#n #m #Hle #P elim Hle; /3/; qed.
    435448
    436449(* le and eq *)
    437450
    438 ntheorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m.
    439 napply pos_elim2; /4/;
    440 nqed.
    441 
    442 ntheorem lt_one_S : ∀n:Pos. one < succ n.
    443 /2/; nqed.
     451theorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m.
     452@pos_elim2 /4/;
     453qed.
     454
     455theorem lt_one_S : ∀n:Pos. one < succ n.
     456/2/; qed.
    444457
    445458(* well founded induction principles *)
    446459
    447 ntheorem pos_elim1 : ∀n:Pos.∀P:Pos → Prop.
     460theorem pos_elim1 : ∀n:Pos.∀P:Pos → Prop.
    448461(∀m.(∀p. p < m → P p) → P m) → P n.
    449 #n; #P; #H;
    450 ncut (∀q:Pos. q ≤ n → P q);/2/;
    451 napply (pos_elim … n);
    452  ##[#q; #HleO; (* applica male *)
    453     napply (le_n_one_elim ? HleO);
    454     napply H; #p; #ltpO;
    455     napply False_ind; /2/; (* 3 *)
    456  ##|#p; #Hind; #q; #HleS;
    457     napply H; #a; #lta; napply Hind;
    458     napply le_S_S_to_le;/2/;
    459  ##]
    460 nqed.
     462#n #P #H
     463cut (∀q:Pos. q ≤ n → P q);/2/;
     464@(pos_elim … n)
     465 [#q #HleO (* applica male *)
     466    @(le_n_one_elim ? HleO)
     467    @H #p #ltpO
     468    @False_ind /2/; (* 3 *)
     469 |#p #Hind #q #HleS
     470    @H #a #lta @Hind
     471    @le_S_S_to_le /2/;
     472 ]
     473qed.
    461474
    462475(*********************** monotonicity ***************************)
    463 ntheorem monotonic_le_plus_r:
     476theorem monotonic_le_plus_r:
    464477∀n:Pos.monotonic Pos le (λm.n + m).
    465 #n; #a; #b; napply (pos_elim … n); nnormalize; /2/;
    466 #m; #H; #leab;/3/; nqed.
    467 
    468 ntheorem monotonic_le_plus_l:
     478#n #a #b @(pos_elim … n) normalize; /2/;
     479#m #H #leab /3/; qed.
     480
     481theorem monotonic_le_plus_l:
    469482∀m:Pos.monotonic Pos le (λn.n + m).
    470 /2/; nqed.
    471 
    472 ntheorem le_plus: ∀n1,n2,m1,m2:Pos. n1 ≤ n2  → m1 ≤ m2
     483/2/; qed.
     484
     485theorem le_plus: ∀n1,n2,m1,m2:Pos. n1 ≤ n2  → m1 ≤ m2
    473486→ n1 + m1 ≤ n2 + m2.
    474 #n1; #n2; #m1; #m2; #len; #lem; napply (transitive_le ? (n1+m2));
    475 /2/; nqed.
    476 
    477 ntheorem le_plus_n :∀n,m:Pos. m ≤ n + m.
    478 /3/; nqed.
    479 
    480 nlemma le_plus_a: ∀a,n,m:Pos. n ≤ m → n ≤ a + m.
    481 /2/; nqed.
    482 
    483 nlemma le_plus_b: ∀b,n,m:Pos. n + b ≤ m → n ≤ m.
    484 /2/; nqed.
    485 
    486 ntheorem le_plus_n_r :∀n,m:Pos. m ≤ m + n.
    487 /2/; nqed.
    488 
    489 ntheorem eq_plus_to_le: ∀n,m,p:Pos.n=m+p → m ≤ n.
    490 //; nqed.
    491 
    492 ntheorem le_plus_to_le: ∀a,n,m:Pos. a + n ≤ a + m → n ≤ m.
    493 napply pos_elim; nnormalize; /3/; nqed.
    494 
    495 ntheorem le_plus_to_le_r: ∀a,n,m:Pos. n + a ≤ m +a → n ≤ m.
    496 /2/; nqed.
     487#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
     488/2/; qed.
     489
     490theorem le_plus_n :∀n,m:Pos. m ≤ n + m.
     491/3/; qed.
     492
     493lemma le_plus_a: ∀a,n,m:Pos. n ≤ m → n ≤ a + m.
     494/2/; qed.
     495
     496lemma le_plus_b: ∀b,n,m:Pos. n + b ≤ m → n ≤ m.
     497/2/; qed.
     498
     499theorem le_plus_n_r :∀n,m:Pos. m ≤ m + n.
     500/2/; qed.
     501
     502theorem eq_plus_to_le: ∀n,m,p:Pos.n=m+p → m ≤ n.
     503//; qed.
     504
     505theorem le_plus_to_le: ∀a,n,m:Pos. a + n ≤ a + m → n ≤ m.
     506@pos_elim normalize; /3/; qed.
     507
     508theorem le_plus_to_le_r: ∀a,n,m:Pos. n + a ≤ m +a → n ≤ m.
     509/2/; qed.
    497510
    498511(* plus & lt *)
    499512
    500 ntheorem monotonic_lt_plus_r:
     513theorem monotonic_lt_plus_r:
    501514∀n:Pos.monotonic Pos lt (λm.n+m).
    502 /2/; nqed.
    503 
    504 ntheorem monotonic_lt_plus_l:
     515/2/; qed.
     516
     517theorem monotonic_lt_plus_l:
    505518∀n:Pos.monotonic Pos lt (λm.m+n).
    506 /2/; nqed.
    507 
    508 ntheorem lt_plus: ∀n,m,p,q:Pos. n < m → p < q → n + p < m + q.
    509 #n; #m; #p; #q; #ltnm; #ltpq;
    510 napply (transitive_lt ? (n+q));/2/; nqed.
    511 
    512 ntheorem le_lt_plus_pos: ∀n,m,p:Pos. n ≤ m → n < m + p.
    513 #n m p H; napply (le_to_lt_to_lt … H);
    514 /2/; nqed.
    515 
    516 ntheorem lt_plus_to_lt_l :∀n,p,q:Pos. p+n < q+n → p<q.
    517 /2/; nqed.
    518 
    519 ntheorem lt_plus_to_lt_r :∀n,p,q:Pos. n+p < n+q → p<q.
    520 /2/; nqed.
     519/2/; qed.
     520
     521theorem lt_plus: ∀n,m,p,q:Pos. n < m → p < q → n + p < m + q.
     522#n #m #p #q #ltnm #ltpq
     523@(transitive_lt ? (n+q)) /2/; qed.
     524
     525theorem le_lt_plus_pos: ∀n,m,p:Pos. n ≤ m → n < m + p.
     526#n #m #p #H @(le_to_lt_to_lt … H)
     527/2/; qed.
     528
     529theorem lt_plus_to_lt_l :∀n,p,q:Pos. p+n < q+n → p<q.
     530/2/; qed.
     531
     532theorem lt_plus_to_lt_r :∀n,p,q:Pos. n+p < n+q → p<q.
     533/2/; qed.
    521534
    522535(* times *)
    523 ntheorem monotonic_le_times_r:
     536theorem monotonic_le_times_r:
    524537∀n:Pos.monotonic Pos le (λm. n * m).
    525 #n; #x; #y; #lexy; napply (pos_elim … n); nnormalize;//;(* lento /2/;*)
    526 #a; #lea; /2/;
    527 nqed.
    528 
    529 ntheorem le_times: ∀n1,n2,m1,m2:Pos.
     538#n #x #y #lexy @(pos_elim … n) normalize;//;(* lento /2/;*)
     539#a #lea /2/;
     540qed.
     541
     542theorem le_times: ∀n1,n2,m1,m2:Pos.
    530543n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
    531 #n1; #n2; #m1; #m2; #len; #lem;
    532 napply (transitive_le ? (n1*m2)); (* /2/ slow *)
    533  ##[ napply monotonic_le_times_r;//;
    534  ##| napplyS monotonic_le_times_r;//;
    535  ##]
    536 nqed.
    537 
    538 ntheorem lt_times_n: ∀n,m:Pos. m ≤ n*m.
    539 #n m; /2/; nqed.
    540 
    541 ntheorem le_times_to_le:
     544#n1 #n2 #m1 #m2 #len #lem
     545@(transitive_le ? (n1*m2)) (* /2/ slow *)
     546 [ @monotonic_le_times_r //;
     547 | applyS monotonic_le_times_r;//;
     548 ]
     549qed.
     550
     551theorem lt_times_n: ∀n,m:Pos. m ≤ n*m.
     552#n #m /2/; qed.
     553
     554theorem le_times_to_le:
    542555∀a,n,m:Pos. a * n ≤ a * m → n ≤ m.
    543 #a; napply pos_elim2; nnormalize;
    544   ##[//;
    545   ##|#n; nrewrite > (times_n_one …); nrewrite < (times_n_succm …);
    546      #H; napply False_ind;
    547      nelim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/;
    548   ##|#n; #m; #H; #le;
    549      napply le_succ_succ; napply H; /2/;
    550   ##]
    551 nqed.
    552 
    553 ntheorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m.
    554 #n; #m; #lenm;  (* interessante *)
    555 napplyS (le_plus n m); //; nqed.
     556#a @pos_elim2 normalize;
     557  [//;
     558  |#n >(times_n_one …) <(times_n_succm …)
     559     #H @False_ind
     560     elim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/;
     561  |#n #m #H #le
     562     @le_succ_succ @H /2/;
     563  ]
     564qed.
     565
     566theorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m.
     567#n #m #lenm  (* interessante *)
     568applyS (le_plus n m); //; qed.
    556569
    557570(* prove injectivity of times from above *)
    558 ntheorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m).
    559 #n m p H; napply le_to_le_to_eq;
     571theorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m).
     572#n #m #p #H @le_to_le_to_eq
    560573/2/;
    561 nqed.
    562 
    563 ntheorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n).
    564 /2/; nqed.
     574qed.
     575
     576theorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n).
     577/2/; qed.
    565578
    566579(* times & lt *)
    567580
    568 ntheorem monotonic_lt_times_l:
     581theorem monotonic_lt_times_l:
    569582  ∀c:Pos. monotonic Pos lt (λt.(t*c)).
    570 #c n m ltnm;
    571 nelim ltnm; nnormalize;
    572   ##[/2/;
    573   ##|#a; #_; #lt1; napply (transitive_le ??? lt1);//;
    574   ##]
    575 nqed.
    576 
    577 ntheorem monotonic_lt_times_r:
     583#c #n #m #ltnm
     584elim ltnm; normalize;
     585  [/2/;
     586  |#a #_ #lt1 @(transitive_le ??? lt1) //;
     587  ]
     588qed.
     589
     590theorem monotonic_lt_times_r:
    578591  ∀c:Pos. monotonic Pos lt (λt.(c*t)).
    579 #a b c H;
    580 nrewrite > (symmetric_times a b); nrewrite > (symmetric_times a c);
    581 /2/; nqed.
    582 
    583 ntheorem lt_to_le_to_lt_times:
     592#a #b #c #H
     593>(commutative_times a b) >(commutative_times a c)
     594/2/; qed.
     595
     596theorem lt_to_le_to_lt_times:
    584597∀n,m,p,q:Pos. n < m → p ≤ q → n*p < m*q.
    585 #n; #m; #p; #q; #ltnm; #lepq;
    586 napply (le_to_lt_to_lt ? (n*q));
    587   ##[napply monotonic_le_times_r;//;
    588   ##|napply monotonic_lt_times_l;//;
    589   ##]
    590 nqed.
    591 
    592 ntheorem lt_times:∀n,m,p,q:Pos. n<m → p<q → n*p < m*q.
    593 #n; #m; #p; #q; #ltnm; #ltpq;
    594 napply lt_to_le_to_lt_times;/2/;
    595 nqed.
    596 
    597 ntheorem lt_times_n_to_lt_l:
     598#n #m #p #q #ltnm #lepq
     599@(le_to_lt_to_lt ? (n*q))
     600  [@monotonic_le_times_r //;
     601  |@monotonic_lt_times_l //;
     602  ]
     603qed.
     604
     605theorem lt_times:∀n,m,p,q:Pos. n<m → p<q → n*p < m*q.
     606#n #m #p #q #ltnm #ltpq
     607@lt_to_le_to_lt_times /2/;
     608qed.
     609
     610theorem lt_times_n_to_lt_l:
    598611∀n,p,q:Pos. p*n < q*n → p < q.
    599 #n; #p; #q; #Hlt;
    600 nelim (decidable_lt p q);//;
    601 #nltpq; napply False_ind;
    602 napply (absurd ? ? (lt_to_not_le ? ? Hlt));
    603 napplyS monotonic_le_times_r;/2/;
    604 nqed.
    605 
    606 ntheorem lt_times_n_to_lt_r:
     612#n #p #q #Hlt
     613elim (decidable_lt p q);//;
     614#nltpq @False_ind
     615@(absurd ? ? (lt_to_not_le ? ? Hlt))
     616applyS monotonic_le_times_r;/2/;
     617qed.
     618
     619theorem lt_times_n_to_lt_r:
    607620∀n,p,q:Pos. n*p < n*q → p < q.
    608 /2/; nqed.
     621/2/; qed.
    609622
    610623(**** minus ****)
    611624
    612 ninductive minusresult : Type
     625inductive minusresult : Type[0]
    613626 | MinusNeg: minusresult
    614627 | MinusZero: minusresult
    615628 | MinusPos: Pos → minusresult.
    616629
    617 nlet rec partial_minus (n,m:Pos) : minusresult ≝
     630let rec partial_minus (n,m:Pos) : minusresult ≝
    618631match n with
    619632[ one ⇒ match m with [ one ⇒ MinusZero | _ ⇒ MinusNeg ]
     
    636649].
    637650
    638 nremark testminus0: partial_minus (p0 one) (p1 one) = MinusNeg. //; nqed.
    639 nremark testminus1: partial_minus (p0 one) (p0 (p0 one)) = MinusNeg. //; nqed.
    640 nremark testminus2: partial_minus (p0 (p0 one)) (p0 one) = MinusPos (p0 one). //; nqed.
    641 nremark testminus3: partial_minus (p0 one) one = MinusPos one. //; nqed.
    642 nremark testminus4: partial_minus (succ (p1 one)) (p1 one) = MinusPos one. //; nqed.
    643 
    644 ndefinition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ].
     651example testminus0: partial_minus (p0 one) (p1 one) = MinusNeg. //; qed.
     652example testminus1: partial_minus (p0 one) (p0 (p0 one)) = MinusNeg. //; qed.
     653example testminus2: partial_minus (p0 (p0 one)) (p0 one) = MinusPos (p0 one). //; qed.
     654example testminus3: partial_minus (p0 one) one = MinusPos one. //; qed.
     655example testminus4: partial_minus (succ (p1 one)) (p1 one) = MinusPos one. //; qed.
     656
     657definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ].
    645658
    646659interpretation "natural minus" 'minus x y = (minus x y).
    647660
    648 nlemma partialminus_S: ∀n,m:Pos.
     661lemma partialminus_S: ∀n,m:Pos.
    649662match partial_minus (succ n) m with
    650663[ MinusPos p ⇒ match p with [ one ⇒ partial_minus n m = MinusZero | _ ⇒ partial_minus n m = MinusPos (pred p) ]
    651664| _ ⇒ partial_minus n m = MinusNeg
    652665].
    653 #n; nelim n;
    654 ##[ #m; ncases m;
    655   ##[ //;
    656   ##| ##2,3: #m'; ncases m'; //;
    657   ##]
     666#n elim n;
     667[ #m cases m;
     668  [ //;
     669  | 2,3: #m' cases m'; //;
     670  ]
    658671(* The other two cases are the same.  I'd combine them, but the numbering
    659672   would be even more horrific. *)
    660 ##| #n' IH m; ncases m;
    661   ##[ nnormalize; nrewrite < (pred_succ_n n'); ncases n'; //;
    662   ##| ##2,3: #m'; nnormalize; nlapply (IH m'); ncases (partial_minus (succ n') m');
    663     ##[ ##1,2,4,5: nnormalize; #H; nrewrite > H; //;
    664     ##| ##3,6: #p; ncases p; ##[ ##1,4: nnormalize; #H; nrewrite > H; //;
    665                       ##| ##2,3,5,6: #p'; nnormalize; #H; nrewrite > H; //;
    666                       ##]
    667     ##]
    668   ##]
    669 ##| #n' IH m; ncases m;
    670   ##[ nnormalize; nrewrite < (pred_succ_n n'); ncases n'; //;
    671   ##| ##2,3: #m'; nnormalize; nlapply (IH m'); ncases (partial_minus (succ n') m');
    672     ##[ ##1,2,4,5: nnormalize; #H; nrewrite > H; //;
    673     ##| ##3,6: #p; ncases p; ##[ ##1,4: nnormalize; #H; nrewrite > H; //;
    674                       ##| ##2,3,5,6: #p'; nnormalize; #H; nrewrite > H; //;
    675                       ##]
    676     ##]
    677   ##]
    678 ##] nqed.
    679 
    680 nlemma partialminus_n_S: ∀n,m:Pos.
     673| #n' #IH #m cases m;
     674  [ normalize; <(pred_succ_n n') cases n'; //;
     675  | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m');
     676    [ 1,2,4,5: normalize; #H >H //;
     677    | 3,6: #p cases p; [ 1,4: normalize; #H >H //;
     678                      | 2,3,5,6: #p' normalize; #H >H //;
     679                      ]
     680    ]
     681  ]
     682| #n' #IH #m cases m;
     683  [ normalize; <(pred_succ_n n') cases n'; //;
     684  | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m');
     685    [ 1,2,4,5: normalize; #H >H //;
     686    | 3,6: #p cases p; [ 1,4: normalize; #H >H //;
     687                      | 2,3,5,6: #p' normalize; #H >H //;
     688                      ]
     689    ]
     690  ]
     691] qed.
     692
     693lemma partialminus_n_S: ∀n,m:Pos.
    681694  match partial_minus n m with
    682695  [ MinusPos p ⇒ match p with [ one ⇒ partial_minus n (succ m) = MinusZero
     
    685698  | _ ⇒ partial_minus n (succ m) = MinusNeg
    686699  ].
    687 #n; nelim n;
    688 ##[ #m; ncases m; //;
     700#n elim n;
     701[ #m cases m; //;
    689702(* Again, lots of unnecessary duplication! *)
    690 ##| #n' IH m; ncases m;
    691   ##[ nnormalize; ncases n'; //;
    692   ##| #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m');
    693     ##[ ##1,2: nnormalize; #H; nrewrite > H; //;
    694     ##| #p; ncases p; nnormalize; ##[ #H; nrewrite > H; //;
    695                                   ##| ##2,3: #p'; #H; nrewrite > H; //;
    696                                   ##]
    697     ##]
    698   ##|  #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m');
    699     ##[ ##1,2: nnormalize; #H; nrewrite > H; //;
    700     ##| #p; ncases p; nnormalize; ##[ #H; nrewrite > H; //;
    701                                   ##| ##2,3: #p'; #H; nrewrite > H; //;
    702                                   ##]
    703     ##]
    704   ##]
    705 ##| #n' IH m; ncases m;
    706   ##[ nnormalize; ncases n'; //;
    707   ##| #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m');
    708     ##[ ##1,2: nnormalize; #H; nrewrite > H; //;
    709     ##| #p; ncases p; nnormalize; ##[ #H; nrewrite > H; //;
    710                                   ##| ##2,3: #p'; #H; nrewrite > H; //;
    711                                   ##]
    712     ##]
    713   ##|  #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m');
    714     ##[ ##1,2: nnormalize; #H; nrewrite > H; //;
    715     ##| #p; ncases p; nnormalize; ##[ #H; nrewrite > H; //;
    716                                   ##| ##2,3: #p'; #H; nrewrite > H; //;
    717                                   ##]
    718     ##]
    719   ##]
    720 ##] nqed.
    721 
    722 ntheorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m.
    723 #n; nelim n;
    724 ##[ #m; ncases m;
    725   ##[ //;
    726   ##| ##2,3: #m'; ncases m'; //;
    727   ##]
    728 ##| #n' IH m; ncases m;
    729   ##[ nnormalize; ncases n'; /2/; nnormalize; #n''; nrewrite < (pred_succ_n n''); ncases n'';//;
    730   ##| #m'; nnormalize; nrewrite > (IH ?); //;
    731   ##| #m'; nnormalize; nlapply (partialminus_S n' m'); ncases (partial_minus (succ n') m');
    732     ##[ ##1,2: nnormalize; #H; nrewrite > H; //;
    733     ##| #p; ncases p; ##[ nnormalize; #H; nrewrite > H; //;
    734                       ##| ##2,3: #p';nnormalize; #H; nrewrite > H; //;
    735                       ##]
    736     ##]
    737   ##]
    738 ##|  #n' IH m; ncases m;
    739   ##[ nnormalize; ncases n'; /2/;
    740   ##| #m'; nnormalize; nlapply (partialminus_n_S n' m'); ncases (partial_minus n' m');
    741     ##[ ##1,2: nnormalize; #H; nrewrite > H; //;
    742     ##| #p; ncases p;   ##[ nnormalize; #H; nrewrite > H; //;
    743                       ##| ##2,3: #p';nnormalize; #H; nrewrite > H; //;
    744                       ##]
    745     ##]
    746   ##| #m'; nnormalize; nrewrite > (IH ?); //;
    747   ##]
    748 ##] nqed.
    749 
    750 ntheorem minus_S_S: ∀n,m:Pos. (succ n) - (succ m) = n-m.
    751 #n m; nnormalize; nrewrite > (partialminus_S_S n m); //; nqed.
    752 
    753 ntheorem minus_one_n: ∀n:Pos.one=one-n.
    754 #n; ncases n; //; nqed.
    755 
    756 ntheorem minus_n_one: ∀n:Pos.pred n=n-one.
    757 #n; ncases n; //; nqed.
    758 
    759 nlemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero.
    760 #n; nelim n;
    761 ##[ //;
    762 ##| ##2,3: nnormalize; #n' IH; nrewrite > IH; //
    763 ##] nqed.
    764 
    765 ntheorem minus_n_n: ∀n:Pos.one=n-n.
    766 #n; nnormalize; nrewrite > (partial_minus_n_n n); //;
    767 nqed.
    768 
    769 ntheorem minus_Sn_n: ∀n:Pos. one = (succ n)-n.
    770 #n; ncut (partial_minus (succ n) n = MinusPos one);
    771 ##[ nelim n;
    772   ##[ //;
    773   ##| nnormalize; #n' IH; nrewrite > IH; //;
    774   ##| nnormalize; #n' IH; nrewrite > (partial_minus_n_n n'); //;
    775   ##]
    776 ##| #H; nnormalize; nrewrite > H; //;
    777 ##] nqed.
    778 
    779 ntheorem minus_Sn_m: ∀m,n:Pos. m < n → succ n -m = succ (n-m).
     703| #n' #IH #m cases m;
     704  [ normalize; cases n'; //;
     705  | #m' normalize; lapply (IH m'); cases (partial_minus n' m');
     706    [ 1,2: normalize; #H >H //;
     707    | #p cases p; normalize; [ #H >H //;
     708                                  | 2,3: #p' #H >H //;
     709                                  ]
     710    ]
     711  |  #m' normalize; lapply (IH m'); cases (partial_minus n' m');
     712    [ 1,2: normalize; #H >H //;
     713    | #p cases p; normalize; [ #H >H //;
     714                                  | 2,3: #p' #H >H //;
     715                                  ]
     716    ]
     717  ]
     718| #n' #IH #m cases m;
     719  [ normalize; cases n'; //;
     720  | #m' normalize; lapply (IH m'); cases (partial_minus n' m');
     721    [ 1,2: normalize; #H >H //;
     722    | #p cases p; normalize; [ #H >H //;
     723                                  | 2,3: #p' #H >H //;
     724                                  ]
     725    ]
     726  |  #m' normalize; lapply (IH m'); cases (partial_minus n' m');
     727    [ 1,2: normalize; #H >H //;
     728    | #p cases p; normalize; [ #H >H //;
     729                                  | 2,3: #p' #H >H //;
     730                                  ]
     731    ]
     732  ]
     733] qed.
     734
     735theorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m.
     736#n elim n;
     737[ #m cases m;
     738  [ //;
     739  | 2,3: #m' cases m'; //;
     740  ]
     741| #n' #IH #m cases m;
     742  [ normalize; cases n'; /2/; normalize; #n'' <(pred_succ_n n'') cases n'';//;
     743  | #m' normalize; >(IH ?) //;
     744  | #m' normalize; lapply (partialminus_S n' m'); cases (partial_minus (succ n') m');
     745    [ 1,2: normalize; #H >H //;
     746    | #p cases p; [ normalize; #H >H //;
     747                      | 2,3: #p' normalize; #H >H //;
     748                      ]
     749    ]
     750  ]
     751|  #n' #IH #m cases m;
     752  [ normalize; cases n'; /2/;
     753  | #m' normalize; lapply (partialminus_n_S n' m'); cases (partial_minus n' m');
     754    [ 1,2: normalize; #H >H //;
     755    | #p cases p;   [ normalize; #H >H //;
     756                      | 2,3: #p' normalize; #H >H //;
     757                      ]
     758    ]
     759  | #m' normalize; >(IH ?) //;
     760  ]
     761] qed.
     762
     763theorem minus_S_S: ∀n,m:Pos. (succ n) - (succ m) = n-m.
     764#n #m normalize; >(partialminus_S_S n m) //; qed.
     765
     766theorem minus_one_n: ∀n:Pos.one=one-n.
     767#n cases n; //; qed.
     768
     769theorem minus_n_one: ∀n:Pos.pred n=n-one.
     770#n cases n; //; qed.
     771
     772lemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero.
     773#n elim n;
     774[ //;
     775| 2,3: normalize; #n' #IH >IH //
     776] qed.
     777
     778theorem minus_n_n: ∀n:Pos.one=n-n.
     779#n normalize; >(partial_minus_n_n n) //;
     780qed.
     781
     782theorem minus_Sn_n: ∀n:Pos. one = (succ n)-n.
     783#n cut (partial_minus (succ n) n = MinusPos one);
     784[ elim n;
     785  [ //;
     786  | normalize; #n' #IH >IH //;
     787  | normalize; #n' #IH >(partial_minus_n_n n') //;
     788  ]
     789| #H normalize; >H //;
     790] qed.
     791
     792theorem minus_Sn_m: ∀m,n:Pos. m < n → succ n -m = succ (n-m).
    780793(* qualcosa da capire qui
    781 #n; #m; #lenm; nelim lenm; napplyS refl_eq. *)
    782 napply pos_elim2;
    783   ##[#n H; napply (lt_one_n_elim n H); //;
    784   ##|#n; #abs; napply False_ind; /2/
    785   ##|#n; #m; #Hind; #c; napplyS Hind; /2/;
    786   ##]
    787 nqed.
    788 
    789 ntheorem not_eq_to_le_to_le_minus:
     794#n #m #lenm elim lenm; napplyS refl_eq. *)
     795@pos_elim2
     796  [#n #H @(lt_one_n_elim n H) //;
     797  |#n #abs @False_ind /2/
     798  |#n #m #Hind #c applyS Hind; /2/;
     799  ]
     800qed.
     801
     802theorem not_eq_to_le_to_le_minus:
    790803  ∀n,m:Pos.n ≠ m → n ≤ m → n ≤ m - one.
    791 #n; napply pos_cases; //; #m;
    792 #H; #H1; napply le_S_S_to_le;
    793 napplyS (not_eq_to_le_to_lt n (succ m) H H1);
    794 nqed.
    795 
    796 ntheorem eq_minus_S_pred: ∀n,m:Pos. n - (succ m) = pred(n -m).
    797 napply pos_elim2;
    798 ##[ #n; ncases n; nnormalize; //;
    799 ##| #n; napply (pos_elim … n); //;
    800 ##| //;
    801 ##] nqed.
    802 
    803 nlemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m).
    804 #n m H;
    805 napply (lt_one_n_elim … H); /3/;
    806 nqed.
    807 
    808 ntheorem plus_minus:
     804#n @pos_cases //; #m
     805#H #H1 @le_S_S_to_le
     806applyS (not_eq_to_le_to_lt n (succ m) H H1);
     807qed.
     808
     809theorem eq_minus_S_pred: ∀n,m:Pos. n - (succ m) = pred(n -m).
     810@pos_elim2
     811[ #n cases n; normalize; //;
     812| #n @(pos_elim … n) //;
     813| //;
     814] qed.
     815
     816lemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m).
     817#n #m #H
     818@(lt_one_n_elim … H) /3/;
     819qed.
     820
     821theorem plus_minus:
    809822∀m,n,p:Pos. m < n → (n-m)+p = (n+p)-m.
    810 napply pos_elim2;
    811   ##[ #n p H; nrewrite < (minus_n_one ?); nrewrite < (minus_n_one ?); /2/;
    812   ##|#n; #p; #abs; napply False_ind; /2/;
    813   ##|#n m IH p H; nrewrite > (eq_minus_S_pred …); nrewrite > (eq_minus_S_pred …);
    814      ncut (n<m); ##[ /2/ ##] #H';
    815      nrewrite > (pred_Sn_plus …);
    816      ##[ nrewrite > (minus_Sn_m …); /2/;
    817          nrewrite < (pluss_succn_m …);
    818          nrewrite < (pluss_succn_m …);
    819          nrewrite > (minus_Sn_m …);
    820          ##[ nrewrite < (pred_succ_n …);
    821              nrewrite < (pred_succ_n …);
    822              napply IH; /2/;
    823          ##| /2/;
    824          ##]
    825      ##| nrewrite > (minus_Sn_m … H'); //;
    826      ##]
    827   ##] nqed.
     823@pos_elim2
     824  [ #n #p #H <(minus_n_one ?) <(minus_n_one ?) /2/;
     825  |#n #p #abs @False_ind /2/;
     826  |#n #m #IH #p #H >(eq_minus_S_pred …) >(eq_minus_S_pred …)
     827     cut (n<m); [ /2/ ] #H'
     828     >(pred_Sn_plus …)
     829     [ >(minus_Sn_m …) /2/;
     830         <(pluss_succn_m …)
     831         <(pluss_succn_m …)
     832         >(minus_Sn_m …)
     833         [ <(pred_succ_n …)
     834             <(pred_succ_n …)
     835             @IH /2/;
     836         | /2/;
     837         ]
     838     | >(minus_Sn_m … H') //;
     839     ]
     840  ] qed.
    828841
    829842(* XXX: putting this in the appropriate case screws up auto?! *)
    830 ntheorem succ_plus_one: ∀n. succ n = n + one.
    831 #n; nelim n; //; nqed.
    832 
    833 ntheorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p).
    834 #p; nelim p; nnormalize;
    835 ##[ //;
    836 ##| #q IH; nrewrite < (plus_n_O …); nrewrite < (plus_n_O …);
    837     nrewrite > IH; nrewrite < (plus_n_Sm …); //;
    838 ##| //;
    839 ##] nqed.
    840 
    841 ntheorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n.
    842 #n; nelim n; //; nqed.
    843 
    844 ntheorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m.
    845 #n; napply pos_elim;
    846 ##[ //;
    847 ##| #m IH; nrewrite < (plus_n_succm …);
    848     nrewrite > (eq_minus_S_pred …);
    849     nrewrite > (minus_Sn_m …); /2/;
    850 ##] nqed.
    851 
    852 ntheorem plus_minus_m_m: ∀n,m:Pos.
     843theorem succ_plus_one: ∀n. succ n = n + one.
     844#n elim n; //; qed.
     845
     846theorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p).
     847#p elim p; normalize;
     848[ //;
     849| #q #IH <(plus_n_O …) <(plus_n_O …)
     850    >IH <(plus_n_Sm …) //;
     851| //;
     852] qed.
     853
     854theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n.
     855#n elim n; //; qed.
     856
     857theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m.
     858#n @pos_elim
     859[ //;
     860| #m #IH <(plus_n_succm …)
     861    >(eq_minus_S_pred …)
     862    >(minus_Sn_m …) /2/;
     863] qed.
     864
     865theorem plus_minus_m_m: ∀n,m:Pos.
    853866  m < n → n = (n-m)+m.
    854 #n; #m; #lemn; napplyS sym_eq;
    855 napplyS (plus_minus m n m); //; nqed.
    856 
    857 ntheorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (n-m)+m.
    858 napply pos_elim;
    859   ##[//
    860   ##|#a; #Hind; napply pos_cases; //; 
    861      #n;
    862      nrewrite > (minus_S_S …);
     867#n #m #lemn applyS sym_eq;
     868applyS (plus_minus m n m); //; qed.
     869
     870theorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (n-m)+m.
     871@pos_elim
     872  [//
     873  |#a #Hind @pos_cases //; 
     874     #n
     875     >(minus_S_S …)
    863876     /2/;
    864   ##]
    865 nqed.
    866 
    867 ntheorem minus_to_plus :∀n,m,p:Pos.
     877  ]
     878qed.
     879
     880theorem minus_to_plus :∀n,m,p:Pos.
    868881  m < n → n-m = p → n = m+p.
    869 #n; #m; #p; #lemn; #eqp; napplyS plus_minus_m_m; //;
    870 nqed.
    871 
    872 ntheorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p.
     882#n #m #p #lemn #eqp applyS plus_minus_m_m; //;
     883qed.
     884
     885theorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p.
    873886(* /4/ done in 43.5 *)
    874 #n; #m; #p; #eqp;
    875 napply sym_eq;
    876 napplyS (minus_plus_m_m p m);
    877 nqed.
    878 
    879 ntheorem minus_pred_pred : ∀n,m:Pos. one < n → one < m →
     887#n #m #p #eqp
     888@sym_eq
     889applyS (minus_plus_m_m p m);
     890qed.
     891
     892theorem minus_pred_pred : ∀n,m:Pos. one < n → one < m →
    880893pred n - pred m = n - m.
    881 #n; #m; #posn; #posm;
    882 napply (lt_one_n_elim n posn);
    883 napply (lt_one_n_elim m posm);//.
    884 nqed.
     894#n #m #posn #posm
     895@(lt_one_n_elim n posn)
     896@(lt_one_n_elim m posm) //.
     897qed.
    885898
    886899(* monotonicity and galois *)
    887900
    888 ntheorem monotonic_le_minus_l:
     901theorem monotonic_le_minus_l:
    889902∀p,q,n:Pos. q ≤ p → q-n ≤ p-n.
    890 napply pos_elim2; #p; #q;
    891   ##[#lePO; napply (le_n_one_elim ? lePO);//;
    892   ##|//;
    893   ##|#Hind; napply pos_cases;
    894     ##[/2/;
    895     ##|#a; #leSS; nrewrite > (minus_S_S …); nrewrite > (minus_S_S …); napply Hind; /2/;
    896     ##]
    897   ##]
    898 nqed.
    899 
    900 ntheorem le_minus_to_plus: ∀n,m,p:Pos. n-m ≤ p → n≤ p+m.
    901 #n; #m; #p; #lep;
    902 napply transitive_le;
    903   ##[##|napply le_plus_minus_m_m
    904   ##|napply monotonic_le_plus_l;//;
    905   ##]
    906 nqed.
    907 
    908 ntheorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → n-m ≤ p.
    909 #n; #m; #p; #lep;
     903@pos_elim2 #p #q
     904  [#lePO @(le_n_one_elim ? lePO) //;
     905  |//;
     906  |#Hind @pos_cases
     907    [/2/;
     908    |#a #leSS >(minus_S_S …) >(minus_S_S …) @Hind /2/;
     909    ]
     910  ]
     911qed.
     912
     913theorem le_minus_to_plus: ∀n,m,p:Pos. n-m ≤ p → n≤ p+m.
     914#n #m #p #lep
     915@transitive_le
     916  [|apply le_plus_minus_m_m
     917  |@monotonic_le_plus_l //;
     918  ]
     919qed.
     920
     921theorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → n-m ≤ p.
     922#n #m #p #lep
    910923(* bello *)
    911 napplyS monotonic_le_minus_l;//;
     924applyS monotonic_le_minus_l;//;
    912925(* /2/; *)
    913 nqed.
    914 
    915 ntheorem monotonic_le_minus_r:
     926qed.
     927
     928theorem monotonic_le_minus_r:
    916929∀p,q,n:Pos. q ≤ p → n-p ≤ n-q.
    917 #p; #q; #n; #lepq;
    918 napply le_plus_to_minus;
    919 napply (transitive_le ??? (le_plus_minus_m_m ? q));/2/;
    920 nqed.
     930#p #q #n #lepq
     931@le_plus_to_minus
     932@(transitive_le ??? (le_plus_minus_m_m ? q)) /2/;
     933qed.
    921934
    922935(*********************** boolean arithmetics ********************)
    923936include "basics/bool.ma".
    924937
    925 nlet rec eqb n m ≝
     938let rec eqb n m ≝
    926939match n with
    927940  [ one ⇒ match m with [ one ⇒ true | _ ⇒ false]
     
    929942  | p1 p ⇒ match m with [ p1 q ⇒ eqb p q | _ ⇒ false]
    930943  ].
    931            
    932 ntheorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop.
     944
     945theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop.
    933946(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
    934 #n; nelim n;
    935 ##[ #m; ncases m; nnormalize;
    936   ##[ /2/;
    937   ##| ##2,3: #m' P t f; napply f; @; #H; ndestruct;
    938   ##]
    939 ##| #n' IH m; ncases m; nnormalize;
    940   ##[ #P t f; napply f; @; #H; ndestruct;
    941   ##| #m' P t f; napply IH;
    942     ##[ /2/;
    943     ##| (* XXX: automation assertion *) #ne; napply f; @; #e; ndestruct;
    944         nelim ne; /2/;
    945     ##]
    946   ##| #m' P t f; napply f; @; #H; ndestruct;
    947   ##]
    948 ##| #n' IH m; ncases m; nnormalize;
    949   ##[ #P t f; napply f; @; #H; ndestruct;
    950   ##| #m' P t f; napply f; @; #H; ndestruct;
    951   ##| #m' P t f; napply IH;
    952     ##[ /2/;
    953     ##| (* XXX: automation assertion *) #ne; napply f; @; #e; ndestruct;
    954         nelim ne; /2/;
    955     ##]
    956   ##]
    957 ##] nqed.
    958 
    959 ntheorem eqb_n_n: ∀n:Pos. eqb n n = true.
    960 #n; nelim n; nnormalize; //.
    961 nqed.
    962 
    963 ntheorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m.
    964 #n; #m; napply (eqb_elim n m);//;
    965 #_; #abs; napply False_ind; /2/;
    966 nqed.
    967 
    968 ntheorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m.
    969 #n; #m; napply (eqb_elim n m);/2/;
    970 nqed.
    971 
    972 ntheorem eq_to_eqb_true: ∀n,m:Pos.
     947#n elim n;
     948[ #m cases m normalize
     949  [ /2/
     950  | 2,3: #m' #P #t #f @f % #H destruct
     951  ]
     952| #n' #IH #m cases m normalize
     953  [ #P #t #f @f % #H destruct
     954  | #m' #P #t #f @IH
     955    [ /2/
     956    | * #ne @f % #e @ne destruct @refl
     957    ]
     958  | #m' #P #t #f @f % #H destruct;
     959  ]
     960| #n' #IH #m cases m; normalize;
     961  [ #P #t #f @f % #H destruct;
     962  | #m' #P #t #f @f % #H destruct;
     963  | #m' #P #t #f @IH
     964    [ /2/;
     965    | * #ne @f % #e @ne destruct @refl
     966    ]
     967  ]
     968] qed.
     969
     970theorem eqb_n_n: ∀n:Pos. eqb n n = true.
     971#n elim n; normalize; //.
     972qed.
     973
     974theorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m.
     975#n #m @(eqb_elim n m) //;
     976#_ #abs @False_ind /2/;
     977qed.
     978
     979theorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m.
     980#n #m @(eqb_elim n m) /2/;
     981qed.
     982
     983theorem eq_to_eqb_true: ∀n,m:Pos.
    973984  n = m → eqb n m = true.
    974 //; nqed.
    975 
    976 ntheorem not_eq_to_eqb_false: ∀n,m:Pos.
     985//; qed.
     986
     987theorem not_eq_to_eqb_false: ∀n,m:Pos.
    977988  n ≠  m → eqb n m = false.
    978 #n; #m; #noteq;
    979 napply eqb_elim;//;
    980 #Heq; napply False_ind; /2/;
    981 nqed.
    982 
    983 nlet rec leb n m ≝
     989#n #m #noteq
     990@eqb_elim //;
     991#Heq @False_ind /2/;
     992qed.
     993
     994let rec leb n m ≝
    984995match partial_minus n m with
    985996[ MinusNeg ⇒ true
     
    988999].
    9891000
    990 nlemma leb_unfold_hack: ∀n,m:Pos. leb n m =
     1001lemma leb_unfold_hack: ∀n,m:Pos. leb n m =
    9911002match partial_minus n m with
    9921003[ MinusNeg ⇒ true
    9931004| MinusZero ⇒ true
    9941005| MinusPos _ ⇒ false
    995 ]. #n m; (* XXX: why on earth do I need to case split? *) ncases n; //; nqed.
    996 
    997 ntheorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop.
     1006]. #n #m (* XXX: why on earth do I need to case split? *) cases n; //; qed.
     1007
     1008theorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop.
    9981009(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
    999 napply pos_elim2;
    1000 ##[ #n; ncases n; nnormalize; /2/;
    1001 ##| #n; ncases n; nnormalize;
    1002   ##[ /2/;
    1003   ##| ##2,3: #m' P t f; napply f; /2/; @; #H; ninversion H;
    1004     ##[ #H'; ndestruct;
    1005     ##| #p; /2/;
    1006     ##]
    1007   ##]
    1008 ##| #n m IH P t f; nrewrite > (leb_unfold_hack …);
    1009     nrewrite > (partialminus_S_S n m);
    1010     nrewrite < (leb_unfold_hack …);
    1011     napply IH; #H; /3/;
    1012 ##] nqed.
    1013 
    1014 ntheorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m.
    1015 #n; #m; napply leb_elim;
    1016   ##[//;
    1017   ##|#_; #abs; napply False_ind; /2/;
    1018   ##]
    1019 nqed.
    1020 
    1021 ntheorem leb_false_to_not_le:∀n,m:Pos.
     1010@pos_elim2
     1011[ #n cases n; normalize; /2/;
     1012| #n cases n; normalize;
     1013  [ /2/;
     1014  | 2,3: #m' #P #t #f @f /2/; % #H inversion H;
     1015    [ #H' destruct;
     1016    | #p /2/;
     1017    ]
     1018  ]
     1019| #n #m #IH #P #t #f >(leb_unfold_hack …)
     1020    >(partialminus_S_S n m)
     1021    <(leb_unfold_hack …)
     1022    @IH #H /3/;
     1023] qed.
     1024
     1025theorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m.
     1026#n #m @leb_elim
     1027  [//;
     1028  |#_ #abs @False_ind /2/;
     1029  ]
     1030qed.
     1031
     1032theorem leb_false_to_not_le:∀n,m:Pos.
    10221033  leb n m = false → n ≰ m.
    1023 #n; #m; napply leb_elim;
    1024   ##[#_; #abs; napply False_ind; /2/;
    1025   ##|//;
    1026   ##]
    1027 nqed.
    1028 
    1029 ntheorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true.
    1030 #n; #m; napply leb_elim; //;
    1031 #H; #H1; napply False_ind; /2/;
    1032 nqed.
    1033 
    1034 ntheorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false.
    1035 #n; #m; napply leb_elim; //;
    1036 #H; #H1; napply False_ind; /2/;
    1037 nqed.
    1038 
    1039 ntheorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false.
    1040 /3/; nqed.
     1034#n #m @leb_elim
     1035  [#_ #abs @False_ind /2/;
     1036  |//;
     1037  ]
     1038qed.
     1039
     1040theorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true.
     1041#n #m @leb_elim //;
     1042#H #H1 @False_ind /2/;
     1043qed.
     1044
     1045theorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false.
     1046#n #m @leb_elim //;
     1047#H #H1 @False_ind /2/;
     1048qed.
     1049
     1050theorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false.
     1051/3/; qed.
    10411052
    10421053
    10431054(***** comparison *****)
    10441055
    1045 ndefinition pos_compare : Pos → Pos → compare ≝
     1056definition pos_compare : Pos → Pos → compare ≝
    10461057λn,m.match partial_minus n m with
    10471058[ MinusNeg ⇒ LT
     
    10501061].
    10511062
    1052 ntheorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ.
    1053 #n; nnormalize; nrewrite > (partial_minus_n_n n);
    1054 //; nqed.
    1055 
    1056 ntheorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m).
    1057 #n m; nnormalize;
    1058 nrewrite > (partialminus_S_S …);
     1063theorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ.
     1064#n normalize; >(partial_minus_n_n n)
     1065//; qed.
     1066
     1067theorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m).
     1068#n #m normalize;
     1069>(partialminus_S_S …)
    10591070//;
    1060 nqed.
    1061 
    1062 ntheorem pos_compare_pred_pred:
     1071qed.
     1072
     1073theorem pos_compare_pred_pred:
    10631074  ∀n,m.one < n → one < m → pos_compare n m = pos_compare (pred n) (pred m).
    1064 #n;#m;#Hn;#Hm;
    1065 napply (lt_one_n_elim n Hn);
    1066 napply (lt_one_n_elim m Hm);
    1067 #p;#q; nrewrite < (pred_succ_n ?); nrewrite < (pred_succ_n ?);
    1068 nrewrite < (pos_compare_S_S …); //;
    1069 nqed.
    1070 
    1071 ntheorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT.
    1072 #n; nelim n; //; nqed.
    1073 
    1074 ntheorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT.
    1075 #n; nelim n; //; nqed.
    1076 
    1077 ntheorem pos_compare_to_Prop:
     1075#n #m #Hn #Hm
     1076@(lt_one_n_elim n Hn)
     1077@(lt_one_n_elim m Hm)
     1078#p #q <(pred_succ_n ?) <(pred_succ_n ?)
     1079<(pos_compare_S_S …) //;
     1080qed.
     1081
     1082theorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT.
     1083#n elim n; //; qed.
     1084
     1085theorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT.
     1086#n elim n; //; qed.
     1087
     1088theorem pos_compare_to_Prop:
    10781089  ∀n,m.match (pos_compare n m) with
    10791090    [ LT ⇒ n < m
    10801091    | EQ ⇒ n = m
    10811092    | GT ⇒ m < n ].
    1082 #n;#m;
    1083 napply (pos_elim2 (λn,m.match (pos_compare n m) with
     1093#n #m
     1094@(pos_elim2 (λn,m.match (pos_compare n m) with
    10841095  [ LT ⇒ n < m
    10851096  | EQ ⇒ n = m
    10861097  | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *)
    1087 ##[##1,2:napply pos_cases;
    1088   ##[ ##1,3: /2/;
    1089   ##| ##2,4: #m'; ncases m'; //;
    1090   ##]
    1091 ##|#n1;#m1;nnormalize;nrewrite < (pos_compare_S_S …); ncases (pos_compare n1 m1);
    1092    ##[##1,3:nnormalize;#IH;napply le_succ_succ;//;
    1093    ##|nnormalize;#IH;nrewrite > IH;//]
    1094 nqed.
    1095 
    1096 ntheorem pos_compare_n_m_m_n:
     1098[1,2:@pos_cases
     1099  [ 1,3: /2/;
     1100  | 2,4: #m' cases m'; //;
     1101  ]
     1102|#n1 #m1 normalize;<(pos_compare_S_S …) cases (pos_compare n1 m1);
     1103   [1,3:normalize;#IH @le_succ_succ //;
     1104   |normalize;#IH >IH //]
     1105qed.
     1106
     1107theorem pos_compare_n_m_m_n:
    10971108  ∀n,m:Pos.pos_compare n m = compare_invert (pos_compare m n).
    1098 #n;#m;
    1099 napply (pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n)))
    1100 ##[##1,2:#n1;ncases n1;/2/;
    1101 ##|#n1;#m1;
    1102 nrewrite < (pos_compare_S_S …);
    1103 nrewrite < (pos_compare_S_S …);
    1104 #IH;nnormalize;napply IH]
    1105 nqed.
     1109#n #m
     1110@(pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n)))
     1111[1,2:#n1 cases n1;/2/;
     1112|#n1 #m1
     1113<(pos_compare_S_S …)
     1114<(pos_compare_S_S …)
     1115#IH normalize @IH]
     1116qed.
    11061117     
    1107 ntheorem pos_compare_elim :
     1118theorem pos_compare_elim :
    11081119  ∀n,m:Pos. ∀P:compare → Prop.
    11091120    (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (pos_compare n m).
    1110 #n;#m;#P;#Hlt;#Heq;#Hgt;
    1111 ncut (match (pos_compare n m) with
     1121#n #m #P #Hlt #Heq #Hgt
     1122cut (match (pos_compare n m) with
    11121123    [ LT ⇒ n < m
    11131124    | EQ ⇒ n=m
    11141125    | GT ⇒ m < n] →
    11151126  P (pos_compare n m))
    1116 ##[ncases (pos_compare n m);
    1117    ##[napply Hlt
    1118    ##|napply Heq
    1119    ##|napply Hgt]
    1120 ##|#Hcut;napply Hcut;//;
    1121 nqed.
    1122 
    1123 ninductive cmp_cases (n,m:Pos) : CProp[0] ≝
     1127[cases (pos_compare n m);
     1128   [@Hlt
     1129   |@Heq
     1130   |@Hgt]
     1131|#Hcut @Hcut //;
     1132qed.
     1133
     1134inductive cmp_cases (n,m:Pos) : CProp[0] ≝
    11241135  | cmp_le : n ≤ m → cmp_cases n m
    11251136  | cmp_gt : m < n → cmp_cases n m.
    11261137
    1127 ntheorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m.
     1138theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m.
    11281139(* sic
    1129 #n;#m;#H;nelim H
    1130 ##[//
    1131 ##|/2/] *)
    1132 /2/; nqed.
    1133 
    1134 nlemma cmp_nat: ∀n,m:Pos.cmp_cases n m.
    1135 #n;#m; nlapply (pos_compare_to_Prop n m);
    1136 ncases (pos_compare n m);nnormalize; /3/;
    1137 nqed.
    1138 
    1139 
    1140 
    1141 
    1142 
    1143 nlet rec two_power_nat (n:nat) : Pos ≝
     1140#n #m #H elim H
     1141[//
     1142|/2/] *)
     1143/2/; qed.
     1144
     1145lemma cmp_nat: ∀n,m:Pos.cmp_cases n m.
     1146#n #m lapply (pos_compare_to_Prop n m)
     1147cases (pos_compare n m);normalize; /3/;
     1148qed.
     1149
     1150
     1151
     1152
     1153let rec two_power_nat (n:nat) : Pos ≝
    11441154match n with
    11451155[ O ⇒ one
     
    11471157].
    11481158
    1149 ndefinition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
     1159definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
Note: See TracChangeset for help on using the changeset viewer.