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))
40 (Tactics.intros ~howmany:1
41 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
43 (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
44 (fun _ metasenv ugraph -> t,metasenv,ugraph))
47 let by_term_we_proved t ty id ty' =
48 (*BUG: ty' not used *)
55 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
57 [ Tacticals.id_tac ; Tactics.apply t ]
64 (Tactics.apply ~term:t)
67 let we_need_to_prove t id ty =
71 ProofEngineTypes.apply_tactic
73 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
78 [fst; snd] -> [snd; fst]
83 ProofEngineTypes.mk_tactic aux
86 let existselim t id1 t1 id2 t2 =
87 (*BUG: t1 and t2 not used *)
88 (*PARSING BUG: t2 is parsed in the current context, but it may
89 have occurrences of id1 in it *)
91 ~mk_fresh_name_callback:
95 if !i = 1 then Cic.Name id1 else Cic.Name id2)
97 let andelim = existselim;;
99 let rewritingstep lhs rhs just conclude =
100 let aux ((proof,goal) as status) =
101 let (curi,metasenv,proofbo,proofty) = proof in
102 let _,context,_ = CicUtil.lookup_meta goal metasenv in
104 match LibraryObjects.eq_URI () with
105 None -> assert false (*TODO*)
107 Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
110 CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
113 None -> assert false (*TOOD*)
121 (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1)
122 CicUniv.empty_ugraph)
124 Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
125 | _ -> assert false in
128 (Some (Cic.Name id,_))::_ -> id
133 ProofEngineTypes.apply_tactic
135 ~start:(Tactics.apply ~term:trans)
137 [ Tactics.apply prhs ;
138 Tactics.apply (Cic.Rel 1) ;
139 Tactics.apply just]) status
141 let mk_fresh_name_callback =
142 fun metasenv context _ ~typ ->
143 FreshNamesGenerator.mk_fresh_name ~subst:[]
144 metasenv context name ~typ
146 ProofEngineTypes.apply_tactic
148 ~start:(Tactics.cut ~mk_fresh_name_callback
149 (Cic.Appl [eq ; ty ; plhs ; rhs]))
151 [ Tactics.clear ~hyps:[last_hyp_name] ;
153 ~start:(Tactics.apply ~term:trans)
155 [ Tactics.apply prhs ;
156 Tactics.apply (Cic.Rel 1) ;
161 None -> ProofEngineTypes.apply_tactic (Tactics.apply just) status
163 let mk_fresh_name_callback =
164 fun metasenv context _ ~typ ->
165 FreshNamesGenerator.mk_fresh_name ~subst:[]
166 metasenv context name ~typ
168 ProofEngineTypes.apply_tactic
171 (Tactics.cut ~mk_fresh_name_callback
172 (Cic.Appl [eq ; ty ; lhs ; rhs]))
173 ~continuations:[ Tacticals.id_tac ; Tactics.apply just ]) status
175 ProofEngineTypes.mk_tactic aux
178 let we_proceed_by_induction_on t pat =
179 (*BUG here: pat unused *)
180 Tactics.elim_intros ~depth:0 t
183 let case id ~params =
184 (*BUG here: id unused*)
185 (*BUG here: it does not verify that the previous branch is closed *)
186 (*BUG here: the params should be parsed telescopically*)
187 (*BUG here: the tactic_terms should be terms*)
188 let rec aux ~params ((proof,goal) as status) =
192 match ProofEngineTypes.apply_tactic (assume id t) status with
193 proof,[goal] -> aux tl (proof,goal)
196 ProofEngineTypes.mk_tactic (aux ~params)
199 let thesisbecomes t =
200 (*BUG here: nothing done*)
204 let byinduction t id = suppose t id None;;