Minor fixes in typeclasses, avoiding repeated evar normalizations.

Improve generalization by equalities tactic, now allowing to
generalize an arbitrary application, e.g. in preparation for applying an
elimination principle for a function. This adds a flag to generalize_dep
so that it doesn't abstract the variable if it is defined, just
introducing a let-in.


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

6 files changed, 149 insertions, 112 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 40eaec65c6..4a2964a6fc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -275,6 +275,15 @@ let intro_tac : atac =
 	    (g', { info with hints = ldb; auto_last_tac = str"intro" })) gls
       in {it = gls'; sigma = s})
 
+let normevars_tac : atac = 
+  lift_tactic tclNORMEVAR
+    (fun {it = gls; sigma = s} info ->
+      let gls' =
+	List.map (fun g' ->
+	  (g', { info with auto_last_tac = str"NORMEVAR" })) gls
+      in {it = gls'; sigma = s})
+
+
 let id_tac : atac =
   { skft = fun sk fk {it = gl; sigma = s} ->
     sk ({it = [gl]; sigma = s}, fun _ pfs -> List.hd pfs) fk }
@@ -299,14 +308,13 @@ let hints_tac hints =
     let possible_resolve ((lgls,v) as res, pri, b, pp) =
       (pri, pp, b, res)
     in
-    let ({it = normalized; sigma = s}, valid) = tclNORMEVAR {it = gl; sigma = s} in
-    let gl = List.hd normalized in
     let tacs =
-      let concl = Evarutil.nf_evar s gl.evar_concl in
+      let concl = gl.evar_concl in
       let poss = e_possible_resolve hints info.hints concl in
       let l =
+	let tacgl = {it = gl; sigma = s} in
 	Util.list_map_append (fun (tac, pri, b, pptac) ->
-	  try [(tclTHEN tclNORMEVAR tac) {it = gl; sigma = s}, pri, b, pptac] with e when catchable e -> [])
+	  try [tac tacgl, pri, b, pptac] with e when catchable e -> [])
 	  poss
       in
 	if l = [] && !typeclasses_debug then
@@ -333,8 +341,7 @@ let hints_tac hints =
 		    ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s}
 		  else info.hints }
 	    in g, info) 1 gls in
-	  let glsvalid _ pfs = valid [v pfs] in
-	  let glsv = {it = gls'; sigma = s}, glsvalid in
+	  let glsv = {it = gls'; sigma = s}, (fun _ -> v) in
 	    sk glsv fk
       | [] -> fk ()
     in aux 1 tacs }
@@ -403,7 +410,8 @@ let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
 	| None -> raise Not_found
 	| Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk)
 	    
-let eauto_tac hints = fix (or_tac intro_tac (hints_tac hints))
+let eauto_tac hints = 
+  fix (or_tac intro_tac (then_tac normevars_tac (hints_tac hints)))
   
 let eauto ?(only_classes=true) ?st hints g =
   let gl = { it = make_autogoal ~only_classes ?st g; sigma = project g } in
@@ -616,16 +624,16 @@ VERNAC COMMAND EXTEND Typeclasses_Settings
    ]
 END
 
-let typeclasses_eauto ?(st=full_transparent_state) dbs gl =
+let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
   try 
     let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
-    let st = match dbs with [x] -> Hint_db.transparent_state x | _ -> st in
-	eauto ~only_classes:false ~st dbs gl
-  with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl
-
+    let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
+      eauto ~only_classes ~st dbs gl
+   with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl
+ 
 TACTIC EXTEND typeclasses_eauto
 | [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ]
-| [ "typeclasses" "eauto" ] -> [ typeclasses_eauto [typeclasses_db] ]
+| [ "typeclasses" "eauto" ] -> [ typeclasses_eauto ~only_classes:true [typeclasses_db] ]
 END
 
 let _ = Classes.refine_ref := Refine.refine
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index de54453100..b951734e36 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -499,7 +499,12 @@ TACTIC EXTEND specialize_hyp
 END
 
 TACTIC EXTEND dependent_pattern
-| ["dependent_pattern" constr(c) ] -> [ dependent_pattern c ]
+| ["dependent" "pattern" constr(c) ] -> [ dependent_pattern c ]
+END
+
+TACTIC EXTEND dependent_pattern_from
+| ["dependent" "pattern" "from" constr(c) ] ->
+    [ dependent_pattern ~pattern_term:false c ]
 END
 
 TACTIC EXTEND resolve_classes
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 70e8557db9..d54e568e07 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1468,7 +1468,7 @@ let generalize_goal gl i ((occs,c,b),na) cl =
   let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in
     mkProd_or_LetIn (na,b,t) cl'
 
-let generalize_dep c gl =
+let generalize_dep ?(with_let=false) c gl =
   let env = pf_env gl in
   let sign = pf_hyps gl in
   let init_ids = ids_of_named_context (Global.named_context()) in
@@ -1489,10 +1489,17 @@ let generalize_dep c gl =
       | _ -> tothin
   in
   let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
-  let cl'' = generalize_goal gl 0 ((all_occurrences,c,None),Anonymous) cl' in
+  let body = 
+    if with_let then
+      match kind_of_term c with 
+      | Var id -> pi2 (pf_get_hyp gl id)
+      | _ -> None
+    else None
+  in
+  let cl'' = generalize_goal gl 0 ((all_occurrences,c,body),Anonymous) cl' in
   let args = Array.to_list (instance_from_named_context to_quantify_rev) in
   tclTHEN
-    (apply_type cl'' (c::args))
+    (apply_type cl'' (if body = None then c::args else args))
     (thin (List.rev tothin'))
     gl
 
@@ -2225,10 +2232,10 @@ let mk_term_eq env sigma ty t ty' t' =
   else
     mkHEq ty t ty' t', mkHRefl ty' t'
 
-let make_abstract_generalize gl id concl dep ctx c eqs args refls =
+let make_abstract_generalize gl id concl dep ctx body c eqs args refls =
   let meta = Evarutil.new_meta() in
-  let term, typ = mkVar id, pf_get_hyp_typ gl id (* de Bruijn closed! *) in
   let eqslen = List.length eqs in
+  let term, typ = mkVar id, pf_get_hyp_typ gl id in
     (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
   let abshypeq, abshypt =
     if dep then
@@ -2240,7 +2247,7 @@ let make_abstract_generalize gl id concl dep ctx c eqs args refls =
   let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
   let abseqs = it_mkProd_or_LetIn ~init:(lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in
     (* Abstract by the "generalized" hypothesis. *)
-  let genarg = mkProd (Name id, c, abseqs) in
+  let genarg = mkProd_or_LetIn (Name id, body, c) abseqs in
     (* Abstract by the extension of the context *)
   let genctyp = it_mkProd_or_LetIn ~init:genarg ctx in
     (* The goal will become this product. *)
@@ -2248,7 +2255,7 @@ let make_abstract_generalize gl id concl dep ctx c eqs args refls =
     (* Apply the old arguments giving the proper instantiation of the hyp *)
   let instc = mkApp (genc, Array.of_list args) in
     (* Then apply to the original instanciated hyp. *)
-  let instc = mkApp (instc, [| mkVar id |]) in
+  let instc = Option.cata (fun _ -> instc) (mkApp (instc, [| mkVar id |])) body in
     (* Apply the reflexivity proofs on the indices. *)
   let appeqs = mkApp (instc, Array.of_list refls) in
     (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
@@ -2299,8 +2306,7 @@ let linear vars args =
       true
     with Seen -> false
 
-let abstract_args gl generalize_vars dep id = 
-  let c = pf_get_hyp_typ gl id in
+let abstract_args gl generalize_vars dep id defined f args =
   let sigma = project gl in
   let env = pf_env gl in
   let concl = pf_concl gl in
@@ -2310,90 +2316,101 @@ let abstract_args gl generalize_vars dep id =
     let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> id_of_string "gen_x") gl in
       avoid := id :: !avoid; id
   in
-    match kind_of_term c with
-    | App (f, args) -> 
-	(* Build application generalized w.r.t. the argument plus the necessary eqs.
-	   From env |- c : forall G, T and args : G we build
-	   (T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G, vars to generalize)
-	   
-	   eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
-	*)
-	let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg =
-	  let (name, _, ty), arity =
-	    let rel, c = Reductionops.splay_prod_n env sigma 1 prod in
-	      List.hd rel, c
+    (* Build application generalized w.r.t. the argument plus the necessary eqs.
+       From env |- c : forall G, T and args : G we build
+       (T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G, vars to generalize)
+       
+       eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
+    *)
+  let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg =
+    let (name, _, ty), arity =
+      let rel, c = Reductionops.splay_prod_n env sigma 1 prod in
+	List.hd rel, c
+    in
+    let argty = pf_type_of gl arg in
+    let argty = if isSort argty then new_Type () else argty in
+    let liftargty = lift (List.length ctx) argty in
+    let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
+      match kind_of_term arg with
+      (* 	    | Var id -> *)
+      (* 		let deps = deps_of_var id env in *)
+      (* 		  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, Idset.union deps vars, env) *)
+      | _ ->
+	  let name = get_id name in
+	  let decl = (Name name, None, ty) in
+	  let ctx = decl :: ctx in
+	  let c' = mkApp (lift 1 c, [|mkRel 1|]) in
+	  let args = arg :: args in
+	  let liftarg = lift (List.length ctx) arg in
+	  let eq, refl =
+	    if convertible then
+	      mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl argty arg
+	    else
+	      mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
 	  in
-	  let argty = pf_type_of gl arg in
-	  let argty = if isSort argty then new_Type () else argty in
-	  let liftargty = lift (List.length ctx) argty in
-	  let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
-	    match kind_of_term arg with
-(* 	    | Var id -> *)
-(* 		let deps = deps_of_var id env in *)
-(* 		  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, Idset.union deps vars, env) *)
-	    | _ ->
-		let name = get_id name in
-		let decl = (Name name, None, ty) in
-		let ctx = decl :: ctx in
-		let c' = mkApp (lift 1 c, [|mkRel 1|]) in
-		let args = arg :: args in
-		let liftarg = lift (List.length ctx) arg in
-		let eq, refl =
-		  if convertible then
-		    mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl argty arg
-		  else
-		    mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
-		in
-		let eqs = eq :: lift_list eqs in
-		let refls = refl :: refls in
-		let argvars = ids_of_constr vars arg in
-		  (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, Idset.union argvars vars, env)
-	in 
-	let f', args' = decompose_indapp f args in
-	let dogen, f', args' =
-	  let parvars = ids_of_constr ~all:true Idset.empty f' in
-	  if not (linear parvars args') then true, f, args
-	  else
-	    match array_find_i (fun i x -> not (isVar x)) args' with
-	    | None -> false, f', args'
-	    | Some nonvar ->
-		let before, after = array_chop nonvar args' in
-		  true, mkApp (f', before), after
-	in
-	  if dogen then
-	    let arity, ctx, ctxenv, c', args, eqs, refls, vars, env = 
-	      Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,env) args'
-	    in
-	    let args, refls = List.rev args, List.rev refls in
-	    let vars = 
-	      if generalize_vars then
-		let nogen = Idset.add id Idset.empty in
-		  hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
-	      else []
-	    in
-	      Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls,
-		   dep, succ (List.length ctx), vars)
-	  else None
-    | _ -> None
-
+	  let eqs = eq :: lift_list eqs in
+	  let refls = refl :: refls in
+	  let argvars = ids_of_constr vars arg in
+	    (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, Idset.union argvars vars, env)
+  in 
+  let f', args' = decompose_indapp f args in
+  let dogen, f', args' =
+    let parvars = ids_of_constr ~all:true Idset.empty f' in
+      if not (linear parvars args') then true, f, args
+      else
+	match array_find_i (fun i x -> not (isVar x)) args' with
+	| None -> false, f', args'
+	| Some nonvar ->
+	    let before, after = array_chop nonvar args' in
+	      true, mkApp (f', before), after
+  in
+    if dogen then
+      let arity, ctx, ctxenv, c', args, eqs, refls, vars, env = 
+	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,env) args'
+      in
+      let args, refls = List.rev args, List.rev refls in
+      let vars = 
+	if generalize_vars then
+	  let nogen = Idset.singleton id in
+	    hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
+	else []
+      in
+      let body, c' = if defined then Some c', Retyping.get_type_of ctxenv Evd.empty c' else None, c' in
+	Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls,
+	     dep, succ (List.length ctx), vars)
+    else None
+      
 let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
   Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
-  let oldid = pf_get_new_id id gl in
-  let newc = abstract_args gl generalize_vars force_dep id in
-    match newc with
-    | None -> tclIDTAC gl
-    | Some (newc, dep, n, vars) -> 
-	let tac =
-	  if dep then
-	    tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro; 
-			 generalize_dep (mkVar oldid)]	      
-	  else
-	    tclTHENLIST [refine newc; clear [id]; tclDO n intro]
-	in 
-	  if vars = [] then tac gl
-	  else tclTHEN tac 
-	    (fun gl -> tclFIRST [revert vars ;
-				 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars] gl) gl
+  let f, args, def, id, oldid = 
+    let oldid = pf_get_new_id id gl in
+    let (_, b, t) = pf_get_hyp gl id in
+      match b with
+      | None -> let f, args = decompose_app t in
+		  f, args, false, id, oldid
+      | Some t -> 
+	  let f, args = decompose_app t in
+	    f, args, true, id, oldid
+  in
+  if args = [] then tclIDTAC gl
+  else 
+    let args = Array.of_list args in
+    let newc = abstract_args gl generalize_vars force_dep id def f args in
+      match newc with
+      | None -> tclIDTAC gl
+      | Some (newc, dep, n, vars) -> 
+	  let tac =
+	    if dep then
+	      tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro; 
+			   generalize_dep ~with_let:true (mkVar oldid)]	      
+	    else
+	      tclTHENLIST [refine newc; clear [id]; tclDO n intro]
+	  in 
+	    if vars = [] then tac gl
+	    else tclTHEN tac 
+	      (fun gl -> tclFIRST [revert vars ;
+				   tclMAP (fun id -> 
+				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl) gl
 
 let specialize_hypothesis id gl =
   let env = pf_env gl in
@@ -2444,11 +2461,11 @@ let specialize_hypothesis id gl =
       
 
 let specialize_hypothesis id gl =
-  if occur_var (pf_env gl) id (pf_concl gl) then
+  if try ignore(clear [id] gl); false with _ -> true then
     tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl 
   else specialize_hypothesis id gl
 
-let dependent_pattern c gl =
+let dependent_pattern ?(pattern_term=true) c gl =
   let cty = pf_type_of gl c in
   let deps =
     match kind_of_term cty with
@@ -2465,7 +2482,11 @@ let dependent_pattern c gl =
     let conclvar = subst_term_occ all_occurrences c ty in
       mkNamedLambda id cty conclvar
   in
-  let subst = (c, varname c, cty) :: List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in
+  let subst = 
+    let deps = List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in
+      if pattern_term then (c, varname c, cty) :: deps
+      else deps
+  in
   let concllda = List.fold_left mklambda (pf_concl gl) subst in
   let conclapp = applistc concllda (List.rev_map pi1 subst) in
     convert_concl_no_check conclapp DEFAULTcast gl
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 19c0ba3332..2202fa8c88 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -373,7 +373,7 @@ val pose_proof : name -> constr -> tactic
 
 val generalize      : constr list -> tactic
 val generalize_gen  : ((occurrences * constr) * name) list -> tactic
-val generalize_dep  : constr  -> tactic
+val generalize_dep  : ?with_let:bool (* Don't lose let bindings *) -> constr  -> tactic
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> tactic
 val resolve_classes : tactic
@@ -385,7 +385,7 @@ val admit_as_an_axiom : tactic
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic
 val specialize_hypothesis : identifier -> tactic
 
-val dependent_pattern : constr -> tactic
+val dependent_pattern : ?pattern_term:bool -> constr -> tactic
 
 val register_general_multi_rewrite :
   (bool -> evars_flag -> open_constr with_bindings -> clause -> tactic) -> unit
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 76dc09b26e..c9ec29d2b0 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -22,7 +22,7 @@ Ltac is_ground_goal :=
 
 (** Try to find a contradiction. *)
 
-Hint Extern 10 => is_ground_goal ; progress (elimtype False).
+Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso.
 
 (** We will use the [block] definition to separate the goal from the 
    equalities generated by the tactic. *)
diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v
index a7bb661ea7..e35c7c651c 100644
--- a/theories/Structures/OrderedType2Facts.v
+++ b/theories/Structures/OrderedType2Facts.v
@@ -23,7 +23,10 @@ Module OTF_to_OrderSig (O : OrderedTypeFull) :
  OrderSig with Definition t := O.t
           with Definition eq := O.eq
           with Definition lt := O.lt
-          with Definition le := O.le.
+          with Definition le := O.le
+          with Definition eq_equiv := O.eq_equiv
+          with Definition lt_strorder := O.lt_strorder
+          with Definition lt_compat := O.lt_compat.
  Include O.
  Lemma lt_total : forall x y, O.lt x y \/ O.eq x y \/ O.lt y x.
  Proof. intros; destruct (O.compare_spec x y); auto. Qed.
@@ -156,7 +159,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
 
   Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
   Proof.
-   intros; elim_compare x y; autorewrite with order; order.
+   intros; elim_compare x y; simpl; autorewrite with order; order.
   Qed.
 
   (** For compatibility reasons *)