# Library Coq.NArith.BinPos

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

Postfix notation for positive numbers, allowing to mimic the position of bits in a big-endian representation. For instance, we can write 1~1~0 instead of (xO (xI xH)) for the number 6 (which is 110 in binary notation).

Notation "p ~ 1" := (xI p)
(at level 7, left associativity, format "p '~' '1'") : positive_scope.
Notation "p ~ 0" := (xO p)
(at level 7, left associativity, format "p '~' '0'") : positive_scope.

Open Local Scope positive_scope.

Notation Local "1" := xH (at level 7).

Successor

Fixpoint Psucc (x:positive) : positive :=
match x with
| p~1 => (Psucc p)~0
| p~0 => p~1
| 1 => 1~0
end.

Fixpoint Pplus (x y:positive) : positive :=
match x, y with
| p~1, q~1 => (Pplus_carry p q)~0
| p~1, q~0 => (Pplus p q)~1
| p~1, 1 => (Psucc p)~0
| p~0, q~1 => (Pplus p q)~1
| p~0, q~0 => (Pplus p q)~0
| p~0, 1 => p~1
| 1, q~1 => (Psucc q)~0
| 1, q~0 => q~1
| 1, 1 => 1~0
end

with Pplus_carry (x y:positive) : positive :=
match x, y with
| p~1, q~1 => (Pplus_carry p q)~1
| p~1, q~0 => (Pplus_carry p q)~0
| p~1, 1 => (Psucc p)~1
| p~0, q~1 => (Pplus_carry p q)~0
| p~0, q~0 => (Pplus p q)~1
| p~0, 1 => (Psucc p)~0
| 1, q~1 => (Psucc q)~1
| 1, q~0 => (Psucc q)~0
| 1, 1 => 1~1
end.

Infix "+" := Pplus : positive_scope.

From binary positive numbers to Peano natural numbers

Fixpoint Pmult_nat (x:positive) (pow2:nat) : nat :=
match x with
| p~1 => (pow2 + Pmult_nat p (pow2 + pow2))%nat
| p~0 => Pmult_nat p (pow2 + pow2)%nat
| 1 => pow2
end.

Definition nat_of_P (x:positive) := Pmult_nat x (S O).

From Peano natural numbers to binary positive numbers

Fixpoint P_of_succ_nat (n:nat) : positive :=
match n with
| O => 1
| S x => Psucc (P_of_succ_nat x)
end.

Operation x -> 2*x-1

Fixpoint Pdouble_minus_one (x:positive) : positive :=
match x with
| p~1 => p~0~1
| p~0 => (Pdouble_minus_one p)~1
| 1 => 1
end.

Predecessor

Definition Ppred (x:positive) :=
match x with
| p~1 => p~0
| p~0 => Pdouble_minus_one p
| 1 => 1
end.

An auxiliary type for subtraction
Operation x -> 2*x+1

match x with
| IsNul => IsPos 1
| IsNeg => IsNeg
| IsPos p => IsPos p~1
end.

Operation x -> 2*x

match x with
| IsNul => IsNul
| IsNeg => IsNeg
| IsPos p => IsPos p~0
end.

Operation x -> 2*x-2

Definition Pdouble_minus_two (x:positive) :=
match x with
| p~1 => IsPos p~0~0
| p~0 => IsPos (Pdouble_minus_one p)~0
| 1 => IsNul
end.

Subtraction of binary positive numbers into a positive numbers mask

match x, y with
| p~1, 1 => IsPos p~0
| p~0, 1 => IsPos (Pdouble_minus_one p)
| 1, 1 => IsNul
| 1, _ => IsNeg
end

match x, y with
| p~1, 1 => IsPos (Pdouble_minus_one p)
| p~0, 1 => Pdouble_minus_two p
| 1, _ => IsNeg
end.

Subtraction of binary positive numbers x and y, returns 1 if x<=y

Definition Pminus (x y:positive) :=
| IsPos z => z
| _ => 1
end.

Infix "-" := Pminus : positive_scope.

Multiplication on binary positive numbers

Fixpoint Pmult (x y:positive) : positive :=
match x with
| p~1 => y + (Pmult p y)~0
| p~0 => (Pmult p y)~0
| 1 => y
end.

