diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 1 |
4 files changed, 5 insertions, 0 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index b99df747a..da33059c9 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -61,6 +61,7 @@ Ltac wsimpl := unfold eq, zero, succ, pred, add, sub, mul; autorewrite with w. Ltac wcongruence := repeat red; intros; wsimpl; congruence. +Instance znz_measure: Measure w_op.(znz_to_Z). Instance eq_equiv : Equivalence eq. Instance succ_wd : Proper (eq ==> eq) succ. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index d3f4776a6..410af329d 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -36,6 +36,7 @@ Hint Rewrite Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec. Ltac zcongruence := repeat red; intros; zsimpl; congruence. +Instance Z_measure: @Measure Z.t Z Z.to_Z. Instance eq_equiv : Equivalence Z.eq. Obligation Tactic := zcongruence. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 49e7d7256..aa291cfdc 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -34,6 +34,8 @@ Ltac ncongruence := unfold N.eq; repeat red; intros; nsimpl; congruence. Obligation Tactic := ncongruence. +Instance: @Measure N.t Z N.to_Z. + Instance eq_equiv : Equivalence N.eq. Program Instance succ_wd : Proper (N.eq==>N.eq) N.succ. diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index d0cf499ab..14646fa84 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -94,6 +94,7 @@ Local Open Scope bigQ_scope. (** [BigQ] is a setoid *) +Instance bigQ_measure: RelationPairs.Measure BigQ.to_Q. Instance BigQeq_rel : Equivalence BigQ.eq. Instance BigQadd_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.add. |