Changeset 1523 for src/utilities

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/utilities

Files:

• binary/Z.ma (modified) (2 diffs)
• binary/division.ma (added)
• binary/positive.ma (modified) (1 diff)
• extralib.ma (modified) (4 diffs)

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.

src/utilities/extralib.ma

@@ -17 +17 @@
 include "basics/logic.ma".
 include "utilities/pair.ma".
-include "utilities/binary/Z.ma".
-include "utilities/binary/positive.ma".
 
 lemma eq_rect_Type0_r:
@@ -51 +49 @@
   λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
   
-
-(* TODO: move to Z.ma *)
-
-lemma eqZb_z_z : ∀z.eqZb z z = true.
-#z cases z;normalize;//;
-qed.
-
-(* XXX: divides goes to arithmetics *)
-inductive dividesP (n,m:Pos) : Prop ≝
-| witness : ∀p:Pos.m = times n p → dividesP n m.
-interpretation "positive divides" 'divides n m = (dividesP n m).
-interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).
-
-definition dividesZ : Z → Z → Prop ≝
-λx,y. match x with
-[ OZ ⇒ False
-| pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
-| neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
-].
-
-interpretation "integer divides" 'divides n m = (dividesZ n m).
-interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).
+  
+  
 
 (* should be proved in nat.ma, but it's not! *)
@@ -82 +60 @@
 ] 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.
-
-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.
-
-(* XXX: Zmax must go to arithmetics *)
-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.
-
-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.
-
-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).
 (* datatypes/list.ma *)
 
@@ -338 +75 @@
   ]
 ] qed. 