Infix "*" := Pmult : positive_scope.

Division by 2 rounded below but for 1

Definition Pdiv2 (z:positive) :=
match z with
| 1 => 1
| p~0 => p
| p~1 => 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
| p~1, q~1 => Pcompare p q r
| p~1, q~0 => Pcompare p q Gt
| p~1, 1 => Gt
| p~0, q~1 => Pcompare p q Lt
| p~0, q~0 => Pcompare p q r
| p~0, 1 => Gt
| 1, q~1 => Lt
| 1, q~0 => Lt
| 1, 1 => r
end.

Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.

Definition Plt (x y:positive) := (Pcompare x y Eq) = Lt.
Definition Pgt (x y:positive) := (Pcompare x y Eq) = Gt.
Definition Ple (x y:positive) := (Pcompare x y Eq) <> Gt.
Definition Pge (x y:positive) := (Pcompare x y Eq) <> Lt.

Infix "<=" := Ple : positive_scope.
Infix "<" := Plt : positive_scope.
Infix ">=" := Pge : positive_scope.
Infix ">" := Pgt : positive_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.

Definition Pmin (p p' : positive) := match Pcompare p p' Eq with
| Lt | Eq => p
| Gt => p'
end.

Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
| Lt | Eq => p'
| Gt => p
end.

Boolean equality

Fixpoint Peqb (x y : positive) {struct y} : bool :=
match x, y with
| 1, 1 => true
| p~1, q~1 => Peqb p q
| p~0, q~0 => Peqb p q
| _, _ => false
end.

Decidability of equality on binary positive numbers

Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}.

Properties of successor on binary positive numbers

Specification of xI in term of Psucc and xO

Lemma xI_succ_xO : forall p:positive, p~1 = Psucc p~0.

Lemma Psucc_discr : forall p:positive, p <> Psucc p.

Successor and double
Successor and predecessor

Lemma Psucc_not_one : forall p:positive, Psucc p <> 1.

Lemma Ppred_succ : forall p:positive, Ppred (Psucc p) = p.

Lemma Psucc_pred : forall p:positive, p = 1 \/ Psucc (Ppred p) = p.

Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)).

Injectivity of successor

Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q.

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 + 1.

Lemma Pplus_one_succ_l : forall p:positive, Psucc p = 1 + p.

Specification of Pplus_carry

Theorem Pplus_carry_spec :
forall p q:positive, Pplus_carry p q = Psucc (p + q).

Commutativity

Theorem Pplus_comm : forall p q:positive, p + q = q + p.

Permutation of Pplus and Psucc

Theorem Pplus_succ_permute_r :
forall p q:positive, p + Psucc q = Psucc (p + q).

Theorem Pplus_succ_permute_l :
forall p q:positive, Psucc p + q = Psucc (p + q).

Theorem Pplus_carry_pred_eq_plus :
forall p q:positive, q <> 1 -> Pplus_carry p (Ppred q) = p + q.

No neutral for addition on strictly positive numbers

Lemma Pplus_no_neutral : forall p q:positive, q + p <> p.

Lemma Pplus_carry_no_neutral :
forall p q:positive, Pplus_carry q p <> Psucc p.

Simplification

Lemma Pplus_carry_plus :
forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s.

Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q.

Lemma Pplus_reg_l : forall p q r:positive, p + q = p + r -> q = r.

Lemma Pplus_carry_reg_r :
forall p q r:positive, Pplus_carry p r = Pplus_carry q r -> p = q.

Lemma Pplus_carry_reg_l :
forall p q r:positive, Pplus_carry p q = Pplus_carry p r -> q = r.

Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r.

Commutation of addition with the double of a positive number

Lemma Pplus_xO : forall m n : positive, (m + n)~0 = m~0 + n~0.

Lemma Pplus_xI_double_minus_one :
forall p q:positive, (p + q)~0 = p~1 + Pdouble_minus_one q.

Lemma Pplus_xO_double_minus_one :
forall p q:positive, Pdouble_minus_one (p + q) = p~0 + Pdouble_minus_one q.

Misc

Lemma Pplus_diag : forall p:positive, p + p = p~0.

