From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- tactics/contradiction.ml | 87 ++++++++++++++++++++++++------------------------ 1 file changed, 43 insertions(+), 44 deletions(-) (limited to 'tactics/contradiction.ml') diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 445a104d..c285f21e 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -1,82 +1,82 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* + Proofview.Goal.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 sigma, j = Coercion.inh_coerce_to_sort env sigma j in let t = j.Environ.utj_val in - let tac = + Proofview.Unsafe.tclEVARS sigma <*> + Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot -> + Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse -> Tacticals.New.tclTHENLIST [ - elim_type (build_coq_False ()); - Simple.apply (mk_absurd_proof t) - ] in - Sigma.Unsafe.of_pair (tac, sigma) - end } + elim_type coqfalse; + Simple.apply (mk_absurd_proof coqnot t) + ] + 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 - | d::rest when f (get_type d) -> tac (get_id d) + | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in - Proofview.Goal.enter { enter = begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + Proofview.Goal.enter begin fun gl -> + let hyps = Proofview.Goal.hyps gl in seek hyps - end } + end let contradiction_context = - 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 rec seek_neg l = match l with | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | d :: rest -> - let id = get_id d in - let typ = nf_evar sigma (get_type d) in + let id = NamedDecl.get_id d in + let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in - if is_empty_type typ then + if is_empty_type sigma 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 + else match EConstr.kind sigma typ with + | Prod (na,t,u) when is_empty_type sigma u -> + let is_unit_or_eq = match_with_unit_or_eq_type sigma t 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 hd,args = decompose_app sigma t in + let (ind,_ as indu) = destInd sigma 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 @@ -85,36 +85,35 @@ let contradiction_context = | None -> Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type.")) (Proofview.tclORELSE - (Proofview.Goal.enter { enter = begin fun gl -> + (Proofview.Goal.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 end) | _ -> seek_neg rest in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in seek_neg hyps - end } + end let is_negation_of env sigma typ t = - match kind_of_term (whd_all env sigma t) with + match EConstr.kind sigma (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 + is_empty_type sigma u && is_conv_leq env sigma typ t | _ -> false let contradiction_term (c,lbind as cl) = - Proofview.Goal.nf_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 type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in let _, ccl = splay_prod env sigma typ in - if is_empty_type ccl then + if is_empty_type sigma ccl then Tacticals.New.tclTHEN (elim false None cl None) (Tacticals.New.tclTRY assumption) @@ -122,7 +121,7 @@ let contradiction_term (c,lbind as cl) = Proofview.tclORELSE begin if lbind = NoBindings then - filter_hyp (is_negation_of env sigma typ) + filter_hyp (fun c -> is_negation_of env sigma typ c) (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) else Proofview.tclZERO Not_found @@ -131,7 +130,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