Library Coq.NArith.BinNat
Binary natural numbers, operations and properties
The type
N and its constructors
N0 and
Npos are now
defined in
BinNums.v
Every definitions and properties about binary natural numbers
are placed in a module
N for qualification purpose.
Local Open Scope N_scope.
Every definitions and early properties about positive numbers
are placed in a module N for qualification purpose.
Definitions of operations, now in a separate file
When including property functors, only inline t eq zero one two
Logical predicates
Proofs of morphisms, obvious since eq is Leibniz
Decidability of equality.
Discrimination principle
Convenient induction principles
Peano induction on binary natural numbers
Generic induction / recursion
Specification of constants
Properties of mixed successor and predecessor.
Properties of successor and predecessor
Specification of addition
Specification of subtraction.
Specification of multiplication
Specification of boolean comparisons.
Basic properties of comparison
Some more advanced properties of comparison and orders,
including compare_spec and lt_irrefl and lt_eq_cases.
Specification of minimum and maximum
Specification of lt and le.
We can now derive all properties of basic functions and orders,
and use these properties for proving the specs of more advanced
functions.
Properties of double and succ_double
0 is the least natural number
Specifications of power
Specification of square
Specification of Base-2 logarithm
Specification of parity functions
Specification of the euclidean division
Specification of square root
Specification of gcd
The first component of ggcd is gcd
The other components of ggcd are indeed the correct factors.
We can use this fact to prove a part of the gcd correctness
We now prove directly that gcd is the greatest amongst common divisors
Specification of bitwise functions
Correctness proofs for
testbit.
Correctness proofs for shifts
Semantics of bitwise operations
Instantiation of generic properties of advanced functions
(pow, sqrt, log2, div, gcd, ...)
In generic statements, the predicates lt and le have been
favored, whereas gt and ge don't even exist in the abstract
layers. The use of gt and ge is hence not recommended. We provide
here the bare minimal results to related them with lt and le.
Auxiliary results about right shift on positive numbers,
used in BinInt
Lemma iter_swap_gen :
forall A B (
f:
A -> B) (
g:
A -> A) (
h:
B -> B),
(forall a,
f (
g a)
= h (
f a)
) -> forall n a,
f (
iter n g a)
= iter n h (
f a).
Theorem iter_swap :
forall n (
A:
Type) (
f:
A -> A) (
x:
A),
iter n f (
f x)
= f (
iter n f x).
Theorem iter_succ :
forall n (
A:
Type) (
f:
A -> A) (
x:
A),
iter (
succ n)
f x = f (
iter n f x).
Theorem iter_succ_r :
forall n (
A:
Type) (
f:
A -> A) (
x:
A),
iter (
succ n)
f x = iter n f (
f x).
Theorem iter_add :
forall p q (
A:
Type) (
f:
A -> A) (
x:
A),
iter (
p+q)
f x = iter p f (
iter q f x).
Theorem iter_ind :
forall (
A:
Type) (
f:
A -> A) (
a:
A) (
P:
N -> A -> Prop),
P 0
a ->
(forall n a',
P n a' -> P (
succ n) (
f a')
) ->
forall n,
P n (
iter n f a).
Theorem iter_invariant :
forall (
n:
N) (
A:
Type) (
f:
A -> A) (
Inv:
A -> Prop),
(forall x:
A,
Inv x -> Inv (
f x)
) ->
forall x:
A,
Inv x -> Inv (
iter n f x).
End N.
Exportation of notations
Infix "+" :=
N.add :
N_scope.
Infix "-" :=
N.sub :
N_scope.
Infix "*" :=
N.mul :
N_scope.
Infix "^" :=
N.pow :
N_scope.
Infix "?=" :=
N.compare (
at level 70,
no associativity) :
N_scope.
Infix "<=" :=
N.le :
N_scope.
Infix "<" :=
N.lt :
N_scope.
Infix ">=" :=
N.ge :
N_scope.
Infix ">" :=
N.gt :
N_scope.
Notation "x <= y <= z" := (
x <= y /\ y <= z) :
N_scope.
Notation "x <= y < z" := (
x <= y /\ y < z) :
N_scope.
Notation "x < y < z" := (
x < y /\ y < z) :
N_scope.
Notation "x < y <= z" := (
x < y /\ y <= z) :
N_scope.
Infix "=?" :=
N.eqb (
at level 70,
no associativity) :
N_scope.
Infix "<=?" :=
N.leb (
at level 70,
no associativity) :
N_scope.
Infix "<?" :=
N.ltb (
at level 70,
no associativity) :
N_scope.
Infix "/" :=
N.div :
N_scope.
Infix "mod" :=
N.modulo (
at level 40,
no associativity) :
N_scope.
Notation "( p | q )" := (
N.divide p q) (
at level 0) :
N_scope.
Compatibility notations
More complex compatibility facts, expressed as lemmas
(to preserve scopes for instance)
Not kept : Ncompare_n_Sm Nplus_lt_cancel_l