Peano induction and recursion on binary positive positive numbers
(a nice proof from Conor McBride, see "The view from the left")

Inductive PeanoView : positive -> Type :=
| PeanoOne : PeanoView 1
| PeanoSucc : forall p, PeanoView p -> PeanoView (Psucc p).

Fixpoint peanoView_xO p (q:PeanoView p) : PeanoView (p~0) :=
match q in PeanoView x return PeanoView (x~0) with
| PeanoOne => PeanoSucc _ PeanoOne
| PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xO _ q))
end.

Fixpoint peanoView_xI p (q:PeanoView p) : PeanoView (p~1) :=
match q in PeanoView x return PeanoView (x~1) with
| PeanoOne => PeanoSucc _ (PeanoSucc _ PeanoOne)
| PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xI _ q))
end.

Fixpoint peanoView p : PeanoView p :=
match p return PeanoView p with
| 1 => PeanoOne
| p~0 => peanoView_xO p (peanoView p)
| p~1 => peanoView_xI p (peanoView p)
end.

Definition PeanoView_iter (P:positive->Type)
(a:P 1) (f:forall p, P p -> P (Psucc p)) :=
(fix iter p (q:PeanoView p) : P p :=
match q in PeanoView p return P p with
| PeanoOne => a
| PeanoSucc _ q => f _ (iter _ q)
end).

Require Import Eqdep_dec EqdepFacts.

Theorem eq_dep_eq_positive :
forall (P:positive->Type) (p:positive) (x y:P p),
eq_dep positive P p x p y -> x = y.

Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.

Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p))
(p:positive) :=
PeanoView_iter P a f p (peanoView p).

Theorem Prect_succ : forall (P:positive->Type) (a:P 1)
(f:forall p, P p -> P (Psucc p)) (p:positive),
Prect P a f (Psucc p) = f _ (Prect P a f p).

Theorem Prect_base : forall (P:positive->Type) (a:P 1)
(f:forall p, P p -> P (Psucc p)), Prect P a f 1 = a.

Definition Prec (P:positive->Set) := Prect P.

Peano induction

Definition Pind (P:positive->Prop) := Prect P.

Peano case analysis

Theorem Pcase :
forall P:positive -> Prop,
P 1 -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p.

Properties of multiplication on binary positive numbers

One is right neutral for multiplication

Lemma Pmult_1_r : forall p:positive, p * 1 = p.

Successor and multiplication

Lemma Pmult_Sn_m : forall n m : positive, (Psucc n) * m = m + n * m.

Right reduction properties for multiplication

Lemma Pmult_xO_permute_r : forall p q:positive, p * q~0 = (p * q)~0.

Lemma Pmult_xI_permute_r : forall p q:positive, p * q~1 = p + (p * q)~0.

Commutativity of multiplication

Theorem Pmult_comm : forall p q:positive, p * q = q * p.

Theorem Pmult_plus_distr_l :
forall p q r:positive, p * (q + r) = p * q + p * r.

Theorem Pmult_plus_distr_r :
forall p q r:positive, (p + q) * r = p * r + q * r.

Associativity of multiplication

Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r.

Parity properties of multiplication

Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, p~1 * r <> q~0 * r.

Lemma Pmult_xO_discr : forall p q:positive, p~0 * q <> q.

Simplification properties of multiplication

Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q.

Theorem Pmult_reg_l : forall p q r:positive, r * p = r * q -> p = q.

Inversion of multiplication

Lemma Pmult_1_inversion_l : forall p q:positive, p * q = 1 -> p = 1.

Properties of boolean equality

Theorem Peqb_refl : forall x:positive, Peqb x x = true.

Theorem Peqb_true_eq : forall x y:positive, Peqb x y = true -> x=y.

Theorem Peqb_eq : forall x y : positive, Peqb x y = true <-> x=y.

Properties of comparison on binary positive numbers

Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq.

Theorem Pcompare_refl_id : forall (p : positive) (r : comparison), (p ?= p) r = r.

Theorem Pcompare_not_Eq :
forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq.

Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.

Lemma Pcompare_eq_iff : forall p q:positive, (p ?= q) Eq = Eq <-> p = q.

Lemma Pcompare_Gt_Lt :
forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt.

