Implementation of rewriting under lambdas. Tested on exists only.

Adds some instances that incur again a small performance penalty because they cannot
be discriminated against for now (the discrimination net is considering
the head constructor to be Morphism).


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

2 files changed, 67 insertions, 0 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index a6ca6a0316..4fbbe2a408 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -544,3 +544,67 @@ Ltac morphism_normalization :=
   end.
 
 Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
+
+(** Morphisms for quantifiers *)
+
+Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.     
+    split ; intros.
+    destruct H0 as [x₁ H₁].
+    exists x₁. rewrite H in H₁. assumption.
+    
+    destruct H0 as [x₁ H₁].
+    exists x₁. rewrite H. assumption.
+  Qed.
+
+Program Instance {A : Type} => ex_impl_morphism :
+  Morphism (pointwise_relation impl ==> impl) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.  
+    exists H0. apply H. assumption.
+  Qed.
+
+Program Instance {A : Type} => ex_inverse_impl_morphism : 
+  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.  
+    exists H0. apply H. assumption.
+  Qed.
+
+Program Instance {A : Type} => all_iff_morphism : 
+  Morphism (pointwise_relation iff ==> iff) (@all A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+
+Program Instance {A : Type} => all_impl_morphism : 
+  Morphism (pointwise_relation impl ==> impl) (@all A).
+  
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+
+Program Instance {A : Type} => all_inverse_impl_morphism : 
+  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A).
+  
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+
+Lemma inverse_pointwise_relation A (R : relation A) : 
+  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 68352abd0a..b053b27f24 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -40,6 +40,9 @@ Definition inverse {A} : relation A -> relation A := flip.
 
 Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
 
+Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
+  fun f g => forall x : A, R (f x) (g x).
+
 (** These are convertible. *)
 
 Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).