aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/equality.ml')
-rw-r--r--tactics/equality.ml161
1 files changed, 74 insertions, 87 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d64cc38ef..05c5cd5ec 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -40,7 +40,6 @@ open Eqschemes
open Locus
open Locusops
open Misctypes
-open Sigma.Notations
open Proofview.Notations
open Unification
open Context.Named.Declaration
@@ -254,16 +253,16 @@ let rewrite_keyed_unif_flags = {
}
let rewrite_elim with_evars frzevars cls c e =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let flags = if Unification.is_keyed_unification ()
then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in
let flags = make_flags frzevars (Tacmach.New.project gl) flags c in
general_elim_clause with_evars flags cls c e
- end }
+ end
let tclNOTSAMEGOAL tac =
let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let sigma = project gl in
let ev = goal gl in
tac >>= fun () ->
@@ -278,7 +277,7 @@ let tclNOTSAMEGOAL tac =
tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.")
else
Proofview.tclUNIT ()
- end }
+ end
(* Ad hoc asymmetric general_elim_clause *)
let general_elim_clause with_evars frzevars cls rew elim =
@@ -313,7 +312,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
(general_elim_clause with_evars frzevars cls c elim))
tac
in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let instantiate_lemma concl =
if not all then instantiate_lemma gl c t l l2r concl
else instantiate_lemma_all frzevars gl c t l l2r concl
@@ -325,7 +324,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
let cs = instantiate_lemma typ in
if firstonly then tclFIRST (List.map try_clause cs)
else tclMAP try_clause cs
- end }
+ end
(* The next function decides in particular whether to try a regular
rewrite or a generalized rewrite.
@@ -387,9 +386,9 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
Logic.eq or Jmeq just before *)
assert false
in
- let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+ let (sigma, elim) = fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
let elim = EConstr.of_constr elim in
- Sigma ((elim, Safe_typing.empty_private_constants), sigma, p)
+ (sigma, (elim, Safe_typing.empty_private_constants))
else
let scheme_name = match dep, lft2rgt, inccl with
(* Non dependent case *)
@@ -407,11 +406,11 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
| Ind (ind,u) ->
let c, eff = find_scheme scheme_name ind in
(* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
- let Sigma (elim, sigma, p) =
- Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
+ let (sigma, elim) =
+ fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
in
let elim = EConstr.of_constr elim in
- Sigma ((elim, eff), sigma, p)
+ (sigma, (elim, eff))
| _ -> assert false
let type_of_clause cls gl = match cls with
@@ -419,21 +418,19 @@ let type_of_clause cls gl = match cls with
| Some id -> pf_get_hyp_typ id gl
let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
- Proofview.Goal.s_enter { s_enter = begin fun gl ->
- let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+ Proofview.Goal.enter begin fun gl ->
+ let evd = Proofview.Goal.sigma gl in
let isatomic = isProd evd (whd_zeta evd hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
let type_of_cls = type_of_clause cls gl in
let dep = dep_proof_ok && dep_fun evd c type_of_cls in
- let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
- let tac =
+ let (sigma, (elim, effs)) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
+ Proofview.Unsafe.tclEVARS sigma <*>
Proofview.tclEFFECTS effs <*>
general_elim_clause with_evars frzevars tac cls c t l
(match lft2rgt with None -> false | Some b -> b)
{elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
- in
- Sigma (tac, sigma, p)
- end }
+ end
let adjust_rewriting_direction args lft2rgt =
match args with
@@ -456,7 +453,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
if occs != AllOccurrences then (
rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
else
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let ctype = get_type_of env sigma c in
@@ -485,7 +482,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
| None -> Proofview.tclZERO ~info e
(* error "The provided term does not end with an equality or a declared rewrite relation." *)
end
- end }
+ end
let general_rewrite_ebindings =
general_rewrite_ebindings_clause None
@@ -547,9 +544,9 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
let ids_of_hyps = pf_ids_of_hyps gl in
Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
do_hyps_atleastonce (ids gl)
- end }
+ end
in
if cl.concl_occs == NoOccurrences then do_hyps else
tclIFTHENTRYELSEMUST
@@ -557,25 +554,25 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
do_hyps
let apply_special_clear_request clear_flag f =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
try
- let ((c, bl), sigma) = run_delayed env sigma f in
+ let (sigma, (c, bl)) = f env sigma in
apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
with
e when catchable_exception e -> tclIDTAC
- end }
+ end
let general_multi_rewrite with_evars l cl tac =
let do1 l2r f =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
- let (c, sigma) = run_delayed env sigma f in
+ let (sigma, c) = f env sigma in
tclWITHHOLES with_evars
(general_rewrite_clause l2r with_evars ?tac c cl) sigma
- end }
+ end
in
let rec doN l2r c = function
| Precisely n when n <= 0 -> Proofview.tclUNIT ()
@@ -638,7 +635,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
| None -> Proofview.tclUNIT ()
| Some tac -> tclCOMPLETE tac
in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let get_type_of = pf_apply get_type_of gl in
let t1 = get_type_of c1
and t2 = get_type_of c2 in
@@ -664,7 +661,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
tclTHEN (apply sym) assumption;
try_prove_eq
])
- end }
+ end
let replace c1 c2 =
replace_using_leibniz onConcl c2 c1 false false None
@@ -934,13 +931,9 @@ let build_selector env sigma dirn c ind special default =
let ci = make_case_info env ind RegularStyle in
sigma, mkCase (ci, p, c, Array.of_list brl)
-let new_global sigma gr =
- let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
- in Sigma.to_evar_map sigma, c
-
-let build_coq_False sigma = new_global sigma (build_coq_False ())
-let build_coq_True sigma = new_global sigma (build_coq_True ())
-let build_coq_I sigma = new_global sigma (build_coq_I ())
+let build_coq_False sigma = Evarutil.new_global sigma (build_coq_False ())
+let build_coq_True sigma = Evarutil.new_global sigma (build_coq_True ())
+let build_coq_I sigma = Evarutil.new_global sigma (build_coq_I ())
let rec build_discriminator env sigma dirn c = function
| [] ->
@@ -967,7 +960,7 @@ let rec build_discriminator env sigma dirn c = function
*)
let gen_absurdity id =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
if is_empty_type sigma hyp_typ
@@ -975,7 +968,7 @@ let gen_absurdity id =
simplest_elim (mkVar id)
else
tclZEROMSG (str "Not the negation of an equality.")
- end }
+ end
(* Precondition: eq is leibniz equality
@@ -1032,17 +1025,17 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
match find_positions env sigma ~no_discr:false t1 t2 with
| Inr _ ->
tclZEROMSG (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
discr_positions env sigma u eq_clause cpath dirn
- end }
+ end
let onEquality with_evars tac (c,lbindc) =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let type_of = pf_unsafe_type_of gl in
let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
let t = type_of c in
@@ -1054,10 +1047,10 @@ let onEquality with_evars tac (c,lbindc) =
tclTHEN
(Proofview.Unsafe.tclEVARS eq_clause'.evd)
(tac (eq,eqn,eq_args) eq_clause')
- end }
+ end
let onNegatedEquality with_evars tac =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let ccl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
@@ -1068,7 +1061,7 @@ let onNegatedEquality with_evars tac =
onEquality with_evars tac (mkVar id,NoBindings)))
| _ ->
tclZEROMSG (str "Not a negated primitive equality.")
- end }
+ end
let discrSimpleClause with_evars = function
| None -> onNegatedEquality with_evars discrEq
@@ -1327,7 +1320,7 @@ let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
let inject_if_homogenous_dependent_pair ty =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
try
let sigma = Tacmach.New.project gl in
let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
@@ -1367,7 +1360,7 @@ let inject_if_homogenous_dependent_pair ty =
])]
with Exit ->
Proofview.tclUNIT ()
- end }
+ end
(* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it
expands then only when the whdnf has a constructor of an inductive type
@@ -1451,7 +1444,7 @@ let injEq ?(old=false) with_evars clear_flag ipats =
let post_tac c n =
match ipats_style with
| Some ipats ->
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
let destopt = match EConstr.kind sigma c with
| Var id -> get_previous_hyp_position id gl
@@ -1464,7 +1457,7 @@ let injEq ?(old=false) with_evars clear_flag ipats =
then intro_patterns_bound_to with_evars n destopt ipats
else intro_patterns_to with_evars destopt ipats in
tclTHEN clear_tac intro_tac
- end }
+ end
| None -> tclIDTAC in
injEqThen post_tac l2r
@@ -1482,7 +1475,7 @@ let injConcl = injClause None false None
let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
match find_positions env sigma ~no_discr:false t1 t2 with
@@ -1493,7 +1486,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
| Inr posns ->
inject_at_positions env sigma true u clause posns
(ntac (clenv_value clause))
- end }
+ end
let dEqThen with_evars ntac = function
| None -> onNegatedEquality with_evars (decompEqThen (ntac None))
@@ -1504,10 +1497,10 @@ let dEq with_evars =
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
let intro_decomp_eq tac data (c, t) =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
decompEqThen (fun _ -> tac) data cl
- end }
+ end
let _ = declare_intro_decomp_eq intro_decomp_eq
@@ -1558,7 +1551,6 @@ let decomp_tuple_term env sigma c t =
in decomprec (mkRel 1) c t
let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
- let sigma = Sigma.to_evar_map sigma in
let typ = get_type_of env sigma dep_pair1 in
(* We find all possible decompositions *)
let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
@@ -1583,7 +1575,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
(* Retype to get universes right *)
let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
let sigma, _ = Typing.type_of env sigma body in
- Sigma.Unsafe.of_pair ((body, expected_goal), sigma)
+ (sigma, (body, expected_goal))
(* Like "replace" but decompose dependent equalities *)
(* i.e. if equality is "exists t v = exists u w", and goal is "phi(t,u)", *)
@@ -1591,42 +1583,38 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
(* on for further iterated sigma-tuples *)
let cutSubstInConcl l2r eqn =
- Proofview.Goal.s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
let typ = pf_concl gl in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
- let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
- let tac =
- tclTHENFIRST
+ let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
+ tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (tclTHENFIRST
(tclTHENLIST [
(change_concl typ); (* Put in pattern form *)
(replace_core onConcl l2r eqn)
])
- (change_concl expected) (* Put in normalized form *)
- in
- Sigma (tac, sigma, p)
- end }
+ (change_concl expected)) (* Put in normalized form *)
+ end
let cutSubstInHyp l2r eqn id =
- Proofview.Goal.s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
let typ = pf_get_hyp_typ id gl in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
- let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
- let tac =
- tclTHENFIRST
+ let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
+ tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (tclTHENFIRST
(tclTHENLIST [
(change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
(replace_core (onHyp id) l2r eqn)
])
- (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))
- in
- Sigma (tac, sigma, p)
- end }
+ (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)))
+ end
let try_rewrite tac =
Proofview.tclORELSE tac begin function (e, info) -> match e with
@@ -1648,11 +1636,11 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
let substClause l2r c cls =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let eq = pf_apply get_type_of gl c in
tclTHENS (cutSubstClause l2r eq cls)
[Proofview.tclUNIT (); exact_no_check c]
- end }
+ end
let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
@@ -1713,7 +1701,7 @@ let is_eq_x gl x d =
erase hyp and x; proceed by generalizing all dep hyps *)
let subst_one dep_proof_ok x (hyp,rhs,dir) =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
@@ -1742,13 +1730,13 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
else
[Proofview.tclUNIT ()]) @
[tclTRY (clear [x; hyp])])
- end }
+ end
(* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite
it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *)
let subst_one_var dep_proof_ok x =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let gl = Proofview.Goal.assume gl in
let decl = pf_get_hyp x gl in
(* If x has a body, simply replace x with body and clear x *)
@@ -1765,7 +1753,7 @@ let subst_one_var dep_proof_ok x =
str".")
with FoundHyp res -> res in
subst_one dep_proof_ok x res
- end }
+ end
let subst_gen dep_proof_ok ids =
tclMAP (subst_one_var dep_proof_ok) ids
@@ -1818,7 +1806,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
(* Second step: treat equations *)
let process hyp =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let gl = Proofview.Goal.assume gl in
let sigma = project gl in
let env = Proofview.Goal.env gl in
@@ -1834,19 +1822,19 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
| _ ->
Proofview.tclUNIT ()
- end }
+ end
in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let ids = find_equations gl in
tclMAP process ids
- end }
+ end
else
(* Old implementation, not able to manage configurations like a=b, a=t,
or situations like "a = S b, b = S a", or also accidentally unfolding
let-ins *)
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
let find_eq_data_decompose = find_eq_data_decompose gl in
let test (_,c) =
@@ -1865,7 +1853,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let ids = List.map_filter test hyps in
let ids = List.uniquize ids in
subst_gen flags.rewrite_dependent_proof ids
- end }
+ end
(* Rewrite the first assumption for which a condition holds
and gives the direction of the rewrite *)
@@ -1902,11 +1890,10 @@ let rewrite_assumption_cond cond_eq_term cl =
with | Failure _ | UserError _ -> arec rest gl
end
in
- Proofview.Goal.enter { enter = begin fun gl ->
- let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in
+ Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
arec hyps gl
- end }
+ end
(* Generalize "subst x" to substitution of subterm appearing as an
equation in the context, but not clearing the hypothesis *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 15:29:30 +0000