diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /tactics/leminv.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'tactics/leminv.ml')
-rw-r--r-- | tactics/leminv.ml | 104 |
1 files changed, 44 insertions, 60 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index bae81df7..f00ecf8f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -1,42 +1,36 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp +open Errors open Util open Names -open Nameops open Term +open Vars open Termops open Namegen -open Sign +open Context open Evd open Printer open Reductionops -open Declarations open Entries open Inductiveops open Environ -open Tacmach -open Proof_type -open Pfedit -open Evar_refiner +open Tacmach.New open Clenv open Declare -open Tacticals +open Tacticals.New open Tactics -open Inv -open Vernacexpr -open Safe_typing open Decl_kinds -let no_inductive_inconstr env constr = +let no_inductive_inconstr env sigma constr = (str "Cannot recognize an inductive predicate in " ++ - pr_lconstr_env env constr ++ + pr_lconstr_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.") @@ -146,7 +140,7 @@ 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 p = next_ident_away (id_of_string "P") allvars 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 @@ -161,7 +155,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let revargs,ownsign = fold_named_context (fun env (id,_,_ as d) (revargs,hyps) -> - if List.mem id ivars then + if Id.List.mem id ivars then ((mkVar id)::revargs,add_named_decl d hyps) else (revargs,hyps)) @@ -187,21 +181,24 @@ 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 i) + errorlabstrm "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 + (List.subset (global_vars env invGoal) (ids_of_named_context (named_context invEnv))); (* errorlabstrm "lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start [invEnv,invGoal] in - Proof.run_tactic env (Proofview.V82.tactic (tclTHEN intro (onLastHypId inv_op))) pf; + let pf = Proof.start (Evd.from_env ~ctx:(evar_universe_context sigma) invEnv) [invEnv,invGoal] in + let pf = + fst (Proof.run_tactic env ( + tclTHEN intro (onLastHypId inv_op)) pf) + in let pfterm = List.hd (Proof.partial_proof pf) in let global_named_context = Global.named_context () in let ownSign = ref begin @@ -216,7 +213,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let rec fill_holes c = match kind_of_term c with | Evar (e,args) -> - let h = next_ident_away (id_of_string "H") !avoid in + 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; ownSign := add_named_decl (h,None,ty) !ownSign; @@ -231,37 +228,21 @@ let inversion_scheme env sigma t sort dep_option inv_op = let add_inversion_lemma name env sigma t sort dep inv_op = let invProof = inversion_scheme env sigma t sort dep inv_op in - let _ = - declare_constant name - (DefinitionEntry - { const_entry_body = invProof; - const_entry_secctx = None; - const_entry_type = None; - const_entry_opaque = false }, - IsProof Lemma) - in () + let entry = definition_entry ~poly:true (*FIXME*) 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 inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op = - let pts = get_pftreestate() in - let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in - let gl = { it = List.nth gls (n-1) ; sigma=sigma } in - let t = - try pf_get_hyp_typ gl id - with Not_found -> Pretype_errors.error_var_not_found_loc loc id in - let env = pf_env gl and sigma = project gl in - add_inversion_lemma na env sigma t sort dep_option inv_op - let add_inversion_lemma_exn na com comsort bool tac = - let env = Global.env () and sigma = Evd.empty in - let c = Constrintern.interp_type sigma env com in - let sort = Pretyping.interp_sort comsort in + let env = Global.env () and evd = ref Evd.empty in + let c = Constrintern.interp_type_evars env evd com in + let sigma, sort = Pretyping.interp_sort !evd comsort in try add_inversion_lemma na env sigma c sort bool tac with - | UserError ("Case analysis",s) -> (* référence à Indrec *) + | UserError ("Case analysis",s) -> (* Reference to Indrec *) errorlabstrm "Inv needs Nodep Prop Set" s (* ================================= *) @@ -272,7 +253,7 @@ let lemInv id c gls = try let clause = mk_clenv_type_of gls c in let clause = clenv_constrain_last_binding (mkVar id) clause in - Clenvtac.res_pf clause ~flags:Unification.elim_flags gls + Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls with | NoSuchBinding -> errorlabstrm "" @@ -280,21 +261,24 @@ let lemInv id c gls = | UserError (a,b) -> errorlabstrm "LemInv" (str "Cannot refine current goal with the lemma " ++ - pr_lconstr_env (Global.env()) c) - -let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id - -let lemInvIn id c ids gls = - let hyps = List.map (pf_get_hyp gls) ids in - let intros_replace_ids gls = - let nb_of_new_hyp = nb_prod (pf_concl gls) - List.length ids in - if nb_of_new_hyp < 1 then - intros_replacing ids gls - else - (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)) gls - in - ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c)) - (intros_replace_ids)) gls) + pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c) + +let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id + +let lemInvIn id c ids = + Proofview.Goal.nf_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 + 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))) + (intros_replace_ids))) + end let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id |