Library Coq.Numbers.Natural.Peano.NPeano



Require Import Arith MinMax NAxioms NProperties.

Implementation of NAxiomsSig by nat


Module NPeanoAxiomsMod <: NAxiomsSig.

Bi-directional induction.

Theorem bi_induction :
  forall A : nat -> Prop, Proper (eq==>iff) A ->
    A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.

Basic operations.

Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
Program Instance succ_wd : Proper (eq==>eq) S.
Program Instance pred_wd : Proper (eq==>eq) pred.
Program Instance add_wd : Proper (eq==>eq==>eq) plus.
Program Instance sub_wd : Proper (eq==>eq==>eq) minus.
Program Instance mul_wd : Proper (eq==>eq==>eq) mult.

Theorem pred_succ : forall n : nat, pred (S n) = n.

Theorem add_0_l : forall n : nat, 0 + n = n.

Theorem add_succ_l : forall n m : nat, (S n) + m = S (n + m).

Theorem sub_0_r : forall n : nat, n - 0 = n.

Theorem sub_succ_r : forall n m : nat, n - (S m) = pred (n - m).

Theorem mul_0_l : forall n : nat, 0 * n = 0.

Theorem mul_succ_l : forall n m : nat, S n * m = n * m + m.

Order on natural numbers

Program Instance lt_wd : Proper (eq==>eq==>iff) lt.

Theorem lt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m.

Theorem lt_irrefl : forall n : nat, ~ (n < n).

Theorem lt_succ_r : forall n m : nat, n < S m <-> n <= m.

Theorem min_l : forall n m : nat, n <= m -> min n m = n.

Theorem min_r : forall n m : nat, m <= n -> min n m = m.

Theorem max_l : forall n m : nat, m <= n -> max n m = n.

Theorem max_r : forall n m : nat, n <= m -> max n m = m.

Facts specific to natural numbers, not integers.

Theorem pred_0 : pred 0 = 0.

Definition recursion (A : Type) : A -> (nat -> A -> A) -> nat -> A :=
  nat_rect (fun _ => A).
Implicit Arguments recursion [A].

Instance recursion_wd (A : Type) (Aeq : relation A) :
 Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).

Theorem recursion_0 :
  forall (A : Type) (a : A) (f : nat -> A -> A), recursion a f 0 = a.

Theorem recursion_succ :
  forall (A : Type) (Aeq : relation A) (a : A) (f : nat -> A -> A),
    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
      forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).

The instantiation of operations. Placing them at the very end avoids having indirections in above lemmas.

Definition t := nat.
Definition eq := @eq nat.
Definition zero := 0.
Definition succ := S.
Definition pred := pred.
Definition add := plus.
Definition sub := minus.
Definition mul := mult.
Definition lt := lt.
Definition le := le.
Definition min := min.
Definition max := max.

End NPeanoAxiomsMod.

Now we apply the largest property functor

Module Export NPeanoPropMod := NPropFunct NPeanoAxiomsMod.

Euclidean Division

Definition divF div x y := if leb y x then S (div (x-y) y) else 0.
Definition modF mod x y := if leb y x then mod (x-y) y else x.
Definition initF (_ _ : nat) := 0.

Fixpoint loop {A} (F:A->A)(i:A) (n:nat) : A :=
 match n with
  | 0 => i
  | S n => F (loop F i n)
 end.

Definition div x y := loop divF initF x x y.
Definition modulo x y := loop modF initF x x y.
Infix "/" := div : nat_scope.
Infix "mod" := modulo (at level 40, no associativity) : nat_scope.

Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y.

Lemma mod_upper_bound : forall x y, y<>0 -> x mod y < y.

Require Import NDiv.

Module NDivMod <: NDivSig.
 Include NPeanoAxiomsMod.
 Definition div := div.
 Definition modulo := modulo.
 Definition div_mod := div_mod.
 Definition mod_upper_bound := mod_upper_bound.
 Local Obligation Tactic := simpl_relation.
 Program Instance div_wd : Proper (eq==>eq==>eq) div.
 Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
End NDivMod.

Module Export NDivPropMod := NDivPropFunct NDivMod NPeanoPropMod.