# Library Coq.Numbers.Natural.SpecViaZ.NSigNAxioms

Require Import ZArith Nnat NAxioms NDiv NSig.

# The interface NSig.NType implies the interface NAxiomsSig

Module NTypeIsNAxioms (Import N : NType').
Hint Rewrite
spec_0 spec_succ spec_add spec_mul spec_pred spec_sub
spec_div spec_modulo spec_gcd spec_compare spec_eq_bool
spec_max spec_min spec_power_pos spec_power
: nsimpl.
Ltac nsimpl := autorewrite with nsimpl.
Ltac ncongruence := unfold eq; repeat red; intros; nsimpl; congruence.
Ltac zify := unfold eq, lt, le in *; nsimpl.
Local Obligation Tactic := ncongruence.
Instance eq_equiv : Equivalence eq.
Program Instance succ_wd : Proper (eq ==> eq) succ.
Program Instance pred_wd : Proper (eq ==> eq) pred.
Program Instance add_wd : Proper (eq ==> eq ==> eq) add.
Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
Theorem pred_succ : forall n, pred (succ n) == n.
Definition N_of_Z z := of_N (Zabs_N z).
Section Induction.
Variable A : N.t -> Prop.
Hypothesis A_wd : Proper (eq ==> iff) A.
Hypothesis A0 : A 0.
Hypothesis AS : forall n, A n <-> A (succ n).
Let B (z : Z) := A (N_of_Z z).
Lemma B0 : B 0.
Lemma BS : forall z : Z, (0 <= z)%Z -> B z -> B (z + 1).
Lemma B_holds : forall z : Z, (0 <= z)%Z -> B z.
Theorem bi_induction : forall n, A n.
End Induction.
Theorem add_0_l : forall n, 0 + n == n.
Theorem add_succ_l : forall n m, ( succ n ) + m == succ (n + m).
Theorem sub_0_r : forall n, n - 0 == n.
Theorem sub_succ_r : forall n m, n - ( succ m ) == pred (n - m).
Theorem mul_0_l : forall n, 0 * n == 0.
Theorem mul_succ_l : forall n m, ( succ n ) * m == n * m + m.
Order
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
Definition eqb := eq_bool.
Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
Theorem lt_irrefl : forall n, ~ n < n.
Theorem lt_succ_r : forall n m, n < ( succ m ) <-> n <= m.
Theorem min_l : forall n m, n <= m -> min n m == n.
Theorem min_r : forall n m, m <= n -> min n m == m.
Theorem max_l : forall n m, m <= n -> max n m == n.
Theorem max_r : forall n m, n <= m -> max n m == m.
Properties specific to natural numbers, not integers.
Theorem pred_0 : pred 0 == 0.
Program Instance div_wd : Proper (eq ==> eq ==> eq) div.
Program Instance mod_wd : Proper (eq ==> eq ==> eq) modulo.
Theorem div_mod : forall a b, ~ b ==0 -> a == b *( div a b ) + ( modulo a b ).
Theorem mod_upper_bound : forall a b, ~ b ==0 -> modulo a b < b.
Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=
Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n).
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 : N.t -> A -> A), recursion a f 0 = a.
Theorem recursion_succ :
forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A),
Aeq a a -> Proper (eq ==> Aeq ==> Aeq) f ->
forall n, Aeq (recursion a f (succ n)) (f n (recursion a f n)).
End NTypeIsNAxioms.
Module NType_NAxioms (N : NType)
<: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N <: HasMinMax N
:= N <+ NTypeIsNAxioms.