Library Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms



Require Import ZArith.
Require Import ZAxioms.
Require Import ZSig.

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.