Lemma Pcompare_eq_Lt :
forall p q : positive, (p ?= q) Eq = Lt <-> (p ?= q) Gt = Lt.

Lemma Pcompare_Lt_Gt :
forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt.

Lemma Pcompare_eq_Gt :
forall p q : positive, (p ?= q) Eq = Gt <-> (p ?= q) Lt = Gt.

Lemma Pcompare_Lt_Lt :
forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q.

Lemma Pcompare_Lt_eq_Lt :
forall p q:positive, (p ?= q) Lt = Lt <-> (p ?= q) Eq = Lt \/ p = q.

Lemma Pcompare_Gt_Gt :
forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q.

Lemma Pcompare_Gt_eq_Gt :
forall p q:positive, (p ?= q) Gt = Gt <-> (p ?= q) Eq = Gt \/ p = q.

Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt.

Ltac ElimPcompare c1 c2 :=
elim (Dcompare ((c1 ?= c2) Eq));
[ idtac | let x := fresh "H" in (intro x; case x; clear x) ].

Lemma Pcompare_antisym :
forall (p q:positive) (r:comparison),
CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r).

Lemma ZC1 : forall p q:positive, (p ?= q) Eq = Gt -> (q ?= p) Eq = Lt.

Lemma ZC2 : forall p q:positive, (p ?= q) Eq = Lt -> (q ?= p) Eq = Gt.

Lemma ZC3 : forall p q:positive, (p ?= q) Eq = Eq -> (q ?= p) Eq = Eq.

Lemma ZC4 : forall p q:positive, (p ?= q) Eq = CompOpp ((q ?= p) Eq).

Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq).

Comparison and the successor

Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.

Theorem Pcompare_p_Sq : forall p q : positive,
(p ?= Psucc q) Eq = Lt <-> (p ?= q) Eq = Lt \/ p = q.

1 is the least positive number

Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt.

Properties of the strict order on positive numbers

Lemma Plt_1 : forall p, ~ p < 1.

Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m.

Lemma Plt_irrefl : forall p : positive, ~ p < p.

Lemma Plt_trans : forall n m p : positive, n < m -> m < p -> n < p.

Theorem Plt_ind : forall (A : positive -> Prop) (n : positive),
A (Psucc n) ->
(forall m : positive, n < m -> A m -> A (Psucc m)) ->
forall m : positive, n < m -> A m.

Lemma Ple_lteq : forall p q, p <= q <-> p < q \/ p = q.

Properties of subtraction on binary positive numbers

Lemma Ppred_minus : forall p, Ppred p = Pminus p 1.

match p with
| IsPos 1 => IsNul
| IsPos q => IsPos (Ppred q)
| IsNul => IsNeg
| IsNeg => IsNeg
end.

forall p q : positive, Pminus_mask p (Psucc q) = Pminus_mask_carry p q.

Theorem Pminus_succ_r : forall p q : positive, p - (Psucc q) = Ppred (p - q).

Lemma double_eq_zero_inversion :

Lemma double_plus_one_zero_discr :

Lemma double_plus_one_eq_one_inversion :

Lemma double_eq_one_discr :

Lemma Pminus_mask_IsNeg : forall p q:positive,

Lemma ZL10 :
forall p q:positive,
Pminus_mask p q = IsPos 1 -> Pminus_mask_carry p q = IsNul.

Properties of subtraction valid only for x>y

forall p q:positive,
(p ?= q) Eq = Gt ->
exists h : positive,
Pminus_mask p q = IsPos h /\
q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)).

Theorem Pplus_minus :
forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p.

When x<y, the substraction of x by y returns 1

Lemma Pminus_mask_Lt : forall p q:positive, p<q -> Pminus_mask p q = IsNeg.

Lemma Pminus_Lt : forall p q:positive, p<q -> p-q = 1.

The substraction of x by x returns 1

Lemma Pminus_Eq : forall p:positive, p-p = 1.

Number of digits in a number

Fixpoint Psize (p:positive) : nat :=
match p with
| 1 => S O
| p~1 => S (Psize p)
| p~0 => S (Psize p)
end.

Lemma Psize_monotone : forall p q, (p?=q) Eq = Lt -> (Psize p <= Psize q)%nat.