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/.
29 (Tactics.intros ~howmany:1
30 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
32 (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
33 (fun _ metasenv ugraph -> t,metasenv,ugraph))
37 (*BUG: check on t missing *)
38 let ty = match ty with None -> t | Some ty -> ty in
41 (Tactics.intros ~howmany:1
42 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
44 (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
45 (fun _ metasenv ugraph -> ty,metasenv,ugraph))
48 let by_term_we_proved ~dbd ~universe t ty id ty' =
51 None -> Tactics.auto ~dbd ~params:[] ~universe
52 | Some t -> Tactics.apply t
60 ~start:(Tactics.change
61 ~pattern:(ProofEngineTypes.conclusion_pattern None)
62 (fun _ metasenv ugraph -> ty,metasenv,ugraph))
68 None -> Tacticals.id_tac
70 Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
71 (fun _ metasenv ugraph -> ty',metasenv,ugraph)
76 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
77 ~continuations:[ continuation ; just ]
80 let bydone ~dbd ~universe t =
83 None -> Tactics.auto ~dbd ~params:[] ~universe
84 | Some t -> Tactics.apply t
89 let we_need_to_prove t id ty =
93 None -> Tacticals.id_tac (*BUG: check missing here *)
95 Tactics.change ~pattern:(ProofEngineTypes.conclusion_pattern None)
96 (fun _ metasenv ugraph -> ty,metasenv,ugraph))
101 None -> Tacticals.id_tac,t
103 Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
104 (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
106 ProofEngineTypes.apply_tactic
110 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
111 ~continuations:[cont])
116 [fst; snd] -> [snd; fst]
121 ProofEngineTypes.mk_tactic aux
124 let existselim ~dbd ~universe t id1 t1 id2 t2 =
125 let aux (proof, goal) =
126 let (n,metasenv,bo,ty,attrs) = proof in
127 let metano,context,_ = CicUtil.lookup_meta goal metasenv in
128 let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
129 let proof' = (n,metasenv,bo,ty,attrs) in
130 let pattern = ProofEngineTypes.conclusion_pattern (Some (Cic.Rel 1)) in
131 ProofEngineTypes.apply_tactic (
133 ~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)]))
135 [ Tactics.elim_intros pattern
136 ~mk_fresh_name_callback:
140 if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
142 None -> Tactics.auto ~dbd ~params:[] ~universe
143 | Some t -> Tactics.apply t)
146 ProofEngineTypes.mk_tactic aux
149 let andelim t id1 t1 id2 t2 =
150 Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t))
151 ~mk_fresh_name_callback:
155 if !i = 1 then Cic.Name id1 else Cic.Name id2)
157 let rewritingstep ~dbd ~universe lhs rhs just last_step =
158 let aux ((proof,goal) as status) =
159 let (curi,metasenv,proofbo,proofty, attrs) = proof in
160 let _,context,gty = CicUtil.lookup_meta goal metasenv in
162 match LibraryObjects.eq_URI () with
163 None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
165 Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
168 CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
173 if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
174 ("paramodulation","1")::params
177 if not (List.exists (fun (k,_) -> k = "timeout") params) then
178 ("timeout","3")::params
181 Tactics.auto ~dbd ~params ~universe
182 | `Term just -> Tactics.apply just
184 let plhs,prhs,prepare =
189 Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
194 ProofEngineTypes.apply_tactic continuation status)
198 Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
201 (*CSC: manca check plhs convertibile con lhs *)
204 ProofEngineTypes.apply_tactic continuation status)
205 | Some (Some name,lhs) ->
206 let newmeta = CicMkImplicit.new_meta metasenv [] in
208 CicMkImplicit.identity_relocation_list_for_metavariable context in
210 let prhs = Cic.Meta(newmeta,irl) in
213 let metasenv = (newmeta, context, ty)::metasenv in
214 let mk_fresh_name_callback =
215 fun metasenv context _ ~typ ->
216 FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
219 let proof = curi,metasenv,proofbo,proofty, attrs in
221 ProofEngineTypes.apply_tactic
223 ~start:(Tactics.cut ~mk_fresh_name_callback
224 (Cic.Appl [eq ; ty ; lhs ; prhs]))
225 ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
229 [g1;g2] -> [g2;newmeta;g1]
236 (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
240 ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs]))
241 ~continuations:[just ; Tacticals.id_tac]
245 ProofEngineTypes.mk_tactic aux
248 let we_proceed_by_cases_on t pat =
249 (*BUG here: pat unused *)
250 Tactics.cases_intros t
253 let we_proceed_by_induction_on t pat =
254 let pattern = Some (fun c m u -> t, m, u), [], Some pat in
255 Tactics.elim_intros ~depth:0 pattern
258 let case id ~params =
259 (*BUG here: id unused*)
260 (*BUG here: it does not verify that the previous branch is closed *)
261 (*BUG here: the params should be parsed telescopically*)
262 (*BUG here: the tactic_terms should be terms*)
263 let rec aux ~params ((proof,goal) as status) =
267 match ProofEngineTypes.apply_tactic (assume id t) status with
268 proof,[goal] -> aux tl (proof,goal)
271 ProofEngineTypes.mk_tactic (aux ~params)
274 let thesisbecomes t =
278 Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
279 (fun _ metasenv ugraph -> t,metasenv,ugraph)
281 (*BUG here: missing check on t *)
282 Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
283 (fun _ metasenv ugraph -> ty,metasenv,ugraph)
286 let byinduction t id = suppose t id None;;