From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- tactics/contradiction.ml | 63 ++++++++++++++++++++++++++++++++---------------- 1 file changed, 42 insertions(+), 21 deletions(-) (limited to 'tactics/contradiction.ml') diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 6eebf494..445a104d 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Term open Hipattern open Tactics open Coqlib open Reductionops open Misctypes +open Proofview.Notations +open Context.Named.Declaration (* Absurd *) @@ -22,53 +23,73 @@ let mk_absurd_proof t = mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|]))) let absurd c = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in + Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let sigma = Sigma.to_evar_map sigma in let j = Retyping.get_judgment_of env sigma c in let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in let t = j.Environ.utj_val in + let tac = Tacticals.New.tclTHENLIST [ - Proofview.Unsafe.tclEVARS sigma; elim_type (build_coq_False ()); Simple.apply (mk_absurd_proof t) - ] - end + ] in + Sigma.Unsafe.of_pair (tac, sigma) + end } let absurd c = absurd c (* Contradiction *) +let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 + (** [f] does not assume its argument to be [nf_evar]-ed. *) let filter_hyp f tac = let rec seek = function | [] -> Proofview.tclZERO Not_found - | (id,_,t)::rest when f t -> tac id + | d::rest when f (get_type d) -> tac (get_id d) | _::rest -> seek rest in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek hyps - end + end } let contradiction_context = - 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 rec seek_neg l = match l with | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") - | (id,_,typ)::rest -> - let typ = nf_evar sigma typ in - let typ = whd_betadeltaiota env sigma typ in + | d :: rest -> + let id = get_id d in + let typ = nf_evar sigma (get_type d) in + let typ = whd_all env sigma typ in if is_empty_type typ then simplest_elim (mkVar id) else match kind_of_term typ with | Prod (na,t,u) when is_empty_type u -> + let is_unit_or_eq = + if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type t + else None in + Tacticals.New.tclORELSE + (match is_unit_or_eq with + | Some _ -> + let hd,args = decompose_app t in + let (ind,_ as indu) = destInd hd in + let nparams = Inductiveops.inductive_nparams_env env ind in + let params = Util.List.firstn nparams args in + let p = applist ((mkConstructUi (indu,1)), params) in + (* Checking on the fly that it type-checks *) + simplest_elim (mkApp (mkVar id,[|p|])) + | None -> + Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type.")) (Proofview.tclORELSE - (Proofview.Goal.enter begin fun gl -> + (Proofview.Goal.enter { enter = begin fun gl -> let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in filter_hyp (fun typ -> is_conv_leq typ t) (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) - end) + end }) begin function (e, info) -> match e with | Not_found -> seek_neg rest | e -> Proofview.tclZERO ~info e @@ -77,18 +98,18 @@ let contradiction_context = in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek_neg hyps - end + end } let is_negation_of env sigma typ t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term (whd_all env sigma t) with | Prod (na,t,u) -> let u = nf_evar sigma u in is_empty_type u && is_conv_leq env sigma typ t | _ -> false let contradiction_term (c,lbind as cl) = - 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 env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in @@ -110,7 +131,7 @@ let contradiction_term (c,lbind as cl) = | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.") | e -> Proofview.tclZERO ~info e end - end + end } let contradiction = function | None -> Tacticals.New.tclTHEN intros contradiction_context -- cgit v1.2.3