Library Coq.Numbers.Natural.Abstract.NDefOps
In this module, we derive generic implementations of usual operators
just via the use of a recursion function.
Nullity Test
Addition
Multiplication
Order
Even
Division by 2
Definition half_aux (
x :
N.t) :
N.t * N.t :=
recursion (0
, 0
) (
fun _ p =>
let (
x1,
x2) :=
p in (S x2, x1))
x.
Definition half (
x :
N.t) :=
snd (
half_aux x).
Instance half_aux_wd :
Proper (
N.eq ==> N.eq*N.eq)
half_aux.
Instance half_wd :
Proper (
N.eq==>N.eq)
half.
Lemma half_aux_0 :
half_aux 0
= (0
,0
).
Lemma half_aux_succ :
forall x,
half_aux (
S x)
= (S (
snd (
half_aux x))
, fst (
half_aux x)
).
Theorem half_aux_spec :
forall n,
n == fst (
half_aux n)
+ snd (
half_aux n).
Theorem half_aux_spec2 :
forall n,
fst (
half_aux n)
== snd (
half_aux n)
\/
fst (
half_aux n)
== S (
snd (
half_aux n)).
Theorem half_0 :
half 0
== 0.
Theorem half_1 :
half 1
== 0.
Theorem half_double :
forall n,
n == 2
* half n \/ n == 1
+ 2
* half n.
Theorem half_upper_bound :
forall n, 2
* half n <= n.
Theorem half_lower_bound :
forall n,
n <= 1
+ 2
* half n.
Theorem half_nz :
forall n, 1
< n -> 0
< half n.
Theorem half_decrease :
forall n, 0
< n ->
half n < n.
Power
Logarithm for the base 2