-
-(* division *)
-
-inductive natp : Type[0] ≝
-| pzero : natp
-| ppos  : Pos → natp.
-
-definition natp0 ≝
-λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
-
-definition natp1 ≝
-λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
-
-let rec divide (m,n:Pos) on m ≝ 
-match m with 
-[ one ⇒
-  match n with
-  [ one ⇒ 〈ppos one,pzero〉
-  | _ ⇒ 〈pzero,ppos one〉
-  ]
-| p0 m' ⇒
-  match divide m' n with
-  [ pair q r ⇒
-    match r with
-    [ pzero ⇒ 〈natp0 q,pzero〉
-    | ppos r' ⇒
-      match partial_minus (p0 r') n with
-      [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
-      | MinusZero ⇒ 〈natp1 q, pzero〉
-      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
-      ]
-    ]
-  ]
-| p1 m' ⇒
-  match divide m' n with
-  [ pair q r ⇒
-    match r with
-    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
-    | ppos r' ⇒
-      match partial_minus (p1 r') n with
-      [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
-      | MinusZero ⇒ 〈natp1 q, pzero〉
-      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
-      ]
-    ]
-  ]
-].
-
-definition div ≝ λm,n. fst ?? (divide m n).
-definition mod ≝ λm,n. snd ?? (divide m n).
-
-lemma pred_minus: ∀n,m:Pos. pred n - m = pred (n-m).
-@pos_elim /3/;
-qed.
-
-lemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
-@pos_elim
-[ //
-| #n #IH #m #p >(succ_plus_one …) >(IH m one) /2/;
-] qed.
-
-theorem plus_minus_r:
-∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
-#m #n #p #le >(commutative_plus …)
->(commutative_plus p ?) @plus_minus //; qed.
-
-lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
-#m #n #p elim m;/2/; qed.
-(*
-lemma le_to_minus: ∀m,n. m≤n → m-n = 0.
-#m #n elim n;
-[ <(minus_n_O …) /2/;
-| #n' #IH #le inversion le; /2/; #n'' #A #B #C destruct;
-    >(eq_minus_S_pred …) >(IH A) /2/
-] qed.
-*)
-lemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
-#n #m #p (*elim (decidable_lt n m);*)#lt
-(*[*) @(pos_elim … p) //;#p' #IH
-    <(times_succn_m …) <(times_succn_m …) <(times_succn_m …)
-    >(minus_plus_distrib …)
-    <(plus_minus … lt) <IH
-    >(plus_minus_r …) /2/;
-qed.
-(*|
-lapply (not_lt_to_le … lt); #le
-@(pos_elim … p) //; #p'
- cut (m-n = one); [ /3/ ]
-  #mn >mn >(times_n_one …) >(times_n_one …)
-  #H <H in ⊢ (???%)
-  @sym_eq @le_n_one_to_eq <H
-  >(minus_plus_distrib …) @monotonic_le_minus_l
-  /2/;
-] qed.
-
-lemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
-#m #n #H lapply (refl ? (m-n));elim (m-n) in ⊢ (???% → %);//;
-#H' lapply (minus_to_plus … H'); /2/;
-<(plus_n_O …) #H'' >H'' in H #H
-@False_ind @(absurd ? H ( not_le_Sn_n n))
-qed.
-*)
-
-let rec natp_plus (n,m:natp) ≝
-match n with
-[ pzero ⇒ m
-| ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
-].
-
-let rec natp_times (n,m:natp) ≝
-match n with
-[ pzero ⇒ pzero
-| ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
-].
-
-inductive natp_lt : natp → Pos → Prop ≝
-| plt_zero : ∀n. natp_lt pzero n
-| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
-
-lemma lt_p0: ∀n:Pos. one < p0 n.
-#n normalize; /2/; qed.
-
-lemma lt_p1: ∀n:Pos. one < p1 n.
-#n' normalize; >(?:p1 n' = succ (p0 n')) //; qed.
-
-lemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
-#m elim m;
-[ //;
-| 2,3: #m' #IH normalize; >IH //;
-] qed.
-
-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).
-#n #P #Q @succ_elim /2/; qed.
-
-lemma partial_minus_to_Prop: ∀n,m.
-  match partial_minus n m with
-  [ MinusNeg ⇒ n < m
-  | MinusZero ⇒ n = m
-  | MinusPos r ⇒ n = m+r
-  ].
-#n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m);
-normalize; cases (partial_minus n m); /2/; qed.
-
-lemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
-#n #m #lt elim lt; /2/;
-qed.
-
-lemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
-#n #m #lt @(transitive_lt ? (p0 m) ?) /2/;
-qed.
-
-lemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
-#n #m #lt inversion lt;
-[ #H >(succ_injective … H) //;
-| #p #H1 #H2 #H3 >(succ_injective … H3)
-    @(transitive_lt ? (p0 p) ?) /2/;
-] 
-qed.
-
-lemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
-#n #m #lt elim lt; /2/;
-qed.
-
-
-
-lemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
-#n #m #lt inversion lt;
-[ #p #H destruct;
-| #n' #m' #lt #e1 #e2 destruct @lt
-] qed.
-
-lemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
-#a #b /2/; qed.
-
-lemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
-#a #b >(?:p1 b = succ (p0 b)) /2/; qed.
-
-lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
-/2/; qed.
-
-theorem divide_ok : ∀m,n,dv,md.
- divide m n = 〈dv,md〉 →
- ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
-#m #n @(pos_cases … n)
-[ >(divide_by_one m) #dv #md #H destruct normalize /2/
-| #n' elim m;
-  [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/
-  | #m' #IH #dv #md whd in ⊢ (??%? → ?(???%)?);
-      lapply (refl ? (divide m' (succ n')));
-      elim (divide m' (succ n')) in ⊢ (???% → % → ?);
-      #dv' #md' #DIVr elim (IH … DIVr);
-      whd in ⊢ (? → ? → ??%? → ?);
-      cases md';
-      [ cases dv'; normalize;
-        [ #H destruct
-        | #dv'' #Hr1 #Hr2 >(pos_nonzero …) #H destruct % /2/
-        ]
-      | cases dv'; [ 2: #dv'' ] @succ_elim
-          normalize; #n #md'' #Hr1 #Hr2
-          lapply (plt_lt … Hr2); #Hr2'
-          lapply (partial_minus_to_Prop md'' n);
-          cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
-          #lt #e destruct % [ normalize /3 by le_to_le_to_eq, le_n, eq_f/ | *: normalize /2 by plt_zero, plt_pos/ ] @plt_pos
-          [ 1,3,5,7: @double_lt1 /2/;
-          | 2,4: @double_lt3 /2/;
-          | *: @double_lt2 /2/;
-          ]
-      ]
-  | #m' #IH #dv #md whd in ⊢ (??%? → ?);
-      lapply (refl ? (divide m' (succ n')));
-      elim (divide m' (succ n')) in ⊢ (???% → % → ?);
-      #dv' #md' #DIVr elim (IH … DIVr);
-      whd in ⊢ (? → ? → ??%? → ?); cases md';
-      [ cases dv'; normalize;
-        [ #H destruct;
-        | #dv'' #Hr1 #Hr2 #H destruct; /3/;
-        ]
-      | (*cases dv'; [ 2: #dv'' ] @succ_elim
-          normalize; #n #md'' #Hr1 #Hr2 *) #md'' #Hr1 #Hr2
-          lapply (plt_lt … Hr2); #Hr2'
-          whd in ⊢ (??%? → ?);
-          lapply (partial_minus_to_Prop (p0 md'') (succ n'));
-          cases (partial_minus (p0 md'') (succ n')); [ 3(*,6,9,12*): #r'' ]
-          cases dv' in Hr1 ⊢ %; [ 2,4,6: #dv'' ] normalize
-          #Hr1 destruct [ 1,2,3: >(p0_plus ? md'') ]
-          #lt #e [ 1,3,4,6: >lt ]
-          <(pair_eq1 ?????? e) <(pair_eq2 ?????? e)
-          normalize in ⊢ (?(???%)?); % /2/; @plt_pos
-          [ cut (succ n' + r'' < p0 (succ n')); /2/;
-          | cut (succ n' + r'' < p0 (succ n')); /2/; ]]]]
-qed.
-
-lemma mod0_divides: ∀m,n,dv:Pos.
-  divide n m = 〈ppos dv,pzero〉 → m∣n.
-#m #n #dv #DIVIDE %{dv} lapply (divide_ok … DIVIDE) *; (* XXX: need ; or it eats normalize *)
-normalize #H destruct //
-qed.
-
-lemma divides_mod0: ∀dv,m,n:Pos.
-  n = dv*m → divide n m = 〈ppos dv,pzero〉.
-#dv #m #n #DIV lapply (refl ? (divide n m));
-elim (divide n m) in ⊢ (???% → ?); #dv' #md' #DIVIDE
-lapply (divide_ok … DIVIDE); *;
-cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ]
-cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
->DIV in ⊢ (% → ?); #H #lt destruct;
-[ lapply (plus_to_minus … e0);
-    >(commutative_times …) >(commutative_times dv'' …)
-    cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt
-    >(minus_times_distrib_l …) //;
-
- (*cut (0 < dv-dv'); [ lapply (not_le_to_lt … nle); /2/ ]
-    #Hdv *) #H' cut (md'' ≥ m); /2/; lapply (plt_lt … lt); #A #B @False_ind
-    @(absurd ? B (lt_to_not_le … A))
-
-| @False_ind @(absurd ? (plt_lt … lt) ?) /2/;
-
-| >DIVIDE cut (dv = dv''); /2/;
-]
-qed.
-
-lemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
-#m #n lapply (refl ? (divide n m)); elim (divide n m) in ⊢ (???% → %);
-#dv #md cases md; cases dv;
-[ #DIVIDES lapply (divide_ok … DIVIDES); *; normalize; #H destruct
-| #dv' #H %1 @mod0_divides /2/;
-| #md' #DIVIDES %2 @nmk *; #dv'
-    >(commutative_times …) #H lapply (divides_mod0 … H);
-    >DIVIDES #H'
-    destruct;
-| #md' #dv' #DIVIDES %2 @nmk *; #dv'
-    >(commutative_times …) #H lapply (divides_mod0 … H);
-    >DIVIDES #H'
-    destruct;
-] qed.
-
-theorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
-#p #q cases p;
-[ cases q; normalize; [ %2 /2/; | *: #m %2 /2/; ]
-| *: #n cases q; normalize; /2/;
-] qed.
-
-definition natp_to_Z ≝
-λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
-
-definition natp_to_negZ ≝
-λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].
-
-(* TODO: check these definitions are right.  They are supposed to be the same
-   as Zdiv/Zmod in Coq. *)
-definition divZ ≝ λx,y.
-  match x with
-  [ OZ ⇒ OZ
-  | pos n ⇒
-    match y with
-    [ OZ ⇒ OZ
-    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
-    | neg m ⇒ match divide n m with [ pair q r ⇒
-                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
-    ]
-  | neg n ⇒
-    match y with
-    [ OZ ⇒ OZ
-    | pos m ⇒ match divide n m with [ pair q r ⇒
-                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
-    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
-    ]
-  ].
-
-definition modZ ≝ λx,y.
-  match x with
-  [ OZ ⇒ OZ
-  | pos n ⇒
-    match y with
-    [ OZ ⇒ OZ
-    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
-    | neg m ⇒ match divide n m with [ pair q r ⇒
-                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
-    ]
-  | neg n ⇒
-    match y with
-    [ OZ ⇒ OZ
-    | pos m ⇒ match divide n m with [ pair q r ⇒
-                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
-    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
-    ]
-  ].
-
-interpretation "natural division" 'divide m n = (div m n).
-interpretation "natural modulus" 'module m n = (mod m n).
-interpretation "integer division" 'divide m n = (divZ m n).
-interpretation "integer modulus" 'module m n = (modZ m n).
-
-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.
-
-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.
-
-theorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
-#x #y cases y;
-[ #H @(False_ind … H)
-| #m #_ cases x;
-  [ % //;
-  | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
-      cases (divide n m) in ⊢ (???% → %); #dv #md #H
-      elim (divide_ok … H); #e #l elim l; /2/;
-  | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
-      cases (divide n m) in ⊢ (???% → %); #dv #md #H
-      elim (divide_ok … H); #e #l elim l;
-      [ /2/;
-      | #md' #m' #l' %
-        [ whd in ⊢ (??%); >(pos_compare_n_m_m_n …)
-            >(pos_compare_lt … l') //;
-        | @Zminus_Zlt //;
-        ]
-      ]
-  ]
-| #m #H @(False_ind … H)
-] qed.