# 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.
Addition
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
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 1
| IsNeg => IsNeg
| IsPos p => IsPos p~1
end.
Operation x -> 2*x
Definition Pdouble_mask (x:positive_mask) :=
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
Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask :=
match x, y with
| p~1, q~1 => Pdouble_mask (Pminus_mask p q)
| p~1, q~0 => Pdouble_plus_one_mask (Pminus_mask p q)
| p~1, 1 => IsPos p~0
| p~0, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
| p~0, q~0 => Pdouble_mask (Pminus_mask p q)
| p~0, 1 => IsPos (Pdouble_minus_one p)
| 1, 1 => IsNul
| 1, _ => IsNeg
end
with Pminus_mask_carry (x y:positive) {struct y} : positive_mask :=
match x, y with
| p~1, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
| p~1, q~0 => Pdouble_mask (Pminus_mask p q)
| p~1, 1 => IsPos (Pdouble_minus_one p)
| p~0, q~1 => Pdouble_mask (Pminus_mask_carry p q)
| p~0, q~0 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
| 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) :=
match Pminus_mask x y with
| 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
Lemma Psucc_o_double_minus_one_eq_xO :
forall p:positive, Psucc (Pdouble_minus_one p) = p~0.
Lemma Pdouble_minus_one_o_succ_eq_xI :
forall p:positive, Pdouble_minus_one (Psucc p) = p~1.
Lemma xO_succ_permute :
forall p:positive, (Psucc p)~0 = Psucc (Psucc p~0).
Lemma double_moins_un_xO_discr :
forall p:positive, Pdouble_minus_one p <> p~0.
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.
Addition on positive is associative
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.
Distributivity of multiplication over addition
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.
Definition Ppred_mask (p : positive_mask) :=
match p with
| IsPos 1 => IsNul
| IsPos q => IsPos (Ppred q)
| IsNul => IsNeg
| IsNeg => IsNeg
end.
Lemma Pminus_mask_succ_r :
forall p q : positive, Pminus_mask p (Psucc q) = Pminus_mask_carry p q.
Theorem Pminus_mask_carry_spec :
forall p q : positive, Pminus_mask_carry p q = Ppred_mask (Pminus_mask p q).
Theorem Pminus_succ_r : forall p q : positive, p - (Psucc q) = Ppred (p - q).
Lemma double_eq_zero_inversion :
forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul.
Lemma double_plus_one_zero_discr :
forall p:positive_mask, Pdouble_plus_one_mask p <> IsNul.
Lemma double_plus_one_eq_one_inversion :
forall p:positive_mask, Pdouble_plus_one_mask p = IsPos 1 -> p = IsNul.
Lemma double_eq_one_discr :
forall p:positive_mask, Pdouble_mask p <> IsPos 1.
Theorem Pminus_mask_diag : forall p:positive, Pminus_mask p p = IsNul.
Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg.
Lemma Pminus_mask_IsNeg : forall p q:positive,
Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg.
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
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 = 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.