diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 385 |
1 files changed, 209 insertions, 176 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index b4c027382..26e4f01f2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -40,8 +40,10 @@ open Eqschemes open Locus open Locusops open Misctypes +open Sigma.Notations open Proofview.Notations open Unification +open Context.Named.Declaration (* Options *) @@ -70,14 +72,27 @@ let _ = declare_bool_option { optsync = true; optdepr = false; - optname = "injection left-to-right pattern order"; + optname = "injection left-to-right pattern order and clear by default when with introduction pattern"; optkey = ["Injection";"L2R";"Pattern";"Order"]; optread = (fun () -> !injection_pattern_l2r_order) ; optwrite = (fun b -> injection_pattern_l2r_order := b) } -(* Rewriting tactics *) +let injection_in_context = ref false + +let use_injection_in_context () = + !injection_in_context + && Flags.version_strictly_greater Flags.V8_5 + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "injection in context"; + optkey = ["Structural";"Injection"]; + optread = (fun () -> !injection_in_context) ; + optwrite = (fun b -> injection_in_context := b) } -let clear ids = Proofview.V82.tactic (clear ids) +(* Rewriting tactics *) let tclNOTSAMEGOAL tac = Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac)) @@ -158,7 +173,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let try_occ (evd', c') = Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'} in - let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_unif_flags eqclause in + let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = w_unify_to_subterm_all ~flags env eqclause.evd ((if l2r then c1 else c2),concl) @@ -242,12 +257,12 @@ let rewrite_keyed_unif_flags = { } let rewrite_elim with_evars frzevars cls c e = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { 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 (Proofview.Goal.sigma gl) flags c in + let flags = make_flags frzevars (Tacmach.New.project gl) flags c in general_elim_clause with_evars flags cls c e - end + end } (* Ad hoc asymmetric general_elim_clause *) let general_elim_clause with_evars frzevars cls rew elim = @@ -282,7 +297,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 begin fun gl -> + Proofview.Goal.enter { 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 @@ -294,7 +309,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. @@ -313,7 +328,7 @@ let jmeq_same_dom gl = function let rels, t = decompose_prod_assum t in let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in match decompose_app t with - | _, [dom1; _; dom2;_] -> is_conv env (Proofview.Goal.sigma gl) dom1 dom2 + | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2 | _ -> false (* find_elim determines which elimination principle is necessary to @@ -354,8 +369,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl = Logic.eq or Jmeq just before *) assert false in - let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - sigma, elim, Safe_typing.empty_private_constants + let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in + Sigma ((elim, Safe_typing.empty_private_constants), sigma, p) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -373,10 +388,10 @@ 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 = - Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) + let Sigma (elim, sigma, p) = + Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - sigma, elim, eff + Sigma ((elim, eff), sigma, p) | _ -> assert false let type_of_clause cls gl = match cls with @@ -384,17 +399,21 @@ 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.nf_enter begin fun gl -> - let isatomic = isProd (whd_zeta hdcncl) in + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let isatomic = isProd (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 c type_of_cls in - let (sigma,elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in - Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*> + let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in + let tac = + 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} - end + in + Sigma (tac, sigma, p) + end } let adjust_rewriting_direction args lft2rgt = match args with @@ -417,8 +436,8 @@ 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 begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { 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 let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in @@ -445,7 +464,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 @@ -507,9 +526,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 begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> do_hyps_atleastonce (ids gl) - end + end } in if cl.concl_occs == NoOccurrences then do_hyps else tclIFTHENTRYELSEMUST @@ -517,25 +536,25 @@ let general_rewrite_clause l2r with_evars ?tac c cl = do_hyps let apply_special_clear_request clear_flag f = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try - let sigma,(c,bl) = f env sigma in + let ((c, bl), sigma) = run_delayed env sigma f 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 begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let sigma,c = f env sigma in + let (c, sigma) = run_delayed env sigma f 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 () @@ -598,14 +617,14 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = | None -> Proofview.tclUNIT () | Some tac -> tclCOMPLETE tac in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { 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 let evd = - if unsafe then Some (Proofview.Goal.sigma gl) + if unsafe then Some (Tacmach.New.project gl) else - try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Proofview.Goal.sigma gl)) + try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl)) with Evarconv.UnableToUnify _ -> None in match evd with @@ -624,7 +643,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 @@ -702,8 +721,8 @@ let find_positions env sigma t1 t2 = then [(List.rev posn,t1,t2)] else [] in let rec findrec sorts posn t1 t2 = - let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in - let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in + let hd1,args1 = whd_all_stack env sigma t1 in + let hd2,args2 = whd_all_stack env sigma t2 in match (kind_of_term hd1, kind_of_term hd2) with | Construct (sp1,_), Construct (sp2,_) when Int.equal (List.length args1) (constructor_nallargs_env env sp1) @@ -841,7 +860,7 @@ let descend_then env sigma head dirn = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - mkCase (ci, p, head, Array.of_list brl))) + Inductiveops.make_case_or_project env indf ci p head (Array.of_list brl))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: @@ -856,13 +875,13 @@ let descend_then env sigma head dirn = *) -(* [construct_discriminator env dirn headval] - constructs a case-split on [headval], with the [dirn]-th branch - giving [True], and all the rest giving False. *) +(* [construct_discriminator env sigma dirn c ind special default]] + constructs a case-split on [c] of type [ind], with the [dirn]-th + branch giving [special], and all the rest giving [default]. *) -let construct_discriminator env sigma dirn c sort = +let build_selector env sigma dirn c ind special default = let IndType(indf,_) = - try find_rectype env sigma (get_type_of env sigma c) + try find_rectype env sigma ind with Not_found -> (* one can find Rel(k) in case of dependent constructors like T := c : (A:Set)A->T and a discrimination @@ -874,25 +893,29 @@ let construct_discriminator env sigma dirn c sort = dependent types.") in let (indp,_) = dest_ind_family indf in let ind, _ = check_privacy env indp in + let typ = Retyping.get_type_of env sigma default in let (mib,mip) = lookup_mind_specif env ind in - let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in let deparsign = make_arity_signature env true indf in - let p = it_mkLambda_or_LetIn (mkSort sort_0) deparsign in + let p = it_mkLambda_or_LetIn typ deparsign in let cstrs = get_constructors env indf in let build_branch i = - let endpt = if Int.equal i dirn then true_0 else false_0 in + let endpt = if Int.equal i dirn then special else default in it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in let brl = List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in mkCase (ci, p, c, Array.of_list brl) -let rec build_discriminator env sigma dirn c sort = function - | [] -> construct_discriminator env sigma dirn c sort +let rec build_discriminator env sigma dirn c = function + | [] -> + let ind = get_type_of env sigma c in + let true_0,false_0 = + build_coq_True(),build_coq_False() in + build_selector env sigma dirn c ind true_0 false_0 | ((sp,cnum),argnum)::l -> let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in - let subval = build_discriminator cnum_env sigma dirn newc sort l in + let subval = build_discriminator cnum_env sigma dirn newc l in kont subval (build_coq_False (),mkSort (Prop Null)) (* Note: discrimination could be more clever: if some elimination is @@ -907,7 +930,7 @@ let rec build_discriminator env sigma dirn c sort = function *) let gen_absurdity id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in let hyp_typ = pf_nf_evar gl hyp_typ in if is_empty_type hyp_typ @@ -915,7 +938,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 @@ -954,11 +977,11 @@ let apply_on_clause (f,t) clause = | _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in clenv_fchain ~with_univs:false argmv f_clause clause -let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = +let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let e = next_ident_away eq_baseid (ids_of_context env) in - let e_env = push_named (e,None,t) env in + let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in let discriminator = - build_discriminator e_env sigma dirn (mkVar e) sort cpath in + build_discriminator e_env sigma dirn (mkVar e) cpath in let sigma,(pf, absurd_term), eff = discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in let pf_ty = mkArrow eqn absurd_term in @@ -967,23 +990,21 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS eff <*> tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))] + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl gl in match find_positions env sigma t1 t2 with | Inr _ -> tclZEROMSG (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> - let sort = pf_apply get_type_of gl concl in - discr_positions env sigma u eq_clause cpath dirn sort - end + discr_positions env sigma u eq_clause cpath dirn + end } let onEquality with_evars tac (c,lbindc) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { 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 @@ -995,11 +1016,11 @@ 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.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.nf_enter { 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 match kind_of_term (hnf_constr env sigma ccl) with @@ -1009,7 +1030,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 @@ -1060,7 +1081,7 @@ let make_tuple env sigma (rterm,rty) lind = assert (dependent (mkRel lind) rty); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in - let (na,_,_) = lookup_rel lind env in + let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in (* Now [lind] is [mkRel 1] and we abstract on (na:a) *) @@ -1135,7 +1156,7 @@ let minimal_free_rels_rec env sigma = let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigdata = find_sigma_data env sort_of_ty in - let evdref = ref (Evd.create_goal_evar_defs sigma) in + let evdref = ref (Evd.clear_metas sigma) in let rec sigrec_clausal_form siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) @@ -1263,7 +1284,7 @@ let build_injector env sigma dflt c cpath = (* let try_delta_expand env sigma t = - let whdt = whd_betadeltaiota env sigma t in + let whdt = whd_all env sigma t in let rec hd_rec c = match kind_of_term c with | Construct _ -> whdt @@ -1278,7 +1299,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.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> try let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) @@ -1311,12 +1332,12 @@ let inject_if_homogenous_dependent_pair ty = onLastHyp (fun hyp -> tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar hyp]; - Proofview.V82.tactic (refine + Proofview.V82.tactic (Tacmach.refine (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) ])] 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 @@ -1331,7 +1352,7 @@ let simplify_args env sigma t = let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let e = next_ident_away eq_baseid (ids_of_context env) in - let e_env = push_named (e, None,t) env in + let e_env = push_named (LocalAssum (e,t)) env in let evdref = ref sigma in let filter (cpath, t1', t2') = try @@ -1353,13 +1374,13 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = tclZEROMSG (str "Failed to decompose the equality.") else Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) - (Proofview.tclBIND - (Proofview.Monad.List.map + (Tacticals.New.tclTHENFIRST + (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; - Proofview.V82.tactic (refine pf)]) - (if l2r then List.rev injectors else injectors)) - (fun _ -> tac (List.length injectors))) + Proofview.V82.tactic (Tacmach.refine pf)]) + (if l2r then List.rev injectors else injectors))) + (tac (List.length injectors))) let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1376,51 +1397,68 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = inject_at_positions env sigma l2r u eq_clause posns (tac (clenv_value eq_clause)) -let use_clear_hyp_by_default () = false - -let postInjEqTac clear_flag ipats c n = - match ipats with - | Some ipats -> - let clear_tac = - let dft = - use_injection_pattern_l2r_order () || use_clear_hyp_by_default () in - tclTRY (apply_clear_request clear_flag dft c) in - let intro_tac = - if use_injection_pattern_l2r_order () - then intro_patterns_bound_to n MoveLast ipats - else intro_patterns_to MoveLast ipats in - tclTHEN clear_tac intro_tac - | None -> tclIDTAC - -let injEq clear_flag ipats = - let l2r = - if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false +let get_previous_hyp_position id gl = + let rec aux dest = function + | [] -> raise (RefinerError (NoSuchHyp id)) + | d :: right -> + let hyp = Context.Named.Declaration.get_id d in + if Id.equal hyp id then dest else aux (MoveAfter hyp) right in - injEqThen (fun c i -> postInjEqTac clear_flag ipats c i) l2r - -let inj ipats with_evars clear_flag = onEquality with_evars (injEq clear_flag ipats) + aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + +let injEq ?(old=false) with_evars clear_flag ipats = + (* Decide which compatibility mode to use *) + let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with + | None when not old && use_injection_in_context () -> + Some [], true, true, true + | None -> None, false, false, false + | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in + (* Built the post tactic depending on compatibility mode *) + let post_tac c n = + match ipats_style with + | Some ipats -> + Proofview.Goal.enter { enter = begin fun gl -> + let destopt = match kind_of_term c with + | Var id -> get_previous_hyp_position id gl + | _ -> MoveLast in + let clear_tac = + tclTRY (apply_clear_request clear_flag dft_clear_flag c) in + (* Try should be removal if dependency were treated *) + let intro_tac = + if bounded_intro + 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 } + | None -> tclIDTAC in + injEqThen post_tac l2r + +let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats) let injClause ipats with_evars = function - | None -> onNegatedEquality with_evars (injEq None ipats) + | None -> onNegatedEquality with_evars (injEq with_evars None ipats) | Some c -> onInductionArg (inj ipats with_evars) c +let simpleInjClause with_evars = function + | None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None) + | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c + let injConcl = injClause None false None let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id))) let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = - Proofview.Goal.nf_enter begin fun gl -> - let sort = pf_apply get_type_of gl (Proofview.Goal.concl gl) in + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in match find_positions env sigma t1 t2 with | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u clause cpath dirn sort + discr_positions env sigma u clause cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) ntac (clenv_value clause) 0 | 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)) @@ -1430,13 +1468,13 @@ let dEq with_evars = dEqThen with_evars (fun clear_flag c x -> (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) -let intro_decompe_eq tac data cl = - Proofview.Goal.enter begin fun gl -> +let intro_decomp_eq tac data cl = + Proofview.Goal.enter { enter = begin fun gl -> let cl = pf_apply make_clenv_binding gl cl NoBindings in decompEqThen (fun _ -> tac) data cl - end + end } -let _ = declare_intro_decomp_eq intro_decompe_eq +let _ = declare_intro_decomp_eq intro_decomp_eq (* [subst_tuple_term dep_pair B] @@ -1485,6 +1523,7 @@ let decomp_tuple_term env 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 dep_pair1 typ in @@ -1509,7 +1548,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,body,expected_goal + Sigma.Unsafe.of_pair ((body, expected_goal), sigma) (* Like "replace" but decompose dependent equalities *) (* i.e. if equality is "exists t v = exists u w", and goal is "phi(t,u)", *) @@ -1517,34 +1556,42 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* on for further iterated sigma-tuples *) let cutSubstInConcl l2r eqn = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_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 = pf_apply subst_tuple_term gl e1 e2 typ in + let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in + let tac = tclTHENFIRST (tclTHENLIST [ - (Proofview.Unsafe.tclEVARS sigma); (change_concl typ); (* Put in pattern form *) (replace_core onConcl l2r eqn) ]) (change_concl expected) (* Put in normalized form *) - end + in + Sigma (tac, sigma, p) + end } let cutSubstInHyp l2r eqn id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_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 = pf_apply subst_tuple_term gl e1 e2 typ in - tclTHENFIRST + let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in + let tac = + tclTHENFIRST (tclTHENLIST [ - (Proofview.Unsafe.tclEVARS sigma); (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)) - end + in + Sigma (tac, sigma, p) + end } let try_rewrite tac = Proofview.tclORELSE tac begin function (e, info) -> match e with @@ -1566,11 +1613,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 begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let eq = pf_apply get_type_of gl c in tclTHENS (cutSubstClause l2r eq cls) - [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)] - end + [Proofview.tclUNIT (); exact_no_check c] + end } let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls) let rewriteInHyp l2r c id = rewriteClause l2r c (Some id) @@ -1595,7 +1642,7 @@ user = raise user error specific to rewrite (**********************************************************************) (* Substitutions tactics (JCF) *) -let regular_subst_tactic = ref false +let regular_subst_tactic = ref true let _ = declare_bool_option @@ -1606,26 +1653,6 @@ let _ = optread = (fun () -> !regular_subst_tactic); optwrite = (:=) regular_subst_tactic } -let unfold_body x = - Proofview.Goal.enter begin fun gl -> - (** We normalize the given hypothesis immediately. *) - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let (_, xval, _) = Context.lookup_named x hyps in - let xval = match xval with - | None -> errorlabstrm "unfold_body" - (pr_id x ++ str" is not a defined hypothesis.") - | Some xval -> pf_nf_evar gl xval - in - afterHyp x begin fun aft -> - let hl = List.fold_right (fun (y,yval,_) cl -> (y,InHyp) :: cl) aft [] in - let xvar = mkVar x in - let rfun _ _ c = replace_term xvar xval c in - let reducth h = Proofview.V82.tactic (fun gl -> reduct_in_hyp rfun h gl) in - let reductc = Proofview.V82.tactic (fun gl -> reduct_in_concl (rfun, DEFAULTcast) gl) in - tclTHENLIST [tclMAP reducth hl; reductc] - end - end - let restrict_to_eq_and_identity eq = (* compatibility *) if not (is_global glob_eq eq) && not (is_global glob_identity eq) @@ -1634,12 +1661,17 @@ let restrict_to_eq_and_identity eq = (* compatibility *) exception FoundHyp of (Id.t * constr * bool) (* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *) -let is_eq_x gl x (id,_,c) = +let is_eq_x gl x d = + let id = get_id d in try - let c = pf_nf_evar gl c in + let is_var id c = match kind_of_term c with + | Var id' -> Id.equal id id' + | _ -> false + in + let c = pf_nf_evar gl (get_type d) in let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in - if (Term.eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true)); - if (Term.eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false)) + if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true)); + if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false)) with Constr_matching.PatternMatchingFailure -> () @@ -1647,18 +1679,19 @@ let is_eq_x gl x (id,_,c) = erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in (* The set of hypotheses using x *) let dephyps = - List.rev (pi3 (List.fold_right (fun (id,b,_ as dcl) (dest,deps,allhyps) -> + List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> + let id = get_id dcl in if not (Id.equal id hyp) && List.exists (fun y -> occur_var_in_decl env y dcl) deps then let id_dest = if !regular_subst_tactic then dest else MoveLast in - (dest,(if b = None then deps else id::deps), (id_dest,id)::allhyps) + (dest,id::deps,(id_dest,id)::allhyps) else (MoveBefore id,deps,allhyps)) hyps @@ -1674,35 +1707,33 @@ 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 begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in - let (_,xval,_) = pf_get_hyp x gl in + let xval = pf_get_hyp x gl |> get_value in (* If x has a body, simply replace x with body and clear x *) if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) else - (* x is a variable: *) - let varx = mkVar x in (* Find a non-recursive definition for x *) let res = try (** [is_eq_x] ensures nf_evar on its side *) let hyps = Proofview.Goal.hyps gl in - let test hyp _ = is_eq_x gl varx hyp in - Context.fold_named_context test ~init:() hyps; + let test hyp _ = is_eq_x gl x hyp in + Context.Named.fold_outside test ~init:() hyps; errorlabstrm "Subst" (str "Cannot find any non-recursive equality over " ++ pr_id x ++ str".") with FoundHyp res -> res in subst_one dep_proof_ok x res - end + end } let subst_gen dep_proof_ok ids = - tclTHEN Proofview.V82.nf_evar_goals (tclMAP (subst_one_var dep_proof_ok) ids) + tclMAP (subst_one_var dep_proof_ok) ids (* For every x, look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite it everywhere, and erase hyp and x; proceed by generalizing @@ -1730,16 +1761,16 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in - let select_equation_name (hyp,_,c) = + let select_equation_name decl = try - let lbeq,u,(_,x,y) = find_eq_data_decompose c in + let lbeq,u,(_,x,y) = find_eq_data_decompose (get_type decl) in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match kind_of_term x, kind_of_term y with | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> - Some hyp + Some (get_id decl) | _, Var z when not (is_evaluable env (EvalVarRef z)) -> - Some hyp + Some (get_id decl) | _ -> None with Constr_matching.PatternMatchingFailure -> None @@ -1750,10 +1781,10 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* Second step: treat equations *) let process hyp = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let find_eq_data_decompose = find_eq_data_decompose gl in - let (_,_,c) = pf_get_hyp hyp gl in + let c = pf_get_hyp hyp gl |> get_type in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else @@ -1764,19 +1795,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.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { 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.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let find_eq_data_decompose = find_eq_data_decompose gl in let test (_,c) = try @@ -1793,7 +1824,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 *) @@ -1821,18 +1852,20 @@ let cond_eq_term c t gl = let rewrite_assumption_cond cond_eq_term cl = let rec arec hyps gl = match hyps with | [] -> error "No such assumption." - | (id,_,t) ::rest -> + | hyp ::rest -> + let id = get_id hyp in begin try - let dir = cond_eq_term t gl in + let dir = cond_eq_term (get_type hyp) gl in general_rewrite_clause dir false (mkVar id,NoBindings) cl with | Failure _ | UserError _ -> arec rest gl end in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in 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 *) |