]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_tactics/nInversion.ml
relocate fixed
[helm.git] / helm / software / components / ng_tactics / nInversion.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
13
14 (*let pp m = prerr_endline (Lazy.force m);;*)
15 let pp _ = ();;
16
17 let fresh_name =
18  let i = ref 0 in
19  function () ->
20   incr i;
21   "z" ^ string_of_int !i
22 ;;
23
24 let mk_id id =
25  let id = if id = "_" then fresh_name () else id in
26   CicNotationPt.Ident (id,None)
27 ;;
28
29 let rec split_arity ~subst context te =
30   match NCicReduction.whd ~subst context te with
31    | NCic.Prod (name,so,ta) -> 
32        split_arity ~subst ((name, (NCic.Decl so))::context) ta
33    | t -> context, t
34 ;;
35
36 let mk_appl =
37  function
38     [] -> assert false
39   | [x] -> x
40   | l -> CicNotationPt.Appl l
41 ;;
42
43 let rec mk_prods l t =
44   match l with
45     [] -> t
46   | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
47 ;;
48
49 let rec mk_lambdas l t =
50   match l with
51     [] -> t
52   | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t)
53 ;;
54
55 let rec mk_arrows xs ys selection target = 
56   match selection,xs,ys with
57     [],[],[] -> target
58   | false :: l,x::xs,y::ys -> mk_arrows xs ys l target
59   | true :: l,x::xs,y::ys  -> 
60      CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
61                            mk_arrows xs ys l target)
62   | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
63 ;;
64
65 let subst_metasenv_and_fix_names status =
66   let u,h,metasenv, subst,o = status#obj in
67   let o = 
68     NCicUntrusted.map_obj_kind ~skip_body:true 
69      (NCicUntrusted.apply_subst subst []) o
70   in
71    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
72 ;;
73
74 let mk_inverter name it leftno ?selection outsort status baseuri =
75  pp (lazy ("leftno = " ^ string_of_int leftno));
76  let _,ind_name,ty,cl = it in
77  pp (lazy ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
78  let ncons = List.length cl in
79  (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
80  let params = List.rev_map (function name,_ -> mk_id name) params in
81  pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));*)
82  let args,sort= split_arity ~subst:[] [] ty in
83  pp (lazy ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort));
84  (*let args = List.rev_map (function name,_ -> mk_id name) args in
85  pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));*)
86  let nparams = List.length args in
87  pp (lazy ("nparams = " ^ string_of_int nparams));
88  if nparams <= leftno 
89    then raise (Failure "inverter: the type must have at least one right parameter") 
90    else 
91      let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in
92      pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs)));
93      let ls, rs = HExtlib.split_nth leftno xs in
94      pp (lazy ("lunghezza ls = " ^ string_of_int (List.length ls)));
95      pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs)));
96      let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in
97     
98      let _id_xs = List.map mk_id xs in
99      let id_ls = List.map mk_id ls in
100      let id_rs = List.map mk_id rs in
101      let id_ys = List.map mk_id ys in
102     
103      (* pseudocode  let t = Lambda y1 ... yr. xs_ = ys_ -> pred *)
104     
105      (* check: assuming we have more than one right parameter *) 
106      (* pred := P yr- *)
107      let pred = mk_appl ((mk_id "P")::id_ys) in
108      
109      let selection = match selection with 
110          None -> HExtlib.mk_list true (List.length ys) 
111        | Some s -> s
112      in
113      let prods = mk_arrows id_rs id_ys selection pred in
114     
115      let lambdas = mk_lambdas (ys@["p"]) prods in
116      
117      let hyplist = 
118        let rec hypaux k = function
119            0 -> []
120          | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1)
121        in (hypaux 1 ncons)
122      in
123      pp (lazy ("lunghezza ys = " ^ string_of_int (List.length ys)));
124     
125      let outsort, suffix = NCicElim.ast_of_sort outsort in
126      let theorem = mk_prods xs
127                     (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))),
128                     mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *)
129                                       Some (CicNotationPt.Implicit `JustOne)),
130                                       mk_appl (mk_id "P"::id_rs)))))
131      in 
132      let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @
133                        List.map mk_id hyplist @
134                        CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in
135     
136      let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
137                              (baseuri ^ name ^ ".def",
138                                0,CicNotationPt.Theorem (`Theorem,name,theorem,Some
139                                (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) in 
140      let uri,height,nmenv,nsubst,nobj = theorem in
141      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
142      let status = status#set_obj theorem in
143      let status = status#set_stack ninitial_stack in
144      let status = subst_metasenv_and_fix_names status in
145     
146      let cut_theorem = 
147        let rs = List.map (fun x -> mk_id x) rs in
148          mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in
149     
150      let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
151                         CicNotationPt.Implicit (`Tagged "end"));
152                         CicNotationPt.Implicit (`Tagged "cut")] in
153      let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
154      
155      let status = NTactics.block_tac 
156                             (NTactics.branch_tac::
157                              NTactics.case_tac "inv"::
158                              (intros @
159                               [NTactics.apply_tac ("",0,cut);
160                                NTactics.branch_tac;
161                                NTactics.case_tac "end";
162                                NTactics.apply_tac ("",0,mk_id "Hcut");
163                                NTactics.apply_tac ("",0,mk_id "refl_eq"); 
164                                NTactics.shift_tac;
165                                NTactics.case_tac "cut";
166                                NTactics.apply_tac ("",0,t)
167                              (*    ;
168                                NTactics.merge_tac;
169                                NTactics.merge_tac;
170                                NTactics.skip_tac*)])) status in
171      status,status#obj
172 ;;
173