1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Term
open EConstr
open Hipattern
open Tactics
open Coqlib
open Reductionops
open Misctypes
open Proofview.Notations
module NamedDecl = Context.Named.Declaration
(* Absurd *)
let mk_absurd_proof t =
let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ 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|])))
let absurd c =
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 env sigma j in
let t = j.Environ.utj_val in
let tac =
Tacticals.New.tclTHENLIST [
elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()));
Simple.apply (mk_absurd_proof t)
] 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
| 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
seek hyps
end }
let contradiction_context =
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")
| 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 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 t
else None in
Tacticals.New.tclORELSE
(match is_unit_or_eq with
| Some _ ->
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 (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 typ t)
(fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
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
seek_neg hyps
end }
let is_negation_of env sigma typ t =
match EConstr.kind sigma (whd_all env sigma t) with
| Prod (na,t,u) ->
is_empty_type sigma u && is_conv_leq env sigma typ t
| _ -> false
let contradiction_term (c,lbind as cl) =
Proofview.Goal.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
let _, ccl = splay_prod env sigma typ in
if is_empty_type sigma ccl then
Tacticals.New.tclTHEN
(elim false None cl None)
(Tacticals.New.tclTRY assumption)
else
Proofview.tclORELSE
begin
if lbind = NoBindings then
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
begin function (e, info) -> match e with
| Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
| e -> Proofview.tclZERO ~info e
end
end }
let contradiction = function
| None -> Tacticals.New.tclTHEN intros contradiction_context
| Some c -> contradiction_term c
|
