Library Coq.Numbers.Natural.SpecViaZ.NSigNAxioms
The interface NSig.NType implies the interface NAxiomsSig
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.