Changeset 1523


Ignore:
Timestamp:
Nov 21, 2011, 4:29:16 PM (8 years ago)
Author:
campbell
Message:

Separate out positive and Z definitions from extralib.ma.
Minor syntax updates.

Location:
src
Files:
1 added
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/Mem.ma

    r1516 r1523  
    3434include "common/Values.ma".
    3535(*include "AST.ma".*)
    36 include "utilities/extralib.ma".
     36include "utilities/binary/division.ma".
    3737
    3838definition update : ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z → A. Z → A ≝
  • src/utilities/binary/Z.ma

    r1521 r1523  
    635635qed.
    636636
    637 lemma eq_rect_Type0_r:
    638  ∀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 @(eq_rect_r ??? p0) assumption.
    640 qed.
    641 
    642637theorem associative_Zplus: associative Z Zplus.
    643638(* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
     
    719714| neg _ ⇒ OZ  (* same fib as Coq *)
    720715].
     716
     717
     718
     719lemma eqZb_z_z : ∀z.eqZb z z = true.
     720#z cases z;normalize;//;
     721qed.
     722
     723
     724
     725lemma injective_Z_of_nat : injective ? ? Z_of_nat.
     726normalize;
     727#n #m cases n;cases m;normalize;//;
     728[ 1,2: #n' #H destruct
     729| #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) //
     730] qed.
     731
     732lemma reflexive_Zle : reflexive ? Zle.
     733#x cases x; //; qed.
     734
     735lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
     736#n cases n;normalize;//;qed.
     737
     738lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
     739#x cases x; //;
     740#n cases n; //; qed.
     741
     742lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
     743#x #y
     744@pos_elim
     745 [ 2: #n' #IH ]
     746>(Zplus_Zsucc_Zpred y ?)
     747[ >(Zpred_Zsucc (pos n'))
     748 #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??)
     749    @Zsucc_le
     750| #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le
     751] qed.
     752
     753theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
     754#x #y cases x;
     755[ cases y;
     756  [ 1,2: //
     757  | #n @False_ind
     758  ]
     759| #n cases y;
     760  [ normalize; @False_ind
     761  | #m @(pos_cases … n) /2/;
     762  | #m normalize; @False_ind
     763  ]
     764| #n cases y; /2/;
     765] qed.
     766   
     767theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
     768#n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt
     769@(transitive_Zle … Hle) /2/;
     770qed.
     771
     772include "basics/types.ma".
     773
     774definition decidable_eq_Z_Type : ∀z1,z2:Z. (z1 = z2) + (z1 ≠ z2).
     775#z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H
     776[% //
     777|%2 //]
     778qed.
     779
     780lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
     781#z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //;
     782#H #H' @False_ind @(absurd ? H H')
     783qed.
     784
     785(* Z.ma *)
     786
     787definition Zge: Z → Z → Prop ≝
     788λn,m:Z.m ≤ n.
     789
     790interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).
     791
     792definition Zgt: Z → Z → Prop ≝
     793λn,m:Z.m<n.
     794
     795interpretation "integer 'greater than'" 'gt x y = (Zgt x y).
     796
     797interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
     798
     799let rec Zleb (x:Z) (y:Z) : bool ≝
     800  match x with
     801  [ OZ ⇒
     802    match y with
     803    [ OZ ⇒ true
     804    | pos m ⇒ true
     805    | neg m ⇒ false ]
     806  | pos n ⇒
     807    match y with
     808    [ OZ ⇒ false
     809    | pos m ⇒ leb n m
     810    | neg m ⇒ false ]
     811  | neg n ⇒
     812    match y with
     813    [ OZ ⇒ true
     814    | pos m ⇒ true
     815    | neg m ⇒ leb m n ]].
     816   
     817let rec Zltb (x:Z) (y:Z) : bool ≝
     818  match x with
     819  [ OZ ⇒
     820    match y with
     821    [ OZ ⇒ false
     822    | pos m ⇒ true
     823    | neg m ⇒ false ]
     824  | pos n ⇒
     825    match y with
     826    [ OZ ⇒ false
     827    | pos m ⇒ leb (succ n) m
     828    | neg m ⇒ false ]
     829  | neg n ⇒
     830    match y with
     831    [ OZ ⇒ true
     832    | pos m ⇒ true
     833    | neg m ⇒ leb (succ m) n ]].
     834
     835
     836
     837theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
     838#n #m cases n;cases m; //;
     839[ 1,2: #m' normalize; #H @(False_ind ? H)
     840| 3,5: #n' #m' normalize; @le_to_leb_true
     841| 4: #n' #m' normalize; #H @(False_ind ? H)
     842] qed.
     843
     844theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
     845#n #m cases n;cases m; //;
     846[ 1,2: #m' normalize; #H destruct
     847| 3,5: #n' #m' normalize; @leb_true_to_le
     848| 4: #n' #m' normalize; #H destruct
     849] qed.
     850
     851theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
     852#n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct;
     853qed.
     854
     855theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
     856#n #m cases n;cases m; //;
     857[ normalize; #H @(False_ind ? H)
     858| 2,3: #m' normalize; #H @(False_ind ? H)
     859| 4,6: #n' #m' normalize; @le_to_leb_true
     860| #n' #m' normalize; #H @(False_ind ? H)
     861] qed.
     862
     863theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
     864#n #m cases n;cases m; //;
     865[ normalize; #H destruct
     866| 2,3: #m' normalize; #H destruct
     867| 4,6: #n' #m' @leb_true_to_le
     868| #n' #m' normalize; #H destruct
     869] qed.
     870
     871theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
     872#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct;
     873qed.
     874
     875theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
     876(n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
     877#n #m #P #Hle #Hnle
     878lapply (refl ? (Zleb n m));
     879elim (Zleb n m) in ⊢ ((???%)→%);
     880#Hb
     881[ @Hle @(Zleb_true_to_Zle … Hb)
     882| @Hnle @(Zleb_false_to_not_Zle … Hb)
     883] qed.
     884
     885theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
     886(n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
     887#n #m #P #Hlt #Hnlt
     888lapply (refl ? (Zltb n m));
     889elim (Zltb n m) in ⊢ ((???%)→%);
     890#Hb
     891[ @Hlt @(Zltb_true_to_Zlt … Hb)
     892| @Hnlt @(Zltb_false_to_not_Zlt … Hb)
     893] qed.
     894
     895lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
     896#x #y cases x; cases y; /2/;
     897#n #m @(pos_cases … n) @(pos_cases … m)
     898[ //;
     899| #n' /2/;
     900| #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/;
     901| #n' #m' #H normalize in H;
     902    >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/;
     903] qed.
     904
     905lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
     906#x #y cases x; cases y;
     907[ 1,2,7,8,9: /2/;
     908| 3,4: #m normalize; *;
     909| #m #n @(pos_cases … n) @(pos_cases … m)
     910  [ 1,2: /2/;
     911  | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/;
     912  | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/;
     913  ]
     914| #m #n normalize; *;
     915] qed.
     916
     917lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
     918#n cases n; //; #n' #a #b #H
     919[ @(pos_elim … n')
     920  [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/;
     921  | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //;
     922      >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/;
     923  ]
     924| @(pos_elim … n')
     925  [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;
     926  | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //;
     927      >(Zplus_Zpred …) >(Zplus_Zpred …) /2/;
     928  ]
     929] qed.
     930
     931lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
     932/2/; qed.
     933
     934let rec Z_times (x:Z) (y:Z) : Z ≝
     935match x with
     936[ OZ ⇒ OZ
     937| pos n ⇒
     938  match y with
     939  [ OZ ⇒ OZ
     940  | pos m ⇒ pos (n*m)
     941  | neg m ⇒ neg (n*m)
     942  ]
     943| neg n ⇒
     944  match y with
     945  [ OZ ⇒ OZ
     946  | pos m ⇒ neg (n*m)
     947  | neg m ⇒ pos (n*m)
     948  ]
     949].
     950interpretation "integer multiplication" 'times x y = (Z_times x y).
     951
     952
     953
     954definition Zmax : Z → Z → Z ≝
     955  λx,y.match Z_compare x y with
     956  [ LT ⇒ y
     957  | _ ⇒ x ].
     958
     959lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
     960#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     961/3/ qed.
     962
     963lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
     964#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     965whd in ⊢ (% → ??%); /3/ qed.
     966
     967
     968lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
     969#x #y cases y;
     970[ #H @(False_ind … H)
     971| #m #_ cases x; //; #n
     972    whd in ⊢ (?%?);
     973    lapply (pos_compare_to_Prop n m);
     974    cases (pos_compare n m); /2/
     975    #lt whd <(minus_Sn_m … lt) /2/;
     976| #m #H @(False_ind … H)
     977] qed.
     978
  • src/utilities/binary/positive.ma

    r1517 r1523  
    11601160definition max : Pos → Pos → Pos ≝
    11611161λn,m. match leb n m with [ true ⇒ m | _ ⇒ n].
     1162
     1163
     1164
     1165lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
     1166#n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m);
     1167[ //;
     1168| 2,3: #H @False_ind @(absurd ? lt ?) /3/;
     1169] qed.
     1170
     1171lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     1172#n #m @eqb_elim //; qed.
  • src/utilities/extralib.ma

    r1516 r1523  
    1717include "basics/logic.ma".
    1818include "utilities/pair.ma".
    19 include "utilities/binary/Z.ma".
    20 include "utilities/binary/positive.ma".
    2119
    2220lemma eq_rect_Type0_r:
     
    5149  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
    5250 
    53 
    54 (* TODO: move to Z.ma *)
    55 
    56 lemma eqZb_z_z : ∀z.eqZb z z = true.
    57 #z cases z;normalize;//;
    58 qed.
    59 
    60 (* XXX: divides goes to arithmetics *)
    61 inductive dividesP (n,m:Pos) : Prop ≝
    62 | witness : ∀p:Pos.m = times n p → dividesP n m.
    63 interpretation "positive divides" 'divides n m = (dividesP n m).
    64 interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).
    65 
    66 definition dividesZ : Z → Z → Prop ≝
    67 λx,y. match x with
    68 [ OZ ⇒ False
    69 | pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
    70 | neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
    71 ].
    72 
    73 interpretation "integer divides" 'divides n m = (dividesZ n m).
    74 interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).
     51 
     52 
    7553
    7654(* should be proved in nat.ma, but it's not! *)
     
    8260] qed.
    8361
    84 lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
    85 #n #m @eqb_elim //; qed.
    86 
    87 lemma injective_Z_of_nat : injective ? ? Z_of_nat.
    88 normalize;
    89 #n #m cases n;cases m;normalize;//;
    90 [ 1,2: #n' #H destruct
    91 | #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) //
    92 ] qed.
    93 
    94 lemma reflexive_Zle : reflexive ? Zle.
    95 #x cases x; //; qed.
    96 
    97 lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
    98 #n cases n;normalize;//;qed.
    99 
    100 lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
    101 #x cases x; //;
    102 #n cases n; //; qed.
    103 
    104 lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
    105 #x #y
    106 @pos_elim
    107  [ 2: #n' #IH ]
    108 >(Zplus_Zsucc_Zpred y ?)
    109 [ >(Zpred_Zsucc (pos n'))
    110  #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??)
    111     @Zsucc_le
    112 | #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le
    113 ] qed.
    114 
    115 (* XXX: Zmax must go to arithmetics *)
    116 definition Zmax : Z → Z → Z ≝
    117   λx,y.match Z_compare x y with
    118   [ LT ⇒ y
    119   | _ ⇒ x ].
    120 
    121 lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
    122 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
    123 /3/ qed.
    124 
    125 lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
    126 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
    127 whd in ⊢ (% → ??%); /3/ qed.
    128 
    129 theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
    130 #x #y cases x;
    131 [ cases y;
    132   [ 1,2: //
    133   | #n @False_ind
    134   ]
    135 | #n cases y;
    136   [ normalize; @False_ind
    137   | #m @(pos_cases … n) /2/;
    138   | #m normalize; @False_ind
    139   ]
    140 | #n cases y; /2/;
    141 ] qed.
    142    
    143 theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
    144 #n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt
    145 @(transitive_Zle … Hle) /2/;
    146 qed.
    147 
    148 definition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
    149 #z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H
    150 [% //
    151 |%2 //]
    152 qed.
    153 
    154 lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
    155 #z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //;
    156 #H #H' @False_ind @(absurd ? H H')
    157 qed.
    158 
    159 (* Z.ma *)
    160 
    161 definition Zge: Z → Z → Prop ≝
    162 λn,m:Z.m ≤ n.
    163 
    164 interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).
    165 
    166 definition Zgt: Z → Z → Prop ≝
    167 λn,m:Z.m<n.
    168 
    169 interpretation "integer 'greater than'" 'gt x y = (Zgt x y).
    170 
    171 interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
    172 
    173 let rec Zleb (x:Z) (y:Z) : bool ≝
    174   match x with
    175   [ OZ ⇒
    176     match y with
    177     [ OZ ⇒ true
    178     | pos m ⇒ true
    179     | neg m ⇒ false ]
    180   | pos n ⇒
    181     match y with
    182     [ OZ ⇒ false
    183     | pos m ⇒ leb n m
    184     | neg m ⇒ false ]
    185   | neg n ⇒
    186     match y with
    187     [ OZ ⇒ true
    188     | pos m ⇒ true
    189     | neg m ⇒ leb m n ]].
    190    
    191 let rec Zltb (x:Z) (y:Z) : bool ≝
    192   match x with
    193   [ OZ ⇒
    194     match y with
    195     [ OZ ⇒ false
    196     | pos m ⇒ true
    197     | neg m ⇒ false ]
    198   | pos n ⇒
    199     match y with
    200     [ OZ ⇒ false
    201     | pos m ⇒ leb (succ n) m
    202     | neg m ⇒ false ]
    203   | neg n ⇒
    204     match y with
    205     [ OZ ⇒ true
    206     | pos m ⇒ true
    207     | neg m ⇒ leb (succ m) n ]].
    208 
    209 
    210 
    211 theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
    212 #n #m cases n;cases m; //;
    213 [ 1,2: #m' normalize; #H @(False_ind ? H)
    214 | 3,5: #n' #m' normalize; @le_to_leb_true
    215 | 4: #n' #m' normalize; #H @(False_ind ? H)
    216 ] qed.
    217 
    218 theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
    219 #n #m cases n;cases m; //;
    220 [ 1,2: #m' normalize; #H destruct
    221 | 3,5: #n' #m' normalize; @leb_true_to_le
    222 | 4: #n' #m' normalize; #H destruct
    223 ] qed.
    224 
    225 theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
    226 #n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct;
    227 qed.
    228 
    229 theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
    230 #n #m cases n;cases m; //;
    231 [ normalize; #H @(False_ind ? H)
    232 | 2,3: #m' normalize; #H @(False_ind ? H)
    233 | 4,6: #n' #m' normalize; @le_to_leb_true
    234 | #n' #m' normalize; #H @(False_ind ? H)
    235 ] qed.
    236 
    237 theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
    238 #n #m cases n;cases m; //;
    239 [ normalize; #H destruct
    240 | 2,3: #m' normalize; #H destruct
    241 | 4,6: #n' #m' @leb_true_to_le
    242 | #n' #m' normalize; #H destruct
    243 ] qed.
    244 
    245 theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
    246 #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct;
    247 qed.
    248 
    249 theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
    250 (n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
    251 #n #m #P #Hle #Hnle
    252 lapply (refl ? (Zleb n m));
    253 elim (Zleb n m) in ⊢ ((???%)→%);
    254 #Hb
    255 [ @Hle @(Zleb_true_to_Zle … Hb)
    256 | @Hnle @(Zleb_false_to_not_Zle … Hb)
    257 ] qed.
    258 
    259 theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
    260 (n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
    261 #n #m #P #Hlt #Hnlt
    262 lapply (refl ? (Zltb n m));
    263 elim (Zltb n m) in ⊢ ((???%)→%);
    264 #Hb
    265 [ @Hlt @(Zltb_true_to_Zlt … Hb)
    266 | @Hnlt @(Zltb_false_to_not_Zlt … Hb)
    267 ] qed.
    268 
    269 lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
    270 #x #y cases x; cases y; /2/;
    271 #n #m @(pos_cases … n) @(pos_cases … m)
    272 [ //;
    273 | #n' /2/;
    274 | #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/;
    275 | #n' #m' #H normalize in H;
    276     >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/;
    277 ] qed.
    278 
    279 lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
    280 #x #y cases x; cases y;
    281 [ 1,2,7,8,9: /2/;
    282 | 3,4: #m normalize; *;
    283 | #m #n @(pos_cases … n) @(pos_cases … m)
    284   [ 1,2: /2/;
    285   | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/;
    286   | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/;
    287   ]
    288 | #m #n normalize; *;
    289 ] qed.
    290 
    291 lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
    292 #n cases n; //; #n' #a #b #H
    293 [ @(pos_elim … n')
    294   [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/;
    295   | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //;
    296       >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/;
    297   ]
    298 | @(pos_elim … n')
    299   [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;
    300   | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //;
    301       >(Zplus_Zpred …) >(Zplus_Zpred …) /2/;
    302   ]
    303 ] qed.
    304 
    305 lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
    306 /2/; qed.
    307 
    308 let rec Z_times (x:Z) (y:Z) : Z ≝
    309 match x with
    310 [ OZ ⇒ OZ
    311 | pos n ⇒
    312   match y with
    313   [ OZ ⇒ OZ
    314   | pos m ⇒ pos (n*m)
    315   | neg m ⇒ neg (n*m)
    316   ]
    317 | neg n ⇒
    318   match y with
    319   [ OZ ⇒ OZ
    320   | pos m ⇒ neg (n*m)
    321   | neg m ⇒ pos (n*m)
    322   ]
    323 ].
    324 interpretation "integer multiplication" 'times x y = (Z_times x y).
    32562(* datatypes/list.ma *)
    32663
     
    33875  ]
    33976] qed.
    340 
    341 (* division *)
    342 
    343 inductive natp : Type[0] ≝
    344 | pzero : natp
    345 | ppos  : Pos → natp.
    346 
    347 definition natp0 ≝
    348 λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
    349 
    350 definition natp1 ≝
    351 λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
    352 
    353 let rec divide (m,n:Pos) on m ≝
    354 match m with
    355 [ one ⇒
    356   match n with
    357   [ one ⇒ 〈ppos one,pzero〉
    358   | _ ⇒ 〈pzero,ppos one〉
    359   ]
    360 | p0 m' ⇒
    361   match divide m' n with
    362   [ pair q r ⇒
    363     match r with
    364     [ pzero ⇒ 〈natp0 q,pzero〉
    365     | ppos r' ⇒
    366       match partial_minus (p0 r') n with
    367       [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
    368       | MinusZero ⇒ 〈natp1 q, pzero〉
    369       | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
    370       ]
    371     ]
    372   ]
    373 | p1 m' ⇒
    374   match divide m' n with
    375   [ pair q r ⇒
    376     match r with
    377     [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
    378     | ppos r' ⇒
    379       match partial_minus (p1 r') n with
    380       [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
    381       | MinusZero ⇒ 〈natp1 q, pzero〉
    382       | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
    383       ]
    384     ]
    385   ]
    386 ].
    387 
    388 definition div ≝ λm,n. fst ?? (divide m n).
    389 definition mod ≝ λm,n. snd ?? (divide m n).
    390 
    391 lemma pred_minus: ∀n,m:Pos. pred n - m = pred (n-m).
    392 @pos_elim /3/;
    393 qed.
    394 
    395 lemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
    396 @pos_elim
    397 [ //
    398 | #n #IH #m #p >(succ_plus_one …) >(IH m one) /2/;
    399 ] qed.
    400 
    401 theorem plus_minus_r:
    402 ∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
    403 #m #n #p #le >(commutative_plus …)
    404 >(commutative_plus p ?) @plus_minus //; qed.
    405 
    406 lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
    407 #m #n #p elim m;/2/; qed.
    408 (*
    409 lemma le_to_minus: ∀m,n. m≤n → m-n = 0.
    410 #m #n elim n;
    411 [ <(minus_n_O …) /2/;
    412 | #n' #IH #le inversion le; /2/; #n'' #A #B #C destruct;
    413     >(eq_minus_S_pred …) >(IH A) /2/
    414 ] qed.
    415 *)
    416 lemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
    417 #n #m #p (*elim (decidable_lt n m);*)#lt
    418 (*[*) @(pos_elim … p) //;#p' #IH
    419     <(times_succn_m …) <(times_succn_m …) <(times_succn_m …)
    420     >(minus_plus_distrib …)
    421     <(plus_minus … lt) <IH
    422     >(plus_minus_r …) /2/;
    423 qed.
    424 (*|
    425 lapply (not_lt_to_le … lt); #le
    426 @(pos_elim … p) //; #p'
    427  cut (m-n = one); [ /3/ ]
    428   #mn >mn >(times_n_one …) >(times_n_one …)
    429   #H <H in ⊢ (???%)
    430   @sym_eq @le_n_one_to_eq <H
    431   >(minus_plus_distrib …) @monotonic_le_minus_l
    432   /2/;
    433 ] qed.
    434 
    435 lemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
    436 #m #n #H lapply (refl ? (m-n));elim (m-n) in ⊢ (???% → %);//;
    437 #H' lapply (minus_to_plus … H'); /2/;
    438 <(plus_n_O …) #H'' >H'' in H #H
    439 @False_ind @(absurd ? H ( not_le_Sn_n n))
    440 qed.
    441 *)
    442 
    443 let rec natp_plus (n,m:natp) ≝
    444 match n with
    445 [ pzero ⇒ m
    446 | ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
    447 ].
    448 
    449 let rec natp_times (n,m:natp) ≝
    450 match n with
    451 [ pzero ⇒ pzero
    452 | ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
    453 ].
    454 
    455 inductive natp_lt : natp → Pos → Prop ≝
    456 | plt_zero : ∀n. natp_lt pzero n
    457 | plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
    458 
    459 lemma lt_p0: ∀n:Pos. one < p0 n.
    460 #n normalize; /2/; qed.
    461 
    462 lemma lt_p1: ∀n:Pos. one < p1 n.
    463 #n' normalize; >(?:p1 n' = succ (p0 n')) //; qed.
    464 
    465 lemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
    466 #m elim m;
    467 [ //;
    468 | 2,3: #m' #IH normalize; >IH //;
    469 ] qed.
    470 
    471 lemma pos_nonzero2: ∀n. ∀P:Pos→Type[0]. ∀Q:Type[0]. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n).
    472 #n #P #Q @succ_elim /2/; qed.
    473 
    474 lemma partial_minus_to_Prop: ∀n,m.
    475   match partial_minus n m with
    476   [ MinusNeg ⇒ n < m
    477   | MinusZero ⇒ n = m
    478   | MinusPos r ⇒ n = m+r
    479   ].
    480 #n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m);
    481 normalize; cases (partial_minus n m); /2/; qed.
    482 
    483 lemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
    484 #n #m #lt elim lt; /2/;
    485 qed.
    486 
    487 lemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
    488 #n #m #lt @(transitive_lt ? (p0 m) ?) /2/;
    489 qed.
    490 
    491 lemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
    492 #n #m #lt inversion lt;
    493 [ #H >(succ_injective … H) //;
    494 | #p #H1 #H2 #H3 >(succ_injective … H3)
    495     @(transitive_lt ? (p0 p) ?) /2/;
    496 ]
    497 qed.
    498 
    499 lemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
    500 #n #m #lt elim lt; /2/;
    501 qed.
    502 
    503 
    504 
    505 lemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
    506 #n #m #lt inversion lt;
    507 [ #p #H destruct;
    508 | #n' #m' #lt #e1 #e2 destruct @lt
    509 ] qed.
    510 
    511 lemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
    512 #a #b /2/; qed.
    513 
    514 lemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
    515 #a #b >(?:p1 b = succ (p0 b)) /2/; qed.
    516 
    517 lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
    518 /2/; qed.
    519 
    520 theorem divide_ok : ∀m,n,dv,md.
    521  divide m n = 〈dv,md〉 →
    522  ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
    523 #m #n @(pos_cases … n)
    524 [ >(divide_by_one m) #dv #md #H destruct normalize /2/
    525 | #n' elim m;
    526   [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/
    527   | #m' #IH #dv #md whd in ⊢ (??%? → ?(???%)?);
    528       lapply (refl ? (divide m' (succ n')));
    529       elim (divide m' (succ n')) in ⊢ (???% → % → ?);
    530       #dv' #md' #DIVr elim (IH … DIVr);
    531       whd in ⊢ (? → ? → ??%? → ?);
    532       cases md';
    533       [ cases dv'; normalize;
    534         [ #H destruct
    535         | #dv'' #Hr1 #Hr2 >(pos_nonzero …) #H destruct % /2/
    536         ]
    537       | cases dv'; [ 2: #dv'' ] @succ_elim
    538           normalize; #n #md'' #Hr1 #Hr2
    539           lapply (plt_lt … Hr2); #Hr2'
    540           lapply (partial_minus_to_Prop md'' n);
    541           cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
    542           #lt #e destruct % [ normalize /3 by le_to_le_to_eq, le_n, eq_f/ | *: normalize /2 by plt_zero, plt_pos/ ] @plt_pos
    543           [ 1,3,5,7: @double_lt1 /2/;
    544           | 2,4: @double_lt3 /2/;
    545           | *: @double_lt2 /2/;
    546           ]
    547       ]
    548   | #m' #IH #dv #md whd in ⊢ (??%? → ?);
    549       lapply (refl ? (divide m' (succ n')));
    550       elim (divide m' (succ n')) in ⊢ (???% → % → ?);
    551       #dv' #md' #DIVr elim (IH … DIVr);
    552       whd in ⊢ (? → ? → ??%? → ?); cases md';
    553       [ cases dv'; normalize;
    554         [ #H destruct;
    555         | #dv'' #Hr1 #Hr2 #H destruct; /3/;
    556         ]
    557       | (*cases dv'; [ 2: #dv'' ] @succ_elim
    558           normalize; #n #md'' #Hr1 #Hr2 *) #md'' #Hr1 #Hr2
    559           lapply (plt_lt … Hr2); #Hr2'
    560           whd in ⊢ (??%? → ?);
    561           lapply (partial_minus_to_Prop (p0 md'') (succ n'));
    562           cases (partial_minus (p0 md'') (succ n')); [ 3(*,6,9,12*): #r'' ]
    563           cases dv' in Hr1 ⊢ %; [ 2,4,6: #dv'' ] normalize
    564           #Hr1 destruct [ 1,2,3: >(p0_plus ? md'') ]
    565           #lt #e [ 1,3,4,6: >lt ]
    566           <(pair_eq1 ?????? e) <(pair_eq2 ?????? e)
    567           normalize in ⊢ (?(???%)?); % /2/; @plt_pos
    568           [ cut (succ n' + r'' < p0 (succ n')); /2/;
    569           | cut (succ n' + r'' < p0 (succ n')); /2/; ]]]]
    570 qed.
    571 
    572 lemma mod0_divides: ∀m,n,dv:Pos.
    573   divide n m = 〈ppos dv,pzero〉 → m∣n.
    574 #m #n #dv #DIVIDE %{dv} lapply (divide_ok … DIVIDE) *; (* XXX: need ; or it eats normalize *)
    575 normalize #H destruct //
    576 qed.
    577 
    578 lemma divides_mod0: ∀dv,m,n:Pos.
    579   n = dv*m → divide n m = 〈ppos dv,pzero〉.
    580 #dv #m #n #DIV lapply (refl ? (divide n m));
    581 elim (divide n m) in ⊢ (???% → ?); #dv' #md' #DIVIDE
    582 lapply (divide_ok … DIVIDE); *;
    583 cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ]
    584 cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
    585 >DIV in ⊢ (% → ?); #H #lt destruct;
    586 [ lapply (plus_to_minus … e0);
    587     >(commutative_times …) >(commutative_times dv'' …)
    588     cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt
    589     >(minus_times_distrib_l …) //;
    590 
    591  (*cut (0 < dv-dv'); [ lapply (not_le_to_lt … nle); /2/ ]
    592     #Hdv *) #H' cut (md'' ≥ m); /2/; lapply (plt_lt … lt); #A #B @False_ind
    593     @(absurd ? B (lt_to_not_le … A))
    594 
    595 | @False_ind @(absurd ? (plt_lt … lt) ?) /2/;
    596 
    597 | >DIVIDE cut (dv = dv''); /2/;
    598 ]
    599 qed.
    600 
    601 lemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
    602 #m #n lapply (refl ? (divide n m)); elim (divide n m) in ⊢ (???% → %);
    603 #dv #md cases md; cases dv;
    604 [ #DIVIDES lapply (divide_ok … DIVIDES); *; normalize; #H destruct
    605 | #dv' #H %1 @mod0_divides /2/;
    606 | #md' #DIVIDES %2 @nmk *; #dv'
    607     >(commutative_times …) #H lapply (divides_mod0 … H);
    608     >DIVIDES #H'
    609     destruct;
    610 | #md' #dv' #DIVIDES %2 @nmk *; #dv'
    611     >(commutative_times …) #H lapply (divides_mod0 … H);
    612     >DIVIDES #H'
    613     destruct;
    614 ] qed.
    615 
    616 theorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
    617 #p #q cases p;
    618 [ cases q; normalize; [ %2 /2/; | *: #m %2 /2/; ]
    619 | *: #n cases q; normalize; /2/;
    620 ] qed.
    621 
    622 definition natp_to_Z ≝
    623 λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
    624 
    625 definition natp_to_negZ ≝
    626 λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].
    627 
    628 (* TODO: check these definitions are right.  They are supposed to be the same
    629    as Zdiv/Zmod in Coq. *)
    630 definition divZ ≝ λx,y.
    631   match x with
    632   [ OZ ⇒ OZ
    633   | pos n ⇒
    634     match y with
    635     [ OZ ⇒ OZ
    636     | pos m ⇒ natp_to_Z (fst ?? (divide n m))
    637     | neg m ⇒ match divide n m with [ pair q r ⇒
    638                 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
    639     ]
    640   | neg n ⇒
    641     match y with
    642     [ OZ ⇒ OZ
    643     | pos m ⇒ match divide n m with [ pair q r ⇒
    644                 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
    645     | neg m ⇒ natp_to_Z (fst ?? (divide n m))
    646     ]
    647   ].
    648 
    649 definition modZ ≝ λx,y.
    650   match x with
    651   [ OZ ⇒ OZ
    652   | pos n ⇒
    653     match y with
    654     [ OZ ⇒ OZ
    655     | pos m ⇒ natp_to_Z (snd ?? (divide n m))
    656     | neg m ⇒ match divide n m with [ pair q r ⇒
    657                 match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
    658     ]
    659   | neg n ⇒
    660     match y with
    661     [ OZ ⇒ OZ
    662     | pos m ⇒ match divide n m with [ pair q r ⇒
    663                 match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
    664     | neg m ⇒ natp_to_Z (snd ?? (divide n m))
    665     ]
    666   ].
    667 
    668 interpretation "natural division" 'divide m n = (div m n).
    669 interpretation "natural modulus" 'module m n = (mod m n).
    670 interpretation "integer division" 'divide m n = (divZ m n).
    671 interpretation "integer modulus" 'module m n = (modZ m n).
    672 
    673 lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
    674 #x #y cases y;
    675 [ #H @(False_ind … H)
    676 | #m #_ cases x; //; #n
    677     whd in ⊢ (?%?);
    678     lapply (pos_compare_to_Prop n m);
    679     cases (pos_compare n m); /2/
    680     #lt whd <(minus_Sn_m … lt) /2/;
    681 | #m #H @(False_ind … H)
    682 ] qed.
    683 
    684 lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
    685 #n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m);
    686 [ //;
    687 | 2,3: #H @False_ind @(absurd ? lt ?) /3/;
    688 ] qed.
    689 
    690 theorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
    691 #x #y cases y;
    692 [ #H @(False_ind … H)
    693 | #m #_ cases x;
    694   [ % //;
    695   | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
    696       cases (divide n m) in ⊢ (???% → %); #dv #md #H
    697       elim (divide_ok … H); #e #l elim l; /2/;
    698   | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
    699       cases (divide n m) in ⊢ (???% → %); #dv #md #H
    700       elim (divide_ok … H); #e #l elim l;
    701       [ /2/;
    702       | #md' #m' #l' %
    703         [ whd in ⊢ (??%); >(pos_compare_n_m_m_n …)
    704             >(pos_compare_lt … l') //;
    705         | @Zminus_Zlt //;
    706         ]
    707       ]
    708   ]
    709 | #m #H @(False_ind … H)
    710 ] qed.
Note: See TracChangeset for help on using the changeset viewer.