Library Coq.Numbers.Natural.Peano.NPeano
Require Import Arith.
Require Import Min.
Require Import Max.
Require Import NSub.
Module NPeanoAxiomsMod <:
NAxiomsSig.
Module Export NZOrdAxiomsMod <:
NZOrdAxiomsSig.
Module Export NZAxiomsMod <:
NZAxiomsSig.
Definition NZ :=
nat.
Definition NZeq := (@
eq nat).
Definition NZ0 := 0.
Definition NZsucc :=
S.
Definition NZpred :=
pred.
Definition NZadd :=
plus.
Definition NZsub :=
minus.
Definition NZmul :=
mult.
Theorem NZeq_equiv :
equiv nat NZeq.
Add Relation nat NZeq
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 NZeq ==>
NZeq as NZsucc_wd.
Add Morphism NZpred with signature NZeq ==>
NZeq as NZpred_wd.
Add Morphism NZadd with signature NZeq ==>
NZeq ==>
NZeq as NZadd_wd.
Add Morphism NZsub with signature NZeq ==>
NZeq ==>
NZeq as NZsub_wd.
Add Morphism NZmul with signature NZeq ==>
NZeq ==>
NZeq as NZmul_wd.
Theorem NZinduction :
forall A :
nat ->
Prop,
predicate_wd (@
eq nat)
A ->
A 0 -> (
forall n :
nat,
A n <->
A (
S n)) ->
forall n :
nat,
A n.
Theorem NZpred_succ :
forall n :
nat,
pred (
S n) =
n.
Theorem NZadd_0_l :
forall n :
nat, 0 +
n =
n.
Theorem NZadd_succ_l :
forall n m :
nat, (
S n) +
m =
S (
n +
m).
Theorem NZsub_0_r :
forall n :
nat,
n - 0 =
n.
Theorem NZsub_succ_r :
forall n m :
nat,
n - (
S m) =
pred (
n -
m).
Theorem NZmul_0_l :
forall n :
nat, 0 *
n = 0.
Theorem NZmul_succ_l :
forall n m :
nat,
S n *
m =
n *
m +
m.
End NZAxiomsMod.
Definition NZlt :=
lt.
Definition NZle :=
le.
Definition NZmin :=
min.
Definition NZmax :=
max.
Add Morphism NZlt with signature NZeq ==>
NZeq ==>
iff as NZlt_wd.
Add Morphism NZle with signature NZeq ==>
NZeq ==>
iff as NZle_wd.
Add Morphism NZmin with signature NZeq ==>
NZeq ==>
NZeq as NZmin_wd.
Add Morphism NZmax with signature NZeq ==>
NZeq ==>
NZeq as NZmax_wd.
Theorem NZlt_eq_cases :
forall n m :
nat,
n <=
m <->
n <
m \/
n =
m.
Theorem NZlt_irrefl :
forall n :
nat, ~ (
n <
n).
Theorem NZlt_succ_r :
forall n m :
nat,
n <
S m <->
n <=
m.
Theorem NZmin_l :
forall n m :
nat,
n <=
m ->
NZmin n m =
n.
Theorem NZmin_r :
forall n m :
nat,
m <=
n ->
NZmin n m =
m.
Theorem NZmax_l :
forall n m :
nat,
m <=
n ->
NZmax n m =
n.
Theorem NZmax_r :
forall n m :
nat,
n <=
m ->
NZmax n m =
m.
End NZOrdAxiomsMod.
Definition recursion :
forall A :
Type,
A -> (
nat ->
A ->
A) ->
nat ->
A :=
fun A :
Type =>
nat_rect (
fun _ =>
A).
Implicit Arguments recursion [
A].
Theorem succ_neq_0 :
forall n :
nat,
S n <> 0.
Theorem pred_0 :
pred 0 = 0.
Theorem recursion_wd :
forall (
A :
Type) (
Aeq :
relation A),
forall a a' :
A,
Aeq a a' ->
forall f f' :
nat ->
A ->
A,
fun2_eq (@
eq nat)
Aeq Aeq f f' ->
forall n n' :
nat,
n =
n' ->
Aeq (
recursion a f n) (
recursion a' f' n').
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 ->
fun2_wd (@
eq nat)
Aeq Aeq f ->
forall n :
nat,
Aeq (
recursion a f (
S n)) (
f n (
recursion a f n)).
End NPeanoAxiomsMod.
Module Export NPeanoSubPropMod :=
NSubPropFunct NPeanoAxiomsMod.