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