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.