Changeset 1523 for src/utilities/binary

Timestamp:

Nov 21, 2011, 4:29:16 PM (9 years ago)

Author:

campbell

Message:

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

Location:

src/utilities/binary

Files:

• Z.ma (modified) (2 diffs)
• division.ma (added)
• positive.ma (modified) (1 diff)

src/utilities/binary/Z.ma

@@ -635 +635 @@
 qed.
 
-lemma eq_rect_Type0_r:
- ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption.
-qed.
-
 theorem associative_Zplus: associative Z Zplus.
 (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
@@ -719 +714 @@
 | neg _ ⇒ OZ  (* same fib as Coq *)
 ].
+
+
+
+lemma eqZb_z_z : ∀z.eqZb z z = true.
+#z cases z;normalize;//;
+qed.
+
+
+
+lemma injective_Z_of_nat : injective ? ? Z_of_nat.
+normalize;
+#n #m cases n;cases m;normalize;//;
+[ 1,2: #n' #H destruct
+| #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) //
+] qed.
+
+lemma reflexive_Zle : reflexive ? Zle.
+#x cases x; //; qed.
+
+lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
+#n cases n;normalize;//;qed.
+
+lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
+#x cases x; //;
+#n cases n; //; qed.
+
+lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
+#x #y
+@pos_elim
+ [ 2: #n' #IH ]
+>(Zplus_Zsucc_Zpred y ?)
+[ >(Zpred_Zsucc (pos n'))
+ #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??)
+    @Zsucc_le
+| #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le
+] qed.
+
+theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
+#x #y cases x;
+[ cases y;
+  [ 1,2: //
+  | #n @False_ind
+  ]
+| #n cases y;
+  [ normalize; @False_ind
+  | #m @(pos_cases … n) /2/;
+  | #m normalize; @False_ind
+  ]
+| #n cases y; /2/;
+] qed.
+    
+theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
+#n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt
+@(transitive_Zle … Hle) /2/;
+qed.
+
+include "basics/types.ma".
+
+definition decidable_eq_Z_Type : ∀z1,z2:Z. (z1 = z2) + (z1 ≠ z2).
+#z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H
+[% //
+|%2 //]
+qed.
+
+lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
+#z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //;
+#H #H' @False_ind @(absurd ? H H')
+qed.
+
+(* Z.ma *)
+
+definition Zge: Z → Z → Prop ≝
+λn,m:Z.m ≤ n.
+
+interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).
+
+definition Zgt: Z → Z → Prop ≝
+λn,m:Z.m<n.
+
+interpretation "integer 'greater than'" 'gt x y = (Zgt x y).
+
+interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
+
+let rec Zleb (x:Z) (y:Z) : bool ≝
+  match x with
+  [ OZ ⇒ 
+    match y with 
+    [ OZ ⇒ true
+    | pos m ⇒ true
+    | neg m ⇒ false ]
+  | pos n ⇒
+    match y with 
+    [ OZ ⇒ false
+    | pos m ⇒ leb n m
+    | neg m ⇒ false ]
+  | neg n ⇒
+    match y with 
+    [ OZ ⇒ true
+    | pos m ⇒ true
+    | neg m ⇒ leb m n ]].
+    
+let rec Zltb (x:Z) (y:Z) : bool ≝
+  match x with
+  [ OZ ⇒
+    match y with 
+    [ OZ ⇒ false
+    | pos m ⇒ true
+    | neg m ⇒ false ]
+  | pos n ⇒
+    match y with 
+    [ OZ ⇒ false
+    | pos m ⇒ leb (succ n) m
+    | neg m ⇒ false ]
+  | neg n ⇒
+    match y with 
+    [ OZ ⇒ true
+    | pos m ⇒ true
+    | neg m ⇒ leb (succ m) n ]].
+
+
+
+theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
+#n #m cases n;cases m; //;
+[ 1,2: #m' normalize; #H @(False_ind ? H)
+| 3,5: #n' #m' normalize; @le_to_leb_true
+| 4: #n' #m' normalize; #H @(False_ind ? H)
+] qed.
+
+theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
+#n #m cases n;cases m; //;
+[ 1,2: #m' normalize; #H destruct
+| 3,5: #n' #m' normalize; @leb_true_to_le
+| 4: #n' #m' normalize; #H destruct
+] qed.
+
+theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
+#n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct;
+qed.
+
+theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
+#n #m cases n;cases m; //;
+[ normalize; #H @(False_ind ? H)
+| 2,3: #m' normalize; #H @(False_ind ? H)
+| 4,6: #n' #m' normalize; @le_to_leb_true
+| #n' #m' normalize; #H @(False_ind ? H)
+] qed.
+
+theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
+#n #m cases n;cases m; //;
+[ normalize; #H destruct
+| 2,3: #m' normalize; #H destruct
+| 4,6: #n' #m' @leb_true_to_le
+| #n' #m' normalize; #H destruct
+] qed.
+
+theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
+#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct;
+qed.
+
+theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 
+(n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
+#n #m #P #Hle #Hnle
+lapply (refl ? (Zleb n m));
+elim (Zleb n m) in ⊢ ((???%)→%);
+#Hb
+[ @Hle @(Zleb_true_to_Zle … Hb)
+| @Hnle @(Zleb_false_to_not_Zle … Hb) 
+] qed.
+
+theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 
+(n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
+#n #m #P #Hlt #Hnlt
+lapply (refl ? (Zltb n m));
+elim (Zltb n m) in ⊢ ((???%)→%);
+#Hb
+[ @Hlt @(Zltb_true_to_Zlt … Hb)
+| @Hnlt @(Zltb_false_to_not_Zlt … Hb) 
+] qed.
+
+lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
+#x #y cases x; cases y; /2/;
+#n #m @(pos_cases … n) @(pos_cases … m)
+[ //;
+| #n' /2/;
+| #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/;
+| #n' #m' #H normalize in H;
+    >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/;
+] qed.
+
+lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
+#x #y cases x; cases y;
+[ 1,2,7,8,9: /2/;
+| 3,4: #m normalize; *;
+| #m #n @(pos_cases … n) @(pos_cases … m)
+  [ 1,2: /2/;
+  | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/;
+  | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/;
+  ]
+| #m #n normalize; *;
+] qed.
+
+lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
+#n cases n; //; #n' #a #b #H
+[ @(pos_elim … n')
+  [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/;
+  | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //;
+      >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/;
+  ]
+| @(pos_elim … n')
+  [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;
+  | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //;
+      >(Zplus_Zpred …) >(Zplus_Zpred …) /2/;
+  ]
+] qed.
+
+lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
+/2/; qed.
+
+let rec Z_times (x:Z) (y:Z) : Z ≝
+match x with
+[ OZ ⇒ OZ
+| pos n ⇒
+  match y with
+  [ OZ ⇒ OZ
+  | pos m ⇒ pos (n*m)
+  | neg m ⇒ neg (n*m)
+  ]
+| neg n ⇒
+  match y with
+  [ OZ ⇒ OZ
+  | pos m ⇒ neg (n*m)
+  | neg m ⇒ pos (n*m)
+  ]
+].
+interpretation "integer multiplication" 'times x y = (Z_times x y).
+
+
+
+definition Zmax : Z → Z → Z ≝ 
+  λx,y.match Z_compare x y with
+  [ LT ⇒ y
+  | _ ⇒ x ].
+
+lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
+#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
+/3/ qed.
+
+lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
+#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
+whd in ⊢ (% → ??%); /3/ qed.
+
+
+lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
+#x #y cases y;
+[ #H @(False_ind … H)
+| #m #_ cases x; //; #n
+    whd in ⊢ (?%?);
+    lapply (pos_compare_to_Prop n m);
+    cases (pos_compare n m); /2/
+    #lt whd <(minus_Sn_m … lt) /2/;
+| #m #H @(False_ind … H)
+] qed.
+

src/utilities/binary/positive.ma

@@ -1160 +1160 @@
 definition max : Pos → Pos → Pos ≝
 λn,m. match leb n m with [ true ⇒ m | _ ⇒ n].
+
+
+
+lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
+#n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m);
+[ //;
+| 2,3: #H @False_ind @(absurd ? lt ?) /3/;
+] qed.
+
+lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
+#n #m @eqb_elim //; qed.