1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
27 let constructor_tac ~n ~status:(proof, goal) =
29 let module R = CicReduction in
30 let (_,metasenv,_,_) = proof in
31 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
32 match (R.whd context ty) with
33 (C.MutInd (uri, typeno, exp_named_subst))
34 | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
35 PrimitiveTactics.apply_tac ~status:(proof, goal)
36 ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
37 | _ -> raise (ProofEngineTypes.Fail "Constructor failed")
41 let exists_tac ~status =
42 constructor_tac ~n:1 ~status
46 let split_tac ~status =
47 constructor_tac ~n:1 ~status
51 let left_tac ~status =
52 constructor_tac ~n:1 ~status
56 let right_tac ~status =
57 constructor_tac ~n:2 ~status
66 let symmetry_tac ~status:(proof, goal) =
68 let module R = CicReduction in
69 let module U = UriManager in
70 let (_,metasenv,_,_) = proof in
71 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
72 match (R.whd context ty) with
73 (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
74 PrimitiveTactics.apply_tac ~status:(proof,goal)
75 ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", []))
77 | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
78 PrimitiveTactics.apply_tac ~status:(proof,goal)
79 ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", []))
81 | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
85 let transitivity_tac ~term ~status:((proof, goal) as status) =
87 let module R = CicReduction in
88 let module U = UriManager in
89 let module T = Tacticals in
90 let (_,metasenv,_,_) = proof in
91 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
92 match (R.whd context ty) with
93 (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
95 ~start:(PrimitiveTactics.apply_tac
96 ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", [])))
98 [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term]
101 | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
103 ~start:(PrimitiveTactics.apply_tac
104 ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", [])))
106 [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term]
109 | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
113 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
115 let assumption_tac ~status:((proof,goal) as status) =
116 let module C = Cic in
117 let module R = CicReduction in
118 let module S = CicSubstitution in
119 let _,metasenv,_,_ = proof in
120 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
121 let rec find n = function
124 (Some (_, C.Decl t)) when
125 (R.are_convertible context (S.lift n t) ty) -> n
126 | (Some (_, C.Def t)) when
127 (R.are_convertible context
128 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
131 | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
132 in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
135 (* Questa invece era in fourierR.ml
136 let assumption_tac ~status:(proof,goal)=
137 let curi,metasenv,pbo,pty = proof in
138 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
140 let tac_list = List.map
141 ( fun x -> num := !num + 1;
143 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
144 | _ -> ("fake",tcl_fail 1)
148 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
153 (* ANCORA DA DEBUGGARE *)
156 let elim_type_tac ~term ~status =
157 let module C = Cic in
158 let module P = PrimitiveTactics in
159 let module T = Tacticals in
161 ~start: (P.cut_tac ~term)
162 ~continuations:[ P.elim_simpl_intros_tac ~term:(C.Rel 1) ; T.id_tac ]
166 (* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-)
167 let elim_type_tac ~term ~status =
168 warn "in Ring.elim_type_tac";
169 Tacticals.thens ~start:(cut_tac ~term)
170 ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
174 let absurd_tac ~term ~status:((proof,goal) as status) =
175 let module C = Cic in
176 let module U = UriManager in
177 let module P = PrimitiveTactics in
178 let _,metasenv,_,_ = proof in
179 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
180 if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop))
181 then P.apply_tac ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status
182 else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
186 let contradiction_tac ~status =
187 let module C = Cic in
188 let module U = UriManager in
189 let module P = PrimitiveTactics in
190 let module T = Tacticals in
192 ~start: (P.intros_tac ~mknames:(function () -> "FOO"))
195 ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ))
196 ~continuation: assumption_tac)
200 (* Questa era in fourierR.ml
201 (* !!!!! fix !!!!!!!!!! *)
202 let contradiction_tac ~status:(proof,goal)=
204 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
205 ~continuation:(Tacticals.then_
206 ~start:(VariousTactics.elim_type_tac ~term:_False)
207 ~continuation:(assumption_tac))
213 (* IN FASE DI IMPLEMENTAZIONE *)
216 let generalize_tac ~term ~status:((proof,goal) as status) =
217 let module C = Cic in
218 let module P = PrimitiveTactics in
219 let module T = Tacticals in
220 let struct_equality t a = (t == a) in
221 let _,metasenv,_,_ = proof in
222 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
227 (C.Name "dummy_for_gen"),
228 (CicTypeChecker.type_of_aux' metasenv context term),
229 (ProofEngineReduction.replace
231 ~with_what:(C.Rel 1)(* (C.Name "dummy_for_gen") *)
233 ~where:ty)))) (* dove?? nel goal va bene?*)
235 [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac] (* in quest'ordine o viceversa? provare *)
239 (* PROVE DI DECOMPOSE
241 (* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *)
242 let decompose_tac ~what ~where ~status:((proof,goal) as status) =
243 let module C = Cic in
244 let module R = CicReduction in
245 let module P = PrimitiveTactics in
246 let module T = Tacticals in
247 let module S = ProofEngineStructuralRules in
249 let rec decomposing ty what =
251 [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *)
254 (C.Appl (hd::_)) -> hd
255 | _ -> decomposing ty tl
258 let (_,metasenv,_,_) = proof in
259 let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
262 ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what))
263 ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where)))) (* ma che ipotesi sto cancellando??? *)
269 let decompose_tac ~clist ~status:((proof,goal) as status) =
270 let module C = Cic in
271 let module R = CicReduction in
272 let module P = PrimitiveTactics in
273 let module T = Tacticals in
274 let module S = ProofEngineStructuralRules in
275 let (_,metasenv,_,_) = proof in
276 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
278 let rec repeat_elim ~term ~status = (* term -> status -> proof * (goal list) *)
280 let (proof, goallist) =
282 ~start:(P.elim_simpl_intros_tac ~term)
283 ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty)))) (* non so che ipotesi sto cancellando??? *)
286 let rec step proof goallist =
290 let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in
291 let (proof'', goallist'') = step proof' tl in
292 proof'', goallist'@goallist''
299 let rec decomposing ty clist = (* term -> (term list) -> bool *)
304 (C.Appl (hd::_)) -> true
305 | _ -> decomposing ty tl
308 let term = decomposing (R.whd context ty) clist in
309 if (term == C.Implicit)
310 then (Fail "Decompose: nothing to decompose or no application")
311 else repeat_elim ~term ~status
315 let decompose_tac ~clist ~status =
316 let module C = Cic in
317 let module R = CicReduction in
318 let module P = PrimitiveTactics in
319 let module T = Tacticals in
320 let module S = ProofEngineStructuralRules in
324 [] -> C.Implicit (* a cosa serve? *)
327 (C.Appl (hd::_)) -> hd
331 let decompose_one_tac ~clist ~status:((proof,goal) as status) =
332 let (_,metasenv,_,_) = proof in
333 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
334 let term = choose (R.whd context ty) clist in
335 if (term == C.Implicit)
336 then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
338 ~start:(P.elim_simpl_intros_tac ~term)
339 ~continuation:(S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty)))) (* ma che ipotesi sto cancellando??? *)
342 T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status
346 let decide_equality_tac =
351 let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
352 let module C = Cic in
353 let module U = UriManager in
354 let module P = PrimitiveTactics in
355 let module T = Tacticals in
356 let _,metasenv,_,_ = proof in
357 let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
358 if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
359 (* controllo che i due termini siano comparabili *)
362 ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
363 ~continuations:[split_tac ; intros_tac ~name:"FOO"]
364 else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
369 let rewrite_tac ~term:equality ~status:(proof,goal) =
370 let module C = Cic in
371 let module U = UriManager in
372 let curi,metasenv,pbo,pty = proof in
373 let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
374 let eq_ind_r,ty,t1,t2 =
375 match CicTypeChecker.type_of_aux' metasenv context equality with
376 C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
377 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
380 (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
383 | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
384 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
387 (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
392 (ProofEngineTypes.Fail
393 "Rewrite: the argument is not a proof of an equality")
396 let gty' = CicSubstitution.lift 1 gty in
397 let t1' = CicSubstitution.lift 1 t1 in
399 ProofEngineReduction.replace_lifting
400 ~equality:ProofEngineReduction.alpha_equivalence
401 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
403 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
405 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
406 let fresh_meta = ProofEngineHelpers.new_meta proof in
408 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
409 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
412 PrimitiveTactics.exact_tac
414 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
415 ~status:((curi,metasenv',pbo,pty),goal)
417 assert (List.length goals = 0) ;
418 (proof',[fresh_meta])
422 let rewrite_simpl_tac ~term ~status =
423 Tacticals.then_ ~start:(rewrite_tac ~term)
425 (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
430 let rewrite_back_tac ~term:equality ~status:(proof,goal) =
431 let module C = Cic in
432 let module U = UriManager in
433 let curi,metasenv,pbo,pty = proof in
434 let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
435 let eq_ind_r,ty,t1,t2 =
436 match CicTypeChecker.type_of_aux' metasenv context equality with
437 C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
438 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
441 (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[])
444 | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
445 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
448 (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con",[])
453 (ProofEngineTypes.Fail
454 "Rewrite: the argument is not a proof of an equality")
457 let gty' = CicSubstitution.lift 1 gty in
458 let t1' = CicSubstitution.lift 1 t1 in
460 ProofEngineReduction.replace_lifting
461 ~equality:ProofEngineReduction.alpha_equivalence
462 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
464 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
466 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
467 let fresh_meta = ProofEngineHelpers.new_meta proof in
469 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
470 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
473 PrimitiveTactics.exact_tac
475 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
476 ~status:((curi,metasenv',pbo,pty),goal)
478 assert (List.length goals = 0) ;
479 (proof',[fresh_meta])
484 let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
485 let module C = Cic in
486 let module U = UriManager in
487 let module P = PrimitiveTactics in
488 let module T = Tacticals in
489 let _,metasenv,_,_ = proof in
490 let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
491 let wty = CicTypeChecker.type_of_aux' metasenv context what in
492 if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
494 ~start:(P.cut_tac ~term:(C.Appl [(C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; wty ; what ; with_what]))
495 (* quale uguaglianza usare, eq o eqT ? *)
499 (P.intros_tac ~mknames:(function () ->"dummy_for_replace"))
500 ~continuation:(T.then_
501 ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
502 ~continuation:(ProofEngineStructuralRules.clear
503 ~hyp:(Some((C.Name "dummy_for_replace") , (C.Def C.Implicit) (* NO!! tipo di dummy *) ))
508 else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")