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

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/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
Note: See TracChangeset for help on using the changeset viewer.