Library Coq.Numbers.Natural.SpecViaZ.NSigNAxioms
Module NSig_NAxioms (N:NType) <: NAxiomsSig.
Delimit Scope IntScope with Int.
Open Local Scope IntScope.
Notation "[ x ]" := (N.to_Z x) : IntScope.
Infix "==" := N.eq (at level 70) : IntScope.
Notation "0" := N.zero : IntScope.
Infix "+" := N.add : IntScope.
Infix "-" := N.sub : IntScope.
Infix "*" := N.mul : IntScope.
Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
Module Export NZAxiomsMod <: NZAxiomsSig.
Definition NZ := N.t.
Definition NZeq := N.eq.
Definition NZ0 := N.zero.
Definition NZsucc := N.succ.
Definition NZpred := N.pred.
Definition NZadd := N.add.
Definition NZsub := N.sub.
Definition NZmul := N.mul.
Theorem NZeq_equiv : equiv N.t N.eq.
Add Relation N.t N.eq
reflexivity proved by (proj1 NZeq_equiv)
symmetry proved by (proj2 (proj2 NZeq_equiv))
transitivity proved by (proj1 (proj2 NZeq_equiv))
as NZeq_rel.
Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd.
Add Morphism NZpred with signature N.eq ==> N.eq as NZpred_wd.
Add Morphism NZadd with signature N.eq ==> N.eq ==> N.eq as NZadd_wd.
Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd.
Add Morphism NZmul with signature N.eq ==> N.eq ==> N.eq as NZmul_wd.
Theorem NZpred_succ : forall n, N.pred (N.succ n) == n.
Definition N_of_Z z := N.of_N (Zabs_N z).
Section Induction.
Variable A : N.t -> Prop.
Hypothesis A_wd : predicate_wd N.eq A.
Hypothesis A0 : A 0.
Hypothesis AS : forall n, A n <-> A (N.succ n).
Add Morphism A with signature N.eq ==> iff as A_morph.
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 NZinduction : forall n, A n.
End Induction.
Theorem NZadd_0_l : forall n, 0 + n == n.
Theorem NZadd_succ_l : forall n m, (N.succ n) + m == N.succ (n + m).
Theorem NZsub_0_r : forall n, n - 0 == n.
Theorem NZsub_succ_r : forall n m, n - (N.succ m) == N.pred (n - m).
Theorem NZmul_0_l : forall n, 0 * n == 0.
Theorem NZmul_succ_l : forall n m, (N.succ n) * m == n * m + m.
End NZAxiomsMod.
Definition NZlt := N.lt.
Definition NZle := N.le.
Definition NZmin := N.min.
Definition NZmax := N.max.
Infix "<=" := N.le : IntScope.
Infix "<" := N.lt : IntScope.
Lemma spec_compare_alt : forall x y, N.compare x y = ([x] ?= [y])%Z.
Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z.
Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z.
Lemma spec_min : forall x y, [N.min x y] = Zmin [x] [y].
Lemma spec_max : forall x y, [N.max x y] = Zmax [x] [y].
Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd.
Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd.
Add Morphism N.le with signature N.eq ==> N.eq ==> iff as NZle_wd.
Add Morphism N.min with signature N.eq ==> N.eq ==> N.eq as NZmin_wd.
Add Morphism N.max with signature N.eq ==> N.eq ==> N.eq as NZmax_wd.
Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
Theorem NZlt_irrefl : forall n, ~ n < n.
Theorem NZlt_succ_r : forall n m, n < (N.succ m) <-> n <= m.
Theorem NZmin_l : forall n m, n <= m -> N.min n m == n.
Theorem NZmin_r : forall n m, m <= n -> N.min n m == m.
Theorem NZmax_l : forall n m, m <= n -> N.max n m == n.
Theorem NZmax_r : forall n m, n <= m -> N.max n m == m.
End NZOrdAxiomsMod.
Theorem pred_0 : N.pred 0 == 0.
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].
Theorem recursion_wd :
forall (A : Type) (Aeq : relation A),
forall a a' : A, Aeq a a' ->
forall f f' : N.t -> A -> A, fun2_eq N.eq Aeq Aeq f f' ->
forall x x' : N.t, x == x' ->
Aeq (recursion a f x) (recursion a' f' x').
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 -> fun2_wd N.eq Aeq Aeq f ->
forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)).
End NSig_NAxioms.