diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-19 00:20:30 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:53 +0100 |
commit | 118ae18590dbc7d01cf34e0cd6133b1e34ef9090 (patch) | |
tree | 67fbad3b3105dfdc75eb4692517e7d22337a94ee | |
parent | 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 (diff) |
Contradiction API using EConstr.
-rw-r--r-- | engine/eConstr.ml | 1 | ||||
-rw-r--r-- | engine/eConstr.mli | 2 | ||||
-rw-r--r-- | ltac/extratactics.ml4 | 2 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 1 | ||||
-rw-r--r-- | tactics/contradiction.ml | 49 | ||||
-rw-r--r-- | tactics/contradiction.mli | 3 |
6 files changed, 33 insertions, 25 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 1dd9d0c00..629be8e4b 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -99,6 +99,7 @@ let mkIndU pi = of_kind (Ind pi) let mkInd i = of_kind (Ind (in_punivs i)) let mkConstructU pc = of_kind (Construct pc) let mkConstruct c = of_kind (Construct (in_punivs c)) +let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u)) let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p)) let mkFix f = of_kind (Fix f) let mkCoFix f = of_kind (CoFix f) diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e6270fa78..cb671154c 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -69,7 +69,7 @@ val mkInd : inductive -> t val mkIndU : pinductive -> t val mkConstruct : constructor -> t val mkConstructU : pconstructor -> t -(* val mkConstructUi : pinductive * int -> t *) +val mkConstructUi : pinductive * int -> t val mkCase : case_info * t * t * t array -> t val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index bcfa13c79..f87aa407d 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -185,7 +185,7 @@ END open Contradiction TACTIC EXTEND absurd - [ "absurd" constr(c) ] -> [ absurd c ] + [ "absurd" constr(c) ] -> [ absurd (EConstr.of_constr c) ] END let onSomeWithHoles tac = function diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 35d763ccc..f39549514 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1092,6 +1092,7 @@ let replay_history tactic_normalisation = Lazy.force coq_Gt; Lazy.force coq_Gt |]) in + let not_sup_sup = EConstr.of_constr not_sup_sup in Tacticals.New.tclTHENS (Tacticals.New.tclTHENLIST [ unfold sp_Zle; diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index a92b14dbe..596f1a759 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -7,6 +7,7 @@ (************************************************************************) open Term +open EConstr open Hipattern open Tactics open Coqlib @@ -19,6 +20,7 @@ module NamedDecl = Context.Named.Declaration (* Absurd *) let mk_absurd_proof t = + let build_coq_not () = EConstr.of_constr (build_coq_not ()) in let id = Namegen.default_dependent_ident in mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]), mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|]))) @@ -28,13 +30,13 @@ let absurd c = 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 (EConstr.of_constr c) 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 = EConstr.Unsafe.to_constr j.Environ.utj_val in + let t = j.Environ.utj_val in let tac = Tacticals.New.tclTHENLIST [ elim_type (EConstr.of_constr (build_coq_False ())); - Simple.apply (EConstr.of_constr (mk_absurd_proof t)) + Simple.apply (mk_absurd_proof t) ] in Sigma.Unsafe.of_pair (tac, sigma) end } @@ -49,7 +51,7 @@ let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 let filter_hyp f tac = let rec seek = function | [] -> Proofview.tclZERO Not_found - | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) + | d::rest when f (EConstr.of_constr (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 @@ -65,31 +67,33 @@ let contradiction_context = | d :: rest -> let id = NamedDecl.get_id d in let typ = nf_evar sigma (NamedDecl.get_type d) in - let typ = whd_all env sigma (EConstr.of_constr typ) in - if is_empty_type sigma (EConstr.of_constr typ) then - simplest_elim (EConstr.mkVar id) - else match kind_of_term typ with - | Prod (na,t,u) when is_empty_type sigma (EConstr.of_constr u) -> + let typ = EConstr.of_constr typ in + let typ = whd_all env sigma typ in + let typ = EConstr.of_constr typ in + if is_empty_type sigma typ then + simplest_elim (mkVar id) + else match EConstr.kind sigma typ with + | Prod (na,t,u) when is_empty_type sigma u -> let is_unit_or_eq = - if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma (EConstr.of_constr t) + if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma 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 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 (* Checking on the fly that it type-checks *) - simplest_elim (EConstr.mkApp (EConstr.mkVar id,[|EConstr.of_constr p|])) + simplest_elim (mkApp (mkVar id,[|p|])) | None -> Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type.")) (Proofview.tclORELSE (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 (EConstr.of_constr typ) (EConstr.of_constr t)) - (fun id' -> simplest_elim (EConstr.mkApp (EConstr.mkVar id,[|EConstr.mkVar id'|]))) + filter_hyp (fun typ -> is_conv_leq typ t) + (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) end }) begin function (e, info) -> match e with | Not_found -> seek_neg rest @@ -102,10 +106,9 @@ let contradiction_context = end } let is_negation_of env sigma typ t = - match kind_of_term (whd_all env sigma t) with + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with | Prod (na,t,u) -> - let u = nf_evar sigma u in - is_empty_type sigma (EConstr.of_constr u) && is_conv_leq env sigma (EConstr.of_constr typ) (EConstr.of_constr t) + is_empty_type sigma u && is_conv_leq env sigma typ t | _ -> false let contradiction_term (c,lbind as cl) = @@ -114,8 +117,10 @@ let contradiction_term (c,lbind as cl) = 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 (EConstr.of_constr typ) in - if is_empty_type sigma (EConstr.of_constr ccl) then + let typ = EConstr.of_constr typ in + let _, ccl = splay_prod env sigma typ in + let ccl = EConstr.of_constr ccl in + if is_empty_type sigma ccl then Tacticals.New.tclTHEN (elim false None cl None) (Tacticals.New.tclTRY assumption) @@ -123,8 +128,8 @@ let contradiction_term (c,lbind as cl) = Proofview.tclORELSE begin if lbind = NoBindings then - filter_hyp (fun c -> is_negation_of env sigma typ (EConstr.of_constr c)) - (fun id -> simplest_elim (EConstr.mkApp (EConstr.mkVar id,[|c|]))) + filter_hyp (fun c -> is_negation_of env sigma typ c) + (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) else Proofview.tclZERO Not_found end diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 5cc4b2e01..510b135b0 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -7,7 +7,8 @@ (************************************************************************) open Term +open EConstr open Misctypes val absurd : constr -> unit Proofview.tactic -val contradiction : EConstr.constr with_bindings option -> unit Proofview.tactic +val contradiction : constr with_bindings option -> unit Proofview.tactic |