Using the "relation" constant made some unifications fail in the new

setoid rewrite. Refine and use the new unification flags setup by Hugo
to do a little bit of delta in clenv_unify/w_unify. Moved from a boolean
indicating conversion is wanted to a Cpred representing the
constants one wants to get unfolded to have more precise control. Add
corresponding test-suite file.


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

10 files changed, 134 insertions, 37 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1741d7fea7..02f8e6fe8e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -96,10 +96,10 @@ let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
 	metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
     | _ -> assert false
 
-let expand_constant env c = 
+let expand_constant env predcst c = 
   let (ids,csts) = Conv_oracle.freeze() in
   match kind_of_term c with
-  | Const cst when Cpred.mem cst csts -> constant_opt_value env cst
+  | Const cst when Cpred.mem cst csts && Cpred.mem cst predcst -> constant_opt_value env cst
   | Var id when Idpred.mem id ids -> named_body id env
   | _ -> None
 
@@ -126,13 +126,13 @@ let sort_eqns = unify_r2l
 type unify_flags = { 
   modulo_conv_on_closed_terms : bool; 
   use_metas_eagerly : bool;
-  modulo_conv : bool
+  modulo_delta : Cpred.t;
 }
 
 let default_unify_flags = {
   modulo_conv_on_closed_terms = true;
   use_metas_eagerly = true;
-  modulo_conv = false
+  modulo_delta = Cpred.empty;
 }
 
 let unify_0_with_initial_metas metas is_subterm env sigma cv_pb flags m n =
@@ -215,12 +215,12 @@ let unify_0_with_initial_metas metas is_subterm env sigma cv_pb flags m n =
 
   and expand curenv pb b substn cM f1 l1 cN f2 l2 =
     if trivial_unify pb substn cM cN then substn
-    else if b & flags.modulo_conv then
-      match expand_constant curenv f1 with
+    else if b & not (Cpred.is_empty flags.modulo_delta) then
+      match expand_constant curenv flags.modulo_delta f1 with
       | Some c ->
 	  unirec_rec curenv pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
       | None ->
