aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/equality.ml31
-rw-r--r--tactics/equality.mli4
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/hiddentac.ml8
-rw-r--r--tactics/inv.ml13
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/setoid_replace.ml2
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--tactics/tactics.ml81
-rw-r--r--tactics/tactics.mli21
11 files changed, 105 insertions, 65 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index c450bf622..aceba6e25 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -69,7 +69,7 @@ let e_constructor_tac boundopt i lbind gl =
| None -> ()
end;
let cons = mkConstruct (ith_constructor_of_inductive mind i) in
- let apply_tac = eapply_with_bindings (cons,lbind) in
+ let apply_tac = eapply_with_ebindings (cons,lbind) in
(tclTHENLIST [convert_concl_no_check redcl DEFAULTcast
; intros; apply_tac]) gl
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d46b6f142..8c8716110 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -81,7 +81,7 @@ let elimination_sort_of_clause = function
else back to the old approach
*)
-let general_rewrite_bindings_clause cls lft2rgt (c,l) with_evars gl =
+let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl =
let ctype = pf_apply get_type_of gl c in
(* A delta-reduction would be here too strong, since it would
break search for a defined setoid relation in head position. *)
@@ -111,13 +111,20 @@ let general_rewrite_bindings_clause cls lft2rgt (c,l) with_evars gl =
in
general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
-let general_rewrite_bindings = general_rewrite_bindings_clause None
-let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings) false
+let general_rewrite_ebindings =
+ general_rewrite_ebindings_clause None
+let general_rewrite_bindings l2r (c,bl) =
+ general_rewrite_ebindings_clause None l2r (c,inj_ebindings bl)
-let general_rewrite_bindings_in l2r id =
- general_rewrite_bindings_clause (Some id) l2r
+let general_rewrite l2r c =
+ general_rewrite_bindings l2r (c,NoBindings) false
+
+let general_rewrite_ebindings_in l2r id =
+ general_rewrite_ebindings_clause (Some id) l2r
+let general_rewrite_bindings_in l2r id (c,bl) =
+ general_rewrite_ebindings_clause (Some id) l2r (c,inj_ebindings bl)
let general_rewrite_in l2r id c =
- general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
+ general_rewrite_ebindings_clause (Some id) l2r (c,NoBindings)
let general_multi_rewrite l2r with_evars c cl =
if cl.concl_occs <> [] then
@@ -130,12 +137,12 @@ let general_multi_rewrite l2r with_evars c cl =
| [] -> tclIDTAC
| ((_,id),_) :: l ->
tclTHENFIRST
- (general_rewrite_bindings_in l2r id c with_evars)
+ (general_rewrite_ebindings_in l2r id c with_evars)
(do_hyps l)
in
if not cl.onconcl then do_hyps l else
tclTHENFIRST
- (general_rewrite_bindings l2r c with_evars)
+ (general_rewrite_ebindings l2r c with_evars)
(do_hyps l)
| None ->
(* Otherwise, if we are told to rewrite in all hypothesis via the
@@ -144,7 +151,7 @@ let general_multi_rewrite l2r with_evars c cl =
| [] -> (fun gl -> error "Nothing to rewrite.")
| id :: l ->
tclIFTHENTRYELSEMUST
- (general_rewrite_bindings_in l2r id c with_evars)
+ (general_rewrite_ebindings_in l2r id c with_evars)
(do_hyps_atleastonce l)
in
let do_hyps gl =
@@ -156,14 +163,14 @@ let general_multi_rewrite l2r with_evars c cl =
in
if not cl.onconcl then do_hyps else
tclIFTHENTRYELSEMUST
- (general_rewrite_bindings l2r c with_evars)
+ (general_rewrite_ebindings l2r c with_evars)
do_hyps
(* Conditional rewriting, the success of a rewriting is related
to the resolution of the conditions by a given tactic *)
let conditional_rewrite lft2rgt tac (c,bl) =
- tclTHENSFIRSTn (general_rewrite_bindings lft2rgt (c,bl) false)
+ tclTHENSFIRSTn (general_rewrite_ebindings lft2rgt (c,bl) false)
[|tclIDTAC|] (tclCOMPLETE tac)
let rewriteLR_bindings = general_rewrite_bindings true
@@ -176,7 +183,7 @@ let rewriteLRin_bindings = general_rewrite_bindings_in true
let rewriteRLin_bindings = general_rewrite_bindings_in false
let conditional_rewrite_in lft2rgt id tac (c,bl) =
- tclTHENSFIRSTn (general_rewrite_bindings_in lft2rgt id (c,bl) false)
+ tclTHENSFIRSTn (general_rewrite_ebindings_in lft2rgt id (c,bl) false)
[|tclIDTAC|] (tclCOMPLETE tac)
let rewriteRL_clause = function
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 9254e5f0d..36fc99594 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -26,7 +26,7 @@ open Genarg
(*i*)
val general_rewrite_bindings :
- bool -> constr with_ebindings -> evars_flag -> tactic
+ bool -> constr with_bindings -> evars_flag -> tactic
val general_rewrite :
bool -> constr -> tactic
@@ -42,7 +42,7 @@ val rewriteRL : constr -> tactic
(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
val general_rewrite_bindings_in :
- bool -> identifier -> constr with_ebindings -> evars_flag -> tactic
+ bool -> identifier -> constr with_bindings -> evars_flag -> tactic
val general_rewrite_in :
bool -> identifier -> constr -> evars_flag -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ea33ead5d..d51d17aaf 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -323,7 +323,7 @@ let step left x tac =
let l =
List.map (fun lem ->
tclTHENLAST
- (apply_with_bindings (lem, ImplicitBindings [Evd.empty,x]))
+ (apply_with_bindings (lem, ImplicitBindings [x]))
tac)
!(if left then transitivity_left_table else transitivity_right_table)
in
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 85a85083e..b6c8f2ef8 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -41,7 +41,7 @@ let h_vm_cast_no_check c =
abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c)
let h_apply ev cb =
abstract_tactic (TacApply (ev,inj_open_wb cb))
- (apply_with_bindings_gen ev cb)
+ (apply_with_ebindings_gen ev cb)
let h_elim cb cbo =
abstract_tactic (TacElim (inj_open_wb cb,option_map inj_open_wb cbo))
(elim cb cbo)
@@ -96,9 +96,9 @@ let h_rename id1 id2 =
abstract_tactic (TacRename (id1,id2)) (rename_hyp id1 id2)
(* Constructors *)
-let h_left l = abstract_tactic (TacLeft l) (left l)
-let h_right l = abstract_tactic (TacLeft l) (right l)
-let h_split l = abstract_tactic (TacSplit (false,l)) (split l)
+let h_left l = abstract_tactic (TacLeft l) (left_with_ebindings l)
+let h_right l = abstract_tactic (TacLeft l) (right_with_ebindings l)
+let h_split l = abstract_tactic (TacSplit (false,l)) (split_with_ebindings l)
(* Moved to tacinterp because of dependence in Tacinterp.interp
let h_any_constructor t =
abstract_tactic (TacAnyConstructor t) (any_constructor t)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 47b8ca64b..6a9dc632b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -441,15 +441,14 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
tac
-let raw_inversion inv_kind indbinding id status names gl =
+let raw_inversion inv_kind id status names gl =
let env = pf_env gl and sigma = project gl in
let c = mkVar id in
let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
let indclause = mk_clenv_from gl (c,t) in
- let indclause' = clenv_constrain_with_bindings indbinding indclause in
- let newc = clenv_value indclause' in
- let ccl = clenv_type indclause' in
- check_no_metas indclause' ccl;
+ let newc = clenv_value indclause in
+ let ccl = clenv_type indclause in
+ check_no_metas indclause ccl;
let IndType (indf,realargs) =
try find_rectype env sigma ccl
with Not_found ->
@@ -503,13 +502,13 @@ let wrap_inv_error id = function
| UserError ("Case analysis",s) -> errorlabstrm "Inv needs Nodep Prop Set" s
| UserError("mind_specif_of_mind",_) -> not_inductive_here id
| UserError (a,b) -> errorlabstrm "Inv" b
- | Invalid_argument (*"it_list2"*) "List.fold_left2" -> dep_prop_prop_message id
+ | Invalid_argument "List.fold_left2" -> dep_prop_prop_message id
| Not_found -> errorlabstrm "Inv" (not_found_message [id])
| e -> raise e
(* The most general inversion tactic *)
let inversion inv_kind status names id gls =
- try (raw_inversion inv_kind [] id status names) gls
+ try (raw_inversion inv_kind id status names) gls
with e -> wrap_inv_error id e
(* Specializing it... *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1b308e298..f34c9e38d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -292,7 +292,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
let lemInv id c gls =
try
let clause = mk_clenv_type_of gls c in
- let clause = clenv_constrain_with_bindings [(-1,(Evd.empty,mkVar id))] clause in
+ let clause = clenv_constrain_last_binding (mkVar id) clause in
Clenvtac.res_pf clause ~allow_K:true gls
with
| UserError (a,b) ->
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 8fc95b408..1e70bf277 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1983,7 +1983,7 @@ let setoid_transitivity c gl =
| _ -> assert false
in
apply_with_bindings
- (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, (Evd.empty,c) ]) gl
+ (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
with
Optimize -> transitivity c gl
;;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 4aad135c6..f13897d1f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -324,7 +324,7 @@ let general_elim_then_using
let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
(* applying elimination_scheme just a little modified *)
let indclause = mk_clenv_from gl (c,t) in
- let indclause' = clenv_constrain_with_bindings indbindings indclause in
+ let indclause' = clenv_match_args indbindings indclause in
let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in
let indmv =
match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
@@ -345,7 +345,7 @@ let general_elim_then_using
error ("The elimination combinator " ^ name_elim ^ " is not known")
in
let elimclause' = clenv_fchain indmv elimclause indclause' in
- let elimclause' = clenv_constrain_with_bindings elimbindings elimclause' in
+ let elimclause' = clenv_match_args elimbindings elimclause' in
let branchsigns = compute_construtor_signatures isrec ity in
let brnames = compute_induction_names (Array.length branchsigns) allnames in
let after_tac ce i gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b042a8422..8b10913de 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -55,6 +55,23 @@ let rec nb_prod x =
| _ -> n
in count 0 x
+let inj_open c = (Evd.empty,c)
+
+let inj_occ (occ,c) = (occ,inj_open c)
+
+let inj_red_expr = function
+ | Simpl lo -> Simpl (option_map inj_occ lo)
+ | Fold l -> Fold (List.map inj_open l)
+ | Pattern l -> Pattern (List.map inj_occ l)
+ | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c)
+ -> c
+
+let inj_ebindings = function
+ | NoBindings -> NoBindings
+ | ImplicitBindings l -> ImplicitBindings (List.map inj_open l)
+ | ExplicitBindings l ->
+ ExplicitBindings (List.map (fun (l,id,c) -> (l,id,inj_open c)) l)
+
(*********************************************)
(* Tactics *)
(*********************************************)
@@ -527,7 +544,7 @@ let clenv_refine_in with_evars id clenv gl =
(* Resolution with missing arguments *)
-let apply_with_bindings_gen with_evars (c,lbind) gl =
+let apply_with_ebindings_gen with_evars (c,lbind) gl =
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
@@ -553,24 +570,20 @@ let apply_with_bindings_gen with_evars (c,lbind) gl =
else Clenvtac.res_pf clause gl in
try_apply thm_ty0
-let apply_with_bindings = apply_with_bindings_gen false
-let eapply_with_bindings = apply_with_bindings_gen true
+let apply_with_ebindings = apply_with_ebindings_gen false
+let eapply_with_ebindings = apply_with_ebindings_gen true
-let apply c = apply_with_bindings (c,NoBindings)
+let apply_with_bindings (c,bl) =
+ apply_with_ebindings (c,inj_ebindings bl)
-let inj_open c = (Evd.empty,c)
-
-let inj_occ (occ,c) = (occ,inj_open c)
+let eapply_with_bindings (c,bl) =
+ apply_with_ebindings_gen true (c,inj_ebindings bl)
-let inj_red_expr = function
- | Simpl lo -> Simpl (option_map inj_occ lo)
- | Fold l -> Fold (List.map inj_open l)
- | Pattern l -> Pattern (List.map inj_occ l)
- | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c)
- -> c
+let apply c =
+ apply_with_ebindings (c,NoBindings)
let apply_list = function
- | c::l -> apply_with_bindings (c,ImplicitBindings (List.map inj_open l))
+ | c::l -> apply_with_bindings (c,ImplicitBindings l)
| _ -> assert false
(* Resolution with no reduction on the type *)
@@ -713,6 +726,7 @@ let rec intros_clearing = function
let new_hyp mopt (c,lbind) g =
let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
+ let clause = clenv_unify_meta_types clause in
let (thd,tstack) = whd_stack (clenv_value clause) in
let nargs = List.length tstack in
let cut_pf =
@@ -720,7 +734,10 @@ let new_hyp mopt (c,lbind) g =
match mopt with
| Some m -> if m < nargs then list_firstn m tstack else tstack
| None -> tstack)
- in
+ in
+ if occur_meta cut_pf then
+ errorlabstrm "" (str "Cannot infer an instance for " ++
+ pr_name (meta_name clause.evd (List.hd (collect_metas cut_pf))));
(tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.evd))
(cut (pf_type_of g cut_pf)))
((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
@@ -744,21 +761,24 @@ let keep hyps gl =
(* Introduction tactics *)
(************************)
-let constructor_tac boundopt i lbind gl =
+let check_number_of_constructors expctdnumopt i nconstr =
+ if i=0 then error "The constructors are numbered starting from 1";
+ begin match expctdnumopt with
+ | Some n when n <> nconstr ->
+ error ("Not an inductive goal with "^
+ string_of_int n^plural n " constructor")
+ | _ -> ()
+ end;
+ if i > nconstr then error "Not enough constructors"
+
+let constructor_tac expctdnumopt i lbind gl =
let cl = pf_concl gl in
let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in
let nconstr =
Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
- if i=0 then error "The constructors are numbered starting from 1";
- if i > nconstr then error "Not enough constructors";
- begin match boundopt with
- | Some expctdnum ->
- if expctdnum <> nconstr then
- error "Not the expected number of constructors"
- | None -> ()
- end;
+ check_number_of_constructors expctdnumopt i nconstr;
let cons = mkConstruct (ith_constructor_of_inductive mind i) in
- let apply_tac = apply_with_bindings (cons,lbind) in
+ let apply_tac = apply_with_ebindings (cons,lbind) in
(tclTHENLIST
[convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
@@ -778,15 +798,20 @@ let any_constructor tacopt gl =
tclFIRST (List.map (fun i -> tclTHEN (one_constructor i NoBindings) t)
(interval 1 nconstr)) gl
-let left = constructor_tac (Some 2) 1
+let left_with_ebindings = constructor_tac (Some 2) 1
+let right_with_ebindings = constructor_tac (Some 2) 2
+let split_with_ebindings = constructor_tac (Some 1) 1
+
+let left l = left_with_ebindings (inj_ebindings l)
let simplest_left = left NoBindings
-let right = constructor_tac (Some 2) 2
+let right l = right_with_ebindings (inj_ebindings l)
let simplest_right = right NoBindings
-let split = constructor_tac (Some 1) 1
+let split l = split_with_ebindings (inj_ebindings l)
let simplest_split = split NoBindings
+
(********************************************)
(* Elimination tactics *)
(********************************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6b0f8413a..0c2024162 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -30,6 +30,7 @@ open Rawterm
val inj_open : constr -> open_constr
val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen
+val inj_ebindings : constr bindings -> open_constr bindings
(* Main tactics. *)
@@ -169,9 +170,11 @@ val bring_hyps : named_context -> tactic
val apply : constr -> tactic
val apply_without_reduce : constr -> tactic
val apply_list : constr list -> tactic
-val apply_with_bindings_gen : evars_flag -> constr with_ebindings -> tactic
-val apply_with_bindings : constr with_ebindings -> tactic
-val eapply_with_bindings : constr with_ebindings -> tactic
+val apply_with_ebindings_gen : evars_flag -> constr with_ebindings -> tactic
+val apply_with_bindings : constr with_bindings -> tactic
+val apply_with_ebindings : constr with_ebindings -> tactic
+val eapply_with_bindings : constr with_bindings -> tactic
+val eapply_with_ebindings : constr with_ebindings -> tactic
val cut_and_apply : constr -> tactic
@@ -271,11 +274,17 @@ val constructor_tac : int option -> int ->
open_constr bindings -> tactic
val one_constructor : int -> open_constr bindings -> tactic
val any_constructor : tactic option -> tactic
-val left : open_constr bindings -> tactic
+
+val left : constr bindings -> tactic
+val right : constr bindings -> tactic
+val split : constr bindings -> tactic
+
+val left_with_ebindings : open_constr bindings -> tactic
+val right_with_ebindings : open_constr bindings -> tactic
+val split_with_ebindings : open_constr bindings -> tactic
+
val simplest_left : tactic
-val right : open_constr bindings -> tactic
val simplest_right : tactic
-val split : open_constr bindings -> tactic
val simplest_split : tactic
(*s Logical connective tactics. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 23:22:17 +0000