diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 112 |
1 files changed, 62 insertions, 50 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 40b600c8..a4cdc159 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* 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 @@ -11,27 +13,29 @@ open CErrors open Util open Names open Term -open Vars open Termops +open Environ +open EConstr +open Vars open Namegen open Evd open Printer open Reductionops open Entries open Inductiveops -open Environ open Tacmach.New open Clenv open Declare open Tacticals.New open Tactics open Decl_kinds -open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let no_inductive_inconstr env sigma constr = (str "Cannot recognize an inductive predicate in " ++ - pr_lconstr_env env sigma constr ++ + pr_leconstr_env env sigma constr ++ str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++ spc () ++ str "or of the type of constructors" ++ spc () ++ str "is hidden by constant definitions.") @@ -114,13 +118,13 @@ let max_prefix_sign lid sign = | id::l -> snd (max_rec (id, sign_prefix id sign) l) *) let rec add_prods_sign env sigma t = - match kind_of_term (whd_all env sigma t) with + match EConstr.kind sigma (whd_all env sigma t) with | Prod (na,c1,b) -> - let id = id_of_name_using_hdchar env t na in + let id = id_of_name_using_hdchar env sigma t na in let b'= subst1 (mkVar id) b in add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b' | LetIn (na,c1,t1,b) -> - let id = id_of_name_using_hdchar env t na in + let id = id_of_name_using_hdchar env sigma t na in let b'= subst1 (mkVar id) b in add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b' | _ -> (env,t) @@ -140,11 +144,11 @@ let rec add_prods_sign env sigma t = let compute_first_inversion_scheme env sigma ind sort dep_option = let indf,realargs = dest_ind_type ind in - let allvars = ids_of_context env in + let allvars = vars_of_env env in let p = next_ident_away (Id.of_string "P") allvars in let pty,goal = if dep_option then - let pty = make_arity env true indf sort in + let pty = make_arity env sigma true indf sort in let goal = mkProd (Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1])) @@ -152,11 +156,12 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = pty,goal else let i = mkAppliedInd ind in - let ivars = global_vars env i in + let ivars = global_vars env sigma i in let revargs,ownsign = fold_named_context (fun env d (revargs,hyps) -> - let id = get_id d in + let d = map_named_decl EConstr.of_constr d in + let id = NamedDecl.get_id d in if Id.List.mem id ivars then ((mkVar id)::revargs, Context.Named.add d hyps) else @@ -183,17 +188,17 @@ let inversion_scheme env sigma t sort dep_option inv_op = let ind = try find_rectype env sigma i with Not_found -> - errorlabstrm "inversion_scheme" (no_inductive_inconstr env sigma i) + user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i) in let (invEnv,invGoal) = compute_first_inversion_scheme env sigma ind sort dep_option in assert (List.subset - (global_vars env invGoal) + (global_vars env sigma invGoal) (ids_of_named_context (named_context invEnv))); (* - errorlabstrm "lemma_inversion" + user_err ~hdr:"lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in @@ -206,84 +211,91 @@ let inversion_scheme env sigma t sort dep_option inv_op = let ownSign = ref begin fold_named_context (fun env d sign -> - if mem_named_context_val (get_id d) global_named_context then sign + let d = map_named_decl EConstr.of_constr d in + if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in - let avoid = ref [] in - let { sigma=sigma } = Proof.V82.subgoals pf in - let sigma = Evd.nf_constraints sigma in + let avoid = ref Id.Set.empty in + let _,_,_,_,sigma = Proof.proof pf in + let sigma = Evd.minimize_universes sigma in let rec fill_holes c = - match kind_of_term c with + match EConstr.kind sigma c with | Evar (e,args) -> let h = next_ident_away (Id.of_string "H") !avoid in let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in - avoid := h::!avoid; + avoid := Id.Set.add h !avoid; ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign; applist (mkVar h, inst) - | _ -> Constr.map fill_holes c + | _ -> EConstr.map sigma fill_holes c in let c = fill_holes pfterm in (* warning: side-effect on ownSign *) let invProof = it_mkNamedLambda_or_LetIn c !ownSign in + let invProof = EConstr.Unsafe.to_constr invProof in let p = Evarutil.nf_evars_universes sigma invProof in - p, Evd.universe_context sigma + p, sigma -let add_inversion_lemma name env sigma t sort dep inv_op = - let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in - let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) - ~univs:(snd ctx) invProof in +let add_inversion_lemma ~poly name env sigma t sort dep inv_op = + let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in + let univs = + Evd.const_univ_entry ~poly sigma + in + let entry = definition_entry ~univs invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () (* inv_op = Inv (derives de complete inv. lemma) * inv_op = InvNoThining (derives de semi inversion lemma) *) -let add_inversion_lemma_exn na com comsort bool tac = +let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in - let evd = ref (Evd.from_env env) in - let c = Constrintern.interp_type_evars env evd com in - let sigma, sort = Pretyping.interp_sort !evd comsort in + let sigma = Evd.from_env env in + let sigma, c = Constrintern.interp_type_evars env sigma com in + let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in try - add_inversion_lemma na env sigma c sort bool tac + add_inversion_lemma ~poly na env sigma c sort bool tac with - | UserError ("Case analysis",s) -> (* Reference to Indrec *) - errorlabstrm "Inv needs Nodep Prop Set" s + | UserError (Some "Case analysis",s) -> (* Reference to Indrec *) + user_err ~hdr:"Inv needs Nodep Prop Set" s (* ================================= *) (* Applying a given inversion lemma *) (* ================================= *) -let lemInv id c gls = +let lemInv id c = + Proofview.Goal.enter begin fun gls -> try - let clause = mk_clenv_type_of gls c in - let clause = clenv_constrain_last_binding (mkVar id) clause in - Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls + let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in + let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in + Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false with | NoSuchBinding -> - errorlabstrm "" - (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma.")) + user_err + (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma.")) | UserError (a,b) -> - errorlabstrm "LemInv" + user_err ~hdr:"LemInv" (str "Cannot refine current goal with the lemma " ++ - pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c) + pr_leconstr_env (pf_env gls) (project gls) c) + end -let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id +let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id let lemInvIn id c ids = - 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 intros_replace_ids = let concl = Proofview.Goal.concl gl in - let nb_of_new_hyp = nb_prod concl - List.length ids in + let sigma = project gl in + let nb_of_new_hyp = nb_prod sigma concl - List.length ids in if nb_of_new_hyp < 1 then intros_replacing ids else (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)) in - ((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c))) + ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c)) (intros_replace_ids))) - end } + end let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id |