diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 156 |
1 files changed, 108 insertions, 48 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7e8cb4e632..2a9928a3aa 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2756,7 +2756,7 @@ let letin_tac with_eq id c ty occs = Sigma (tac, sigma, p) end } -let letin_pat_tac with_eq id c occs = +let letin_pat_tac with_evars with_eq id c occs = Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -2765,7 +2765,7 @@ let letin_pat_tac with_eq id c occs = let abs = AbstractPattern (false,check,id,c,occs,false) in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in let Sigma (c, sigma, p) = match res with - | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c + | None -> finish_evar_resolution ~flags:(tactic_infer_flags with_evars) env sigma c | Some res -> res in let tac = (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) @@ -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 *) @@ -3519,27 +3561,32 @@ let error_ind_scheme s = let s = if not (String.is_empty s) then s^" " else s in user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") -let glob c = EConstr.of_constr (Universes.constr_of_global c) +let glob sigma gr = + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr + in Sigma.to_evar_map sigma, c -let coq_eq = lazy (glob (Coqlib.build_coq_eq ())) -let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ())) +let coq_eq sigma = glob sigma (Coqlib.build_coq_eq ()) +let coq_eq_refl sigma = glob sigma (Coqlib.build_coq_eq_refl ()) -let coq_heq = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")) -let coq_heq_refl = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")) +let coq_heq_ref = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq") +let coq_heq sigma = glob sigma (Lazy.force coq_heq_ref) +let coq_heq_refl sigma = glob sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl") -let mkEq t x y = - mkApp (Lazy.force coq_eq, [| t; x; y |]) +let mkEq sigma t x y = + let sigma, eq = coq_eq sigma in + sigma, mkApp (eq, [| t; x; y |]) -let mkRefl t x = - mkApp (Lazy.force coq_eq_refl, [| t; x |]) +let mkRefl sigma t x = + let sigma, refl = coq_eq_refl sigma in + sigma, mkApp (refl, [| t; x |]) -let mkHEq t x u y = - mkApp (Lazy.force coq_heq, - [| t; x; u; y |]) +let mkHEq sigma t x u y = + let sigma, c = coq_heq sigma in + sigma, mkApp (c,[| t; x; u; y |]) -let mkHRefl t x = - mkApp (Lazy.force coq_heq_refl, - [| t; x |]) +let mkHRefl sigma t x = + let sigma, c = coq_heq_refl sigma in + sigma, mkApp (c, [| t; x |]) let lift_togethern n l = let l', _ = @@ -3577,23 +3624,30 @@ let decompose_indapp sigma f args = mkApp (f, pars), args | _ -> f, args -let mk_term_eq env sigma ty t ty' t' = +let mk_term_eq homogeneous env sigma ty t ty' t' = let sigma = Sigma.to_evar_map sigma in - if Reductionops.is_conv env sigma ty ty' then - mkEq ty t t', mkRefl ty' t' + if homogeneous then + let sigma, eq = mkEq sigma ty t t' in + let sigma, refl = mkRefl sigma ty' t' in + Sigma.Unsafe.of_evar_map sigma, (eq, refl) else - mkHEq ty t ty' t', mkHRefl ty' t' + let sigma, heq = mkHEq sigma ty t ty' t' in + let sigma, hrefl = mkHRefl sigma ty' t' in + Sigma.Unsafe.of_evar_map sigma, (heq, hrefl) let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = let open Context.Rel.Declaration in Refine.refine { run = begin fun sigma -> let eqslen = List.length eqs in (* Abstract by the "generalized" hypothesis equality proof if necessary. *) - let abshypeq, abshypt = + let sigma, abshypeq, abshypt = if dep then - let eq, refl = mk_term_eq (push_rel_context ctx env) sigma (lift 1 c) (mkRel 1) typ (mkVar id) in - mkProd (Anonymous, eq, lift 1 concl), [| refl |] - else concl, [||] + let ty = lift 1 c in + let homogeneous = Reductionops.is_conv env (Sigma.to_evar_map sigma) ty typ in + let sigma, (eq, refl) = + mk_term_eq homogeneous (push_rel_context ctx env) sigma ty (mkRel 1) typ (mkVar id) in + sigma, mkProd (Anonymous, eq, lift 1 concl), [| refl |] + else sigma, concl, [||] in (* Abstract by equalities *) let eqs = lift_togethern 1 eqs in (* lift together and past genarg *) @@ -3699,9 +3753,13 @@ let abstract_args gl generalize_vars dep id defined f args = let liftarg = lift (List.length ctx) arg in let eq, refl = if leq then - mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl (lift (-lenctx) ty) arg + let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in + let sigma', refl = mkRefl sigma' (lift (-lenctx) ty) arg in + sigma := sigma'; eq, refl else - mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg + let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in + let sigma', refl = mkHRefl sigma' argty arg in + sigma := sigma'; eq, refl in let eqs = eq :: lift_list eqs in let refls = refl :: refls in @@ -3801,17 +3859,19 @@ let specialize_eqs id gl = match EConstr.kind !evars ty with | Prod (na, t, b) -> (match EConstr.kind !evars t with - | App (eq, [| eqty; x; y |]) when EConstr.eq_constr !evars (Lazy.force coq_eq) eq -> + | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars (Lazy.force coq_eq_ref) eq -> let c = if noccur_between !evars 1 (List.length ctx) x then y else x in - let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in - let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in + let pt = mkApp (eq, [| eqty; c; c |]) in + let ind = destInd !evars eq in + let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty - | App (heq, [| eqty; x; eqty'; y |]) when EConstr.eq_constr !evars heq (Lazy.force coq_heq) -> + | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq -> let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in - let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in - let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in + let pt = mkApp (heq, [| eqt; c; eqt; c |]) in + let ind = destInd !evars heq in + let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty |