aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/RelationPairs.v
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-30 22:59:32 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-30 22:59:32 +0000
commita7273c7bb21305b2f6fb50908b88303a5a744891 (patch)
tree6e2dd00bc10eb076487f641b8980cb96e8b87195 /theories/Classes/RelationPairs.v
parent93a5f1e03e29e375be69a2361ffd6323f5300f86 (diff)
Fix backtracking heuristic in typeclass resolution.
Now that backtracking is working correctly, we need to avoid a non-termination issue introduced by the [RelCompFun] definition in RelationPairs, by adding a [Measure] typeclass. It could be used to have a uniform notation for measures/interpretations in Numbers and be but in the interfaces too, only the mimimal change was implemented. Fix syntax change in test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12547 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/RelationPairs.v')
-rw-r--r--theories/Classes/RelationPairs.v53
1 files changed, 32 insertions, 21 deletions
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index ecc8ecb79..7ae221d44 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -21,9 +21,6 @@ Implicit Arguments pair [[A] [B]].
(* /NB *)
-
-(* NB: is signature_scope the right one for that ? *)
-
Arguments Scope relation_conjunction
[type_scope signature_scope signature_scope].
Arguments Scope relation_equivalence
@@ -37,7 +34,7 @@ Arguments Scope PER [type_scope signature_scope].
Arguments Scope Equivalence [type_scope signature_scope].
Arguments Scope StrictOrder [type_scope signature_scope].
-Generalizable Variables A B RA RB Ri Ro.
+Generalizable Variables A B RA RB Ri Ro f.
(** Any function from [A] to [B] allow to obtain a relation over [A]
out of a relation over [B]. *)
@@ -47,6 +44,16 @@ Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A :=
Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope.
+(** We declare measures to the system using the [Measure] class.
+ Otherwise the instances would easily introduce loops,
+ never instantiating the [f] function. *)
+
+Class Measure {A B} (f : A -> B).
+
+(** Standard measures. *)
+
+Instance fst_measure : @Measure (A * B) A fst.
+Instance snd_measure : @Measure (A * B) B snd.
(** We define a product relation over [A*B]: each components should
satisfy the corresponding initial relation. *)
@@ -56,28 +63,32 @@ Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A*B) :=
Infix "*" := RelProd : signature_scope.
+Section RelCompFun_Instances.
+ Context {A B : Type} (R : relation B).
-Instance RelCompFun_Reflexive {A B}(R:relation B)(f:A->B)
- `(Reflexive _ R) : Reflexive (R@@f).
-Proof. firstorder. Qed.
+ Global Instance RelCompFun_Reflexive
+ `(Measure A B f, Reflexive _ R) : Reflexive (R@@f).
+ Proof. firstorder. Qed.
+
+ Global Instance RelCompFun_Symmetric
+ `(Measure A B f, Symmetric _ R) : Symmetric (R@@f).
+ Proof. firstorder. Qed.
+
+ Global Instance RelCompFun_Transitive
+ `(Measure A B f, Transitive _ R) : Transitive (R@@f).
+ Proof. firstorder. Qed.
-Instance RelCompFun_Symmetric {A B}(R:relation B)(f:A->B)
- `(Symmetric _ R) : Symmetric (R@@f).
-Proof. firstorder. Qed.
+ Global Instance RelCompFun_Irreflexive
+ `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
+ Proof. firstorder. Qed.
-Instance RelCompFun_Transitive {A B}(R:relation B)(f:A->B)
- `(Transitive _ R) : Transitive (R@@f).
-Proof. firstorder. Qed.
-
-Instance RelCompFun_Irreflexive {A B}(R:relation B)(f:A->B)
- `(Irreflexive _ R) : Irreflexive (R@@f).
-Proof. firstorder. Qed.
+ Global Instance RelCompFun_Equivalence
+ `(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
-Instance RelCompFun_Equivalence {A B}(R:relation B)(f:A->B)
- `(Equivalence _ R) : Equivalence (R@@f).
+ Global Instance RelCompFun_StrictOrder
+ `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
-Instance RelCompFun_StrictOrder {A B}(R:relation B)(f:A->B)
- `(StrictOrder _ R) : StrictOrder (R@@f).
+End RelCompFun_Instances.
Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B)
`(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB).