diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZDomain.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDomain.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v index 7ace860f3..3146b9c2c 100644 --- a/theories/Numbers/Integer/Abstract/ZDomain.v +++ b/theories/Numbers/Integer/Abstract/ZDomain.v @@ -3,13 +3,13 @@ Require Export NumPrelude. Module Type ZDomainSignature. Parameter Inline Z : Set. -Parameter Inline E : Z -> Z -> Prop. +Parameter Inline Zeq : Z -> Z -> Prop. Parameter Inline e : Z -> Z -> bool. -Axiom E_equiv_e : forall x y : Z, E x y <-> e x y. -Axiom E_equiv : equiv Z E. +Axiom E_equiv_e : forall x y : Z, Zeq x y <-> e x y. +Axiom E_equiv : equiv Z Zeq. -Add Relation Z E +Add Relation Z Zeq reflexivity proved by (proj1 E_equiv) symmetry proved by (proj2 (proj2 E_equiv)) transitivity proved by (proj1 (proj2 E_equiv)) @@ -17,15 +17,15 @@ as E_rel. Delimit Scope IntScope with Int. Bind Scope IntScope with Z. -Notation "x == y" := (E x y) (at level 70) : IntScope. -Notation "x # y" := (~ E x y) (at level 70) : IntScope. +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 E ==> E ==> eq_bool as e_wd. +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. @@ -49,7 +49,7 @@ Qed. Declare Left Step ZE_stepl. -(* The right step lemma is just transitivity of E *) +(* The right step lemma is just transitivity of Zeq *) Declare Right Step (proj1 (proj2 E_equiv)). End ZDomainProperties. |