summaryrefslogtreecommitdiff
path: root/tactics/leminv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/leminv.ml')
-rw-r--r--tactics/leminv.ml104
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 00:01:41 +0000