1 (* Copyright (C) 2006, 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/.
26 type just = [ `Term of Cic.term | `Auto of Auto.auto_params ]
28 let mk_just ~dbd ~automation_cache =
32 ~params:(l,("skip_trie_filtering","1")::(*("skip_context","1")::*)params) ~automation_cache
33 | `Term t -> Tactics.apply t
39 (Tactics.intros ~howmany:1
40 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
42 (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
43 (fun _ metasenv ugraph -> t,metasenv,ugraph))
47 (*BUG: check on t missing *)
48 let ty = match ty with None -> t | Some ty -> ty in
51 (Tactics.intros ~howmany:1
52 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
54 (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
55 (fun _ metasenv ugraph -> ty,metasenv,ugraph))
58 let by_just_we_proved ~dbd ~automation_cache just ty id ty' =
59 let just = mk_just ~dbd ~automation_cache just in
66 ~start:(Tactics.change
67 ~pattern:(ProofEngineTypes.conclusion_pattern None)
68 (fun _ metasenv ugraph -> ty,metasenv,ugraph))
72 let ty',continuation =
81 ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
82 (fun _ metasenv ugraph -> ty,metasenv,ugraph))
88 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
89 ~continuations:[ Tacticals.id_tac ; continuation ]
92 let bydone ~dbd ~automation_cache just =
93 mk_just ~dbd ~automation_cache just
96 let we_need_to_prove t id ty =
100 None -> Tacticals.id_tac (*BUG: check missing here *)
102 Tactics.change ~pattern:(ProofEngineTypes.conclusion_pattern None)
103 (fun _ metasenv ugraph -> ty,metasenv,ugraph))
108 None -> Tacticals.id_tac,t
110 Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
111 (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
113 ProofEngineTypes.apply_tactic
117 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
118 ~continuations:[cont])
123 [fst; snd] -> [snd; fst]
128 ProofEngineTypes.mk_tactic aux
131 let existselim ~dbd ~automation_cache just id1 t1 id2 t2 =
132 let aux (proof, goal) =
133 let (n,metasenv,_subst,bo,ty,attrs) = proof in
134 let metano,context,_ = CicUtil.lookup_meta goal metasenv in
135 let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
136 let proof' = (n,metasenv,_subst,bo,ty,attrs) in
137 ProofEngineTypes.apply_tactic (
139 ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
141 [ Tactics.elim_intros (Cic.Rel 1)
142 ~mk_fresh_name_callback:
146 if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
147 (mk_just ~dbd ~automation_cache just)
150 ProofEngineTypes.mk_tactic aux
153 let andelim ~dbd ~automation_cache just id1 t1 id2 t2 =
155 ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2]))
157 [ Tactics.elim_intros (Cic.Rel 1)
158 ~mk_fresh_name_callback:
162 if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
163 (mk_just ~dbd ~automation_cache just) ]
166 let rewritingstep ~dbd ~automation_cache lhs rhs just last_step =
167 let aux ((proof,goal) as status) =
168 let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
169 let _,context,gty = CicUtil.lookup_meta goal metasenv in
171 match LibraryObjects.eq_URI () with
172 None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
174 Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
177 CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in
180 `Auto (univ, params) ->
182 if not (List.exists (fun (k,_) -> k = "timeout") params) then
183 ("timeout","3")::params
187 if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
188 ("paramodulation","1")::params
191 if params = params' then
192 Tactics.auto ~dbd ~params:(univ, params) ~automation_cache
195 [Tactics.auto ~dbd ~params:(univ, params) ~automation_cache ;
196 Tactics.auto ~dbd ~params:(univ, params') ~automation_cache]
197 | `Term just -> Tactics.apply just
199 Tactics.demodulate ~automation_cache ~dbd
200 ~params:(Some [term],
201 ["all","1";"steps","1"; "use_context","false"])
205 let plhs,prhs,prepare =
210 Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
215 ProofEngineTypes.apply_tactic continuation status)
219 Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
222 (*CSC: manca check plhs convertibile con lhs *)
225 ProofEngineTypes.apply_tactic continuation status)
226 | Some (Some name,lhs) ->
227 let newmeta = CicMkImplicit.new_meta metasenv [] in
229 CicMkImplicit.identity_relocation_list_for_metavariable context in
231 let prhs = Cic.Meta(newmeta,irl) in
234 let metasenv = (newmeta, context, ty)::metasenv in
235 let mk_fresh_name_callback =
236 fun metasenv context _ ~typ ->
237 FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
240 let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
242 ProofEngineTypes.apply_tactic
244 ~start:(Tactics.cut ~mk_fresh_name_callback
245 (Cic.Appl [eq ; ty ; lhs ; prhs]))
246 ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
249 match just,goals with
250 `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1]
251 | _, [g1;g2] -> [g2;newmeta;g1]
253 prerr_endline (String.concat "," (List.map string_of_int l));
254 prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
261 (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
265 ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs]))
266 ~continuations:[just' ; Tacticals.id_tac]
270 ProofEngineTypes.mk_tactic aux
273 let we_proceed_by_cases_on t pat =
274 (*BUG here: pat unused *)
275 Tactics.cases_intros t
278 let we_proceed_by_induction_on t pat =
279 (* let pattern = None, [], Some pat in *)
280 Tactics.elim_intros ~depth:0 (*~pattern*) t
283 let case id ~params =
284 (*BUG here: id unused*)
285 (*BUG here: it does not verify that the previous branch is closed *)
286 (*BUG here: the params should be parsed telescopically*)
287 (*BUG here: the tactic_terms should be terms*)
288 let rec aux ~params ((proof,goal) as status) =
292 match ProofEngineTypes.apply_tactic (assume id t) status with
293 proof,[goal] -> aux tl (proof,goal)
296 ProofEngineTypes.mk_tactic (aux ~params)
299 let thesisbecomes t =
303 Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
304 (fun _ metasenv ugraph -> t,metasenv,ugraph)
306 (*BUG here: missing check on t *)
307 Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
308 (fun _ metasenv ugraph -> ty,metasenv,ugraph)
311 let byinduction t id = suppose t id None;;