]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/inversion_principle.ml
unified: some theorems on Lift started
[helm.git] / components / tactics / inversion_principle.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 let debug = false;; 
27 let debug_print =
28  fun msg -> if debug then prerr_endline (Lazy.force msg) else ()
29
30 (* cuts away the last element of a list 'l' *)
31 let rec cut_last l =
32  match l with
33  | hd::tl when tl != [] -> hd:: (cut_last tl)
34  | _ -> []
35 ;;
36
37 (* cuts away the first 'n' elements of a list 'l' *)
38 let rec cut_first n l =
39  if n>0 then
40   match l with
41    | hd::tl -> cut_first (n-1) tl
42    | [] -> []
43  else l
44 ;;
45
46 (* returns the first 'n' elements of a list 'l' *)
47 let rec takefirst n l =
48  if n > 0 then
49   match l with
50    hd::tl when n > 0 -> hd:: takefirst (n-1) tl
51   | _ -> assert false
52  else []
53 ;;
54
55 (* from a complex Cic.Prod term, returns the list of its components *)
56 let rec list_of_prod term =
57  match term with
58   | Cic.Prod (_,src,tgt) -> src::(list_of_prod tgt)
59   | _ -> [term]
60 ;;
61
62 let rec build_metas sort cons_list created_vars right_created_vars prop
63  uri typeno =
64  match cons_list with
65   | hd::tl -> 
66    Cic.Prod(
67     Cic.Anonymous, 
68     Cic.Implicit None, 
69     build_metas sort tl
70      (List.map (CicSubstitution.lift 1) created_vars) 
71      (List.map (CicSubstitution.lift 1) right_created_vars) 
72      (List.map (CicSubstitution.lift 1) prop) uri typeno)
73   | [] ->  
74    Cic.Prod(
75     Cic.Name("H"), (*new name?*)
76     Cic.Appl([Cic.MutInd(uri, typeno, [])] @ created_vars), 
77     Cic.Appl (( (List.map (CicSubstitution.lift 1) prop)  @ 
78      (List.map (CicSubstitution.lift 1 ) right_created_vars) @
79       (if Inversion.isSetType sort then [Cic.Rel 1] else [])(*H*))
80   )) 
81 ;;
82
83 (* computes the type of the abstract P *)
84 let rec get_prop_arity sort rightparam_tys(*only to name m's*) created_vars_ty 
85  local_rvars left_created_vars nleft uri typeno =
86   match (created_vars_ty) with
87   hd::tl when (nleft > 0) ->
88    get_prop_arity sort rightparam_tys tl local_rvars left_created_vars 
89     (nleft-1) uri typeno
90   | hd::tl ->
91    Cic.Prod(
92     Cic.Name("m" ^  string_of_int(List.length rightparam_tys) ),
93     hd,
94     get_prop_arity sort (List.tl rightparam_tys) 
95      (List.map (CicSubstitution.lift 1) tl)
96      (List.map (CicSubstitution.lift 1) (local_rvars @ [Cic.Rel 1]))
97      (List.map (CicSubstitution.lift 1) left_created_vars) nleft uri typeno
98    )
99   | [] -> 
100    if Inversion.isSetType sort then
101     Cic.Prod(Cic.Anonymous,
102      Cic.Appl([Cic.MutInd(uri, typeno, [])] 
103       @ (List.map (CicSubstitution.lift (-1)) left_created_vars)
104       @ (List.map (CicSubstitution.lift(-1)) local_rvars)  ),
105      Cic.Sort(Cic.Prop))
106    else
107     Cic.Sort Cic.Prop
108 ;;
109
110 (* created vars is empty at the beginning *)
111 let rec build_theorem rightparam_tys arity_l (*arity_l only to name p's*)
112  arity cons_list created_vars created_vars_ty nleft
113  uri typeno = 
114   match (arity) with
115   Cic.Prod(_,src,tgt) -> 
116    Cic.Prod(
117     Cic.Name("p" ^  string_of_int(List.length arity_l)),
118     src,
119     build_theorem rightparam_tys 
120     (List.tl arity_l) tgt cons_list 
121     (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1])) 
122     (List.map (CicSubstitution.lift 1) (created_vars_ty @ [src]))
123      nleft uri typeno) 
124   | sort ->  
125    Cic.Prod(Cic.Name("P"), 
126     get_prop_arity sort rightparam_tys created_vars_ty [](*local vars*) 
127      (takefirst nleft created_vars) (*left_created_vars*) nleft uri typeno, 
128     build_metas sort cons_list created_vars (cut_first nleft created_vars)
129     [(Cic.Rel 1)] uri typeno ) 
130 ;;
131
132 let build_inversion uri obj =
133  (*uri e obj of InductiveDefinition *)
134  let module PET = ProofEngineTypes in
135  let build_one typeno name nleft arity cons_list =
136      (*check if there are right parameters, else return void*)
137      if List.length (list_of_prod arity) = (nleft + 1) then
138        None
139      else
140        try
141          let arity_l = cut_last (list_of_prod arity) in
142          let rightparam_tys = cut_first nleft arity_l in
143          let theorem = build_theorem rightparam_tys arity_l arity cons_list 
144            [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in
145            debug_print 
146              (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem)));
147            let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem  
148              CicUniv.empty_ugraph in
149              (*DEBUG*) debug_print 
150              (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem)));
151              let buri = UriManager.buri_of_uri uri in
152              let inversor_uri = 
153                UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
154              let goal = CicMkImplicit.new_meta metasenv [] in
155              let metasenv' = (goal,[],ref_theorem)::metasenv in
156              let attrs = [`Class (`InversionPrinciple); `Generated] in
157              let proof= 
158                (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem, attrs) in 
159              let _,applies =
160                List.fold_right
161                  (fun _ (i,applies) ->
162                     i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies) 
163                  cons_list (2,[])
164              in
165              let proof1,gl1 = 
166                PET.apply_tactic
167                  (Tacticals.then_
168                     ~start:(PrimitiveTactics.intros_tac ())
169                     (*if the number of applies is 1, we cannot use 
170                       thens, but then_*)
171                     ~continuation:
172                     (match (List.length applies) with
173                          0 -> (Inversion.private_inversion_tac (Cic.Rel 1))
174                        | 1 -> (Tacticals.then_
175                                  ~start:(Inversion.private_inversion_tac 
176                                            (Cic.Rel 1))
177                                  ~continuation:(PrimitiveTactics.apply_tac 
178                                                   (Cic.Rel 2))
179                               )
180                        | _ -> (Tacticals.thens
181                                  ~start:(Inversion.private_inversion_tac 
182                                            (Cic.Rel 1))
183                                  ~continuations:applies
184                               )
185                     ))
186                  (proof,goal) 
187              in
188              let metasenv,bo,ty, attrs =
189                match proof1 with (_,metasenv,bo,ty, attrs) -> metasenv,bo,ty, attrs
190              in
191                assert (metasenv = []);
192                Some
193                  (inversor_uri,
194                   Cic.Constant 
195                     (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
196        with
197            Inversion.EqualityNotDefinedYet -> None
198  in
199    match obj with
200      | Cic.InductiveDefinition (tys,_,nleft,_) ->
201          let counter = ref (List.length tys) in
202          List.fold_right 
203            (fun (name,_,arity,cons_list) res ->
204               counter := !counter-1;
205               match build_one !counter name nleft arity cons_list with
206                 | None -> res 
207                 | Some inv -> inv::res) 
208            tys []
209      |_ -> assert false
210           
211 ;;
212
213 let init () = ();;
214
215 LibrarySync.build_inversion_principle := build_inversion;;