diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 163 |
1 files changed, 89 insertions, 74 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index bda16b01..067fc894 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -1,21 +1,22 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp open CErrors open Util open Names -open Nameops open Term -open Vars open Termops +open EConstr +open Vars open Namegen -open Environ open Inductiveops open Printer open Retyping @@ -25,15 +26,15 @@ open Tactics open Elim open Equality open Misctypes -open Tacexpr -open Sigma.Notations open Proofview.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration let var_occurs_in_pf gl id = let env = Proofview.Goal.env gl in - occur_var env id (Proofview.Goal.concl gl) || - List.exists (occur_var_in_decl env id) (Proofview.Goal.hyps gl) + let sigma = project gl in + occur_var env sigma id (Proofview.Goal.concl gl) || + List.exists (occur_var_in_decl env sigma id) (Proofview.Goal.hyps gl) (* [make_inv_predicate (ity,args) C] @@ -73,11 +74,12 @@ let make_inv_predicate env evd indf realargs id status concl = | NoDep -> (* We push the arity and leave concl unchanged *) let hyps_arity,_ = get_arity env indf in + let hyps_arity = List.map (fun d -> map_rel_decl EConstr.of_constr d) hyps_arity in (hyps_arity,concl) | Dep dflt_concl -> - if not (occur_var env id concl) then - errorlabstrm "make_inv_predicate" - (str "Current goal does not depend on " ++ pr_id id ++ str"."); + if not (occur_var env !evd id concl) then + user_err ~hdr:"make_inv_predicate" + (str "Current goal does not depend on " ++ Id.print id ++ str"."); (* We abstract the conclusion of goal with respect to realargs and c to * be concl in order to rewrite and have c also rewritten when the case * will be done *) @@ -87,11 +89,11 @@ let make_inv_predicate env evd indf realargs id status concl = | None -> let sort = get_sort_family_of env !evd concl in let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in - let p = make_arity env true indf sort in + let p = make_arity env !evd true indf sort in let evd',(p,ptyp) = Unification.abstract_list_all env !evd p concl (realargs@[mkVar id]) in evd := evd'; p in - let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in + let hyps,bodypred = decompose_lam_n_assum !evd (nrealargs+1) pred in (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) in @@ -109,7 +111,7 @@ let make_inv_predicate env evd indf realargs id status concl = let ai = lift nhyps ai in let (xi, ti) = compute_eqn env' !evd nhyps n ai in let (lhs,eqnty,rhs) = - if closed0 ti then + if closed0 !evd ti then (xi,ti,ai) else let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in @@ -117,17 +119,19 @@ let make_inv_predicate env evd indf realargs id status concl = in let eq_term = eqdata.Coqlib.eq in let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in + let eq = EConstr.of_constr eq in let eqn = applist (eq,[eqnty;lhs;rhs]) in let eqns = (Anonymous, lift n eqn) :: eqns in let refl_term = eqdata.Coqlib.refl in let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in + let refl_term = EConstr.of_constr refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in let args = refl :: args in build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in - let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in + let predicate = it_mkLambda_or_LetIn newconcl (name_context env !evd hyps) in let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) @@ -182,8 +186,8 @@ let dependent_hyps env id idlist gl = | [] -> [] | d::l -> (* Update the type of id1: it may have been subject to rewriting *) - let d = pf_get_hyp (get_id d) gl in - if occur_var_in_decl env id d + let d = pf_get_hyp (NamedDecl.get_id d) gl in + if occur_var_in_decl env (project gl) id d then d :: dep_rec l else dep_rec l in @@ -192,7 +196,7 @@ let dependent_hyps env id idlist gl = let split_dep_and_nodep hyps gl = List.fold_right (fun d (l1,l2) -> - if var_occurs_in_pf gl (get_id d) then (d::l1,l2) else (l1,d::l2)) + if var_occurs_in_pf gl (NamedDecl.get_id d) then (d::l1,l2) else (l1,d::l2)) hyps ([],[]) (* Computation of dids is late; must have been done in rewrite_equations*) @@ -268,47 +272,50 @@ Nota: with Inversion_clear, only four useless hypotheses let generalizeRewriteIntros as_mode tac depids id = Proofview.tclENV >>= fun env -> - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let dids = dependent_hyps env id depids gl in let reintros = if as_mode then intros_replacing else intros_possibly_replacing in (tclTHENLIST [bring_hyps dids; tac; (* may actually fail to replace if dependent in a previous eq *) reintros (ids_of_named_context dids)]) - end } + end let error_too_many_names pats = - let loc = Loc.join_loc (fst (List.hd pats)) (fst (List.last pats)) in + let loc = Loc.merge_opt (List.hd pats).CAst.loc (List.last pats).CAst.loc in Proofview.tclENV >>= fun env -> - tclZEROMSG ~loc ( + Proofview.tclEVARMAP >>= fun sigma -> + tclZEROMSG ?loc ( str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ - str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (fst (run_delayed env Evd.empty c)))) pats ++ + str ": " ++ pr_enum (Miscprint.pr_intro_pattern + (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ str ".") -let get_names (allow_conj,issimple) (loc, pat as x) = match pat with +let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with | IntroNaming IntroAnonymous | IntroForthcoming _ -> - error "Anonymous pattern not allowed for inversion equations." + user_err Pp.(str "Anonymous pattern not allowed for inversion equations.") | IntroNaming (IntroFresh _) -> - error "Fresh pattern not allowed for inversion equations." + user_err Pp.(str "Fresh pattern not allowed for inversion equations.") | IntroAction IntroWildcard -> - error "Discarding pattern not allowed for inversion equations." + user_err Pp.(str "Discarding pattern not allowed for inversion equations.") | IntroAction (IntroRewrite _) -> - error "Rewriting pattern not allowed for inversion equations." + user_err Pp.(str "Rewriting pattern not allowed for inversion equations.") | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, []) - | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l) | IntroOrPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l ])) + | IntroAction (IntroOrAndPattern (IntroAndPattern ({CAst.v=IntroNaming (IntroIdentifier id)} :: _ as l) + | IntroOrPattern [{CAst.v=IntroNaming (IntroIdentifier id)} :: _ as l])) when allow_conj -> (Some id,l) | IntroAction (IntroOrAndPattern (IntroAndPattern _)) -> if issimple then - error"Conjunctive patterns not allowed for simple inversion equations." + user_err Pp.(str"Conjunctive patterns not allowed for simple inversion equations.") else - error"Nested conjunctive patterns not allowed for inversion equations." + user_err Pp.(str"Nested conjunctive patterns not allowed for inversion equations.") | IntroAction (IntroInjection l) -> - error "Injection patterns not allowed for inversion equations." + user_err Pp.(str "Injection patterns not allowed for inversion equations.") | IntroAction (IntroOrAndPattern (IntroOrPattern _)) -> - error "Disjunctive patterns not allowed for inversion equations." + user_err Pp.(str "Disjunctive patterns not allowed for inversion equations.") | IntroAction (IntroApplyOn (c,pat)) -> - error "Apply patterns not allowed for inversion equations." + user_err Pp.(str "Apply patterns not allowed for inversion equations.") | IntroNaming (IntroIdentifier id) -> (Some id,[x]) @@ -331,21 +338,32 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id If it can discriminate then the goal is proved, if not tries to use it as a rewrite rule. It erases the clause which is given as input *) +let dest_nf_eq env sigma t = match EConstr.kind sigma t with +| App (r, [| t; x; y |]) -> + let open Reductionops in + let lazy eq = Coqlib.coq_eq_ref in + if EConstr.is_global sigma eq r then + (t, whd_all env sigma x, whd_all env sigma y) + else user_err Pp.(str "Not an equality.") +| _ -> + user_err Pp.(str "Not an equality.") + let projectAndApply as_mode thin avoid id eqname names depids = let subst_hyp l2r id = - tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id))) + tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id))) (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) in let substHypIfVariable tac id = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> + let sigma = project gl in (** We only look at the type of hypothesis "id" *) - let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in - let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in - match (kind_of_term t1, kind_of_term t2) with + let hyp = pf_nf_evar gl (pf_get_hyp_typ id gl) in + let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in + match (EConstr.kind sigma t1, EConstr.kind sigma t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 | _ -> tac id - end } + end in let deq_trailer id clear_flag _ neqns = assert (clear_flag == None); @@ -367,12 +385,12 @@ let projectAndApply as_mode thin avoid id eqname names depids = (* If no immediate variable in the equation, try to decompose it *) (* and apply a trailer which again try to substitute *) (fun id -> - dEqThen false (deq_trailer id) - (Some (None,ElimOnConstr (mkVar id,NoBindings)))) + dEqThen ~keep_proofs:None false (deq_trailer id) + (Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings)))) id let nLastDecls i tac = - Proofview.Goal.nf_enter { enter = begin fun gl -> tac (nLastDecls gl i) end } + Proofview.Goal.enter begin fun gl -> tac (nLastDecls gl i) end (* Introduction of the equations on arguments othin: discriminates Simple Inversion, Inversion and Inversion_clear @@ -380,10 +398,10 @@ let nLastDecls i tac = Some thin: the equations are rewritten, and cleared if thin is true *) let rewrite_equations as_mode othin neqns names ba = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in let first_eq = ref MoveLast in - let avoid = if as_mode then List.map get_id nodepids else [] in + let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with | Some thin -> tclTHENLIST @@ -399,10 +417,10 @@ let rewrite_equations as_mode othin neqns names ba = tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) names; tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) - let idopt = if as_mode then Some (get_id d) else None in + let idopt = if as_mode then Some (NamedDecl.get_id d) else None in intro_move idopt (if thin then MoveLast else !first_eq)) nodepids; - (tclMAP (fun d -> tclTRY (clear [get_id d])) depids)] + (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)] | None -> (* simple inversion *) if as_mode then @@ -413,7 +431,7 @@ let rewrite_equations as_mode othin neqns names ba = [tclDO neqns intro; bring_hyps nodepids; clear (ids_of_named_context nodepids)]) - end } + end let interp_inversion_kind = function | SimpleInversion -> None @@ -430,17 +448,16 @@ let rewrite_equations_tac as_mode othin id neqns names ba = tac let raw_inversion inv_kind id status names = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) with UserError _ -> - let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in - CErrors.errorlabstrm "" msg + let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in + CErrors.user_err msg in let IndType (indf,realargs) = find_rectype env sigma t in let evdref = ref sigma in @@ -448,30 +465,28 @@ let raw_inversion inv_kind id status names = make_inv_predicate env evdref indf realargs id status concl in let sigma = !evdref in let (cut_concl,case_tac) = - if status != NoDep && (dependent c concl) then - Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), + if status != NoDep && (dependent sigma c concl) then + Reductionops.beta_applist sigma (elim_predicate, realargs@[c]), case_then_using else - Reduction.beta_appvect elim_predicate (Array.of_list realargs), + Reductionops.beta_applist sigma (elim_predicate, realargs), case_nodep_then_using in let refined id = let prf = mkApp (mkVar id, args) in - Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) } + Refine.refine ~typecheck:false (fun h -> (h, prf)) in let neqns = List.length realargs in let as_mode = names != None in - let tac = + tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (assert_before Anonymous cut_concl) [case_tac names (introCaseAssumsThen false (* ApplyOn not supported by inversion *) (rewrite_equations_tac as_mode inv_kind id neqns)) - (Some elim_predicate) ind (c, t); + (Some elim_predicate) ind (c,t); onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + end (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with @@ -496,8 +511,6 @@ let inversion inv_kind status names id = let inv_gen thin status names = try_intros_until (inversion thin status names) -open Tacexpr - let inv k = inv_gen k NoDep let inv_tac id = inv FullInversion None (NamedHyp id) @@ -513,21 +526,23 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) * back to their places in the hyp-list. *) let invIn k names ids id = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let concl = Proofview.Goal.concl gl in - let nb_prod_init = nb_prod concl in + let sigma = project gl in + let nb_prod_init = nb_prod sigma concl in let intros_replace_ids = - Proofview.Goal.enter { enter = begin fun gl -> - let concl = pf_nf_concl gl in + Proofview.Goal.enter begin fun gl -> + let concl = pf_concl gl in + let sigma = project gl in let nb_of_new_hyp = - nb_prod concl - (List.length hyps + nb_prod_init) + nb_prod sigma concl - (List.length hyps + nb_prod_init) in if nb_of_new_hyp < 1 then intros_replacing ids else tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) - end } + end in Proofview.tclORELSE (tclTHENLIST @@ -535,7 +550,7 @@ let invIn k names ids id = inversion k NoDep names id; intros_replace_ids]) (wrap_inv_error id) - end } + end let invIn_gen k names idl = try_intros_until (invIn k names idl) |