Library Coq.Numbers.Natural.Abstract.NDefOps
Addition
Multiplication
Order
Even
Division by 2
Local Notation "a <= b <= c" := (
a<=b /\ b<=c).
Local Notation "a <= b < c" := (
a<=b /\ b<c).
Local Notation "a < b <= c" := (
a<b /\ b<=c).
Local Notation "a < b < c" := (
a<b /\ b<c).
Local Notation "2" := (
S 1).
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
Later:
Theorem log_mul : forall n m, 0 < n -> 0 < m ->
log (n*m) == log n + log m.
Theorem log_pow2 : forall n, log (2^^n) = n.