]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/inversion.ml
New tactic: inversion.
[helm.git] / helm / ocaml / tactics / inversion.ml
1 (* Copyright (C) 2002, HELM Team.
2  * 
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.
6  * 
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.
11
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
27 exception NotAnInductiveTypeToEliminate
28
29 let debug = false;;
30 let debug_print =
31  fun msg -> if debug then prerr_endline (Lazy.force msg) else ()
32
33 let inside_obj = function
34     | Cic.InductiveDefinition (l,params, nleft, _) ->
35       (l,params,nleft)
36     | _ -> raise (Invalid_argument "Errore in inside_obj")
37
38 let term_to_list = function
39         | Cic.Appl l -> l
40         | _ -> raise (Invalid_argument "Errore in term_to_list")
41
42
43 let rec baseuri_of_term = function
44   | Cic.Appl l -> baseuri_of_term (List.hd l)  
45   | Cic.MutInd (baseuri, tyno, []) -> baseuri
46   | _ -> raise (Invalid_argument "baseuri_of_term")
47
48
49 (*prende il numero dei parametri sinistri, la lista dei parametri, la lista dei tipi dei parametri, 
50 il tipo del GOAL e costruisce il termine per la cut ossia DX1 = DX1 -> ... DXn=DXn -> GOALTY *)
51 let rec foo_cut nleft l param_ty_l body uri_of_eq = 
52
53         if nleft >0 then foo_cut (nleft-1) (List.tl l)  (List.tl param_ty_l) body uri_of_eq
54          else   match l with
55                 | hd::tl -> Cic.Prod (Cic.Anonymous,
56                                 Cic.Appl[Cic.MutInd (uri_of_eq  ,0,[]); 
57                                         (List.hd param_ty_l) ;
58                                         hd;
59                                         hd],
60                                 foo_cut nleft (List.map (CicSubstitution.lift 1) tl) (List.tl param_ty_l) (CicSubstitution.lift 1 body) uri_of_eq 
61                         )
62                 | [] -> body
63  ;;
64
65 (* da una catena di prod costruisce una lista dei termini che lo compongono.*)
66 let rec list_of_prod term =
67 match term with 
68  | Cic.Prod (Cic.Anonymous,src,tgt) -> [src] @ (list_of_prod tgt)
69  | _ -> [term]
70
71 ;;
72
73
74 let rec cut_first n l =
75  if n>0 then  
76   match l with
77   | hd::tl -> cut_first (n-1) tl
78   | [] -> []
79   else l
80 ;;
81
82
83 let rec cut_last l =
84 match l with
85  | hd::tl when tl != [] -> hd:: (cut_last tl)
86  | _ -> []
87 ;;
88
89
90 let foo_appl nleft nright_consno term uri =
91  let l = [] in
92  let a = ref l in
93
94  for n = 1 to nleft do
95         a := !a @ [(Cic.Implicit None)]
96         
97  done;
98  a:= !a @ [term];
99
100  for n = 1 to nright_consno do
101         a := !a @ [(Cic.Implicit None)] 
102  done;
103  Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1]) (*L'ipotesi e' sempre Rel 1. (?)  *)
104 ;;
105
106
107
108 let rec foo_prod nright param_ty_l l l2 base_rel body uri_of_eq nleft termty isSetType term =
109  match param_ty_l with
110         | hd::tl -> Cic.Prod (Cic.Anonymous,
111                         Cic.Appl[Cic.MutInd(uri_of_eq,0,[]);
112                                 hd;
113                                 (List.hd l);
114                                 Cic.Rel base_rel
115                         ],
116                         foo_prod (nright-1) tl (List.map (CicSubstitution.lift 1) (List.tl l)) 
117                                 (List.map (CicSubstitution.lift 1) l2) 
118                                 base_rel 
119                                 (CicSubstitution.lift 1 body) 
120                                 uri_of_eq nleft 
121                                 (CicSubstitution.lift 1 termty)
122                                 isSetType 
123                                 (CicSubstitution.lift 1 term))
124                                 
125                                 
126         | [] ->  ProofEngineReduction.replace_lifting ~equality:(ProofEngineReduction.alpha_equivalence)
127                                                         ~what: (if isSetType then ((cut_first (1+nleft) (term_to_list termty) ) @ [term] ) 
128                                                                 else (cut_first (1+nleft) (term_to_list termty) ) )
129                                                         ~with_what: (List.map (CicSubstitution.lift (-1)) l2)
130                                                         ~where:body 
131                                                         (*TODO lo stesso sottotermine di body puo' essere sia sx che dx!*)
132 ;;
133
134
135 let rec foo_lambda nright param_ty_l nright_ param_ty_l_ l l2 base_rel body uri_of_eq nleft termty isSetType ty_indty term =
136  (*assert nright >0 *)
137   match param_ty_l with
138         | hd::tl ->Cic.Lambda ((Cic.Name ("lambda" ^ (string_of_int nright))),
139                                 hd, (* typ *)
140                                 foo_lambda      (nright-1) tl
141                                                 nright_ param_ty_l_ 
142                                                 (List.map (CicSubstitution.lift 1) l) 
143                                                 (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) 
144                                                 base_rel 
145                                                 (CicSubstitution.lift 1 body)  
146                                                 uri_of_eq nleft 
147                                                 (CicSubstitution.lift 1 termty)
148                                                 isSetType ty_indty
149                                                 (CicSubstitution.lift 1 term)) 
150         | [] when isSetType -> Cic.Lambda (
151                                         (Cic.Name ("lambda" ^ (string_of_int nright))),
152                                         (ProofEngineReduction.replace_lifting   ~equality:(ProofEngineReduction.alpha_equivalence)
153                                                                                  ~what: (cut_first (1+nleft) (term_to_list termty) ) 
154                                                                                  ~with_what: (List.map (CicSubstitution.lift (-1)) l2)
155                                                                                  ~where:termty), (* tipo di H con i parametri destri sostituiti *)
156                                         foo_prod nright_ param_ty_l_ 
157                                                 (List.map (CicSubstitution.lift 1) l)  
158                                                 (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) 
159                                                 (base_rel+1) (CicSubstitution.lift 1 body)  
160                                                 uri_of_eq nleft 
161                                                 (CicSubstitution.lift 1 termty) isSetType
162                                                 (CicSubstitution.lift 1 term))
163         | [] -> foo_prod nright_ param_ty_l_ l l2 
164                         base_rel body uri_of_eq 
165                         nleft termty isSetType term
166 ;;
167
168
169
170 let inversion_tac ~term =
171  let module T = CicTypeChecker in
172  let module R = CicReduction in
173  let module C = Cic in
174  let module P = PrimitiveTactics in
175  let module PET = ProofEngineTypes in
176  let inversion_tac ~term (proof, goal) =
177  let (_,metasenv,_,_) = proof in
178  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
179  let (newproof, metasenv') = ProofEngineHelpers.subst_meta_in_proof proof metano term [] in
180  let uri_of_eq = HelmLibraryObjects.Logic.eq_URI in
181
182 (* dall'indice che indentifica il goal nel metasenv, ritorna il suo tipo, che e' la terza componente
183 della relativa congettura *)
184 let (_,_,body) = CicUtil.lookup_meta goal metasenv in
185
186 (* estrae il tipo del termine oggetto di inversion, di solito un Cic.Appl list, ma..*)
187
188  let termty,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
189  let uri = baseuri_of_term termty in  
190  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
191  let l,params,nleft = inside_obj o in
192  let (_,_,typeno,_) =
193        match termty with
194                C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
195                | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
196                                (uri,exp_named_subst,typeno,args)
197                | _ -> raise NotAnInductiveTypeToEliminate
198  in
199
200  let eliminator_uri =
201         
202         let buri = UriManager.buri_of_uri uri in
203         let name =
204                 match o with
205                         C.InductiveDefinition (tys,_,_,_) ->
206                                 let (name,_,_,_) = List.nth tys typeno in
207                                 name
208                         |_ -> assert false
209         in
210         
211         
212 (*      let ty_ty,_ = T.type_of_aux' metasenv context termty CicUniv.empty_ugraph in
213         let ext =
214                 match ty_ty with
215                         C.Sort C.Prop -> "_ind"
216                         | C.Sort C.Set  -> "_rec"
217                         | C.Sort C.CProp -> "_rec"
218                         | C.Sort (C.Type _)-> "_rect"
219                         | C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
220                         | _ -> assert false
221         in
222 *)
223
224         let ext = "_ind" in
225         UriManager.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
226 in
227
228  (* il tipo del tipo induttivo oggetto di inversione *)
229  
230  let (_,_,ty_indty,cons_list) = (List.hd l) in
231  (*la lista ricavata dal tipo del tipo induttivo. *)
232  let param_ty_l = list_of_prod ty_indty in
233  let consno = List.length cons_list in
234  let nright= (List.length param_ty_l)- (nleft+1) in 
235
236  let isSetType = ((Pervasives.compare 
237                         (List.nth param_ty_l ((List.length param_ty_l)-1)) 
238                         (Cic.Sort Cic.Prop)
239                         ) != 0) in
240
241
242
243
244 (* eliminiamo la testa di termty, in quanto e' il nome del predicato e non un parametro.*)
245 let cut_term = foo_cut nleft (List.tl (term_to_list termty)) (list_of_prod ty_indty)  body uri_of_eq in
246
247
248
249 (* cut DXn=DXn \to GOAL *)
250 let proof1,gl1 = PET.apply_tactic (P.cut_tac cut_term) (proof,goal) in
251
252 (* apply Hcut ; reflexivity (su tutti i goals aperti da apply_tac) *)
253 let proof2, gl2 =       PET.apply_tactic
254                                         (Tacticals.then_
255                                                 ~start: (P.apply_tac (C.Rel 1) 
256                                                 ) (* apply Hcut *)
257                                                 ~continuation: (EqualityTactics.reflexivity_tac
258                                                 )
259                                         )       
260                                         (proof1, (List.hd gl1))
261                                         
262  in          
263
264
265
266 (* apply (ledx_ind( lambda x. lambda y, ...)) *)
267
268 let (t1,metasenv,t3,t4) = proof2 in
269 let goal2 = List.hd (List.tl gl1) in
270 let (metano,context,_) = CicUtil.lookup_meta goal2 metasenv in
271
272 let cut_param_ty_l = (cut_first nleft (cut_last param_ty_l)) in
273
274 (* la lista dei soli parametri destri *)
275 let l= cut_first (1+nleft) (term_to_list termty) in
276
277 let lambda_t = foo_lambda nright cut_param_ty_l nright cut_param_ty_l l [] nright body uri_of_eq nleft termty isSetType ty_indty term in 
278 let t = foo_appl nleft (nright+consno) lambda_t eliminator_uri  in
279
280 debug_print (lazy ("Lambda_t: " ^ (CicPp.ppterm t)));
281 prerr_endline ("Term: " ^ (CicPp.ppterm termty));
282 prerr_endline ("Body: " ^ (CicPp.ppterm body));
283 prerr_endline ("Right param: " ^ (CicPp.ppterm (Cic.Appl l)));
284
285
286
287
288
289
290 let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t CicUniv.empty_ugraph in
291
292 let proof2 = (t1,metasenv'',t3,t4) in
293
294 let proof3,gl3 = PET.apply_tactic       (P.apply_tac ref_t)
295                                         (proof2, goal2) in
296
297 let new_goals =
298             ProofEngineHelpers.compare_metasenvs
299              ~oldmetasenv:metasenv ~newmetasenv:metasenv''
300            in
301            
302 let patched_new_goals =
303               let (_,metasenv''',_,_) = proof3 in
304                List.filter
305                 (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
306                 ) new_goals @ gl3
307              in
308
309
310
311
312 (*prerr_endline ("METASENV: " ^ CicMetaSubst.ppmetasenv metasenv []); DEBUG*)
313
314
315 (proof3, patched_new_goals)
316
317 in      
318
319 ProofEngineTypes.mk_tactic (inversion_tac ~term)
320 ;;