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