diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 212 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 961 | ||||
| -rw-r--r-- | theories/NArith/NArith.v | 14 | ||||
| -rw-r--r-- | theories/NArith/Pnat.v | 485 |
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. |