Improve error handling and messages for typeclasses.

Add definitions of relational algebra in Classes/RelationClasses
including equivalence, inclusion, conjunction and disjunction. Add
PartialOrder class and show that we have a partial order on relations. 
Change SubRelation to subrelation for consistency with the standard
library. The caracterization of PartialOrder is a bit original: we
require an equivalence and a preorder so that the equivalence relation
is equivalent to the conjunction of the order relation and its
inverse. We can derive antisymmetry and appropriate morphism instances 
from this. Also add a fully general heterogeneous definition of
respectful from which we can build the non-dependent respectful
combinator.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10728 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 121 insertions, 42 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index b4b217e38c..4765bf0eea 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -30,12 +30,20 @@ Unset Strict Implicit.
 
 (** Respectful morphisms. *)
 
-Definition respectful_dep (A : Type) (R : relation A) 
-  (B : A -> Type) (R' : forall x y, B x -> B y -> Prop) : relation (forall x : A, B x) := 
-  fun f g => forall x y : A, R x y -> R' x y (f x) (g y).
+(** The fully dependent version, not used yet. *)
 
-Definition respectful A B (R : relation A) (R' : relation B) : relation (A -> B) :=
-  fun f g => forall x y : A, R x y -> R' (f x) (g y).
+Definition respectful_hetero 
+  (A B : Type) 
+  (C : A -> Type) (D : B -> Type) 
+  (R : A -> B -> Prop) 
+  (R' : forall (x : A) (y : B), C x -> D y -> Prop) : 
+    (forall x : A, C x) -> (forall x : B, D x) -> Prop := 
+    fun f g => forall x y, R x y -> R' x y (f x) (g y).
+
+(** The non-dependent version is an instance where we forget dependencies. *)
+
+Definition respectful (A B : Type) (R : relation A) (R' : relation B) : relation (A -> B) :=
+  Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
 
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
 
@@ -114,49 +122,32 @@ Implicit Arguments Morphism [A].
 
 Typeclasses unfold relation.
 
-(** Leibniz *)
-
-(* Instance Morphism (eq ++> eq ++> iff) (eq (A:=A)). *)
-(* Proof. intros ; constructor ; intros. *)
-(*   obligations_tactic. *)
-(*   subst. *)
-(*   intuition. *)
-(* Qed. *)
-
-(* Program Definition arrow_morphism `A B` (m : A -> B) : Morphism (eq ++> eq) m. *)
+(** Subrelations induce a morphism on the identity, not used for morphism search yet. *)
 
-(** Any morphism respecting some relations up to [iff] respects 
-   them up to [impl] in each way. Very important instances as we need [impl]
-   morphisms at the top level when we rewrite. *)
+Lemma subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id.
+Proof. firstorder. Qed.
 
-Class SubRelation A (R S : relation A) : Prop :=
-  subrelation :> Morphism (S ==> R) id.
+(** The subrelation property goes through products as usual. *)
 
-Instance iff_impl_subrelation : SubRelation Prop impl iff.
-Proof. reduce. tauto. Qed.
+Instance [ sub : subrelation A R₁ R₂ ] =>
+  morphisms_subrelation : ! subrelation (B -> A) (R ==> R₁) (R ==> R₂).
+Proof. firstorder. Qed.
 
-Instance iff_inverse_impl_subrelation : SubRelation Prop (inverse impl) iff.
-Proof.
-  reduce. tauto.
-Qed.
-
-Instance [ sub : SubRelation A R₁ R₂ ] =>
-  morphisms_subrelation : SubRelation (B -> A) (R ==> R₁) (R ==> R₂).
-Proof.
-  reduce. apply* sub. apply H. assumption.
-Qed.
+Instance [ sub : subrelation A R₂ R₁ ] =>
+  morphisms_subrelation_left : ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
+Proof. firstorder. Qed.
 
-Instance [ sub : SubRelation A R₂ R₁ ] =>
-  morphisms_subrelation_left : SubRelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
-Proof.
-  reduce. apply* H.  apply* sub. assumption.
-Qed.
+(** [Morphism] is itself a covariant morphism for [subrelation]. *)
 
-Lemma subrelation_morphism [ SubRelation A R₁ R₂, ! Morphism R₂ m ] : Morphism R₁ m.
+Lemma subrelation_morphism [ subrelation A R₁ R₂, ! Morphism R₁ m ] : Morphism R₂ m.
 Proof.
   intros. apply* H. apply H0.
 Qed.
 
+Instance morphism_subrelation_morphism : 
+  Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A).
+Proof. reduce. subst. firstorder. Qed.
+
 Inductive done : nat -> Type :=
   did : forall n : nat, done n.
 
@@ -428,6 +419,10 @@ Instance (A : Type) [ Reflexive B R' ] =>
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
+Instance [ Morphism (A -> B) (inverse R ==> R') m ] =>
+  Morphism (R ==> inverse R') m | 10.
+Proof. firstorder. Qed.
+
 (** [respectful] is a morphism for relation equivalence. *)
 
 Instance respectful_morphism : 
@@ -450,7 +445,7 @@ Proof.
 Qed.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
-  inverse (R ==> R') ==rel (inverse R ==> inverse R').
+  inverse (R ==> R') <->rel (inverse R ==> inverse R').
 Proof.
   intros.
   unfold flip, respectful.
@@ -515,6 +510,26 @@ Ltac morphism_normalization :=
 
 Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
 
+(** Morphisms for relations *)
+
+Instance [ PartialOrder A eqA R ] => 
+   partial_order_morphism : Morphism (eqA ==> eqA ==> iff) R.
+Proof with auto.
+  intros. rewrite partial_order_equivalence.
+  simpl_relation. firstorder.
+    transitivity x... transitivity x0... 
+    transitivity y... transitivity y0...
+Qed.
+
+Instance Morphism (relation_equivalence (A:=A) ==> 
+  relation_equivalence ==> relation_equivalence) relation_conjunction.
+  Proof. firstorder. Qed.
+
+Instance Morphism (relation_equivalence (A:=A) ==> 
+  relation_equivalence ==> relation_equivalence) relation_disjunction.
+  Proof. firstorder. Qed.
+
+
 (** Morphisms for quantifiers *)
 
 Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A).
@@ -576,5 +591,5 @@ Program Instance {A : Type} => all_inverse_impl_morphism :
   Qed.
 
 Lemma inverse_pointwise_relation A (R : relation A) : 
-  pointwise_relation (inverse R) ==rel inverse (pointwise_relation (A:=A) R).
+  pointwise_relation (inverse R) <->rel inverse (pointwise_relation (A:=A) R).
 Proof. reflexivity. Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 009ee1e863..3d5c6a7ee4 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -11,7 +11,7 @@
    This is the basic theory needed to formalize morphisms and setoids.
  
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit�copyright Paris Sud
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
@@ -212,10 +212,33 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid
   (fun f g => forall (x y : a), R x y -> R' (f x) (g y)).
 *)
 
+
+(** We define the various operations which define the algebra on relations.
+   They are essentially liftings of the logical operations. *)
+
 Definition relation_equivalence {A : Type} : relation (relation A) :=
   fun (R R' : relation A) => forall x y, R x y <-> R' x y.
 
-Infix "==rel" := relation_equivalence (at level 70).
+Infix "<->rel" := relation_equivalence (at level 70).
+
+Class subrelation {A:Type} (R R' : relation A) :=
+  is_subrelation : forall x y, R x y -> R' x y.
+
+Implicit Arguments subrelation [[A]].
+
+Infix "->rel" := subrelation (at level 70).
+
+Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
+  fun x y => R x y /\ R' x y.
+
+Infix "//\\" := relation_conjunction (at level 55).
+
+Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
+  fun x y => R x y \/ R' x y.
+
+Infix "\\//" := relation_disjunction (at level 55).
+
+(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
 Program Instance relation_equivalence_equivalence :
   Equivalence (relation A) relation_equivalence.
@@ -225,3 +248,42 @@ Program Instance relation_equivalence_equivalence :
     unfold relation_equivalence in *.
     apply transitivity with (y x0 y0) ; [ apply H | apply H0 ].
   Qed.
+
+Program Instance subrelation_preorder :
+  PreOrder (relation A) subrelation.
+
+(** *** Partial Order.
+   A partial order is a preorder which is additionally antisymmetric.
+   We give an equivalent definition, up-to an equivalence relation 
+   on the carrier. *)
+
+Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
+  partial_order_equivalence : relation_equivalence eqA (R //\\ flip R).
+
+
+(** The equivalence proof is sufficient for proving that [R] must be a morphism 
+   for equivalence (see Morphisms).
+   It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
+
+Instance [ PartialOrder A eqA R ] =>  partial_order_antisym : ! Antisymmetric A eqA R.
+Proof with auto.
+  reduce_goal. pose partial_order_equivalence. red in r.
+  apply <- r. firstorder.
+Qed.
+
+(** The partial order defined by subrelation and relation equivalence. *)
+
+Program Instance subrelation_partial_order :
+  ! PartialOrder (relation A) relation_equivalence subrelation.
+
+  Next Obligation.
+  Proof.
+    unfold relation_equivalence in *. firstorder.
+  Qed.
+
+Instance iff_impl_subrelation : subrelation iff impl.
+Proof. firstorder. Qed.
+
+Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
+Proof. firstorder. Qed.
+
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index f31115d99e..f2dcdd0e07 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -27,9 +27,11 @@ Ltac destruct_pairs := repeat (destruct_one_pair).
 
 Ltac destruct_one_ex :=
   let tac H := let ph := fresh "H" in destruct H as [H ph] in
+  let tacT H := let ph := fresh "X" in destruct H as [H ph] in
     match goal with
       | [H : (ex _) |- _] => tac H
       | [H : (sig ?P) |- _ ] => tac H
+      | [H : (sigT ?P) |- _ ] => tacT H
       | [H : (ex2 _) |- _] => tac H
     end.