Imported Upstream version 8.0pl1upstream/8.0pl1

4 files changed, 1672 insertions, 0 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
new file mode 100644
index 00000000..e6a14938
--- /dev/null
+++ b/theories/NArith/BinNat.v
@@ -0,0 +1,212 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: BinNat.v,v 1.7.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
+
+Require Import BinPos.
+
+(**********************************************************************)
+(** Binary natural numbers *)
+
+Inductive N : Set :=
+  | N0 : N
+  | Npos : positive -> N.
+
+(** Declare binding key for scope positive_scope *)
+
+Delimit Scope N_scope with N.
+
+(** Automatically open scope N_scope for the constructors of N *)
+
+Bind Scope N_scope with N.
+Arguments Scope Npos [N_scope].
+
+Open Local Scope N_scope.
+
+(** Operation x -> 2*x+1 *)
+
+Definition Ndouble_plus_one x :=
+  match x with
+  | N0 => Npos 1%positive
+  | Npos p => Npos (xI p)
+  end.
+
+(** Operation x -> 2*x *)
+
+Definition Ndouble n := match n with
+                        | N0 => N0
+                        | Npos p => Npos (xO p)
+                        end.
+
+(** Successor *)
+
+Definition Nsucc n :=
+  match n with
+  | N0 => Npos 1%positive
+  | Npos p => Npos (Psucc p)
+  end.
+
+(** Addition *)
+
+Definition Nplus n m :=
+  match n, m with
+  | N0, _ => m
+  | _, N0 => n
+  | Npos p, Npos q => Npos (p + q)%positive
+  end.
+
+Infix "+" := Nplus : N_scope.
+
+(** Multiplication *)
+
+Definition Nmult n m :=
+  match n, m with
+  | N0, _ => N0
+  | _, N0 => N0
+  | Npos p, Npos q => Npos (p * q)%positive
+  end.
+
+Infix "*" := Nmult : N_scope.
+
+(** Order *)
+
+Definition Ncompare n m :=
+  match n, m with
+  | N0, N0 => Eq
+  | N0, Npos m' => Lt
+  | Npos n', N0 => Gt
+  | Npos n', Npos m' => (n' ?= m')%positive Eq
+  end.
+
+Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
+
+(** Peano induction on binary natural numbers *)
+
+Theorem Nind :
+ forall P:N -> Prop,
+   P N0 -> (forall n:N, P n -> P (Nsucc n)) -> forall n:N, P n.
+Proof.
+destruct n.
+  assumption.
+  apply Pind with (P := fun p => P (Npos p)).
+exact (H0 N0 H).
+intro p'; exact (H0 (Npos p')).
+Qed.
+
+(** Properties of addition *)
+
+Theorem Nplus_0_l : forall n:N, N0 + n = n.
+Proof.
+reflexivity.
+Qed.
+
+Theorem Nplus_0_r : forall n:N, n + N0 = n.
+Proof.
+destruct n; reflexivity.
+Qed.
+
+Theorem Nplus_comm : forall n m:N, n + m = m + n.
+Proof.
+intros.
+destruct n; destruct m; simpl in |- *; try reflexivity.
+rewrite Pplus_comm; reflexivity.
+Qed.
+
+Theorem Nplus_assoc : forall n m p:N, n + (m + p) = n + m + p.
+Proof.
+intros.
+destruct n; try reflexivity.
+destruct m; try reflexivity.
+destruct p; try reflexivity.
+simpl in |- *; rewrite Pplus_assoc; reflexivity.
+Qed.
+
+Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m).
+Proof.
+destruct n; destruct m.
+  simpl in |- *; reflexivity.
+  unfold Nsucc, Nplus in |- *; rewrite <- Pplus_one_succ_l; reflexivity.
+  simpl in |- *; reflexivity.
+  simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity.
+Qed.
+
+Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m.
+Proof.
+destruct n; destruct m; simpl in |- *; intro H; reflexivity || injection H;
+ clear H; intro H.
+  symmetry  in H; contradiction Psucc_not_one with p.
+  contradiction Psucc_not_one with p.
+  rewrite Psucc_inj with (1 := H); reflexivity.
+Qed.
+
+Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p.
+Proof.
+intro n; pattern n in |- *; apply Nind; clear n; simpl in |- *.
+  trivial.
+  intros n IHn m p H0; do 2 rewrite Nplus_succ in H0.
+  apply IHn; apply Nsucc_inj; assumption.
+Qed.
+
+(** Properties of multiplication *)
+
+Theorem Nmult_1_l : forall n:N, Npos 1%positive * n = n.
+Proof.
+destruct n; reflexivity.
+Qed.
+
+Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n.
+Proof.
+destruct n; simpl in |- *; try reflexivity.
+rewrite Pmult_1_r; reflexivity.
+Qed.
+
+Theorem Nmult_comm : forall n m:N, n * m = m * n.
+Proof.
+intros.
+destruct n; destruct m; simpl in |- *; try reflexivity.
+rewrite Pmult_comm; reflexivity.
+Qed.
+
+Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p.
+Proof.
+intros.
+destruct n; try reflexivity.
+destruct m; try reflexivity.
+destruct p; try reflexivity.
+simpl in |- *; rewrite Pmult_assoc; reflexivity.
+Qed.
+
+Theorem Nmult_plus_distr_r : forall n m p:N, (n + m) * p = n * p + m * p.
+Proof.
+intros.
+destruct n; try reflexivity.
+destruct m; destruct p; try reflexivity.
+simpl in |- *; rewrite Pmult_plus_distr_r; reflexivity.
+Qed.
+
+Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m.
+Proof.
+destruct p; intros Hp H.
+contradiction Hp; reflexivity.
+destruct n; destruct m; reflexivity || (try discriminate H).
+injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity.
+Qed. 
+
+Theorem Nmult_0_l : forall n:N, N0 * n = N0.
+Proof.
+reflexivity.
+Qed.
+
+(** Properties of comparison *)
+
+Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m.
+Proof.
+destruct n as [| n]; destruct m as [| m]; simpl in |- *; intro H;
+ reflexivity || (try discriminate H).
+  rewrite (Pcompare_Eq_eq n m H); reflexivity.
+Qed.
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
new file mode 100644
index 00000000..fffb10c1
--- /dev/null
+++ b/theories/NArith/BinPos.v
@@ -0,0 +1,961 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: BinPos.v,v 1.7.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
+
+(**********************************************************************)
+(** Binary positive numbers *)
+
+(** Original development by Pierre Crégut, CNET, Lannion, France *)
+
+Inductive positive : Set :=
+  | xI : positive -> positive
+  | xO : positive -> positive
+  | xH : positive.
+
+(** Declare binding key for scope positive_scope *)
+
+Delimit Scope positive_scope with positive.
+
+(** Automatically open scope positive_scope for type positive, xO and xI *)
+
+Bind Scope positive_scope with positive.
+Arguments Scope xO [positive_scope].
+Arguments Scope xI [positive_scope].
+
+(** Successor *)
+
+Fixpoint Psucc (x:positive) : positive :=
+  match x with
+  | xI x' => xO (Psucc x')
+  | xO x' => xI x'
+  | xH => xO xH
+  end.
+
+(** Addition *)
+
+Fixpoint Pplus (x y:positive) {struct x} : positive :=
+  match x, y with
+  | xI x', xI y' => xO (Pplus_carry x' y')
+  | xI x', xO y' => xI (Pplus x' y')
+  | xI x', xH => xO (Psucc x')
+  | xO x', xI y' => xI (Pplus x' y')
+  | xO x', xO y' => xO (Pplus x' y')
+  | xO x', xH => xI x'
+  | xH, xI y' => xO (Psucc y')
+  | xH, xO y' => xI y'
+  | xH, xH => xO xH
+  end
+ 
+ with Pplus_carry (x y:positive) {struct x} : positive :=
+  match x, y with
+  | xI x', xI y' => xI (Pplus_carry x' y')
+  | xI x', xO y' => xO (Pplus_carry x' y')
+  | xI x', xH => xI (Psucc x')
+  | xO x', xI y' => xO (Pplus_carry x' y')
+  | xO x', xO y' => xI (Pplus x' y')
+  | xO x', xH => xO (Psucc x')
+  | xH, xI y' => xI (Psucc y')
+  | xH, xO y' => xO (Psucc y')
+  | xH, xH => xI xH
+  end.
+
+Infix "+" := Pplus : positive_scope.
+
+Open Local Scope positive_scope.
+
+(** From binary positive numbers to Peano natural numbers *)
+
+Fixpoint Pmult_nat (x:positive) (pow2:nat) {struct x} : nat :=
+  match x with
+  | xI x' => (pow2 + Pmult_nat x' (pow2 + pow2))%nat
+  | xO x' => Pmult_nat x' (pow2 + pow2)%nat
+  | xH => pow2
+  end.
+
+Definition nat_of_P (x:positive) := Pmult_nat x 1.
+
+(** From Peano natural numbers to binary positive numbers *)
+
+Fixpoint P_of_succ_nat (n:nat) : positive :=
+  match n with
+  | O => xH
+  | S x' => Psucc (P_of_succ_nat x')
+  end.
+
+(** Operation x -> 2*x-1 *)
+
+Fixpoint Pdouble_minus_one (x:positive) : positive :=
+  match x with
+  | xI x' => xI (xO x')
+  | xO x' => xI (Pdouble_minus_one x')
+  | xH => xH
+  end.
+
+(** Predecessor *)
+
+Definition Ppred (x:positive) :=
+  match x with
+  | xI x' => xO x'
+  | xO x' => Pdouble_minus_one x'
+  | xH => xH
+  end.
+
+(** An auxiliary type for subtraction *)
+
+Inductive positive_mask : Set :=
+  | IsNul : positive_mask
+  | IsPos : positive -> positive_mask
+  | IsNeg : positive_mask.
+
+(** Operation x -> 2*x+1 *)
+
+Definition Pdouble_plus_one_mask (x:positive_mask) :=
+  match x with
+  | IsNul => IsPos xH
+  | IsNeg => IsNeg
+  | IsPos p => IsPos (xI p)
+  end.
+
+(** Operation x -> 2*x *)
+
+Definition Pdouble_mask (x:positive_mask) :=
+  match x with
+  | IsNul => IsNul
+  | IsNeg => IsNeg
+  | IsPos p => IsPos (xO p)
+  end.
+
+(** Operation x -> 2*x-2 *)
+
+Definition Pdouble_minus_two (x:positive) :=
+  match x with
+  | xI x' => IsPos (xO (xO x'))
+  | xO x' => IsPos (xO (Pdouble_minus_one x'))
+  | xH => IsNul
+  end.
+
+(** Subtraction of binary positive numbers into a positive numbers mask *)
+
+Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask :=
+  match x, y with
+  | xI x', xI y' => Pdouble_mask (Pminus_mask x' y')
+  | xI x', xO y' => Pdouble_plus_one_mask (Pminus_mask x' y')
+  | xI x', xH => IsPos (xO x')
+  | xO x', xI y' => Pdouble_plus_one_mask (Pminus_mask_carry x' y')
+  | xO x', xO y' => Pdouble_mask (Pminus_mask x' y')
+  | xO x', xH => IsPos (Pdouble_minus_one x')
+  | xH, xH => IsNul
+  | xH, _ => IsNeg
+  end
+ 
+ with Pminus_mask_carry (x y:positive) {struct y} : positive_mask :=
+  match x, y with
+  | xI x', xI y' => Pdouble_plus_one_mask (Pminus_mask_carry x' y')
+  | xI x', xO y' => Pdouble_mask (Pminus_mask x' y')
+  | xI x', xH => IsPos (Pdouble_minus_one x')
+  | xO x', xI y' => Pdouble_mask (Pminus_mask_carry x' y')
+  | xO x', xO y' => Pdouble_plus_one_mask (Pminus_mask_carry x' y')
+  | xO x', xH => Pdouble_minus_two x'
+  | xH, _ => IsNeg
+  end.
+
+(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *)
+
+Definition Pminus (x y:positive) :=
+  match Pminus_mask x y with
+  | IsPos z => z
+  | _ => xH
+  end.
+
+Infix "-" := Pminus : positive_scope.
+
+(** Multiplication on binary positive numbers *)
+
+Fixpoint Pmult (x y:positive) {struct x} : positive :=
+  match x with
+  | xI x' => y + xO (Pmult x' y)
+  | xO x' => xO (Pmult x' y)
+  | xH => y
+  end.
+
+Infix "*" := Pmult : positive_scope.
+
+(** Division by 2 rounded below but for 1 *)
+
+Definition Pdiv2 (z:positive) :=
+  match z with
+  | xH => xH
+  | xO p => p
+  | xI p => p
+  end.
+
+Infix "/" := Pdiv2 : positive_scope.
+
+(** Comparison on binary positive numbers *)
+
+Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison :=
+  match x, y with
+  | xI x', xI y' => Pcompare x' y' r
+  | xI x', xO y' => Pcompare x' y' Gt
+  | xI x', xH => Gt
+  | xO x', xI y' => Pcompare x' y' Lt
+  | xO x', xO y' => Pcompare x' y' r
+  | xO x', xH => Gt
+  | xH, xI y' => Lt
+  | xH, xO y' => Lt
+  | xH, xH => r
+  end.
+
+Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
+
+(**********************************************************************)
+(** Miscellaneous properties of binary positive numbers *)
+
+Lemma ZL11 : forall p:positive, p = xH \/ p <> xH.
+Proof.
+intros x; case x; intros; (left; reflexivity) || (right; discriminate).
+Qed.
+
+(**********************************************************************)
+(** Properties of successor on binary positive numbers *)
+
+(** Specification of [xI] in term of [Psucc] and [xO] *)
+
+Lemma xI_succ_xO : forall p:positive, xI p = Psucc (xO p).
+Proof.
+reflexivity.
+Qed.
+
+Lemma Psucc_discr : forall p:positive, p <> Psucc p.
+Proof.
+intro x; destruct x as [p| p| ]; discriminate.
+Qed.
+
+(** Successor and double *)
+
+Lemma Psucc_o_double_minus_one_eq_xO :
+ forall p:positive, Psucc (Pdouble_minus_one p) = xO p.
+Proof.
+intro x; induction x as [x IHx| x| ]; simpl in |- *; try rewrite IHx;
+ reflexivity.
+Qed.
+
+Lemma Pdouble_minus_one_o_succ_eq_xI :
+ forall p:positive, Pdouble_minus_one (Psucc p) = xI p.
+Proof.
+intro x; induction x as [x IHx| x| ]; simpl in |- *; try rewrite IHx;
+ reflexivity.
+Qed.
+
+Lemma xO_succ_permute :
+ forall p:positive, xO (Psucc p) = Psucc (Psucc (xO p)).
+Proof.
+intro y; induction  y as [y Hrecy| y Hrecy| ]; simpl in |- *; auto.
+Qed.
+
+Lemma double_moins_un_xO_discr :
+ forall p:positive, Pdouble_minus_one p <> xO p.
+Proof.
+intro x; destruct x as [p| p| ]; discriminate.
+Qed.
+
+(** Successor and predecessor *)
+
+Lemma Psucc_not_one : forall p:positive, Psucc p <> xH.
+Proof.
+intro x; destruct x as [x| x| ]; discriminate.
+Qed.
+
+Lemma Ppred_succ : forall p:positive, Ppred (Psucc p) = p.
+Proof.
+intro x; destruct x as [p| p| ]; [ idtac | idtac | simpl in |- *; auto ];
+ (induction p as [p IHp| | ]; [ idtac | reflexivity | reflexivity ]);
+ simpl in |- *; simpl in IHp; try rewrite <- IHp; reflexivity.
+Qed.
+
+Lemma Psucc_pred : forall p:positive, p = xH \/ Psucc (Ppred p) = p.
+Proof.
+intro x; induction  x as [x Hrecx| x Hrecx| ];
+ [ simpl in |- *; auto
+ | simpl in |- *; intros; right; apply Psucc_o_double_minus_one_eq_xO
+ | auto ].
+Qed.
+
+(** Injectivity of successor *)
+
+Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q.
+Proof.
+intro x; induction x; intro y; destruct y as [y| y| ]; simpl in |- *; intro H;
+ discriminate H || (try (injection H; clear H; intro H)).
+rewrite (IHx y H); reflexivity.
+absurd (Psucc x = xH); [ apply Psucc_not_one | assumption ].
+apply f_equal with (1 := H); assumption.
+absurd (Psucc y = xH);
+ [ apply Psucc_not_one | symmetry  in |- *; assumption ].
+reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Properties of addition on binary positive numbers *)
+
+(** Specification of [Psucc] in term of [Pplus] *)
+
+Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + xH.
+Proof.
+intro q; destruct q as [p| p| ]; reflexivity.
+Qed.
+
+Lemma Pplus_one_succ_l : forall p:positive, Psucc p = xH + p.
+Proof.
+intro q; destruct q as [p| p| ]; reflexivity.
+Qed.
+
+(** Specification of [Pplus_carry] *)
+
+Theorem Pplus_carry_spec :
+ forall p q:positive, Pplus_carry p q = Psucc (p + q).
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y;
+ [ destruct y as [p0| p0| ]
+ | destruct y as [p0| p0| ]
+ | destruct y as [p| p| ] ]; simpl in |- *; auto; rewrite IHp; 
+ auto.
+Qed.
+
+(** Commutativity *)
+
+Theorem Pplus_comm : forall p q:positive, p + q = q + p.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y;
+ [ destruct y as [p0| p0| ]
+ | destruct y as [p0| p0| ]
+ | destruct y as [p| p| ] ]; simpl in |- *; auto;
+ try do 2 rewrite Pplus_carry_spec; rewrite IHp; auto.
+Qed. 
+
+(** Permutation of [Pplus] and [Psucc] *)
+
+Theorem Pplus_succ_permute_r :
+ forall p q:positive, p + Psucc q = Psucc (p + q).
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y;
+ [ destruct y as [p0| p0| ]
+ | destruct y as [p0| p0| ]
+ | destruct y as [p| p| ] ]; simpl in |- *; auto;
+ [ rewrite Pplus_carry_spec; rewrite IHp; auto
+ | rewrite Pplus_carry_spec; auto
+ | destruct p; simpl in |- *; auto
+ | rewrite IHp; auto
+ | destruct p; simpl in |- *; auto ].
+Qed.
+
+Theorem Pplus_succ_permute_l :
+ forall p q:positive, Psucc p + q = Psucc (p + q).
+Proof.
+intros x y; rewrite Pplus_comm; rewrite Pplus_comm with (p := x);
+ apply Pplus_succ_permute_r.
+Qed.
+
+Theorem Pplus_carry_pred_eq_plus :
+ forall p q:positive, q <> xH -> Pplus_carry p (Ppred q) = p + q.
+Proof.
+intros q z H; elim (Psucc_pred z);
+ [ intro; absurd (z = xH); auto
+ | intros E; pattern z at 2 in |- *; rewrite <- E;
+    rewrite Pplus_succ_permute_r; rewrite Pplus_carry_spec; 
+    trivial ].
+Qed. 
+
+(** No neutral for addition on strictly positive numbers *)
+
+Lemma Pplus_no_neutral : forall p q:positive, q + p <> p.
+Proof.
+intro x; induction x; intro y; destruct y as [y| y| ]; simpl in |- *; intro H;
+ discriminate H || injection H; clear H; intro H; apply (IHx y H).
+Qed.
+
+Lemma Pplus_carry_no_neutral :
+ forall p q:positive, Pplus_carry q p <> Psucc p.
+Proof.
+intros x y H; absurd (y + x = x);
+ [ apply Pplus_no_neutral
+ | apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption ].
+Qed.
+
+(** Simplification *)
+
+Lemma Pplus_carry_plus :
+ forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s.
+Proof.
+intros x y z t H; apply Psucc_inj; do 2 rewrite <- Pplus_carry_spec;
+ assumption.
+Qed.
+
+Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q.
+Proof.
+intros x y z; generalize x y; clear x y.
+induction z as [z| z| ].
+  destruct x as [x| x| ]; intro y; destruct y as [y| y| ]; simpl in |- *;
+   intro H; discriminate H || (try (injection H; clear H; intro H)).
+    rewrite IHz with (1 := Pplus_carry_plus _ _ _ _ H); reflexivity.
+    absurd (Pplus_carry x z = Psucc z);
+     [ apply Pplus_carry_no_neutral | assumption ].
+    rewrite IHz with (1 := H); reflexivity.
+    symmetry  in H; absurd (Pplus_carry y z = Psucc z);
+     [ apply Pplus_carry_no_neutral | assumption ].
+    reflexivity.
+  destruct x as [x| x| ]; intro y; destruct y as [y| y| ]; simpl in |- *;
+   intro H; discriminate H || (try (injection H; clear H; intro H)).
+    rewrite IHz with (1 := H); reflexivity.
+    absurd (x + z = z); [ apply Pplus_no_neutral | assumption ].
+    rewrite IHz with (1 := H); reflexivity.
+    symmetry  in H; absurd (y + z = z);
+     [ apply Pplus_no_neutral | assumption ].
+    reflexivity.
+  intros H x y; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption.
+Qed.
+
+Lemma Pplus_reg_l : forall p q r:positive, p + q = p + r -> q = r.
+Proof.
+intros x y z H; apply Pplus_reg_r with (r := x);
+ rewrite Pplus_comm with (p := z); rewrite Pplus_comm with (p := y);
+ assumption.
+Qed.
+
+Lemma Pplus_carry_reg_r :
+ forall p q r:positive, Pplus_carry p r = Pplus_carry q r -> p = q.
+Proof.
+intros x y z H; apply Pplus_reg_r with (r := z); apply Pplus_carry_plus;
+ assumption.
+Qed.
+
+Lemma Pplus_carry_reg_l :
+ forall p q r:positive, Pplus_carry p q = Pplus_carry p r -> q = r.
+Proof.
+intros x y z H; apply Pplus_reg_r with (r := x);
+ rewrite Pplus_comm with (p := z); rewrite Pplus_comm with (p := y);
+ apply Pplus_carry_plus; assumption.
+Qed.
+
+(** Addition on positive is associative *)
+
+Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r.
+Proof.
+intros x y; generalize x; clear x.
+induction y as [y| y| ]; intro x.
+  destruct x as [x| x| ]; intro z; destruct z as [z| z| ]; simpl in |- *;
+   repeat rewrite Pplus_carry_spec; repeat rewrite Pplus_succ_permute_r;
+   repeat rewrite Pplus_succ_permute_l;
+   reflexivity || (repeat apply f_equal with (A := positive)); 
+   apply IHy.
+  destruct x as [x| x| ]; intro z; destruct z as [z| z| ]; simpl in |- *;
+   repeat rewrite Pplus_carry_spec; repeat rewrite Pplus_succ_permute_r;
+   repeat rewrite Pplus_succ_permute_l;
+   reflexivity || (repeat apply f_equal with (A := positive)); 
+   apply IHy.
+  intro z; rewrite Pplus_comm with (p := xH);
+   do 2 rewrite <- Pplus_one_succ_r; rewrite Pplus_succ_permute_l;
+   rewrite Pplus_succ_permute_r; reflexivity.
+Qed.
+
+(** Commutation of addition with the double of a positive number *)
+
+Lemma Pplus_xI_double_minus_one :
+ forall p q:positive, xO (p + q) = xI p + Pdouble_minus_one q.
+Proof.
+intros; change (xI p) with (xO p + xH) in |- *.
+rewrite <- Pplus_assoc; rewrite <- Pplus_one_succ_l;
+ rewrite Psucc_o_double_minus_one_eq_xO.
+reflexivity.
+Qed.
+
+Lemma Pplus_xO_double_minus_one :
+ forall p q:positive, Pdouble_minus_one (p + q) = xO p + Pdouble_minus_one q.
+Proof.
+induction p as [p IHp| p IHp| ]; destruct q as [q| q| ]; simpl in |- *;
+ try rewrite Pplus_carry_spec; try rewrite Pdouble_minus_one_o_succ_eq_xI;
+ try rewrite IHp; try rewrite Pplus_xI_double_minus_one; 
+ try reflexivity.
+ rewrite <- Psucc_o_double_minus_one_eq_xO; rewrite Pplus_one_succ_l;
+  reflexivity. 
+Qed.
+
+(** Misc *)
+
+Lemma Pplus_diag : forall p:positive, p + p = xO p.
+Proof.
+intro x; induction x; simpl in |- *; try rewrite Pplus_carry_spec;
+ try rewrite IHx; reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Peano induction on binary positive positive numbers *)
+
+Fixpoint plus_iter (x y:positive) {struct x} : positive :=
+  match x with
+  | xH => Psucc y
+  | xO x => plus_iter x (plus_iter x y)
+  | xI x => plus_iter x (plus_iter x (Psucc y))
+  end.
+
+Lemma plus_iter_eq_plus : forall p q:positive, plus_iter p q = p + q.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y;
+ [ destruct y as [p0| p0| ]
+ | destruct y as [p0| p0| ]
+ | destruct y as [p| p| ] ]; simpl in |- *; reflexivity || (do 2 rewrite IHp);
+ rewrite Pplus_assoc; rewrite Pplus_diag; try reflexivity.
+rewrite Pplus_carry_spec; rewrite <- Pplus_succ_permute_r; reflexivity.
+rewrite Pplus_one_succ_r; reflexivity.
+Qed.
+
+Lemma plus_iter_xO : forall p:positive, plus_iter p p = xO p.
+Proof.
+intro; rewrite <- Pplus_diag; apply plus_iter_eq_plus.
+Qed.
+
+Lemma plus_iter_xI : forall p:positive, Psucc (plus_iter p p) = xI p.
+Proof.
+intro; rewrite xI_succ_xO; rewrite <- Pplus_diag;
+ apply (f_equal (A:=positive)); apply plus_iter_eq_plus.
+Qed.
+
+Lemma iterate_add :
+ forall P:positive -> Type,
+   (forall n:positive, P n -> P (Psucc n)) ->
+   forall p q:positive, P q -> P (plus_iter p q).
+Proof.
+intros P H; induction p; simpl in |- *; intros.
+apply IHp; apply IHp; apply H; assumption.
+apply IHp; apply IHp; assumption.
+apply H; assumption.
+Defined.
+
+(** Peano induction *)
+
+Theorem Pind :
+ forall P:positive -> Prop,
+   P xH -> (forall n:positive, P n -> P (Psucc n)) -> forall p:positive, P p.
+Proof.
+intros P H1 Hsucc n; induction n.
+rewrite <- plus_iter_xI; apply Hsucc; apply iterate_add; assumption.
+rewrite <- plus_iter_xO; apply iterate_add; assumption.
+assumption.
+Qed.
+
+(** Peano recursion *)
+
+Definition Prec (A:Set) (a:A) (f:positive -> A -> A) : 
+  positive -> A :=
+  (fix Prec (p:positive) : A :=
+     match p with
+     | xH => a
+     | xO p => iterate_add (fun _ => A) f p p (Prec p)
+     | xI p => f (plus_iter p p) (iterate_add (fun _ => A) f p p (Prec p))
+     end).
+
+(** Peano case analysis *)
+
+Theorem Pcase :
+ forall P:positive -> Prop,
+   P xH -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p.
+Proof.
+intros; apply Pind; auto.
+Qed.
+
+(*
+Check
+  (let fact := Prec positive xH (fun p r => Psucc p * r) in
+   let seven := xI (xI xH) in
+   let five_thousand_forty :=
+     xO (xO (xO (xO (xI (xI (xO (xI (xI (xI (xO (xO xH))))))))))) in
+   refl_equal _:fact seven = five_thousand_forty).
+*)
+
+(**********************************************************************)
+(** Properties of multiplication on binary positive numbers *)
+
+(** One is right neutral for multiplication *)
+
+Lemma Pmult_1_r : forall p:positive, p * xH = p.
+Proof.
+intro x; induction x; simpl in |- *.
+  rewrite IHx; reflexivity.
+  rewrite IHx; reflexivity.
+  reflexivity.
+Qed.
+
+(** Right reduction properties for multiplication *)
+
+Lemma Pmult_xO_permute_r : forall p q:positive, p * xO q = xO (p * q).
+Proof.
+intros x y; induction x; simpl in |- *.
+  rewrite IHx; reflexivity.
+  rewrite IHx; reflexivity.
+  reflexivity.
+Qed.
+
+Lemma Pmult_xI_permute_r : forall p q:positive, p * xI q = p + xO (p * q).
+Proof.
+intros x y; induction x; simpl in |- *.
+  rewrite IHx; do 2 rewrite Pplus_assoc; rewrite Pplus_comm with (p := y);
+   reflexivity.
+  rewrite IHx; reflexivity.
+  reflexivity.
+Qed.
+
+(** Commutativity of multiplication *)
+
+Theorem Pmult_comm : forall p q:positive, p * q = q * p.
+Proof.
+intros x y; induction y; simpl in |- *.
+  rewrite <- IHy; apply Pmult_xI_permute_r.
+  rewrite <- IHy; apply Pmult_xO_permute_r.
+  apply Pmult_1_r.
+Qed.
+
+(** Distributivity of multiplication over addition *)
+
+Theorem Pmult_plus_distr_l :
+ forall p q r:positive, p * (q + r) = p * q + p * r.
+Proof.
+intros x y z; induction x; simpl in |- *.
+  rewrite IHx; rewrite <- Pplus_assoc with (q := xO (x * y));
+   rewrite Pplus_assoc with (p := xO (x * y));
+   rewrite Pplus_comm with (p := xO (x * y));
+   rewrite <- Pplus_assoc with (q := xO (x * y));
+   rewrite Pplus_assoc with (q := z); reflexivity.
+  rewrite IHx; reflexivity.
+  reflexivity.
+Qed.
+
+Theorem Pmult_plus_distr_r :
+ forall p q r:positive, (p + q) * r = p * r + q * r.
+Proof.
+intros x y z; do 3 rewrite Pmult_comm with (q := z); apply Pmult_plus_distr_l.
+Qed.
+
+(** Associativity of multiplication *)
+
+Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r.
+Proof.
+intro x; induction x as [x| x| ]; simpl in |- *; intros y z.
+  rewrite IHx; rewrite Pmult_plus_distr_r; reflexivity.
+  rewrite IHx; reflexivity.
+  reflexivity.
+Qed.
+
+(** Parity properties of multiplication *)
+
+Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, xI p * r <> xO q * r.
+Proof.
+intros x y z; induction z as [| z IHz| ]; try discriminate.
+intro H; apply IHz; clear IHz.
+do 2 rewrite Pmult_xO_permute_r in H.
+injection H; clear H; intro H; exact H.
+Qed.
+
+Lemma Pmult_xO_discr : forall p q:positive, xO p * q <> q.
+Proof.
+intros x y; induction y; try discriminate.
+rewrite Pmult_xO_permute_r; injection; assumption.
+Qed.
+
+(** Simplification properties of multiplication *)
+
+Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
+ intros z H; reflexivity || apply (f_equal (A:=positive)) || apply False_ind.
+  simpl in H; apply IHp with (xO z); simpl in |- *;
+   do 2 rewrite Pmult_xO_permute_r; apply Pplus_reg_l with (1 := H).
+  apply Pmult_xI_mult_xO_discr with (1 := H).
+  simpl in H; rewrite Pplus_comm in H; apply Pplus_no_neutral with (1 := H).
+  symmetry  in H; apply Pmult_xI_mult_xO_discr with (1 := H).
+  apply IHp with (xO z); simpl in |- *; do 2 rewrite Pmult_xO_permute_r;
+   assumption.
+  apply Pmult_xO_discr with (1 := H).
+  simpl in H; symmetry  in H; rewrite Pplus_comm in H;
+   apply Pplus_no_neutral with (1 := H).
+  symmetry  in H; apply Pmult_xO_discr with (1 := H).
+Qed.
+
+Theorem Pmult_reg_l : forall p q r:positive, r * p = r * q -> p = q.
+Proof.
+intros x y z H; apply Pmult_reg_r with (r := z).
+rewrite Pmult_comm with (p := x); rewrite Pmult_comm with (p := y);
+ assumption.
+Qed.
+
+(** Inversion of multiplication *)
+
+Lemma Pmult_1_inversion_l : forall p q:positive, p * q = xH -> p = xH.
+Proof.
+intros x y; destruct x as [p| p| ]; simpl in |- *.
+ destruct y as [p0| p0| ]; intro; discriminate.
+ intro; discriminate.
+ reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Properties of comparison on binary positive numbers *)
+
+Theorem Pcompare_not_Eq :
+ forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
+ split; simpl in |- *; auto; discriminate || (elim (IHp q); auto).
+Qed.
+
+Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
+ simpl in |- *; auto; intro H;
+ [ rewrite (IHp q); trivial
+ | absurd ((p ?= q) Gt = Eq);
+    [ elim (Pcompare_not_Eq p q); auto | assumption ]
+ | discriminate H
+ | absurd ((p ?= q) Lt = Eq);
+    [ elim (Pcompare_not_Eq p q); auto | assumption ]
+ | rewrite (IHp q); auto
+ | discriminate H
+ | discriminate H
+ | discriminate H ].
+Qed.
+
+Lemma Pcompare_Gt_Lt :
+ forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt.
+Proof.
+intro x; induction  x as [x Hrecx| x Hrecx| ]; intro y;
+ [ induction  y as [y Hrecy| y Hrecy| ]
+ | induction  y as [y Hrecy| y Hrecy| ]
+ | induction  y as [y Hrecy| y Hrecy| ] ]; simpl in |- *; 
+ auto; discriminate || intros H; discriminate H.
+Qed.
+
+Lemma Pcompare_Lt_Gt :
+ forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt.
+Proof.
+intro x; induction  x as [x Hrecx| x Hrecx| ]; intro y;
+ [ induction  y as [y Hrecy| y Hrecy| ]
+ | induction  y as [y Hrecy| y Hrecy| ]
+ | induction  y as [y Hrecy| y Hrecy| ] ]; simpl in |- *; 
+ auto; discriminate || intros H; discriminate H.
+Qed.
+
+Lemma Pcompare_Lt_Lt :
+ forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
+ simpl in |- *; auto; try discriminate; intro H2; elim (IHp q H2); 
+ auto; intros E; rewrite E; auto.
+Qed.
+
+Lemma Pcompare_Gt_Gt :
+ forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
+ simpl in |- *; auto; try discriminate; intro H2; elim (IHp q H2); 
+ auto; intros E; rewrite E; auto.
+Qed.
+
+Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt.
+Proof.
+simple induction r; auto. 
+Qed.
+
+Ltac ElimPcompare c1 c2 :=
+  elim (Dcompare ((c1 ?= c2) Eq));
+   [ idtac | let x := fresh "H" in
+             (intro x; case x; clear x) ].
+
+Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq.
+intro x; induction  x as [x Hrecx| x Hrecx| ]; auto.
+Qed.
+
+Lemma Pcompare_antisym :
+ forall (p q:positive) (r:comparison),
+   CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r).
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y;
+ [ destruct y as [p0| p0| ]
+ | destruct y as [p0| p0| ]
+ | destruct y as [p| p| ] ]; intro r;
+ reflexivity ||
+   (symmetry  in |- *; assumption) || discriminate H || simpl in |- *;
+ apply IHp || (try rewrite IHp); try reflexivity.
+Qed.
+
+Lemma ZC1 : forall p q:positive, (p ?= q) Eq = Gt -> (q ?= p) Eq = Lt.
+Proof.
+intros; change Eq with (CompOpp Eq) in |- *.
+rewrite <- Pcompare_antisym; rewrite H; reflexivity.
+Qed.
+
+Lemma ZC2 : forall p q:positive, (p ?= q) Eq = Lt -> (q ?= p) Eq = Gt.
+Proof.
+intros; change Eq with (CompOpp Eq) in |- *.
+rewrite <- Pcompare_antisym; rewrite H; reflexivity.
+Qed.
+
+Lemma ZC3 : forall p q:positive, (p ?= q) Eq = Eq -> (q ?= p) Eq = Eq.
+Proof.
+intros; change Eq with (CompOpp Eq) in |- *.
+rewrite <- Pcompare_antisym; rewrite H; reflexivity.
+Qed.
+
+Lemma ZC4 : forall p q:positive, (p ?= q) Eq = CompOpp ((q ?= p) Eq).
+Proof.
+intros; change Eq at 1 with (CompOpp Eq) in |- *.
+symmetry  in |- *; apply Pcompare_antisym.
+Qed.
+
+(**********************************************************************)
+(** Properties of subtraction on binary positive numbers *)
+
+Lemma double_eq_zero_inversion :
+ forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul.
+Proof.
+destruct p; simpl in |- *; [ trivial | discriminate 1 | discriminate 1 ].
+Qed.
+
+Lemma double_plus_one_zero_discr :
+ forall p:positive_mask, Pdouble_plus_one_mask p <> IsNul.
+Proof.
+simple induction p; intros; discriminate.
+Qed.
+
+Lemma double_plus_one_eq_one_inversion :
+ forall p:positive_mask, Pdouble_plus_one_mask p = IsPos xH -> p = IsNul.
+Proof.
+destruct p; simpl in |- *; [ trivial | discriminate 1 | discriminate 1 ].
+Qed.
+
+Lemma double_eq_one_discr :
+ forall p:positive_mask, Pdouble_mask p <> IsPos xH.
+Proof.
+simple induction p; intros; discriminate.
+Qed.
+
+Theorem Pminus_mask_diag : forall p:positive, Pminus_mask p p = IsNul.
+Proof.
+intro x; induction x as [p IHp| p IHp| ];
+ [ simpl in |- *; rewrite IHp; simpl in |- *; trivial
+ | simpl in |- *; rewrite IHp; auto
+ | auto ].
+Qed.
+
+Lemma ZL10 :
+ forall p q:positive,
+   Pminus_mask p q = IsPos xH -> Pminus_mask_carry p q = IsNul.
+Proof.
+intro x; induction x as [p| p| ]; intro y; destruct y as [q| q| ];
+ simpl in |- *; intro H; try discriminate H;
+ [ absurd (Pdouble_mask (Pminus_mask p q) = IsPos xH);
+    [ apply double_eq_one_discr | assumption ]
+ | assert (Heq : Pminus_mask p q = IsNul);
+    [ apply double_plus_one_eq_one_inversion; assumption
+    | rewrite Heq; reflexivity ]
+ | assert (Heq : Pminus_mask_carry p q = IsNul);
+    [ apply double_plus_one_eq_one_inversion; assumption
+    | rewrite Heq; reflexivity ]
+ | absurd (Pdouble_mask (Pminus_mask p q) = IsPos xH);
+    [ apply double_eq_one_discr | assumption ]
+ | destruct p; simpl in |- *;
+    [ discriminate H | discriminate H | reflexivity ] ].
+Qed.
+
+(** Properties of subtraction valid only for x>y *)
+
+Lemma Pminus_mask_Gt :
+ forall p q:positive,
+   (p ?= q) Eq = Gt ->
+    exists h : positive,
+     Pminus_mask p q = IsPos h /\
+     q + h = p /\ (h = xH \/ Pminus_mask_carry p q = IsPos (Ppred h)).
+Proof.
+intro x; induction x as [p| p| ]; intro y; destruct y as [q| q| ];
+ simpl in |- *; intro H; try discriminate H.
+  destruct (IHp q H) as [z [H4 [H6 H7]]]; exists (xO z); split.
+    rewrite H4; reflexivity.
+    split.
+      simpl in |- *; rewrite H6; reflexivity.
+      right; clear H6; destruct (ZL11 z) as [H8| H8];
+       [ rewrite H8; rewrite H8 in H4; rewrite ZL10;
+          [ reflexivity | assumption ]
+       | clear H4; destruct H7 as [H9| H9];
+          [ absurd (z = xH); assumption
+          | rewrite H9; clear H9; destruct z as [p0| p0| ];
+             [ reflexivity | reflexivity | absurd (xH = xH); trivial ] ] ].
+  case Pcompare_Gt_Gt with (1 := H);
+   [ intros H3; elim (IHp q H3); intros z H4; exists (xI z); elim H4;
+      intros H5 H6; elim H6; intros H7 H8; split;
+      [ simpl in |- *; rewrite H5; auto
+      | split;
+         [ simpl in |- *; rewrite H7; trivial
+         | right;
+            change (Pdouble_mask (Pminus_mask p q) = IsPos (Ppred (xI z)))
+             in |- *; rewrite H5; auto ] ]
+   | intros H3; exists xH; rewrite H3; split;
+      [ simpl in |- *; rewrite Pminus_mask_diag; auto | split; auto ] ].
+  exists (xO p); auto.
+  destruct (IHp q) as [z [H4 [H6 H7]]].
+    apply Pcompare_Lt_Gt; assumption.
+    destruct (ZL11 z) as [vZ| ];
+     [ exists xH; split;
+        [ rewrite ZL10; [ reflexivity | rewrite vZ in H4; assumption ]
+        | split;
+           [ simpl in |- *; rewrite Pplus_one_succ_r; rewrite <- vZ;
+              rewrite H6; trivial
+           | auto ] ]
+     | exists (xI (Ppred z)); destruct H7 as [| H8];
+        [ absurd (z = xH); assumption
+        | split;
+           [ rewrite H8; trivial
+           | split;
+              [ simpl in |- *; rewrite Pplus_carry_pred_eq_plus;
+                 [ rewrite H6; trivial | assumption ]
+              | right; rewrite H8; reflexivity ] ] ] ].
+  destruct (IHp q H) as [z [H4 [H6 H7]]].
+  exists (xO z); split;
+   [ rewrite H4; auto
+   | split;
+      [ simpl in |- *; rewrite H6; reflexivity
+      | right;
+         change
+           (Pdouble_plus_one_mask (Pminus_mask_carry p q) =
+            IsPos (Pdouble_minus_one z)) in |- *;
+         destruct (ZL11 z) as [H8| H8];
+         [ rewrite H8; simpl in |- *;
+            assert (H9 : Pminus_mask_carry p q = IsNul);
+            [ apply ZL10; rewrite <- H8; assumption
+            | rewrite H9; reflexivity ]
+         | destruct H7 as [H9| H9];
+            [ absurd (z = xH); auto
+            | rewrite H9; destruct z as [p0| p0| ]; simpl in |- *;
+               [ reflexivity
+               | reflexivity
+               | absurd (xH = xH); [ assumption | reflexivity ] ] ] ] ] ].
+  exists (Pdouble_minus_one p); split;
+   [ reflexivity
+   | clear IHp; split;
+      [ destruct p; simpl in |- *;
+         [ reflexivity
+         | rewrite Psucc_o_double_minus_one_eq_xO; reflexivity
+         | reflexivity ]
+      | destruct p; [ right | right | left ]; reflexivity ] ].
+Qed.
+
+Theorem Pplus_minus :
+ forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p.
+Proof.
+intros x y H; elim Pminus_mask_Gt with (1 := H); intros z H1; elim H1;
+ intros H2 H3; elim H3; intros H4 H5; unfold Pminus in |- *; 
+ rewrite H2; exact H4.
+Qed.
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
new file mode 100644
index 00000000..b1bdaaf0
--- /dev/null
+++ b/theories/NArith/NArith.v
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: NArith.v,v 1.2.2.1 2004/07/16 19:31:07 herbelin Exp $ *)
+
+(** Library for binary natural numbers *)
+
+Require Export BinPos.
+Require Export BinNat.
\ No newline at end of file
diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v
new file mode 100644
index 00000000..f5bbb1c9
--- /dev/null
+++ b/theories/NArith/Pnat.v
@@ -0,0 +1,485 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Pnat.v,v 1.3.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
+
+Require Import BinPos.
+
+(**********************************************************************)
+(** Properties of the injection from binary positive numbers to Peano 
+    natural numbers *)
+
+(** Original development by Pierre Crégut, CNET, Lannion, France *)
+
+Require Import Le.
+Require Import Lt.
+Require Import Gt.
+Require Import Plus.
+Require Import Mult.
+Require Import Minus.
+
+(** [nat_of_P] is a morphism for addition *)
+
+Lemma Pmult_nat_succ_morphism :
+ forall (p:positive) (n:nat), Pmult_nat (Psucc p) n = n + Pmult_nat p n.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; simpl in |- *; auto; intro m;
+ rewrite IHp; rewrite plus_assoc; trivial.
+Qed.
+
+Lemma nat_of_P_succ_morphism :
+ forall p:positive, nat_of_P (Psucc p) = S (nat_of_P p).
+Proof.
+  intro; change (S (nat_of_P p)) with (1 + nat_of_P p) in |- *;
+   unfold nat_of_P in |- *; apply Pmult_nat_succ_morphism.
+Qed.
+
+Theorem Pmult_nat_plus_carry_morphism :
+ forall (p q:positive) (n:nat),
+   Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y;
+ [ destruct y as [p0| p0| ]
+ | destruct y as [p0| p0| ]
+ | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; 
+ intro m;
+ [ rewrite IHp; rewrite plus_assoc; trivial with arith
+ | rewrite IHp; rewrite plus_assoc; trivial with arith
+ | rewrite Pmult_nat_succ_morphism; rewrite plus_assoc; trivial with arith
+ | rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ].
+Qed.
+
+Theorem nat_of_P_plus_carry_morphism :
+ forall p q:positive, nat_of_P (Pplus_carry p q) = S (nat_of_P (p + q)).
+Proof.
+intros; unfold nat_of_P in |- *; rewrite Pmult_nat_plus_carry_morphism;
+ simpl in |- *; trivial with arith.
+Qed.
+
+Theorem Pmult_nat_l_plus_morphism :
+ forall (p q:positive) (n:nat),
+   Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n.
+Proof.
+intro x; induction x as [p IHp| p IHp| ]; intro y;
+ [ destruct y as [p0| p0| ]
+ | destruct y as [p0| p0| ]
+ | destruct y as [p| p| ] ]; simpl in |- *; auto with arith;
+ [ intros m; rewrite Pmult_nat_plus_carry_morphism; rewrite IHp;
+    rewrite plus_assoc_reverse; rewrite plus_assoc_reverse;
+    rewrite (plus_permute m (Pmult_nat p (m + m))); 
+    trivial with arith
+ | intros m; rewrite IHp; apply plus_assoc
+ | intros m; rewrite Pmult_nat_succ_morphism;
+    rewrite (plus_comm (m + Pmult_nat p (m + m))); 
+    apply plus_assoc_reverse
+ | intros m; rewrite IHp; apply plus_permute
+ | intros m; rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ].
+Qed.
+
+Theorem nat_of_P_plus_morphism :
+ forall p q:positive, nat_of_P (p + q) = nat_of_P p + nat_of_P q.
+Proof.
+intros x y; exact (Pmult_nat_l_plus_morphism x y 1).
+Qed.
+
+(** [Pmult_nat] is a morphism for addition *)
+
+Lemma Pmult_nat_r_plus_morphism :
+ forall (p:positive) (n:nat),
+   Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n.
+Proof.
+intro y; induction y as [p H| p H| ]; intro m;
+ [ simpl in |- *; rewrite H; rewrite plus_assoc_reverse;
+    rewrite (plus_permute m (Pmult_nat p (m + m)));
+    rewrite plus_assoc_reverse; auto with arith
+ | simpl in |- *; rewrite H; auto with arith
+ | simpl in |- *; trivial with arith ].
+Qed.
+
+Lemma ZL6 : forall p:positive, Pmult_nat p 2 = nat_of_P p + nat_of_P p.
+Proof.
+intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism;
+ trivial.
+Qed.
+ 
+(** [nat_of_P] is a morphism for multiplication *)
+
+Theorem nat_of_P_mult_morphism :
+ forall p q:positive, nat_of_P (p * q) = nat_of_P p * nat_of_P q.
+Proof.
+intros x y; induction x as [x' H| x' H| ];
+ [ change (xI x' * y)%positive with (y + xO (x' * y))%positive in |- *;
+    rewrite nat_of_P_plus_morphism; unfold nat_of_P at 2 3 in |- *;
+    simpl in |- *; do 2 rewrite ZL6; rewrite H; rewrite mult_plus_distr_r;
+    reflexivity
+ | unfold nat_of_P at 1 2 in |- *; simpl in |- *; do 2 rewrite ZL6; rewrite H;
+    rewrite mult_plus_distr_r; reflexivity
+ | simpl in |- *; rewrite <- plus_n_O; reflexivity ].
+Qed.
+
+(** [nat_of_P] maps to the strictly positive subset of [nat] *)
+
+Lemma ZL4 : forall p:positive,  exists h : nat, nat_of_P p = S h.
+Proof.
+intro y; induction y as [p H| p H| ];
+ [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *;
+    simpl in |- *; change 2 with (1 + 1) in |- *;
+    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1; 
+    rewrite H1; auto with arith
+ | destruct H as [x H2]; exists (x + S x); unfold nat_of_P in |- *;
+    simpl in |- *; change 2 with (1 + 1) in |- *;
+    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; 
+    rewrite H2; auto with arith
+ | exists 0; auto with arith ].
+Qed.
+
+(** Extra lemmas on [lt] on Peano natural numbers *)
+
+Lemma ZL7 : forall n m:nat, n < m -> n + n < m + m.
+Proof.
+intros m n H; apply lt_trans with (m := m + n);
+ [ apply plus_lt_compat_l with (1 := H)
+ | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ].
+Qed.
+
+Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m.
+Proof.
+intros m n H; apply le_lt_trans with (m := m + n);
+ [ change (m + m < m + n) in |- *; apply plus_lt_compat_l with (1 := H)
+ | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ].
+Qed.
+
+(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
+    from [compare] on [positive])
+
+    Part 1: [lt] on [positive] is finer than [lt] on [nat]
+*)
+
+Lemma nat_of_P_lt_Lt_compare_morphism :
+ forall p q:positive, (p ?= q)%positive Eq = Lt -> nat_of_P p < nat_of_P q.
+Proof.
+intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ];
+ intro H2;
+ [ unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; do 2 rewrite ZL6;
+    apply ZL7; apply H; simpl in H2; assumption
+ | unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; apply ZL8;
+    apply H; simpl in H2; apply Pcompare_Gt_Lt; assumption
+ | simpl in |- *; discriminate H2
+ | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
+    elim (Pcompare_Lt_Lt p q H2);
+    [ intros H3; apply lt_S; apply ZL7; apply H; apply H3
+    | intros E; rewrite E; apply lt_n_Sn ]
+ | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
+    apply ZL7; apply H; assumption
+ | simpl in |- *; discriminate H2
+ | unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; rewrite ZL6;
+    elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *; 
+    apply lt_O_Sn
+ | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 q);
+    intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm;
+    apply lt_n_S; apply lt_O_Sn
+ | simpl in |- *; discriminate H2 ].
+Qed.
+
+(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
+    from [compare] on [positive])
+
+    Part 1: [gt] on [positive] is finer than [gt] on [nat]
+*)
+
+Lemma nat_of_P_gt_Gt_compare_morphism :
+ forall p q:positive, (p ?= q)%positive Eq = Gt -> nat_of_P p > nat_of_P q.
+Proof.
+unfold gt in |- *; intro x; induction x as [p H| p H| ]; intro y;
+ destruct y as [q| q| ]; intro H2;
+ [ simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
+    apply lt_n_S; apply ZL7; apply H; assumption
+ | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
+    elim (Pcompare_Gt_Gt p q H2);
+    [ intros H3; apply lt_S; apply ZL7; apply H; assumption
+    | intros E; rewrite E; apply lt_n_Sn ]
+ | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p);
+    intros h H3; rewrite H3; simpl in |- *; apply lt_n_S; 
+    apply lt_O_Sn
+ | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
+    apply ZL8; apply H; apply Pcompare_Lt_Gt; assumption
+ | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
+    apply ZL7; apply H; assumption
+ | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p);
+    intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm;
+    apply lt_n_S; apply lt_O_Sn
+ | simpl in |- *; discriminate H2
+ | simpl in |- *; discriminate H2
+ | simpl in |- *; discriminate H2 ].
+Qed.
+
+(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
+    from [compare] on [positive])
+
+    Part 2: [lt] on [nat] is finer than [lt] on [positive]
+*)
+
+Lemma nat_of_P_lt_Lt_compare_complement_morphism :
+ forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q)%positive Eq = Lt.
+Proof.
+intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq));
+ [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H;
+    absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ]
+ | intros H; elim H;
+    [ auto
+    | intros H1 H2; absurd (nat_of_P x < nat_of_P y);
+       [ apply lt_asym; change (nat_of_P x > nat_of_P y) in |- *;
+          apply nat_of_P_gt_Gt_compare_morphism; assumption
+       | assumption ] ] ].
+Qed.
+
+(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
+    from [compare] on [positive])
+
+    Part 2: [gt] on [nat] is finer than [gt] on [positive]
+*)
+
+Lemma nat_of_P_gt_Gt_compare_complement_morphism :
+ forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q)%positive Eq = Gt.
+Proof.
+intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq));
+ [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H;
+    absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ]
+ | intros H; elim H;
+    [ intros H1 H2; absurd (nat_of_P y < nat_of_P x);
+       [ apply lt_asym; apply nat_of_P_lt_Lt_compare_morphism; assumption
+       | assumption ]
+    | auto ] ].
+Qed.
+
+(** [nat_of_P] is strictly positive *)
+
+Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n.
+induction p; simpl in |- *; auto with arith.
+intro m; apply le_trans with (m + m); auto with arith.
+Qed.
+
+Lemma lt_O_nat_of_P : forall p:positive, 0 < nat_of_P p.
+intro; unfold nat_of_P in |- *; apply lt_le_trans with 1; auto with arith.
+apply le_Pmult_nat.
+Qed.
+
+(** Pmult_nat permutes with multiplication *)
+
+Lemma Pmult_nat_mult_permute :
+ forall (p:positive) (n m:nat), Pmult_nat p (m * n) = m * Pmult_nat p n.
+Proof.
+  simple induction p. intros. simpl in |- *. rewrite mult_plus_distr_l. rewrite <- (mult_plus_distr_l m n n).
+  rewrite (H (n + n) m). reflexivity.
+  intros. simpl in |- *. rewrite <- (mult_plus_distr_l m n n). apply H.
+  trivial.
+Qed.
+
+Lemma Pmult_nat_2_mult_2_permute :
+ forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1.
+Proof.
+  intros. rewrite <- Pmult_nat_mult_permute. reflexivity.
+Qed.
+
+Lemma Pmult_nat_4_mult_2_permute :
+ forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2.
+Proof.
+  intros. rewrite <- Pmult_nat_mult_permute. reflexivity.
+Qed.
+
+(** Mapping of xH, xO and xI through [nat_of_P] *)
+
+Lemma nat_of_P_xH : nat_of_P 1 = 1.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p.
+Proof.
+  simple induction p. unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute.
+  rewrite Pmult_nat_4_mult_2_permute. rewrite H. simpl in |- *. rewrite <- plus_Snm_nSm. reflexivity.
+  unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute.
+  rewrite H. reflexivity.
+  reflexivity.
+Qed.
+
+Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p).
+Proof.
+  simple induction p. unfold nat_of_P in |- *. simpl in |- *. intro p0. intro. rewrite Pmult_nat_2_mult_2_permute.
+  rewrite Pmult_nat_4_mult_2_permute; injection H; intro H1; rewrite H1;
+   rewrite <- plus_Snm_nSm; reflexivity.
+  unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute.
+  injection H; intro H1; rewrite H1; reflexivity.
+  reflexivity.
+Qed.
+
+(**********************************************************************)
+(** Properties of the shifted injection from Peano natural numbers to 
+    binary positive numbers *)
+
+(** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *)
+
+Theorem nat_of_P_o_P_of_succ_nat_eq_succ :
+ forall n:nat, nat_of_P (P_of_succ_nat n) = S n.
+Proof.
+intro m; induction m as [| n H];
+ [ reflexivity
+ | simpl in |- *; rewrite nat_of_P_succ_morphism; rewrite H; auto ].
+Qed.
+
+(** Miscellaneous lemmas on [P_of_succ_nat] *)
+
+Lemma ZL3 :
+ forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n).
+Proof.
+intro x; induction x as [| n H];
+ [ simpl in |- *; auto with arith
+ | simpl in |- *; rewrite plus_comm; simpl in |- *; rewrite H;
+    rewrite xO_succ_permute; auto with arith ].
+Qed.
+
+Lemma ZL5 : forall n:nat, P_of_succ_nat (S n + S n) = xI (P_of_succ_nat n).
+Proof.
+intro x; induction x as [| n H]; simpl in |- *;
+ [ auto with arith
+ | rewrite <- plus_n_Sm; simpl in |- *; simpl in H; rewrite H;
+    auto with arith ].
+Qed.
+
+(** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *)
+
+Theorem P_of_succ_nat_o_nat_of_P_eq_succ :
+ forall p:positive, P_of_succ_nat (nat_of_P p) = Psucc p.
+Proof.
+intro x; induction x as [p H| p H| ];
+ [ simpl in |- *; rewrite <- H; change 2 with (1 + 1) in |- *;
+    rewrite Pmult_nat_r_plus_morphism; elim (ZL4 p); 
+    unfold nat_of_P in |- *; intros n H1; rewrite H1; 
+    rewrite ZL3; auto with arith
+ | unfold nat_of_P in |- *; simpl in |- *; change 2 with (1 + 1) in |- *;
+    rewrite Pmult_nat_r_plus_morphism;
+    rewrite <- (Ppred_succ (P_of_succ_nat (Pmult_nat p 1 + Pmult_nat p 1)));
+    rewrite <- (Ppred_succ (xI p)); simpl in |- *; 
+    rewrite <- H; elim (ZL4 p); unfold nat_of_P in |- *; 
+    intros n H1; rewrite H1; rewrite ZL5; simpl in |- *; 
+    trivial with arith
+ | unfold nat_of_P in |- *; simpl in |- *; auto with arith ].
+Qed.
+
+(** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity
+    on [positive] *)
+
+Theorem pred_o_P_of_succ_nat_o_nat_of_P_eq_id :
+ forall p:positive, Ppred (P_of_succ_nat (nat_of_P p)) = p.
+Proof.
+intros x; rewrite P_of_succ_nat_o_nat_of_P_eq_succ; rewrite Ppred_succ;
+ trivial with arith.
+Qed.
+
+(**********************************************************************)
+(** Extra properties of the injection from binary positive numbers to Peano 
+    natural numbers *)
+
+(** [nat_of_P] is a morphism for subtraction on positive numbers *)
+
+Theorem nat_of_P_minus_morphism :
+ forall p q:positive,
+   (p ?= q)%positive Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q.
+Proof.
+intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r;
+ [ rewrite <- nat_of_P_plus_morphism; rewrite Pplus_minus; auto with arith
+ | apply lt_le_weak; exact (nat_of_P_gt_Gt_compare_morphism x y H) ].
+Qed.
+
+(** [nat_of_P] is injective *)
+
+Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q.
+Proof.
+intros x y H; rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id x);
+ rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id y); 
+ rewrite H; trivial with arith.
+Qed.
+
+Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p.
+Proof.
+intros p q; elim (ZL4 p); elim (ZL4 q); intros h H1 i H2; rewrite H1;
+ rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S; 
+ apply le_minus.
+Qed.
+
+Lemma ZL17 : forall p q:positive, nat_of_P p < nat_of_P (p + q).
+Proof.
+intros p q; rewrite nat_of_P_plus_morphism; unfold lt in |- *; elim (ZL4 q);
+ intros k H; rewrite H; rewrite plus_comm; simpl in |- *; 
+ apply le_n_S; apply le_plus_r.
+Qed.
+
+(** Comparison and subtraction *)
+
+Lemma Pcompare_minus_r :
+ forall p q r:positive,
+   (q ?= p)%positive Eq = Lt ->
+   (r ?= p)%positive Eq = Gt ->
+   (r ?= q)%positive Eq = Gt -> (r - p ?= r - q)%positive Eq = Lt.
+Proof.
+intros; apply nat_of_P_lt_Lt_compare_complement_morphism;
+ rewrite nat_of_P_minus_morphism;
+ [ rewrite nat_of_P_minus_morphism;
+    [ apply plus_lt_reg_l with (p := nat_of_P q); rewrite le_plus_minus_r;
+       [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p);
+          rewrite plus_assoc; rewrite le_plus_minus_r;
+          [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l;
+             apply nat_of_P_lt_Lt_compare_morphism; 
+             assumption
+          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
+             apply ZC1; assumption ]
+       | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;
+          assumption ]
+    | assumption ]
+ | assumption ].
+Qed.
+
+Lemma Pcompare_minus_l :
+ forall p q r:positive,
+   (q ?= p)%positive Eq = Lt ->
+   (p ?= r)%positive Eq = Gt ->
+   (q ?= r)%positive Eq = Gt -> (q - r ?= p - r)%positive Eq = Lt.
+Proof.
+intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism;
+ rewrite nat_of_P_minus_morphism;
+ [ rewrite nat_of_P_minus_morphism;
+    [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z);
+       rewrite le_plus_minus_r;
+       [ rewrite le_plus_minus_r;
+          [ apply nat_of_P_lt_Lt_compare_morphism; assumption
+          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
+             apply ZC1; assumption ]
+       | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;
+          assumption ]
+    | assumption ]
+ | assumption ].
+Qed.
+
+(** Distributivity of multiplication over subtraction *)
+
+Theorem Pmult_minus_distr_l :
+ forall p q r:positive,
+   (q ?= r)%positive Eq = Gt ->
+   (p * (q - r))%positive = (p * q - p * r)%positive.
+Proof.
+intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism;
+ rewrite nat_of_P_minus_morphism;
+ [ rewrite nat_of_P_minus_morphism;
+    [ do 2 rewrite nat_of_P_mult_morphism;
+       do 3 rewrite (mult_comm (nat_of_P x)); apply mult_minus_distr_r
+    | apply nat_of_P_gt_Gt_compare_complement_morphism;
+       do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *; 
+       elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l;
+       exact (nat_of_P_gt_Gt_compare_morphism y z H) ]
+ | assumption ].
+Qed.