Library Coq.Numbers.Natural.Abstract.NDefOps



Require Import Bool. Require Import RelationPairs.
Require Export NStrongRec.

In this module, we derive generic implementations of usual operators just via the use of a recursion function.

Module NdefOpsProp (Import N : NAxiomsRecSig').
Include NStrongRecProp N.

Nullity Test

Definition if_zero (A : Type) (a b : A) (n : N.t) : A :=
  recursion a (fun _ _ => b) n.

Arguments if_zero [A] a b n.

#[global]
Instance if_zero_wd (A : Type) :
 Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A).

Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a.

Theorem if_zero_succ :
 forall (A : Type) (a b : A) (n : N.t), if_zero a b (S n) = b.

Addition

Definition def_add (x y : N.t) := recursion y (fun _ => S) x.

Local Infix "+++" := def_add (at level 50, left associativity).

#[global]
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).

#[global]
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).

#[global]
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.

#[global]
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

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).

#[global]
Instance half_aux_wd : Proper (N.eq ==> N.eq*N.eq) half_aux.

#[global]
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).

#[global]
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.

#[global]
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))).

#[global]
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))).
#[global]
Hint Resolve log_good_step : core.

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.

End NdefOpsProp.