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/.
28 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
29 exception NotAnInductiveTypeToEliminate
33 fun msg -> if debug then prerr_endline (Lazy.force msg) else ()
36 let inside_obj = function
37 | Cic.InductiveDefinition (type_list,params, nleft, _) ->
38 (type_list,params,nleft)
39 | _ -> raise (Invalid_argument "Errore in inside_obj")
41 let term_to_list = function
43 | _ -> raise (Invalid_argument "Errore in term_to_list")
46 let rec baseuri_of_term = function
47 | Cic.Appl l -> baseuri_of_term (List.hd l)
48 | Cic.MutInd (baseuri, tyno, []) -> baseuri
49 | _ -> raise (Invalid_argument "baseuri_of_term")
51 (* returns DX1 = DX1 -> ... DXn=DXn -> GOALTY *)
52 let rec foo_cut nleft parameters parameters_ty body uri_of_eq =
55 foo_cut (nleft-1) (List.tl parameters) (List.tl parameters_ty) body
62 Cic.Appl[Cic.MutInd (uri_of_eq ,0,[]);
63 (List.hd parameters_ty) ; hd; hd],
64 foo_cut nleft (List.map (CicSubstitution.lift 1) tl)
65 (List.map (CicSubstitution.lift 1) (List.tl parameters_ty))
66 (CicSubstitution.lift 1 body) uri_of_eq )
70 (* from a complex Cic.Prod term, return the list of its components *)
71 let rec get_sort_type term =
73 | Cic.Prod (_,src,tgt) -> (get_sort_type tgt)
78 let rec cut_first n l =
81 | hd::tl -> cut_first (n-1) tl
89 | hd::tl when tl != [] -> hd:: (cut_last tl)
93 (* returns the term to apply*)
94 let foo_appl nleft nright_consno term uri =
98 a := !a @ [(Cic.Implicit None)]
101 for n = 1 to nright_consno do
102 a := !a @ [(Cic.Implicit None)]
104 (* apply i_ind ? ... ? H *)
105 Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1])
109 let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty
110 uri_of_eq rightparameters_ termty isSetType term =
111 match right_param_tys with
112 | hd::tl -> Cic.Prod (
115 [Cic.MutInd(uri_of_eq,0,[]); hd; (List.hd rightparameters);
118 (List.map (CicSubstitution.lift 1) tl)
119 (List.map (CicSubstitution.lift 1) (List.tl rightparameters))
120 (List.map (CicSubstitution.lift 1) l2)
121 base_rel (CicSubstitution.lift 1 goalty) uri_of_eq
122 (List.map (CicSubstitution.lift 1) rightparameters_)
123 (CicSubstitution.lift 1 termty)
124 isSetType (CicSubstitution.lift 1 term))
125 | [] -> ProofEngineReduction.replace_lifting
126 ~equality:(ProofEngineReduction.alpha_equivalence)
128 then (rightparameters_ @ [term] )
129 else (rightparameters_ ) )
130 ~with_what: (List.map (CicSubstitution.lift (-1)) l2)
132 (* the same subterm of goalty could be simultaneously sx and dx!*)
135 let rec foo_lambda nright right_param_tys nright_ right_param_tys_
136 rightparameters created_vars base_rel goalty uri_of_eq rightparameters_
137 termty isSetType term =
138 match right_param_tys with
139 | hd::tl -> Cic.Lambda (
140 (Cic.Name ("lambda" ^ (string_of_int nright))),
142 foo_lambda (nright-1)
143 (List.map (CicSubstitution.lift 1) tl) nright_
144 (List.map (CicSubstitution.lift 1) right_param_tys_)
145 (List.map (CicSubstitution.lift 1) rightparameters)
146 (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1]))
147 base_rel (CicSubstitution.lift 1 goalty) uri_of_eq
148 (List.map (CicSubstitution.lift 1) rightparameters_)
149 (CicSubstitution.lift 1 termty) isSetType
150 (CicSubstitution.lift 1 term))
151 | [] when isSetType -> Cic.Lambda (
152 (Cic.Name ("lambda" ^ (string_of_int nright))),
153 (ProofEngineReduction.replace_lifting
154 ~equality:(ProofEngineReduction.alpha_equivalence)
155 ~what: (rightparameters_ )
156 ~with_what: (List.map (CicSubstitution.lift (-1)) created_vars)
157 ~where:termty), (* type of H with replaced right parameters *)
158 foo_prod nright_ (List.map (CicSubstitution.lift 1) right_param_tys_)
159 (List.map (CicSubstitution.lift 1) rightparameters)
160 (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1]))
161 (base_rel+1) (CicSubstitution.lift 1 goalty) uri_of_eq
162 (List.map (CicSubstitution.lift 1) rightparameters_)
163 (CicSubstitution.lift 1 termty) isSetType
164 (CicSubstitution.lift 1 term))
165 | [] -> foo_prod nright_ right_param_tys_ rightparameters created_vars
166 base_rel goalty uri_of_eq rightparameters_
167 termty isSetType term
170 let isSetType paramty = ((Pervasives.compare
171 (get_sort_type paramty)
172 (Cic.Sort Cic.Prop)) != 0)
174 let private_inversion_tac ~term =
175 let module T = CicTypeChecker in
176 let module R = CicReduction in
177 let module C = Cic in
178 let module P = PrimitiveTactics in
179 let module PET = ProofEngineTypes in
180 let private_inversion_tac ~term (proof, goal) =
182 (*DEBUG*) debug_print (lazy ("private inversion begins"));
183 let (_,metasenv,_,_) = proof in
184 let uri_of_eq = LibraryObjects.eq_URI () in
185 let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
186 let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
187 let uri = baseuri_of_term termty in
188 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
191 C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
192 | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
193 (uri,exp_named_subst,typeno,args)
194 | _ -> raise NotAnInductiveTypeToEliminate
196 let buri = UriManager.buri_of_uri uri in
197 let name,nleft,paramty,cons_list =
199 C.InductiveDefinition (tys,_,nleft,_) ->
200 let (name,_,paramty,cons_list) = List.nth tys typeno in
201 (name,nleft,paramty,cons_list)
205 UriManager.uri_of_string (buri ^ "/" ^ name ^ "_ind" ^ ".con")
207 let parameters = (List.tl (term_to_list termty)) in
211 match (T.type_of_aux' metasenv context t CicUniv.empty_ugraph) with
216 let consno = List.length cons_list in
217 let nright= ((List.length parameters)- nleft) in
218 let isSetType = isSetType paramty in
219 let cut_term = foo_cut nleft parameters
220 parameters_tys goalty uri_of_eq in
221 (*DEBUG*) debug_print (lazy ("cut term " ^ CicPp.ppterm cut_term));
222 debug_print (lazy ("CONTEXT before apply HCUT: " ^
223 (CicMetaSubst.ppcontext [] context )));
224 debug_print (lazy ("termty " ^ CicPp.ppterm termty));
225 (* cut DXn=DXn \to GOAL *)
226 let proof1,gl1 = PET.apply_tactic (P.cut_tac cut_term) (proof,goal) in
227 (* apply Hcut ; reflexivity *)
228 let proof2, gl2 = PET.apply_tactic
230 ~start: (P.apply_tac (C.Rel 1)) (* apply Hcut *)
231 ~continuation: (EqualityTactics.reflexivity_tac)
232 ) (proof1, (List.hd gl1))
234 (*DEBUG*) debug_print (lazy ("after apply HCUT;reflexivity
235 in private inversion"));
236 (* apply (ledx_ind( lambda x. lambda y, ...)) *)
237 let (t1,metasenv,t3,t4) = proof2 in
238 let goal2 = List.hd (List.tl gl1) in
239 let (_,context,_) = CicUtil.lookup_meta goal2 metasenv in
240 (* rightparameters type list *)
241 let rightparam_ty_l = (cut_first nleft parameters_tys) in
242 (* rightparameters list *)
243 let rightparameters= cut_first nleft parameters in
244 let lambda_t = foo_lambda nright rightparam_ty_l nright rightparam_ty_l
245 rightparameters [] nright goalty uri_of_eq rightparameters termty isSetType
247 let t = foo_appl nleft (nright+consno) lambda_t eliminator_uri in
248 debug_print (lazy ("Lambda_t: " ^ (CicPp.ppterm t)));
249 debug_print (lazy ("Term: " ^ (CicPp.ppterm termty)));
250 debug_print (lazy ("Body: " ^ (CicPp.ppterm goalty)));
252 (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl rightparameters))));
253 debug_print (lazy ("CONTEXT before refinement: " ^
254 (CicMetaSubst.ppcontext [] context )));
255 (*DEBUG*) debug_print (lazy ("private inversion: term before refinement: " ^
257 let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
260 (*DEBUG*) debug_print (lazy ("private inversion: termine after refinement: "
261 ^ CicPp.ppterm ref_t));
262 let proof2 = (t1,metasenv'',t3,t4) in
264 let my_apply_tac status =
266 ProofEngineTypes.apply_tactic (P.apply_tac ref_t) status in
267 let patched_new_goals =
268 let (_,metasenv''',_,_) = proof in
269 let new_goals = ProofEngineHelpers.compare_metasenvs
270 ~oldmetasenv:metasenv ~newmetasenv:metasenv''
272 List.filter (function i -> List.exists (function (j,_,_) -> j=i)
273 metasenv''') new_goals @ goals
275 proof,patched_new_goals
277 ProofEngineTypes.mk_tactic my_apply_tac
284 (ReductionTactics.simpl_tac (ProofEngineTypes.conclusion_pattern(None))))
290 ProofEngineTypes.mk_tactic (private_inversion_tac ~term)
294 let inversion_tac ~term =
295 let module T = CicTypeChecker in
296 let module R = CicReduction in
297 let module C = Cic in
298 let module P = PrimitiveTactics in
299 let module PET = ProofEngineTypes in
300 let inversion_tac ~term (proof, goal) =
301 (*DEBUG*) debug_print (lazy ("inversion begins"));
302 let (_,metasenv,_,_) = proof in
303 let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
304 let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
305 let uri = baseuri_of_term termty in
306 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
307 let name,nleft,arity,cons_list =
309 Cic.InductiveDefinition (tys,_,nleft,_) ->
310 (*we suppose there is only one inductiveType in the definition,
311 so typeno=0 identically *)
313 let (name,_,arity,cons_list) = List.nth tys typeno in
314 (name,nleft,arity,cons_list)
317 let buri = UriManager.buri_of_uri uri in
319 UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
320 (* arity length = number of parameters plus 1 *)
321 let arity_length = (List.length (term_to_list termty)) in
322 (* Check the existence of any right parameter. *)
323 assert (arity_length > (nleft + 1));
324 let appl_term arity_consno uri =
327 for n = 1 to arity_consno do
328 a := (Cic.Implicit None)::(!a)
330 (* apply i_inv ? ...? H). *)
331 Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1])
333 let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
334 let (t1,metasenv,t3,t4) = proof in
335 let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
338 let proof = (t1,metasenv'',t3,t4) in
340 ProofEngineTypes.apply_tactic (P.apply_tac ref_t) (proof,goal) in
341 let patched_new_goals =
342 let (_,metasenv''',_,_) = proof3 in
343 let new_goals = ProofEngineHelpers.compare_metasenvs
344 ~oldmetasenv:metasenv ~newmetasenv:metasenv''
346 List.filter (function i -> List.exists (function (j,_,_) -> j=i)
347 metasenv''') new_goals @ gl3
349 (proof3, patched_new_goals)
351 ProofEngineTypes.mk_tactic (inversion_tac ~term)