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

3 files changed, 89 insertions, 6 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b2684a3928..dd552845dc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -443,6 +443,8 @@ let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Transit
 let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive")
 
 let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse")
+let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement")
+let pointwise_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "pointwise_relation")
 
 let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep")
 let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
@@ -702,7 +704,7 @@ let unfold_id t =
 
 let build_new gl env sigma occs hypinfo concl cstr evars =
   let is_occ occ = occs = [] || List.mem occ occs in
-  let rec aux t occ cstr =
+  let rec aux env t occ cstr =
     match unify_eqn gl hypinfo t with
       | Some (env', (prf, hypinfo as x)) ->
 	  if is_occ occ then (
@@ -725,7 +727,7 @@ let build_new gl env sigma occs hypinfo concl cstr evars =
 	    | App (m, args) ->
 		let args', occ = 
 		  Array.fold_left 
-		    (fun (acc, occ) arg -> let res, occ = aux arg occ None in (res :: acc, occ))
+		    (fun (acc, occ) arg -> let res, occ = aux env arg occ None in (res :: acc, occ))
 		    ([], occ) args
 		in
 		let res =
@@ -737,21 +739,35 @@ let build_new gl env sigma occs hypinfo concl cstr evars =
 		in res, occ
 		  
 	    | Prod (_, x, b) -> 
-		let x', occ = aux x occ None in
-		let b', occ = aux b occ None in
+		let x', occ = aux env x occ None in
+		let b', occ = aux env b occ None in
 		let res = 
 		  if x' = None && b' = None then None
 		  else 
 		    (try 
 			Some (resolve_morphism env sigma t
 				 ~fnewt:unfold_impl
-				 (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |]
+				 (arrow_morphism (Typing.type_of env sigma x) (Typing.type_of env sigma b))
+				 [| x ; b |] [| x' ; b' |]
 				 cstr evars)
 		      with Not_found -> None)
 		in res, occ
 		  
+	    | Lambda (n, t, b) ->
+		let env' = Environ.push_rel (n, None, t) env in
+		let b', occ = aux env' b occ None in
+		let res =
+		  match b' with
+		      None -> None
+		    | Some (prf, (car, rel, c1, c2)) ->
+			let prf' = mkLambda (n, t, prf) in
+			let car' = mkProd (n, t, car) in
+			let rel' = mkApp (Lazy.force pointwise_relation, [| t; car; rel |]) in
+			let c1' = mkLambda(n, t, c1) and c2' = mkLambda (n, t, c2) in
+			  Some (prf', (car', rel', c1', c2'))
+		in res, occ
 	    | _ -> None, occ
-  in aux concl 1 cstr
+  in aux env concl 1 cstr
     
 let resolve_all_typeclasses env evd = 
   resolve_all_evars false (true, 15) env
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).