-      match expand_constant curenv f2 with
+      match expand_constant curenv flags.modulo_delta f2 with
       | Some c ->
 	  unirec_rec curenv pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
       | None ->
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index e59869428b..4ca1d7e4f6 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -17,7 +17,7 @@ open Evd
 type unify_flags = { 
   modulo_conv_on_closed_terms : bool; 
   use_metas_eagerly : bool;
-  modulo_conv : bool
+  modulo_delta : Names.Cpred.t;
 }
 
 val default_unify_flags : unify_flags
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ced684965f..d133beaa9f 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -90,7 +90,7 @@ open Unification
 let fail_quick_unif_flags = {
   modulo_conv_on_closed_terms = true; 
   use_metas_eagerly = false;
-  modulo_conv = false; 
+  modulo_delta = Cpred.empty; 
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fb7959a132..30b2b3fc79 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -564,7 +564,7 @@ open Unification
 let auto_unif_flags = {
   modulo_conv_on_closed_terms = true; 
   use_metas_eagerly = false;
-  modulo_conv = false; 
+  modulo_delta = Cpred.empty; 
 }
 
 (* Try unification with the precompiled clause, then use registered Apply *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 71ab3a5f7c..f06e9112f0 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -51,11 +51,29 @@ let e_give_exact c gl =
 
 let assumption id = e_give_exact (mkVar id)
 
-let unify_e_resolve  (c,clenv) gls = 
+let gen_constant dir s = Coqlib.gen_constant "Class_tactics" dir s
+let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation")
+
+open Unification
+
+let deltaset = lazy
+  (Cpred.singleton (destConst (Lazy.force coq_relation)))
+
+let auto_unif_flags = lazy {
+  modulo_conv_on_closed_terms = true; 
+  use_metas_eagerly = true;
+  modulo_delta = Lazy.force deltaset;
+}
+
+let unify_e_resolve (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver false clenv' gls in
-  h_simplest_eapply c gls
+  let clenv' = clenv_unique_resolver false ~flags:(Lazy.force auto_unif_flags) clenv' gls in
+    Clenvtac.clenv_refine true clenv' gls
 
+let unify_resolve (c,clenv) gls = 
+  let clenv' = connect_clenv gls clenv in
+  let clenv' = clenv_unique_resolver false ~flags:(Lazy.force auto_unif_flags) clenv' gls in  
+    Clenvtac.clenv_refine false clenv' gls
 
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl = 
@@ -142,26 +160,26 @@ module SearchProblem = struct
 (*     if !debug then  *)
 (*       (let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (*       let evars = Evarutil.nf_evars (Refiner.project glls) in *)
-(* 	msg (str"Goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n")); *)
+    (* 	msg (str"Goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n")); *)
     let rec aux = function
       | [] -> []
       | (tac,pptac) :: tacl -> 
 	  try 
-(* 	    if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n"); *)
+	    (* 	    if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n"); *)
 	    let (lgls,ptl) = apply_tac_list tac glls in 
 	    let v' p = v (ptl p) in
-(* 	      if !debug then *)
-(* 		begin *)
-(* 		  let evars = Evarutil.nf_evars (Refiner.project glls) in *)
-(* 		    msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
-(* 		    msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *)
-(* 		end; *)
+	      (* 	      if !debug then *)
+	      (* 		begin *)
+	      (* 		  let evars = Evarutil.nf_evars (Refiner.project glls) in *)
+	      (* 		    msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
+	      (* 		    msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *)
+	      (* 		end; *)
 	      ((lgls,v'),pptac) :: aux tacl
 	  with e when Logic.catchable_exception e ->
-(* 	    if !debug then msg (str"failed\n"); *)
+	    (* 	    if !debug then msg (str"failed\n"); *)
 	    aux tacl
     in aux l
-
+      
   let nb_empty_evars s = 
     Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0
 
@@ -303,7 +321,7 @@ let valid evm p res_sigma l =
       !res_sigma (l, Evd.create_evar_defs !res_sigma)
   in raise (Found (snd evd'))
 
-let default_evars_tactic = 
+let default_evars_tactic =
   fun x -> raise (UserError ("default_evars_tactic", mt()))
 (* tclFAIL 0 (Pp.mt ()) *)
 
@@ -378,15 +396,11 @@ let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence
 let default_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "DefaultRelation")
 
 (* let coq_relation = lazy (gen_constant ["RelationClasses";"Relation_Definitions"] "relation") *)
-let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation")
-let coq_relation a = mkApp (Lazy.force coq_relation, [| a |])
+let mk_relation a = mkApp (Lazy.force coq_relation, [| a |])
 let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
 
 let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl")
 
-let iff_setoid = lazy (gen_constant ["Classes"; "SetoidClass"] "iff_setoid")
-let eq_setoid = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_setoid")
-
 let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv")
 let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morphism")
 let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl")
@@ -423,7 +437,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a optio
   let mk_relty ty obj =
     match obj with
       | None -> 
-	  let relty = coq_relation ty in
+	  let relty = mk_relation ty in
 	    new_evar isevars env relty
       | Some x -> f x
   in
@@ -551,13 +565,13 @@ let decompose_setoid_eqhyp gl c left2right =
 let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = false;
   Unification.use_metas_eagerly = true;
-  Unification.modulo_conv = false
+  Unification.modulo_delta = Cpred.empty
 }
 
 let rewrite2_unif_flags = {
   Unification.modulo_conv_on_closed_terms = true;
   Unification.use_metas_eagerly = true;
-  Unification.modulo_conv = false
+  Unification.modulo_delta = Cpred.empty
  }
 
 (* let unification_rewrite c1 c2 cl but gl =  *)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 7e7b81ebf1..1b3f4d21bb 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1734,13 +1734,13 @@ let check_evar_map_of_evars_defs evd =
 let rewrite_unif_flags = {
   modulo_conv_on_closed_terms = false;
   use_metas_eagerly = true;
-  modulo_conv = false
+  modulo_delta = Cpred.empty
 }
 
 let rewrite2_unif_flags = {
   modulo_conv_on_closed_terms = true;
   use_metas_eagerly = true;
-  modulo_conv = false
+  modulo_delta = Cpred.empty
  }
 
 let unification_rewrite c1 c2 cl but gl = 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7a885687da..b021f5e469 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -842,7 +842,7 @@ let last_arg c = match kind_of_term c with
 let elim_flags = {
   modulo_conv_on_closed_terms = true; 
   use_metas_eagerly = true;
-  modulo_conv = false
+  modulo_delta = Cpred.empty;
 }
 
 let elimination_clause_scheme with_evars allow_K elimclause indclause gl = 
diff --git a/test-suite/typeclasses/unification_delta.v b/test-suite/typeclasses/unification_delta.v
new file mode 100644
index 0000000000..b8789f26e4
--- /dev/null
+++ b/test-suite/typeclasses/unification_delta.v
@@ -0,0 +1,46 @@
+Require Import Coq.Classes.Equivalence.
+Require Import Coq.Program.Program.
+
+Ltac obligations_tactic ::= program_simpl ; simpl_relation.
+
+Lemma bla : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y x.
+Proof.
+  intros.
+  rewrite H0.
+  refl.
+Defined.
+
+Lemma bla' : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y x.
+Proof.
+  intros.
+  (* Need delta no [relation] to unify with the right lemmas. *)
+  rewrite <- H0.
+  refl.
+Qed.
+
+Axiom euclid : nat -> { x : nat | x > 0 } -> nat.
+
+Definition eq_proj {A} {s : A -> Prop} : relation (sig s) :=
+  fun x y => `x = `y.
+
+Program Instance {A : Type} {s : A -> Prop} => Equivalence (sig s) eq_proj.
+
+  Next Obligation.
+  Proof.
+    constructor ; red ; intros.
+    reflexivity.
+  Qed.
+
+  Admit Obligations.
+
+Instance Morphism (eq ==> eq_proj ==> eq) euclid.
+Proof.
+Admitted.
+
+Goal forall (x : nat) (y : nat | y > 0) (z : nat | z > 0), eq_proj y z -> euclid x y = euclid x z.
+Proof.
+  intros.
+  (* Breaks if too much delta in unification *)
+  rewrite H.
+  reflexivity.
+Qed.
\ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index eaf300fd27..dd964433c0 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -305,6 +305,45 @@ Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) (C : T
     apply r ; auto.
   Qed.
 
+
+(** Every transitive relation gives rise to a binary morphism on [impl], 
+   contravariant in the first argument, covariant in the second. *)
+
+Program Instance [ ! Transitive A (R : relation A) ] => 
+  trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    trans x...
+    trans x0...
+  Qed.
+
+(** Dually... *)
+
+Program Instance [ ! Transitive A (R : relation A) ] =>
+  trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R.
+  
+  Next Obligation.
+  Proof with auto.
+    intros.
+    destruct (trans_contra_co_morphism (R:=inverse R)).
+    revert respect0.
+    unfold respectful, inverse, flip, impl in * ; intros.
+    eapply respect0 ; eauto.
+  Qed.
+
+(* Program Instance [ Transitive A (R : relation A), Symmetric A R ] => *)
+(*   trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R. *)
+
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     trans y... *)
+(*     sym... *)
+(*     trans y0... *)
+(*     sym... *)
+(*   Qed. *)
+
+
 (** Morphism declarations for partial applications. *)
 
 Program Instance [ ! Transitive A R ] (x : A) =>
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 86e9078e95..4ae44b3b4e 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -139,8 +139,6 @@ Definition type_eq : relation Type :=
 
 Program Instance type_equivalence : Equivalence Type type_eq.
 
-  Solve Obligations using constructor ; unfold type_eq ; program_simpl.
-
 Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
 
 Ltac obligations_tactic ::= morphism_tac.