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
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
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
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.
Miscellaneous properties of binary positive numbers
Lemma ZL11 :
forall p:positive,
p = 1 \/
p <> 1.
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
Theorem Pplus_comm :
forall p q:positive,
p +
q =
q +
p.
Permutation of Pplus and Psucc
No neutral for addition on strictly positive numbers
Simplification
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
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")
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
Right reduction properties for multiplication
Commutativity of multiplication
Theorem Pmult_comm :
forall p q:positive,
p *
q =
q *
p.
Distributivity of multiplication over addition
Associativity of multiplication
Theorem Pmult_assoc :
forall p q r:positive,
p * (
q *
r) =
p *
q *
r.
Parity properties of multiplication
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
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_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).
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
Lemma Pminus_Eq :
forall p:positive,
p-p = 1.
Number of digits in a number