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.oblivion_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 _subst = [] in
 158              let proof=
 159                (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in
 160              let _,applies =
 161                List.fold_right
 162                  (fun _ (i,applies) ->
 163                     i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies)
 164                  cons_list (2,[])
 165              in
 166              let proof1,gl1 =
 167                PET.apply_tactic
 168                  (Tacticals.then_
 169                     ~start:(PrimitiveTactics.intros_tac ())
 170                     (*if the number of applies is 1, we cannot use
 171                       thens, but then_*)
 172                     ~continuation:
 173                     (match (List.length applies) with
 174                          0 -> (Inversion.private_inversion_tac (Cic.Rel 1))
 175                        | 1 -> (Tacticals.then_
 176                                  ~start:(Inversion.private_inversion_tac
 177                                            (Cic.Rel 1))
 178                                  ~continuation:(PrimitiveTactics.apply_tac
 179                                                   (Cic.Rel 2))
 180                               )
 181                        | _ -> (Tacticals.thens
 182                                  ~start:(Inversion.private_inversion_tac
 183                                            (Cic.Rel 1))
 184                                  ~continuations:applies
 185                               )
 186                     ))
 187                  (proof,goal)
 188              in
 189              let metasenv,bo,ty, attrs =
 190                match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs
 191              in
 192                assert (metasenv = []);
 193                Some
 194                  (inversor_uri,
 195                   Cic.Constant
 196                     (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
 197        with
 198           Inversion.EqualityNotDefinedYet -> None
 199         | CicRefine.RefineFailure ls ->
 200            HLog.warn
 201             ("CicRefine.RefineFailure during generation of inversion principle: " ^
 202              Lazy.force ls) ;
 203            None
 204         | CicRefine.Uncertain ls ->
 205            HLog.warn
 206             ("CicRefine.Uncertain during generation of inversion principle: " ^
 207              Lazy.force ls) ;
 208            None
 209         | CicRefine.AssertFailure ls ->
 210            HLog.warn
 211             ("CicRefine.AssertFailure during generation of inversion principle: " ^
 212              Lazy.force ls) ;
 213            None
 214  in
 215    match obj with
 216      | Cic.InductiveDefinition (tys,_,nleft,_) ->
 217          let counter = ref (List.length tys) in
 218          List.fold_right
 219            (fun (name,_,arity,cons_list) res ->
 220               counter := !counter-1;
 221               match build_one !counter name nleft arity cons_list with
 222                 | None -> res
 223                 | Some inv -> inv::res)
 224            tys []
 225      |_ -> assert false
 226
 227 ;;
 228
 229 let init () = ();;
 230
 231 LibrarySync.build_inversion_principle := build_inversion;;