Changeset 1523 for src/utilities/binary


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

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

Location:
src/utilities/binary
Files:
1 added
2 edited

Legend:

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