Library Coq.NArith.BinPos
Binary positive numbers
Original development by Pierre Crégut, CNET, Lannion, France
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
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
From Peano natural numbers to binary positive numbers
Operation x -> 2*x-1
Predecessor
An auxiliary type for subtraction
Operation x -> 2*x+1
Operation x -> 2*x
Operation x -> 2*x-2
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
Multiplication on binary positive numbers
Division by 2 rounded below but for 1
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
Decidability of equality on binary positive numbers
Properties of successor on binary positive numbers
Specification of xI in term of Psucc and xO
Successor and double
Successor and predecessor
Injectivity of successor
Properties of addition on binary positive numbers
Specification of Psucc in term of Pplus
Specification of Pplus_carry
Commutativity
Permutation of Pplus and Psucc
No neutral for addition on strictly positive numbers
Simplification
Addition on positive is associative
Commutation of addition with the double of a positive number
Misc
Peano induction and recursion on binary positive positive numbers
(a nice proof from Conor McBride, see "The view from the left")
Peano induction
Peano case analysis
Properties of multiplication on binary positive numbers
One is right neutral for multiplication
Successor and multiplication
Right reduction properties for multiplication
Commutativity of multiplication
Distributivity of multiplication over addition
Associativity of multiplication
Parity properties of multiplication
Simplification properties of multiplication
Inversion of multiplication
Properties of boolean equality
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
1 is the least positive number
Properties of the strict order on positive numbers
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
When x<y, the substraction of x by y returns 1
The substraction of x by x returns 1
Number of digits in a number