From d767261f0057d8e846bab65a882254d8e4f4c283 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 28 Feb 2017 21:32:30 +0100 Subject: Make specialize smarter. Now when a partial with-binding is given the unsolved parameters are left quantified. A letin is added when mixing (fun x => ...) and with-bindings. --- tactics/tactics.ml | 72 ++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 57 insertions(+), 15 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7e8cb4e632..bb4610b71e 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 " ++ - - pr_name (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 *) -- cgit v1.2.3 From 0e37dc665cf7a6a9ed7d0d10199dd40134cf0148 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 12 May 2017 10:51:46 +0200 Subject: Documenting the new behaviour of specialize. --- doc/refman/RefMan-tac.tex | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fc3fdd0025..15df2e601d 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1337,12 +1337,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}. -- cgit v1.2.3 From 96bbe0590417d8885ac09abf7d749c12172e16bc Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 12 May 2017 10:58:26 +0200 Subject: Tests for new specialize feature + CHANGES. --- CHANGES | 3 +++ test-suite/success/specialize.v | 46 ++++++++++++++++++++++++++++++++++++++++- 2 files changed, 48 insertions(+), 1 deletion(-) diff --git a/CHANGES b/CHANGES index 30bea7a7b5..847073eaf6 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/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. *) *) -- cgit v1.2.3