# Library Coq.NArith.BinPos

``` Unset Boxed Definitions. ```
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. ```
``` Set Boxed Definitions. 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. Unset Boxed Definitions. 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. ```
``` 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. ```
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. ```
``` 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. ```