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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Compat
open Global
open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Namegen
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Classops
open List
open Recordops
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern
open Vernacexpr
open Subtac_coercion
open Subtac_utils
open Coqlib
open Printer
open Subtac_errors
open Eterm
let require_library dirpath =
let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
Library.require_library [qualid] None
open Pp
open Ppconstr
open Decl_kinds
open Tacinterp
open Tacexpr
let solve_tccs_in_type env id isevars evm c typ =
if not (Evd.is_empty evm) then
let stmt_id = Nameops.add_suffix id "_stmt" in
let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with
| Subtac_obligations.Defined cst -> constant_value (Global.env())
(match cst with ConstRef kn -> kn | _ -> assert false)
| _ ->
errorlabstrm "start_proof"
(str "The statement obligations could not be resolved automatically, " ++ spc () ++
str "write a statement definition first.")
else
let _ = Typeops.infer_type env c in c
let start_proof_com env isevars sopt kind (bl,t) hook =
let id = match sopt with
| Some (loc,id) ->
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
user_err_loc (loc,"start_proof",pr_id id ++ str " already exists");
id
| None ->
next_global_ident_away (id_of_string "Unnamed_thm")
(Pfedit.get_all_proof_names ())
in
let evm, c, typ, imps =
Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None
in
let c = solve_tccs_in_type env id isevars evm c typ in
Lemmas.start_proof id kind c (fun loc gr ->
Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
hook loc gr)
let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
let start_proof_and_print env isevars idopt k t hook =
start_proof_com env isevars idopt k t hook;
print_subgoals ()
let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
let assumption_message id =
Flags.if_verbose message ((string_of_id id) ^ " is assumed")
let declare_assumptions env isevars idl is_coe k bl c nl =
if not (Pfedit.refining ()) then
let id = snd (List.hd idl) in
let evm, c, typ, imps =
Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None
in
let c = solve_tccs_in_type env id isevars evm c typ in
List.iter (Command.declare_assumption is_coe k c imps false nl) idl
else
errorlabstrm "Command.Assumption"
(str "Cannot declare an assumption while in proof editing mode.")
let dump_constraint ty ((loc, n), _, _) =
match n with
| Name id -> Dumpglob.dump_definition (loc, id) false ty
| Anonymous -> ()
let dump_variable lid = ()
let vernac_assumption env isevars kind l nl =
let global = fst kind = Global in
List.iter (fun (is_coe,(idl,c)) ->
if Dumpglob.dump () then
List.iter (fun lid ->
if global then Dumpglob.dump_definition lid (not global) "ax"
else dump_variable lid) idl;
declare_assumptions env isevars idl is_coe kind [] c nl) l
let check_fresh (loc,id) =
if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
user_err_loc (loc,"",pr_id id ++ str " already exists")
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
let env = Global.env () in
let isevars = ref (create_evar_defs Evd.empty) in
try
match command with
| VernacDefinition (defkind, (_, id as lid), expr, hook) ->
check_fresh lid;
Dumpglob.dump_definition lid false "def";
(match expr with
| ProveBody (bl, t) ->
start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
(fun _ _ -> ())
| DefineBody (bl, _, c, tycon) ->
ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
| VernacFixpoint (l, b) ->
List.iter (fun ((lid, _, _, _, _), _) ->
check_fresh lid;
Dumpglob.dump_definition lid false "fix") l;
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l b)
| VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
if guard <> None then
error "Do not support building theorems as a fixpoint.";
Dumpglob.dump_definition id false "prf";
if not(Pfedit.refining ()) then
if lettop then
errorlabstrm "Subtac_command.StartProof"
(str "Let declarations can only be used in proof editing mode");
if Lib.is_modtype () then
errorlabstrm "Subtac_command.StartProof"
(str "Proof editing mode not supported in module types");
check_fresh id;
start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
| VernacAssumption (stre,nl,l) ->
vernac_assumption env isevars stre l nl
| VernacInstance (abst, glob, sup, is, props, pri) ->
dump_constraint "inst" is;
if abst then
error "Declare Instance not supported here.";
ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
| VernacCoFixpoint (l, b) ->
if Dumpglob.dump () then
List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
ignore(Subtac_command.build_corecursive l b)
(*| VernacEndProof e ->
subtac_end_proof e*)
| _ -> user_err_loc (loc,"", str ("Invalid Program command"))
with
| Typing_error e ->
msg_warning (str "Type error in Program tactic:");
let cmds =
(match e with
| NonFunctionalApp (loc, x, mux, e) ->
str "non functional application of term " ++
e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux
| NonSigma (loc, t) ->
str "Term is not of Sigma type: " ++ t
| NonConvertible (loc, x, y) ->
str "Unconvertible terms:" ++ spc () ++
x ++ spc () ++ str "and" ++ spc () ++ y
| IllSorted (loc, t) ->
str "Term is ill-sorted:" ++ spc () ++ t
)
in msg_warning cmds
| Subtyping_error e ->
msg_warning (str "(Program tactic) Subtyping error:");
let cmds =
match e with
| UncoercibleInferType (loc, x, y) ->
str "Uncoercible terms:" ++ spc ()
++ x ++ spc () ++ str "and" ++ spc () ++ y
| UncoercibleInferTerm (loc, x, y, tx, ty) ->
str "Uncoercible terms:" ++ spc ()
++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x
++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y
| UncoercibleRewrite (x, y) ->
str "Uncoercible terms:" ++ spc ()
++ x ++ spc () ++ str "and" ++ spc () ++ y
in msg_warning cmds
| Cases.PatternMatchingError (env, exn) as e -> raise e
| Type_errors.TypeError (env, exn) as e -> raise e
| Pretype_errors.PretypeError (env, exn) as e -> raise e
| (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
Loc.Exc_located (loc, e') as e) -> raise e
| e ->
(* msg_warning (str "Uncaught exception: " ++ Cerrors.explain_exn e); *)
raise e
|
