Even better test for choosing rewrite or setoid_rewrite.

Now there is a class "SetoidRelation" for registering relations that
should always be considered as setoids and never unfolded. Every "Add
Relation" command adds an instance and impl,iff are there by
default. Now the test is: if there is a SetoidRelation instance, use it
; otherwise, allow unfolding to find an eq or fallback on
setoid_rewrite. To avoid searching for SetoidRelation instances
repeateadly we check that it is really needed first by unfolding the
hyp. Only two scripts relied on the now-forbidden semantics of rewriting
by an @eq inside a setoid relation, in Numbers.


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

8 files changed, 115 insertions, 103 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d54eaf00ee..0d15034ce5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -364,8 +364,12 @@ let has_typeclasses evd =
     evd false
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
+let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 
 let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses (Evd.evars_of evd)) then evd
   else
     !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail
+
+let resolve_one_typeclass env evm t =
+  !solve_instanciation_problem env evm t
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 60b5da8226..8960ab21b6 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -76,9 +76,12 @@ val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 val mark_unresolvables : evar_map -> evar_map
 
-val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs
+val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> 
+  env -> evar_defs -> evar_defs
+val resolve_one_typeclass : env -> evar_map -> types -> constr
 
 val register_add_instance_hint : (constant -> int option -> unit) -> unit
 val add_instance_hint : constant -> int option -> unit
 
 val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
+val solve_instanciation_problem : (env -> evar_map -> types -> constr) ref
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e55b09cf7e..64ea47a9bc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -183,15 +183,6 @@ let rec catchable = function
   | Stdpp.Exc_located (_, e) -> catchable e
   | e -> Logic.catchable_exception e
 
-(* let apply_tac_list tac sigr g1 rest =  *)
-(*   let (gl,p) = apply_sig_tac sigr tac g1 in *)
-(*   let n = List.length gl in  *)
-(*     (gl@rest, fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest) *)
-
-let split_list = function 
-  | [] -> assert false
-  | hd :: tl -> hd, tl
-
 let is_dep gl gls =
   let evs = evars_of_term Intset.empty gl.evar_concl in
     if evs = Intset.empty then false
@@ -446,14 +437,17 @@ let resolve_all_evars_once debug (mode, depth) env p evd =
 
 exception FoundTerm of constr
 
