1 files changed, 69 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
new file mode 100644
index 00000000..15beb2b9
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i $Id: ZDomain.v 10934 2008-05-15 21:58:20Z letouzey $ i*)
+
+Require Export NumPrelude.
+
+Module Type ZDomainSignature.
+
+Parameter Inline Z : Set.
+Parameter Inline Zeq : Z -> Z -> Prop.
+Parameter Inline e : Z -> Z -> bool.
+
+Axiom eq_equiv_e : forall x y : Z, Zeq x y <-> e x y.
+Axiom eq_equiv : equiv Z Zeq.
+
+Add Relation Z Zeq
+ reflexivity proved by (proj1 eq_equiv)
+ symmetry proved by (proj2 (proj2 eq_equiv))
+ transitivity proved by (proj1 (proj2 eq_equiv))
+as eq_rel.
+
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.
+Notation "x == y" := (Zeq x y) (at level 70) : IntScope.
+Notation "x # y" := (~ Zeq x y) (at level 70) : IntScope.
+
+End ZDomainSignature.
+
+Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
+Open Local Scope IntScope.
+
+Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
+Proof.
+intros x x' Exx' y y' Eyy'.
+case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
+assert (x == y); [apply <- eq_equiv_e; now rewrite H2 |
+assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
+rewrite <- H1; assert (H3 : e x' y'); [now apply -> eq_equiv_e | now inversion H3]]].
+assert (x' == y'); [apply <- eq_equiv_e; now rewrite H1 |
+assert (x == y); [rewrite Exx'; now rewrite Eyy' |
+rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]].
+Qed.
+
+Theorem neq_symm : forall n m, n # m -> m # n.
+Proof.
+intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
+Qed.
+
+Theorem ZE_stepl : forall x y z : Z, x == y -> x == z -> z == y.
+Proof.
+intros x y z H1 H2; now rewrite <- H1.
+Qed.
+
+Declare Left Step ZE_stepl.
+
+(* The right step lemma is just transitivity of Zeq *)
+Declare Right Step (proj1 (proj2 eq_equiv)).
+
+End ZDomainProperties.
+
+