Library Coq.ZArith.BinInt
Binary Integers (Pierre Crégut, CNET, Lannion, France)
Automatically open scope positive_scope for the constructors of Z
Delimit Scope Z_scope with Z.
Subtraction of positive into Z
Definition Zdouble_plus_one (
x:
Z) :=
match x with
|
Z0 =>
Zpos 1
|
Zpos p =>
Zpos p~1
|
Zneg p =>
Zneg (
Pdouble_minus_one p)
end.
Definition Zdouble_minus_one (
x:
Z) :=
match x with
|
Z0 =>
Zneg 1
|
Zneg p =>
Zneg p~1
|
Zpos p =>
Zpos (
Pdouble_minus_one p)
end.
Definition Zdouble (
x:
Z) :=
match x with
|
Z0 =>
Z0
|
Zpos p =>
Zpos p~0
|
Zneg p =>
Zneg p~0
end.
Open Local Scope positive_scope.
Fixpoint ZPminus (
x y:
positive) {
struct y} :
Z :=
match x,
y with
|
p~1,
q~1 =>
Zdouble (
ZPminus p q)
|
p~1,
q~0 =>
Zdouble_plus_one (
ZPminus p q)
|
p~1, 1 =>
Zpos p~0
|
p~0,
q~1 =>
Zdouble_minus_one (
ZPminus p q)
|
p~0,
q~0 =>
Zdouble (
ZPminus p q)
|
p~0, 1 =>
Zpos (
Pdouble_minus_one p)
| 1,
q~1 =>
Zneg q~0
| 1,
q~0 =>
Zneg (
Pdouble_minus_one q)
| 1, 1 =>
Z0
end.
Close Local Scope positive_scope.
Multiplication on integers
Definition Zcompare (
x y:
Z) :=
match x,
y with
|
Z0,
Z0 =>
Eq
|
Z0,
Zpos y' =>
Lt
|
Z0,
Zneg y' =>
Gt
|
Zpos x',
Z0 =>
Gt
|
Zpos x',
Zpos y' => (
x' ?= y')%
positive Eq
|
Zpos x',
Zneg y' =>
Gt
|
Zneg x',
Z0 =>
Lt
|
Zneg x',
Zpos y' =>
Lt
|
Zneg x',
Zneg y' =>
CompOpp ((
x' ?= y')%
positive Eq)
end.
Infix "?=" :=
Zcompare (
at level 70,
no associativity) :
Z_scope.
Ltac elim_compare com1 com2 :=
case (
Dcompare (
com1 ?= com2)%
Z);
[
idtac |
let x :=
fresh "H"
in
(
intro x;
case x;
clear x) ].
Direct, easier to handle variants of successor and addition
Inductive specification of Z
Theorem Zind :
forall P:
Z ->
Prop,
P Z0 ->
(
forall x:
Z,
P x ->
P (
Zsucc' x)) ->
(
forall x:
Z,
P x ->
P (
Zpred' x)) ->
forall n:
Z,
P n.
Misc properties about binary integer operations
Properties of opposite on binary integer numbers
opp is involutive
Injectivity of the opposite
Other properties of binary integer numbers
Lemma ZL0 : 2%
nat = (1
+ 1)%
nat.
Properties of the addition on integers
Zero is left neutral for addition
Zero is right neutral for addition
Opposite distributes over addition
Opposite is inverse for addition
Associativity mixed with commutativity
Addition and successor permutes
Misc properties, usually redundant or non natural
Properties of successor and predecessor on binary integer numbers
Successor and predecessor are inverse functions
Properties of the direct definition of successor and predecessor
Misc properties, usually redundant or non natural
Properties of subtraction on binary integer numbers
Relating minus with plus and Zsucc
Lemma Zminus_plus_distr :
forall n m p:
Z,
n - (m + p) = n - m - p.
Lemma Zminus_succ_l :
forall n m:
Z,
Zsucc (
n - m)
= Zsucc n - m.
Lemma Zminus_succ_r :
forall n m:
Z,
n - (Zsucc m) = Zpred (
n - m).
Lemma Zplus_minus_eq :
forall n m p:
Z,
n = m + p ->
p = n - m.
Lemma Zminus_plus :
forall n m:
Z,
n + m - n = m.
Lemma Zplus_minus :
forall n m:
Z,
n + (m - n) = m.
Lemma Zminus_plus_simpl_l :
forall n m p:
Z,
p + n - (p + m) = n - m.
Lemma Zminus_plus_simpl_l_reverse :
forall n m p:
Z,
n - m = p + n - (p + m).
Lemma Zminus_plus_simpl_r :
forall n m p:
Z,
n + p - (m + p) = n - m.
Lemma Zpos_minus_morphism :
forall a b:
positive,
Pcompare a b Eq = Lt ->
Zpos (
b-a)
= Zpos b - Zpos a.
Misc redundant properties
Properties of multiplication on binary integer numbers
One is neutral for multiplication
Zero property of multiplication
Commutativity of multiplication
Associativity of multiplication
Associativity mixed with commutativity
Multiplication and Doubling
Multiplication and Opposite
Distributivity of multiplication over addition
Distributivity of multiplication over subtraction
Simplification of multiplication for non-zero integers
Addition and multiplication by 2
Multiplication and successor
Misc redundant properties
Relating binary positive numbers and binary integers
Definition Zlt (
x y:
Z) :=
(x ?= y) = Lt.
Definition Zgt (
x y:
Z) :=
(x ?= y) = Gt.
Definition Zle (
x y:
Z) :=
(x ?= y) <> Gt.
Definition Zge (
x y:
Z) :=
(x ?= y) <> Lt.
Definition Zne (
x y:
Z) :=
x <> y.
Infix "<=" :=
Zle :
Z_scope.
Infix "<" :=
Zlt :
Z_scope.
Infix ">=" :=
Zge :
Z_scope.
Infix ">" :=
Zgt :
Z_scope.
Notation "x <= y <= z" := (
x <= y /\ y <= z) :
Z_scope.
Notation "x <= y < z" := (
x <= y /\ y < z) :
Z_scope.
Notation "x < y < z" := (
x < y /\ y < z) :
Z_scope.
Notation "x < y <= z" := (
x < y /\ y <= z) :
Z_scope.
Absolute value on integers