Merge PR#449: make specialize smarter (bug 5370).

4 files changed, 112 insertions, 19 deletions

diff --git a/CHANGES b/CHANGES
index 8fd71f9247..eac64d6705 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,9 @@ Tactics
 - New tactic "extensionality in H" which applies (possibly dependent)
   functional extensionality in H supposed to be a quantified equality
   until giving a bare equality.
+- Tactic "specialize with ..." now accepts any partial bindings.
+  Missing bindings are either solved by unification or left quantified
+  in the hypothesis.
 - New representation of terms that statically ensure stability by
   evar-expansion. This has several consequences.
   * In terms of performance, this adds a cost to every term destructuration,
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index def42955ff..253eb7f01b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1384,12 +1384,16 @@ in the list of subgoals remaining to prove.
       quantifications or non-dependent implications) are instantiated
       by concrete terms coming either from arguments \term$_1$
       $\ldots$ \term$_n$ or from a bindings list (see
-      Section~\ref{Binding-list} for more about bindings lists). In the
-      second form, all instantiation elements must be given, whereas
-      in the first form the application to \term$_1$ {\ldots}
+      Section~\ref{Binding-list} for more about bindings lists). 
+      In the first form the application to \term$_1$ {\ldots}
       \term$_n$ can be partial. The first form is equivalent to
       {\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}.
 
+      In the second form, instantiation elements can also be partial.
+      In this case the uninstantiated arguments are inferred by
+      unification if possible or left quantified in the hypothesis
+      otherwise.
+
       With the {\tt as} clause, the local hypothesis {\ident} is left
       unchanged and instead, the modified hypothesis is introduced as
       specified by the {\intropattern}.
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6e45739ec3..2a9928a3aa 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2954,6 +2954,19 @@ let quantify lconstr =
 
 (* Modifying/Adding an hypothesis  *)
 
+(* Instantiating some arguments (whatever their position) of an hypothesis
+   or any term, leaving other arguments quantified. If operating on an
+   hypothesis of the goal, the new hypothesis replaces it.
+
+   (c,lbind) are supposed to be of the form
+   ((t t1 t2 ... tm) , someBindings)
+
+   in which case we pose a proof with body
+
+   (fun y1...yp => H t1 t2 ... tm u1 ... uq) where yi are the
+   remaining arguments of H that lbind could not resolve, ui are a mix
+   of inferred args and yi. The overall effect is to remove from H as
+   much quantification as possible given lbind. *)
 let specialize (c,lbind) ipat =
   Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
@@ -2962,22 +2975,49 @@ let specialize (c,lbind) ipat =
     if lbind == NoBindings then
       sigma, c
     else
-      let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in
+      let typ_of_c = Retyping.get_type_of env sigma c in
+      (* If the term is lambda then we put a letin to put avoid
+         interaction between the term and the bindings. *)
+      let c = match EConstr.kind sigma c with
+        | Lambda(_,_,_) ->
+          mkLetIn(Name.Anonymous, c, typ_of_c, (mkRel 1))
+        | _ -> c in
+      let clause = make_clenv_binding env sigma (c,typ_of_c) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
-      let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
-      let rec chk = function
-      | [] -> []
-      | t::l -> if occur_meta clause.evd t then [] else t :: chk l
-      in
-      let tstack = chk tstack in
-      let term = applist(thd,List.map (nf_evar clause.evd) tstack) in
-      if occur_meta clause.evd term then
-	user_err  (str "Cannot infer an instance for " ++
-
-          Name.print (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++
-	  str ".");
-      clause.evd, term in
+      let sigma = clause.evd in
+      let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in
+      let c_hd , c_args = decompose_app sigma c in
+      let liftrel x =
+        match kind sigma x with
+        | Rel n -> mkRel (n+1)
+        | _ -> x in
+      (* We grab names used in product to remember them at re-abstracting phase *)
+      let typ_of_c_hd = pf_get_type_of gl c_hd in
+      let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in
+      (* accumulator args: arguments to apply to c_hd: all infered
+         args + re-abstracted rels *)
+      let rec rebuild_lambdas sigma lprd args hd l =
+        match lprd , l with
+        | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args))
+        | Context.Rel.Declaration.LocalAssum(nme,_)::lp' , t::l' when occur_meta sigma t ->
+          (* nme has not been resolved, let us re-abstract it. Same
+             name but type updated by instanciation of other args. *)
+          let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in
+          let liftedargs = List.map liftrel args in
+          (* lifting rels in the accumulator args *)
+          let sigma,hd' = rebuild_lambdas sigma lp' (liftedargs@[mkRel 1 ]) hd l' in
+          (* replace meta variable by the abstracted variable *)
+          let hd'' = subst_term sigma t hd' in
+          (* lambda expansion *)
+          sigma,mkLambda (nme,new_typ_of_t,hd'')
+        | Context.Rel.Declaration.LocalAssum(_,_)::lp' , t::l' ->
+          let sigma,hd' = rebuild_lambdas sigma lp' (args@[t]) hd l' in
+          sigma,hd'
+        | _ ,_ -> assert false in
+      let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] c_hd tstack in
+      sigma, hd
+  in
   let typ = Retyping.get_type_of env sigma term in
   let tac =
     match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with