-let resolve_one_typeclass env gl =
-  let gls = { it = [ Evd.make_evar (Environ.named_context_val env) gl ] ; sigma = Evd.empty } in
-  let valid x = raise (FoundTerm (fst (Refiner.extract_open_proof Evd.empty (List.hd x)))) in
+let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
+  let gls = { it = [ Evd.make_evar (Environ.named_context_val env) gl ] ; sigma = sigma } in
+  let valid x = raise (FoundTerm (fst (Refiner.extract_open_proof sigma (List.hd x)))) in
   let gls', valid' = typeclasses_eauto false (true, default_eauto_depth) [] (gls, valid) in
     try ignore(valid' []); assert false with FoundTerm t -> 
       let term = Evarutil.nf_evar (sig_sig gls') t in
 	if occur_existential term then raise Not_found else term
 
+let _ = 
+  Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
+
 let has_undefined p oevd evd =
   Evd.fold (fun ev evi has -> has ||
     (evi.evar_body = Evar_empty && p ev evi && 
@@ -517,18 +511,22 @@ let resolve_all_evars debug m env p oevd do_split fail =
 	  | Some evd' -> docomp evd' comps
   in docomp oevd split
 
-(* let resolve_all_evars debug m env p oevd = *)
-(*   let oevm = Evd.evars_of oevd in *)
-(*   try *)
-(*     let rec aux n evd = *)
-(*       if has_undefined p oevm evd then *)
-(* 	if n > 0 then *)
-(* 	  let evd' = resolve_all_evars_once debug m env p evd in *)
-(* 	    aux (pred n) evd' *)
-(* 	else None *)
-(*       else Some evd *)
-(*     in aux 3 oevd *)
-(*   with Not_found -> None *)
+let resolve_typeclass_evars d p env evd onlyargs split fail =
+  let pred = 
+    if onlyargs then 
+      (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) &&
+	class_of_constr evi.Evd.evar_concl <> None)
+    else
+      (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None)
+  in resolve_all_evars d p env pred evd split fail
+
+let solve_inst debug mode depth env evd onlyargs split fail =
+  resolve_typeclass_evars debug (mode, depth) env evd onlyargs split fail
+
+let _ = 
+  Typeclasses.solve_instanciations_problem :=
+    solve_inst false true default_eauto_depth
+
     
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
 | [ "Typeclasses" "unfold" reference_list(cl) ] -> [
@@ -563,6 +561,7 @@ let try_find_reference dir s =
 let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s
 let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
 let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
+let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq")
 let iff = lazy (gen_constant ["Init"; "Logic"] "iff")
 let coq_all = lazy (gen_constant ["Init"; "Logic"] "all")
 let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
@@ -601,6 +600,8 @@ let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalenc
 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"] "Equivalence_Reflexive")
+
+let setoid_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "SetoidRelation")
   
 let arrow_morphism a b = 
   if isprop a && isprop b then
@@ -615,12 +616,25 @@ let morphism_type = lazy (constr_of_global (Lazy.force morphism_class).cl_impl)
 
 let morphism_proxy_type = lazy (constr_of_global (Lazy.force morphism_proxy_class).cl_impl)
 
+let is_applied_setoid_relation t =
+  match kind_of_term t with
+  | App (c, args) when Array.length args >= 2 ->
+      let head = if isApp c then fst (destApp c) else c in 
+	if eq_constr (Lazy.force coq_eq) head then false
+	else (try      
+	    let evd, evar = Evarutil.new_evar (Evd.create_evar_defs Evd.empty) (Global.env()) (new_Type ()) in
+	    let inst = mkApp (Lazy.force setoid_relation, [| evar; c |]) in
+	      ignore(Typeclasses.resolve_one_typeclass (Global.env()) (Evd.evars_of evd) inst);
+	      true
+	  with _ -> false)
+  | _ -> false
+      
+let _ = 
+  Equality.register_is_applied_setoid_relation is_applied_setoid_relation
+
 exception Found of (constr * constr * (types * types) list * constr * constr array *
 		       (constr * (constr * constr * constr * constr)) option array)
 
-let is_equiv env sigma t = 
-  isConst t && Reductionops.is_conv env sigma (Lazy.force setoid_equiv) t
-
 let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
@@ -1020,16 +1034,7 @@ let build_new gl env sigma flags loccs hypinfo concl cstr evars =
   let rest = List.filter (fun o -> o > nbocc_min_1) occs in
   if rest <> [] then error_invalid_occurrence rest;
   eq
-    
-let resolve_typeclass_evars d p env evd onlyargs split fail =
-  let pred = 
-    if onlyargs then 
-      (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) &&
-	class_of_constr evi.Evd.evar_concl <> None)
-    else
-      (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None)
-  in resolve_all_evars d p env pred evd split fail
-      
+          
 let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl =
   let concl, is_hyp = 
     match clause with
@@ -1174,13 +1179,6 @@ let pr_depth _prc _prlc _prt = function
 ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
 | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
 END
-	
-let solve_inst debug mode depth env evd onlyargs split fail =
-  resolve_typeclass_evars debug (mode, depth) env evd onlyargs split fail
-
-let _ = 
-  Typeclasses.solve_instanciations_problem :=
-    solve_inst false true default_eauto_depth
       
 VERNAC COMMAND EXTEND Typeclasses_Settings
  | [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ 
@@ -1278,10 +1276,10 @@ let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyCon
 
 let declare_relation ?(binders=[]) a aeq n refl symm trans = 
   init_setoid ();
+  let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.SetoidTactics.SetoidRelation"
+  in ignore(anew_instance binders instance []);
   match (refl,symm,trans) with 
-      (None, None, None) -> 
-	let instance = declare_instance a aeq n "Coq.Classes.SetoidTactics.DefaultRelation"
-	in ignore(anew_instance binders instance [])
+      (None, None, None) -> ()
     | (Some lemma1, None, None) -> 
 	ignore (declare_instance_refl binders a aeq n lemma1)
     | (None, Some lemma2, None) -> 
@@ -1758,16 +1756,3 @@ TACTIC EXTEND head_of_constr
       letin_tac None (Name h) c allHyps
   ]
 END
-
-(* TACTIC EXTEND solve_evar *)
-(*   [ "solve_evar" int_or_var(n) ] -> [ fun gl -> *)
-(*     let n = match n with ArgArg i -> pred i | _ -> assert false in *)
-(*     let ev, evi = try List.nth (Evd.to_list (project gl)) n with Not_found -> assert false in *)
-(*     let id = pf_get_new_id (add_suffix (id_of_string "evar") (string_of_int n)) gl in *)
-(*       tclTHEN (true_cut (Name id) evi.evar_concl gl) *)
-	
-(*   ] *)
-(* END *)
-
-
-(*      let nprod = nb_prod (pf_concl gl) in *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8d849e643d..ba982ccee0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -88,46 +88,54 @@ let general_s_rewrite_clause = function
 let general_setoid_rewrite_clause = ref general_s_rewrite_clause
 let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause
 
-let dest_applied_relation t =
+let is_applied_setoid_relation = ref (fun _ -> false)
+let register_is_applied_setoid_relation = (:=) is_applied_setoid_relation
+
+let is_applied_relation t =
   match kind_of_term t with
-  | App (c, args) when Array.length args >= 2 ->
-      mkApp (c, Array.append (Array.sub args 0 (Array.length args - 2)) [|mkProp;mkProp|])
-  | _ -> t
+  | App (c, args) when Array.length args >= 2 -> true
+  | _ -> false
+
+let leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl =
+  let hdcncls = string_of_inductive hdcncl in 
+  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+  let dir = if cls=None then lft2rgt else not lft2rgt in
+  let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
+  let elim =
+    try pf_global gl (id_of_string rwr_thm)
+    with Not_found ->
+      error ("Cannot find rewrite principle "^rwr_thm^".")
+  in general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
+
+let leibniz_eq = Lazy.lazy_from_fun build_coq_eq
 
 let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
-  let ctype = pf_apply get_type_of gl c in 
-  let env = pf_env gl in
-  let sigma = project gl in 
-  let t = snd (decompose_prod (whd_betaiotazeta ctype)) in 
-  let head = dest_applied_relation t in
-  let _,t' = splay_prod env sigma head in
-    match match_with_equation t' with
-    | None -> 
-	if l = NoBindings
-	then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
-	else error "The term provided does not end with an equation."
-    | Some (hdcncl,_) -> 
-	if occs <> all_occurrences then (
-	  !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
-	else
-	  let hdcncls = string_of_inductive hdcncl in 
-	  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-	  let dir = if cls=None then lft2rgt else not lft2rgt in
-	  let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
-	  let elim =
-	    try pf_global gl (id_of_string rwr_thm)
-	    with Not_found ->
-	      error ("Cannot find rewrite principle "^rwr_thm^".")
-	  in 
-	    try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
-	    with e -> 
-	      let eq = build_coq_eq () in
-	      let head = if isApp t then fst (destApp t) else t in 
-		if not (eq_constr eq head) then
-		  try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
-		  with _ -> raise e
-		else raise e
-		  
+  if occs <> all_occurrences then (
+    !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
+  else
+    let ctype = pf_apply get_type_of gl c in 
+    let env = pf_env gl in
+    let sigma = project gl in 
+    let t = snd (decompose_prod (whd_betaiotazeta ctype)) in
+      match match_with_equation t with
+      | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *)
+	  leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl
+      | None ->
+	  let _,t' = splay_prod env sigma t in (* Search for underlying eq *)
+	    match match_with_equation t' with
+	    | Some (hdcncl,_) -> (* Maybe a setoid relation with eq inside *)
+		if l = NoBindings && !is_applied_setoid_relation t then
+		  !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
+		else
+		  (try leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl
+		    with e -> 
+		      try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
+		      with _ -> raise e)
+	    | None -> (* Can't be leibniz, try setoid *)
+		if l = NoBindings
+		then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
+		else error "The term provided does not end with an equation."
+	    
 let general_rewrite_ebindings = 
   general_rewrite_ebindings_clause None
 let general_rewrite_bindings l2r occs (c,bl) = 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 3c7f9c6b0c..0f93784afc 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -45,6 +45,7 @@ val rewriteRL   : constr  -> tactic
 val register_general_setoid_rewrite_clause :
   (identifier option -> bool ->
     occurrences -> constr -> new_goals:constr list -> tactic) -> unit
+val register_is_applied_setoid_relation : (constr -> bool) -> unit
 
 val general_rewrite_bindings_in :
   bool -> occurrences -> identifier -> constr with_bindings -> evars_flag -> tactic
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index e939d3ee7c..f8b7f62e97 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -24,11 +24,22 @@ Require Export Coq.Relations.Relation_Definitions.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** Setoid relation on a given support: declares a relation as a setoid
+   for use with rewrite. It helps choosing if a rewrite should be handled
+   by setoid_rewrite or the regular rewrite using leibniz equality.
+   Users can declare an [SetoidRelation A RA] anywhere to declare default 
+   relations. This is also done automatically by the [Declare Relation A RA]
+   commands. *)
+
+Class SetoidRelation A (R : relation A).
+
+Instance impl_setoid_relation : SetoidRelation impl.
+Instance iff_setoid_relation : SetoidRelation iff.
+
 (** Default relation on a given support. Can be used by tactics
    to find a sensible default relation on any carrier. Users can 
-   declare an [Instance A RA] anywhere to declare default relations.
-   This is also done by the [Declare Relation A RA] command with no
-   parameters for backward compatibility. *)
+   declare an [Instance def : DefaultRelation A RA] anywhere to 
+   declare default relations. *)
 
 Class DefaultRelation A (R : relation A).
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index e1f04e45ad..4d1054553f 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -216,7 +216,7 @@ Qed.
 Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd.
 Proof. 
 intros x x' Hx y y' Hy.
-rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition.
+rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition.
 Qed.
 
 Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 4f558e80ad..d5cb2882c0 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -223,7 +223,7 @@ Qed.
 Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd.
 Proof. 
 intros x x' Hx y y' Hy.
-rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition.
+rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition.
 Qed.
 
 Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd.