# Library Coq.Numbers.Natural.Abstract.NDefOps

Require Import Bool. Require Import RelationPairs.
Require Export NStrongRec.
Module NdefOpsPropFunct (Import N : NAxiomsSig').
Include NStrongRecPropFunct N.
Addition
Definition def_add (x y : N.t) := recursion y (fun _ => S) x.
Local Infix "+++" := def_add (at level 50, left associativity).
Instance def_add_prewd : Proper (N.eq ==> N.eq ==> N.eq) (fun _ => S).
Instance def_add_wd : Proper (N.eq ==> N.eq ==> N.eq) def_add.
Theorem def_add_0_l : forall y, 0 +++ y == y.
Theorem def_add_succ_l : forall x y, S x +++ y == S (x +++ y).
Theorem def_add_add : forall n m, n +++ m == n + m.
Multiplication
Definition def_mul (x y : N.t) := recursion 0 (fun _ p => p +++ x) y.
Local Infix "**" := def_mul (at level 40, left associativity).
Instance def_mul_prewd :
Proper (N.eq ==> N.eq ==> N.eq ==> N.eq) (fun x _ p => p +++ x).
Instance def_mul_wd : Proper (N.eq ==> N.eq ==> N.eq) def_mul.
Theorem def_mul_0_r : forall x, x ** 0 == 0.
Theorem def_mul_succ_r : forall x y, x ** S y == x ** y +++ x.
Theorem def_mul_mul : forall n m, n ** m == n * m.
Order
Definition ltb (m : N.t) : N.t -> bool :=
recursion
(if_zero false true)
(fun _ f n => recursion false (fun n' _ => f n') n)
m.
Local Infix "<<" := ltb (at level 70, no associativity).
Instance ltb_prewd1 : Proper (N.eq ==> Logic.eq) (if_zero false true).
Instance ltb_prewd2 : Proper (N.eq ==>( N.eq ==> Logic.eq )==> N.eq ==> Logic.eq)
(fun _ f n => recursion false (fun n' _ => f n') n).
Instance ltb_wd : Proper (N.eq ==> N.eq ==> Logic.eq) ltb.
Theorem ltb_base : forall n, 0 << n = if_zero false true n.
Theorem ltb_step :
forall m n, S m << n = recursion false (fun n' _ => m << n') n.
Theorem ltb_0 : forall n, n << 0 = false.
Theorem ltb_0_succ : forall n, 0 << S n = true.
Theorem succ_ltb_mono : forall n m, ( S n << S m ) = ( n << m ).
Theorem ltb_lt : forall n m, n << m = true <-> n < m.
Theorem ltb_ge : forall n m, n << m = false <-> n >= m.
Even
Definition even (x : N.t) := recursion true (fun _ p => negb p) x.
Instance even_wd : Proper (N.eq ==> Logic.eq) even.
Theorem even_0 : even 0 = true.
Theorem even_succ : forall x, even (S x) = negb (even x).
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
Definition pow (n m : N.t) := recursion 1 (fun _ r => n * r) m.
Local Infix "^^" := pow (at level 30, right associativity).
Instance pow_prewd :
Proper (N.eq ==> N.eq ==> N.eq ==> N.eq) (fun n _ r => n * r).
Instance pow_wd : Proper (N.eq ==> N.eq ==> N.eq) pow.
Lemma pow_0 : forall n, n ^^0 == 1.
Lemma pow_succ : forall n m, n ^^( S m ) == n *( n ^^ m ).
Logarithm for the base 2
Definition log (x : N.t) : N.t :=
strong_rec 0
(fun g x =>
if x << 2 then 0
else S (g (half x)))
x.
Instance log_prewd :
Proper (( N.eq ==> N.eq )==> N.eq ==> N.eq)
(fun g x => if x <<2 then 0 else S (g (half x))).
Instance log_wd : Proper (N.eq ==> N.eq) log.
Lemma log_good_step : forall n h1 h2,
(forall m, m < n -> h1 m == h2 m) ->
( if n << 2 then 0 else S (h1 (half n))) ==
( if n << 2 then 0 else S (h2 (half n))).
Hint Resolve log_good_step.
Theorem log_init : forall n, n < 2 -> log n == 0.
Theorem log_step : forall n, 2 <= n -> log n == S (log (half n)).
Theorem pow2_log : forall n, 0 < n -> half n < 2^^( log n ) <= n.
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.
End NdefOpsPropFunct.