diff options
Diffstat (limited to 'theories/NArith/BinPos.v')
| -rw-r--r-- | theories/NArith/BinPos.v | 961 |
1 files changed, 961 insertions, 0 deletions
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. |