helm/software/components/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 (* $Id$ *)
  27
  28 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
  29 exception NotAnInductiveTypeToEliminate
  30
  31 let debug = false;;
  32 let debug_print =
  33  fun msg -> if debug then prerr_endline (Lazy.force msg) else ()
  34
  35
  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")
  40
  41 let term_to_list = function
  42  | Cic.Appl l -> l
  43  | _ -> raise (Invalid_argument "Errore in term_to_list")
  44
  45
  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")
  50
  51 (* returns DX1 = DX1 -> ... DXn=DXn -> GOALTY *)
  52 let rec foo_cut nleft parameters parameters_ty body uri_of_eq selections =
  53  if nleft > 0
  54  then
  55   foo_cut (nleft-1) (List.tl parameters)  (List.tl parameters_ty) body
  56    uri_of_eq selections
  57  else
  58   match parameters,selections with
  59    | hd::tl, x::xs when x ->
  60     Cic.Prod (
  61      Cic.Anonymous,
  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 xs)
  67    | hd::tl,x::xs ->
  68       foo_cut nleft tl (List.tl parameters_ty) body uri_of_eq xs
  69    | [],[] -> body
  70    | _ -> raise (Invalid_argument "inverter: the selection doesn't match the arity of the specified inductive type")
  71 ;;
  72
  73 (* from a complex Cic.Prod term, return the list of its components *)
  74 let rec get_sort_type term =
  75  match term with
  76   | Cic.Prod (_,src,tgt) -> (get_sort_type tgt)
  77   | _ -> term
  78 ;;
  79
  80
  81 let rec cut_first n l =
  82  if n>0 then
  83   match l with
  84    | hd::tl -> cut_first (n-1) tl
  85    | [] -> []
  86  else l
  87 ;;
  88
  89
  90 let rec cut_last l =
  91  match l with
  92   | hd::tl when tl != [] -> hd:: (cut_last tl)
  93   | _ -> []
  94 ;;
  95
  96 (* returns the term to apply*)
  97 let foo_appl nleft nright_consno term uri =
  98  let l = [] in
  99  let a = ref l in
 100  for n = 1 to nleft do
 101         a := !a @ [(Cic.Implicit None)]
 102  done;
 103  a:= !a @ [term];
 104  for n = 1 to nright_consno do
 105         a := !a @ [(Cic.Implicit None)]
 106  done;
 107  (*  apply     i_ind           ? ... ?    H *)
 108  Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1])
 109 ;;
 110
 111
 112 (* induction/inversion, abbastanza semplicemente, consiste nel generare i prod
 113  * delle uguaglianze corrispondenti ai soli parametri destri appartenenti all'insieme S.
 114  * Attenzione al caso base: cos'e` replace_lifting?
 115  * S = {} e` il principio di induzione
 116  * S = insieme_dei_destri e` il principio di inversione *)
 117 let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty
 118  uri_of_eq rightparameters_ termty isSetType term selections selections_ =
 119   match right_param_tys, selections with
 120    | hd::tl, x::xs when x -> Cic.Prod (
 121     Cic.Anonymous,
 122     Cic.Appl
 123      [Cic.MutInd(uri_of_eq,0,[]); hd; (List.hd rightparameters);
 124      Cic.Rel base_rel],
 125     foo_prod (nright-1)
 126      (List.map (CicSubstitution.lift 1) tl)
 127      (List.map (CicSubstitution.lift 1) (List.tl rightparameters))
 128      (List.map (CicSubstitution.lift 1) l2)
 129      base_rel (CicSubstitution.lift 1 goalty) uri_of_eq
 130      (List.map (CicSubstitution.lift 1) rightparameters_)
 131      (CicSubstitution.lift 1 termty)
 132      isSetType (CicSubstitution.lift 1 term)) xs selections_
 133    | hd::tl, x::xs ->
 134        foo_prod (nright-1) tl (List.tl rightparameters) l2
 135                         (base_rel-1) goalty uri_of_eq rightparameters_ termty
 136                         isSetType term xs selections_
 137    | [],[] ->
 138        ProofEngineReduction.replace_lifting
 139     ~equality:(fun _ -> CicUtil.alpha_equivalence)
 140     ~context:[]
 141     ~what: (if isSetType
 142      then rightparameters_ @ [term]
 143      else rightparameters_ )
 144     ~with_what: (List.map (CicSubstitution.lift (-1)) l2)
 145     ~where:goalty
 146    | _ -> raise (Invalid_argument "inverter: the selection doesn't match the arity of the specified inductive type")
 147 (* the same subterm of goalty could be simultaneously sx and dx!*)
 148 ;;
 149
 150 (* induction/inversion, abbastanza semplicemente, consiste nel generare i lambda
 151  * soltanto per i parametri destri appartenenti all'insieme S.
 152  * Warning: non ne sono piu` cosi` sicuro...
 153  * S = {} e` il principio di induzione
 154  * S = insieme_dei_destri e` il principio di inversione *)
 155 let rec foo_lambda nright right_param_tys nright_ right_param_tys_
 156  rightparameters created_vars base_rel goalty uri_of_eq rightparameters_
 157  termty isSetType term selections =
 158   match right_param_tys with
 159    | hd::tl -> Cic.Lambda (
 160     (Cic.Name ("lambda" ^ (string_of_int nright))),
 161     hd, (* type *)
 162     foo_lambda (nright-1)
 163      (List.map (CicSubstitution.lift 1) tl) nright_
 164      (List.map (CicSubstitution.lift 1) right_param_tys_)
 165      (List.map (CicSubstitution.lift 1) rightparameters)
 166      (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1]))
 167      base_rel (CicSubstitution.lift 1 goalty) uri_of_eq
 168      (List.map (CicSubstitution.lift 1) rightparameters_)
 169      (CicSubstitution.lift 1 termty) isSetType
 170      (CicSubstitution.lift 1 term)) selections
 171    | [] when isSetType -> Cic.Lambda (
 172     (Cic.Name ("lambda" ^ (string_of_int nright))),
 173     (ProofEngineReduction.replace_lifting
 174      ~equality:(fun _ -> CicUtil.alpha_equivalence)
 175      ~context:[]
 176      ~what: (rightparameters_ )
 177      ~with_what: (List.map (CicSubstitution.lift (-1)) created_vars)
 178      ~where:termty), (* type of H with replaced right parameters *)
 179     foo_prod nright_ (List.map (CicSubstitution.lift 1) right_param_tys_)
 180      (List.map (CicSubstitution.lift 1) rightparameters)
 181      (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1]))
 182      (base_rel+1) (CicSubstitution.lift 1 goalty) uri_of_eq
 183      (List.map (CicSubstitution.lift 1) rightparameters_)
 184      (CicSubstitution.lift 1 termty) isSetType
 185      (CicSubstitution.lift 1 term)) selections selections
 186    | [] -> foo_prod nright_ right_param_tys_ rightparameters created_vars
 187              base_rel goalty uri_of_eq rightparameters_
 188              termty isSetType term selections selections
 189 ;;
 190
 191 let isSetType paramty = ((Pervasives.compare
 192   (get_sort_type paramty)
 193   (Cic.Sort Cic.Prop)) != 0)
 194
 195 exception EqualityNotDefinedYet
 196 let private_inversion_tac ~term selections =
 197  let module T = CicTypeChecker in
 198  let module R = CicReduction in
 199  let module C = Cic in
 200  let module P = PrimitiveTactics in
 201  let module PET = ProofEngineTypes in
 202  let private_inversion_tac ~term (proof, goal) =
 203
 204  (*DEBUG*) debug_print (lazy  ("private inversion begins"));
 205  let _,metasenv,_subst,_,_, _ = proof in
 206  let uri_of_eq =
 207   match LibraryObjects.eq_URI () with
 208      None -> raise EqualityNotDefinedYet
 209   | Some uri -> uri
 210  in
 211  let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
 212  let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
 213  let uri = baseuri_of_term termty in
 214  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 215  let (_,_,typeno,_) =
 216   match termty with
 217    C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
 218    | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
 219     (uri,exp_named_subst,typeno,args)
 220    | _ -> raise NotAnInductiveTypeToEliminate
 221  in
 222  let buri = UriManager.buri_of_uri uri in
 223  let name,nleft,paramty,cons_list =
 224   match o with
 225    C.InductiveDefinition (tys,_,nleft,_) ->
 226     let (name,_,paramty,cons_list) = List.nth tys typeno in
 227     (name,nleft,paramty,cons_list)
 228    |_ -> assert false
 229  in
 230  let eliminator_uri =
 231   UriManager.uri_of_string (buri ^ "/" ^ name ^ "_ind" ^ ".con")
 232  in
 233  let parameters = (List.tl (term_to_list termty)) in
 234  let parameters_tys =
 235   (List.map
 236    (fun t -> (
 237     match (T.type_of_aux' metasenv context t CicUniv.oblivion_ugraph) with
 238      (term,graph) -> term))
 239    parameters)
 240  in
 241  let consno = List.length cons_list in
 242  let nright= ((List.length parameters)- nleft) in
 243  let isSetType = isSetType paramty in
 244  let cut_term = foo_cut nleft parameters
 245   parameters_tys goalty uri_of_eq selections in
 246  (*DEBUG*)  debug_print (lazy ("cut term " ^ CicPp.ppterm cut_term));
 247   debug_print (lazy ("CONTEXT before apply HCUT: " ^
 248    (CicMetaSubst.ppcontext ~metasenv [] context )));
 249   debug_print (lazy ("termty " ^ CicPp.ppterm termty));
 250  (* cut DXn=DXn \to GOAL *)
 251  let proof1,gl1 = PET.apply_tactic (P.cut_tac cut_term) (proof,goal) in
 252  (* apply Hcut ; reflexivity  *)
 253  let proof2, gl2 = PET.apply_tactic
 254   (Tacticals.then_
 255    ~start: (P.apply_tac (C.Rel 1)) (* apply Hcut *)
 256    ~continuation: (EqualityTactics.reflexivity_tac)
 257   ) (proof1, (List.hd gl1))
 258  in
 259  (*DEBUG*) debug_print (lazy  ("after apply HCUT;reflexivity
 260   in private inversion"));
 261  (* apply (ledx_ind( lambda x. lambda y, ...)) *)
 262  let t1,metasenv,_subst,t3,t4, attrs = proof2 in
 263  let goal2 = List.hd (List.tl gl1) in
 264  let (_,context,g2ty) = CicUtil.lookup_meta goal2 metasenv in
 265  (* rightparameters type list *)
 266  let rightparam_ty_l = (cut_first nleft parameters_tys) in
 267  (* rightparameters list *)
 268  let rightparameters= cut_first nleft parameters in
 269  debug_print
 270   (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl rightparameters))));
 271  let lambda_t = foo_lambda nright rightparam_ty_l nright rightparam_ty_l
 272  rightparameters [] nright goalty uri_of_eq rightparameters termty isSetType
 273  term selections in
 274  let t = foo_appl nleft (nright+consno) lambda_t eliminator_uri in
 275  debug_print (lazy ("Lambda_t: " ^ (CicPp.ppterm t)));
 276  debug_print (lazy ("Term: " ^ (CicPp.ppterm termty)));
 277  debug_print (lazy ("Body: " ^ (CicPp.ppterm goalty)));
 278  debug_print
 279   (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl rightparameters))));
 280  debug_print (lazy ("CONTEXT before refinement: " ^
 281   (CicMetaSubst.ppcontext ~metasenv [] context )));
 282   (*DEBUG*) debug_print (lazy  ("private inversion: term before refinement: " ^
 283    CicPp.ppterm t));
 284  let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
 285   CicUniv.oblivion_ugraph
 286  in
 287  (*DEBUG*) debug_print (lazy  ("private inversion: termine after refinement: "
 288   ^ CicPp.ppterm ref_t));
 289  let proof2 = (t1,metasenv'',_subst,t3,t4, attrs) in
 290  let my_apply_tac =
 291   let my_apply_tac status =
 292    let proof,goals =
 293     ProofEngineTypes.apply_tactic (P.apply_tac ref_t) status in
 294    let patched_new_goals =
 295     let (_,metasenv''',_subst,_,_, _) = proof in
 296     let new_goals = ProofEngineHelpers.compare_metasenvs
 297      ~oldmetasenv:metasenv ~newmetasenv:metasenv''
 298     in
 299     List.filter (function i -> List.exists (function (j,_,_) -> j=i)
 300      metasenv''') new_goals @ goals
 301    in
 302    proof,patched_new_goals
 303   in
 304  ProofEngineTypes.mk_tactic my_apply_tac
 305  in
 306  let proof3,gl3 =
 307  PET.apply_tactic
 308   (Tacticals.then_
 309    ~start:my_apply_tac
 310    ~continuation:
 311     (ReductionTactics.simpl_tac (ProofEngineTypes.conclusion_pattern(None))))
 312     (proof2,goal2)
 313  in
 314
 315  (proof3, gl3)
 316 in
 317 ProofEngineTypes.mk_tactic (private_inversion_tac ~term)
 318 ;;
 319
 320
 321 let inversion_tac ~term =
 322  let module T = CicTypeChecker in
 323  let module R = CicReduction in
 324  let module C = Cic in
 325  let module P = PrimitiveTactics in
 326  let module PET = ProofEngineTypes in
 327  let inversion_tac ~term (proof, goal) =
 328  (*DEBUG*) debug_print (lazy ("inversion begins"));
 329   let _,metasenv,_subst,_,_, _ = proof in
 330   let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
 331   let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
 332   let uri, typeno =
 333     match termty with
 334       | Cic.MutInd (uri,typeno,_)
 335       | Cic.Appl(Cic.MutInd (uri,typeno,_)::_) -> uri,typeno
 336       | _ -> assert false
 337   in
 338   (* let uri = baseuri_of_term termty in *)
 339   let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 340   let name,nleft,arity,cons_list =
 341    match obj with
 342     Cic.InductiveDefinition (tys,_,nleft,_) ->
 343      let (name,_,arity,cons_list) = List.nth tys typeno in
 344         (name,nleft,arity,cons_list)
 345    |_ -> assert false
 346   in
 347   let buri = UriManager.buri_of_uri uri in
 348   let inversor_uri =
 349    UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
 350   (* arity length = number  of parameters plus 1 *)
 351   let arity_length = (List.length (term_to_list termty)) in
 352   (* Check the existence of any right parameter. *)
 353   assert (arity_length > (nleft + 1));
 354   let appl_term arity_consno uri =
 355    let l = [] in
 356    let a = ref l in
 357    for n = 1 to arity_consno do
 358     a := (Cic.Implicit None)::(!a)
 359    done;
 360    (* apply    i_inv             ? ...?      H).     *)
 361    Cic.Appl ([Cic.Const(uri,[])] @ !a @ [term])
 362   in
 363   let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
 364   let (t1,metasenv,_subst,t3,t4, attrs) = proof in
 365   let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
 366   CicUniv.oblivion_ugraph
 367   in
 368   let proof = (t1,metasenv'',_subst,t3,t4, attrs) in
 369   let proof3,gl3 =
 370      ProofEngineTypes.apply_tactic (P.apply_tac ref_t) (proof,goal) in
 371   let patched_new_goals =
 372      let (_,metasenv''',_subst,_,_, _) = proof3 in
 373      let new_goals = ProofEngineHelpers.compare_metasenvs
 374       ~oldmetasenv:metasenv ~newmetasenv:metasenv''
 375      in
 376      List.filter (function i -> List.exists (function (j,_,_) -> j=i)
 377       metasenv''') new_goals @ gl3
 378     in
 379   (proof3, patched_new_goals)
 380  in
 381 ProofEngineTypes.mk_tactic (inversion_tac ~term)
 382 ;;