Library Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms
The interface ZSig.ZType implies the interface ZAxiomsSig
Module ZSig_ZAxioms (
Z:ZType) <:
ZAxiomsSig.
Delimit Scope IntScope with Int.
Open Local Scope IntScope.
Notation "[ x ]" := (
Z.to_Z x) :
IntScope.
Infix "==" :=
Z.eq (
at level 70) :
IntScope.
Notation "0" :=
Z.zero :
IntScope.
Infix "+" :=
Z.add :
IntScope.
Infix "-" :=
Z.sub :
IntScope.
Infix "*" :=
Z.mul :
IntScope.
Notation "- x" := (
Z.opp x) :
IntScope.
Hint Rewrite
Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ
Z.spec_mul Z.spec_opp Z.spec_of_Z :
Zspec.
Ltac zsimpl :=
unfold Z.eq in *;
autorewrite with Zspec.
Module Export NZOrdAxiomsMod <:
NZOrdAxiomsSig.
Module Export NZAxiomsMod <:
NZAxiomsSig.
Definition NZ :=
Z.t.
Definition NZeq :=
Z.eq.
Definition NZ0 :=
Z.zero.
Definition NZsucc :=
Z.succ.
Definition NZpred :=
Z.pred.
Definition NZadd :=
Z.add.
Definition NZsub :=
Z.sub.
Definition NZmul :=
Z.mul.
Theorem NZeq_equiv :
equiv Z.t Z.eq.
Add Relation Z.t Z.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 Z.eq ==>
Z.eq as NZsucc_wd.
Add Morphism NZpred with signature Z.eq ==>
Z.eq as NZpred_wd.
Add Morphism NZadd with signature Z.eq ==>
Z.eq ==>
Z.eq as NZadd_wd.
Add Morphism NZsub with signature Z.eq ==>
Z.eq ==>
Z.eq as NZsub_wd.
Add Morphism NZmul with signature Z.eq ==>
Z.eq ==>
Z.eq as NZmul_wd.
Theorem NZpred_succ :
forall n,
Z.pred (
Z.succ n) ==
n.
Section Induction.
Variable A :
Z.t ->
Prop.
Hypothesis A_wd :
predicate_wd Z.eq A.
Hypothesis A0 :
A 0.
Hypothesis AS :
forall n,
A n <->
A (
Z.succ n).
Add Morphism A with signature Z.eq ==>
iff as A_morph.
Let B (
z :
Z) :=
A (
Z.of_Z z).
Lemma B0 :
B 0.
Lemma BS :
forall z :
Z,
B z ->
B (
z + 1).
Lemma BP :
forall z :
Z,
B z ->
B (
z - 1).
Lemma B_holds :
forall 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, (
Z.succ n) +
m ==
Z.succ (
n +
m).
Theorem NZsub_0_r :
forall n,
n - 0 ==
n.
Theorem NZsub_succ_r :
forall n m,
n - (
Z.succ m) ==
Z.pred (
n -
m).
Theorem NZmul_0_l :
forall n, 0 *
n == 0.
Theorem NZmul_succ_l :
forall n m, (
Z.succ n) *
m ==
n *
m +
m.
End NZAxiomsMod.
Definition NZlt :=
Z.lt.
Definition NZle :=
Z.le.
Definition NZmin :=
Z.min.
Definition NZmax :=
Z.max.
Infix "<=" :=
Z.le :
IntScope.
Infix "<" :=
Z.lt :
IntScope.
Lemma spec_compare_alt :
forall x y,
Z.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, [
Z.min x y] =
Zmin [
x] [
y].
Lemma spec_max :
forall x y, [
Z.max x y] =
Zmax [
x] [
y].
Add Morphism Z.compare with signature Z.eq ==>
Z.eq ==> (@
eq comparison)
as compare_wd.
Add Morphism Z.lt with signature Z.eq ==>
Z.eq ==>
iff as NZlt_wd.
Add Morphism Z.le with signature Z.eq ==>
Z.eq ==>
iff as NZle_wd.
Add Morphism Z.min with signature Z.eq ==>
Z.eq ==>
Z.eq as NZmin_wd.
Add Morphism Z.max with signature Z.eq ==>
Z.eq ==>
Z.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 < (
Z.succ m) <->
n <=
m.
Theorem NZmin_l :
forall n m,
n <=
m ->
Z.min n m ==
n.
Theorem NZmin_r :
forall n m,
m <=
n ->
Z.min n m ==
m.
Theorem NZmax_l :
forall n m,
m <=
n ->
Z.max n m ==
n.
Theorem NZmax_r :
forall n m,
n <=
m ->
Z.max n m ==
m.
End NZOrdAxiomsMod.
Definition Zopp :=
Z.opp.
Add Morphism Z.opp with signature Z.eq ==>
Z.eq as Zopp_wd.
Theorem Zsucc_pred :
forall n,
Z.succ (
Z.pred n) ==
n.
Theorem Zopp_0 : - 0 == 0.
Theorem Zopp_succ :
forall n, - (
Z.succ n) ==
Z.pred (-
n).
End ZSig_ZAxioms.