helm/software/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_one typeno inversor_uri indty_uri nleft arity cons_list selections =
 133  (*check if there are right parameters, else return void*)
 134  if List.length (list_of_prod arity) = (nleft + 1) then
 135   None
 136  else
 137   try
 138          let arity_l = cut_last (list_of_prod arity) in
 139          let rightparam_tys = cut_first nleft arity_l in
 140          let theorem = build_theorem rightparam_tys arity_l arity cons_list
 141           [](*created_vars*) [](*created_vars_ty*) nleft indty_uri typeno in
 142          debug_print
 143           (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem)));
 144          let (ref_theorem,_,metasenv,_) =
 145     CicRefine.type_of_aux' [] [] theorem CicUniv.oblivion_ugraph in
 146          (*DEBUG*) debug_print
 147            (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem)));
 148          let goal = CicMkImplicit.new_meta metasenv [] in
 149          let metasenv' = (goal,[],ref_theorem)::metasenv in
 150          let attrs = [`Class (`InversionPrinciple); `Generated] in
 151    let _subst = [] in
 152          let proof=
 153           Some inversor_uri,metasenv',_subst,
 154      lazy (Cic.Meta(goal,[])),ref_theorem, attrs in
 155          let _,applies =
 156           List.fold_right
 157                (fun _ (i,applies) ->
 158        i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies
 159      ) cons_list (2,[]) in
 160          let proof1,gl1 =
 161           ProofEngineTypes.apply_tactic
 162                (Tacticals.then_
 163                  ~start:(PrimitiveTactics.intros_tac ())
 164                  (*if the number of applies is 1, we cannot use
 165                    thens, but then_*)
 166                  ~continuation:
 167                    (match List.length applies with
 168                             0 -> Inversion.private_inversion_tac (Cic.Rel 1) selections
 169                     | 1 ->
 170             Tacticals.then_
 171                                    ~start:(Inversion.private_inversion_tac (Cic.Rel 1) selections)
 172                                ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
 173                     | _ ->
 174             Tacticals.thens
 175                                    ~start:(Inversion.private_inversion_tac (Cic.Rel 1) selections)
 176                                    ~continuations:applies))
 177                (proof,goal) in
 178    let _,metasenv,_subst,bo,ty, attrs = proof1 in
 179          assert (metasenv = []);
 180          Some
 181               (inversor_uri,
 182                Cic.Constant
 183                 (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[]))
 184   with
 185            Inversion.EqualityNotDefinedYet ->
 186        HLog.warn "No default equality, no inversion principle";
 187        None
 188    | CicRefine.RefineFailure ls ->
 189      HLog.warn
 190       ("CicRefine.RefineFailure during generation of inversion principle: " ^
 191        Lazy.force ls) ;
 192      None
 193    | CicRefine.Uncertain ls ->
 194      HLog.warn
 195       ("CicRefine.Uncertain during generation of inversion principle: " ^
 196        Lazy.force ls) ;
 197      None
 198    | CicRefine.AssertFailure ls ->
 199      HLog.warn
 200       ("CicRefine.AssertFailure during generation of inversion principle: " ^
 201        Lazy.force ls) ;
 202      None
 203 ;;
 204
 205 let build_inverter ~add_obj status u indty_uri params =
 206   let indty_uri, indty_no, _ = UriManager.ind_uri_split indty_uri in
 207   let indty_no = match indty_no with None -> raise (Invalid_argument "not an inductive type")| Some n -> n in
 208   let indty, univ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph indty_uri
 209   in
 210   match indty with
 211   | Cic.InductiveDefinition (tys,_,nleft,attrs) ->
 212      let _,inductive,_,_ = List.hd tys in
 213      if not inductive then raise (Invalid_argument "not an inductive type")
 214      else
 215      let name,_,arity,cons_list = List.nth tys (indty_no-1) in
 216       (match build_one (indty_no-1) u indty_uri nleft arity cons_list params with
 217        | None -> status,[]
 218        | Some (uri, obj) ->
 219            let status, added = add_obj uri obj status in
 220            status, uri::added)
 221   | _ -> assert false
 222 ;;
 223
 224 let build_inversion ~add_obj ~add_coercion uri obj =
 225  match obj with
 226   | Cic.InductiveDefinition (tys,_,nleft,attrs) ->
 227      let _,inductive,_,_ = List.hd tys in
 228      if not inductive then []
 229      else
 230        let counter = ref (List.length tys) in
 231        let all_inverters =
 232               List.fold_right
 233                (fun (name,_,arity,cons_list) res ->
 234          let arity_l = cut_last (list_of_prod arity) in
 235          let rightparam_tys = cut_first nleft arity_l in
 236          let params = HExtlib.mk_list true (List.length rightparam_tys) in
 237          let buri = UriManager.buri_of_uri uri in
 238          let inversor_uri =
 239            UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
 240            counter := !counter-1;
 241                  match build_one !counter inversor_uri uri nleft arity cons_list params with
 242                           None -> res
 243                         | Some inv -> inv::res
 244          ) tys []
 245        in
 246        List.fold_left
 247         (fun lemmas (uri,obj) -> add_obj uri obj @ uri :: lemmas
 248         ) [] all_inverters
 249   | _ -> []
 250 ;;
 251
 252 let init () =
 253   LibrarySync.add_object_declaration_hook build_inversion;;