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_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
166 let absurd_tac ~term ~status:((proof,goal) as status) =
167 let module C = Cic in
168 let module U = UriManager in
169 let module P = PrimitiveTactics in
170 let _,metasenv,_,_ = proof in
171 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
172 if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop))
173 then P.apply_tac ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status
174 else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
178 let contradiction_tac ~status =
179 let module C = Cic in
180 let module U = UriManager in
181 let module P = PrimitiveTactics in
182 let module T = Tacticals in
187 ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ))
188 ~continuation: assumption_tac)
192 (* Questa era in fourierR.ml
193 (* !!!!! fix !!!!!!!!!! *)
194 let contradiction_tac ~status:(proof,goal)=
196 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
197 ~continuation:(Tacticals.then_
198 ~start:(VariousTactics.elim_type_tac ~term:_False)
199 ~continuation:(assumption_tac))
205 (* IN FASE DI IMPLEMENTAZIONE *)
208 let generalize_tac ~term ~status:((proof,goal) as status) =
209 let module C = Cic in
210 let module P = PrimitiveTactics in
211 let module T = Tacticals in
212 let struct_equality t a = (t == a) in
213 let _,metasenv,_,_ = proof in
214 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
219 (C.Name "dummy_for_gen"),
220 (CicTypeChecker.type_of_aux' metasenv context term),
221 (ProofEngineReduction.replace
223 ~with_what:(C.Rel 1)(* (C.Name "dummy_for_gen") *)
225 ~where:ty)))) (* dove?? nel goal va bene?*)
227 [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac] (* in quest'ordine o viceversa? provare *)
231 (* PROVE DI DECOMPOSE
233 (* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *)
234 let decompose_tac ~what ~where ~status:((proof,goal) as status) =
235 let module C = Cic in
236 let module R = CicReduction in
237 let module P = PrimitiveTactics in
238 let module T = Tacticals in
239 let module S = ProofEngineStructuralRules in
241 let rec decomposing ty what =
243 [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *)
246 (C.Appl (hd::_)) -> hd
247 | _ -> decomposing ty tl
250 let (_,metasenv,_,_) = proof in
251 let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
254 ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what))
255 ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where)))) (* ma che ipotesi sto cancellando??? *)
261 let decompose_tac ~clist ~status:((proof,goal) as status) =
262 let module C = Cic in
263 let module R = CicReduction in
264 let module P = PrimitiveTactics in
265 let module T = Tacticals in
266 let module S = ProofEngineStructuralRules in
267 let (_,metasenv,_,_) = proof in
268 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
270 let rec repeat_elim ~term ~status = (* term -> status -> proof * (goal list) *)
272 let (proof, goallist) =
274 ~start:(P.elim_simpl_intros_tac ~term)
275 ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty)))) (* non so che ipotesi sto cancellando??? *)
278 let rec step proof goallist =
282 let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in
283 let (proof'', goallist'') = step proof' tl in
284 proof'', goallist'@goallist''
291 let rec decomposing ty clist = (* term -> (term list) -> bool *)
296 (C.Appl (hd::_)) -> true
297 | _ -> decomposing ty tl
300 let term = decomposing (R.whd context ty) clist in
301 if (term == C.Implicit)
302 then (Fail "Decompose: nothing to decompose or no application")
303 else repeat_elim ~term ~status
307 let decompose_tac ~clist ~status =
308 let module C = Cic in
309 let module R = CicReduction in
310 let module P = PrimitiveTactics in
311 let module T = Tacticals in
312 let module S = ProofEngineStructuralRules in
316 [] -> C.Implicit (* a cosa serve? *)
319 (C.Appl (hd::_)) -> hd
323 let decompose_one_tac ~clist ~status:((proof,goal) as status) =
324 let (_,metasenv,_,_) = proof in
325 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
326 let term = choose (R.whd context ty) clist in
327 if (term == C.Implicit)
328 then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
330 ~start:(P.elim_intros_simpl_tac ~term)
331 ~continuation:(S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty)))) (* ma che ipotesi sto cancellando??? *)
334 T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status
338 let decide_equality_tac =
343 let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
344 let module C = Cic in
345 let module U = UriManager in
346 let module P = PrimitiveTactics in
347 let module T = Tacticals in
348 let _,metasenv,_,_ = proof in
349 let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
350 if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
351 (* controllo che i due termini siano comparabili *)
354 ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
355 ~continuations:[split_tac ; intros_tac ~name:"FOO"]
356 else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
361 let rewrite_tac ~term:equality ~status:(proof,goal) =
362 let module C = Cic in
363 let module U = UriManager in
364 let curi,metasenv,pbo,pty = proof in
365 let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
366 let eq_ind_r,ty,t1,t2 =
367 match CicTypeChecker.type_of_aux' metasenv context equality with
368 C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
369 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
372 (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
375 | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
376 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
379 (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
384 (ProofEngineTypes.Fail
385 "Rewrite: the argument is not a proof of an equality")
388 let gty' = CicSubstitution.lift 1 gty in
389 let t1' = CicSubstitution.lift 1 t1 in
391 ProofEngineReduction.replace_lifting
392 ~equality:ProofEngineReduction.alpha_equivalence
393 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
395 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
397 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
398 let fresh_meta = ProofEngineHelpers.new_meta proof in
400 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
401 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
404 PrimitiveTactics.exact_tac
406 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
407 ~status:((curi,metasenv',pbo,pty),goal)
409 assert (List.length goals = 0) ;
410 (proof',[fresh_meta])
414 let rewrite_simpl_tac ~term ~status =
415 Tacticals.then_ ~start:(rewrite_tac ~term)
417 (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
422 let rewrite_back_tac ~term:equality ~status:(proof,goal) =
423 let module C = Cic in
424 let module U = UriManager in
425 let curi,metasenv,pbo,pty = proof in
426 let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
427 let eq_ind_r,ty,t1,t2 =
428 match CicTypeChecker.type_of_aux' metasenv context equality with
429 C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
430 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
433 (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[])
436 | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
437 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
440 (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con",[])
445 (ProofEngineTypes.Fail
446 "Rewrite: the argument is not a proof of an equality")
449 let gty' = CicSubstitution.lift 1 gty in
450 let t1' = CicSubstitution.lift 1 t1 in
452 ProofEngineReduction.replace_lifting
453 ~equality:ProofEngineReduction.alpha_equivalence
454 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
456 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
458 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
459 let fresh_meta = ProofEngineHelpers.new_meta proof in
461 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
462 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
465 PrimitiveTactics.exact_tac
467 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
468 ~status:((curi,metasenv',pbo,pty),goal)
470 assert (List.length goals = 0) ;
471 (proof',[fresh_meta])
476 let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
477 let module C = Cic in
478 let module U = UriManager in
479 let module P = PrimitiveTactics in
480 let module T = Tacticals in
481 let _,metasenv,_,_ = proof in
482 let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
483 let wty = CicTypeChecker.type_of_aux' metasenv context what in
484 if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
486 ~start:(P.cut_tac ~term:(C.Appl [(C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; wty ; what ; with_what]))
487 (* quale uguaglianza usare, eq o eqT ? *)
491 ~continuation:(T.then_
492 ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
493 ~continuation:(ProofEngineStructuralRules.clear
494 ~hyp:(Some((C.Name "dummy_for_replace") , (C.Def C.Implicit) (* NO!! tipo di dummy *) ))
499 else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")