Library Stdlib.Numbers.Natural.Abstract.NDefOps



From Stdlib Require Import Bool. From Stdlib Require Import RelationPairs.
From Stdlib 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.