@@ -2994,7 +3034,9 @@ let specialize (c,lbind) ipat =
       | None ->
         (* Like generalize with extra support for "with" bindings *)
         (* even though the "with" bindings forces full application *)
-        Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term)
+        (* TODO: add intro to be more homogeneous. It will break
+           scripts but will be easy to fix *)
+         (Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term))
       | Some (loc,ipat) ->
         (* Like pose proof with extra support for "with" bindings *)
         (* even though the "with" bindings forces full application *)
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 4b41a509e5..f12db8b081 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -17,6 +17,29 @@ specialize (eq_trans (x:=a)(y:=b)). intros _.
 specialize (eq_trans H H0). intros _.
 specialize (eq_trans H0 (z:=b)). intros _.
 
+(* incomplete bindings: y is left quantified and z is instantiated. *)
+specialize eq_trans with (x:=a)(z:=c).
+intro h.
+(* y can be instantiated now *)
+specialize h with (y:=b).
+(* z was instantiated above so this must fail. *)
+Fail specialize h with (z:=c).
+clear h.
+
+(* incomplete bindings: 1st dep hyp is instantiated thus A, x and y
+   instantiated too. *)
+specialize eq_trans with (1:=H).
+intro h.
+(* 2nd dep hyp can be instantiated now, which instatiates z too. *)
+specialize h with (1:=H0).
+(* checking that there is no more products in h. *)
+match type of h with
+| _ = _ => idtac
+| _ => fail "specialize test failed: hypothesis h should be an equality at this point"
+end.
+clear h.
+
+
 (* local "in place" specialization *)
 assert (Eq:=eq_trans).
 
@@ -31,6 +54,27 @@ specialize (Eq _ a b c). Undo.
 specialize (Eq _ _ _ _ H H0). Undo.
 specialize (Eq _ _ _ b H0). Undo.
 
+(* incomplete binding *)
+specialize Eq with (y:=b).
+(* A and y have been instantiated so this works *)
+specialize (Eq _ _ H H0).
+Undo 2.
+
+(* incomplete binding (dependent) *)
+specialize Eq with (1:=H).
+(* A, x and y have been instantiated so this works *)
+specialize (Eq _ H0).
+Undo 2.
+
+(* incomplete binding (dependent) *)
+specialize Eq with (1:=H) (2:=H0).
+(* A, x and y have been instantiated so this works *)
+match type of Eq with
+| _ = _ => idtac
+| _ => fail "specialize test failed: hypothesis Eq should be an equality at this point"
+end.
+Undo 2.
+
 (*
 (** strange behavior to inspect more precisely *)
 
@@ -40,7 +84,7 @@ specialize (Eq _ _ _ b H0). Undo.
 (* 2) echoue moins lorsque zero premise de mangé *)
 specialize eq_trans with (1:=Eq).  (* mal typé !! *)
 
-(* 3) *)
+(* 3) Seems fixed.*)
 specialize eq_trans with _ a b c. intros _.
 (* Anomaly: Evar ?88 was not declared. Please report. *)
 *)