aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-19 00:20:30 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:28:53 +0100
commit118ae18590dbc7d01cf34e0cd6133b1e34ef9090 (patch)
tree67fbad3b3105dfdc75eb4692517e7d22337a94ee
parent3f9e56fcbf479999325a86bbdaeefd6a0be13c65 (diff)
Contradiction API using EConstr.
-rw-r--r--engine/eConstr.ml1
-rw-r--r--engine/eConstr.mli2
-rw-r--r--ltac/extratactics.ml42
-rw-r--r--plugins/omega/coq_omega.ml1
-rw-r--r--tactics/contradiction.ml49
-rw-r--r--tactics/contradiction.mli3
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