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   | _ -> assert false
 109 ;;
 110
 111 (* created vars is empty at the beginning *)
 112 let rec build_theorem rightparam_tys arity_l (*arity_l only to name p's*)
 113  arity cons_list created_vars created_vars_ty nleft
 114  uri typeno =
 115   match (arity) with
 116   Cic.Prod(_,src,tgt) ->
 117    Cic.Prod(
 118     Cic.Name("p" ^  string_of_int(List.length arity_l)),
 119     src,
 120     build_theorem rightparam_tys
 121     (List.tl arity_l) tgt cons_list
 122     (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1]))
 123     (List.map (CicSubstitution.lift 1) (created_vars_ty @ [src]))
 124      nleft uri typeno)
 125   | sort ->
 126    Cic.Prod(Cic.Name("P"),
 127     get_prop_arity sort rightparam_tys created_vars_ty [](*local vars*)
 128      (takefirst nleft created_vars) (*left_created_vars*) nleft uri typeno,
 129     build_metas sort cons_list created_vars (cut_first nleft created_vars)
 130     [(Cic.Rel 1)] uri typeno )
 131 ;;
 132
 133 let build_inversion uri obj =
 134  (*uri e obj of InductiveDefinition *)
 135  let module PET = ProofEngineTypes in
 136  let typeno = 0 in
 137  let name,nleft,arity,cons_list =
 138   match obj with
 139    Cic.InductiveDefinition (tys,_,nleft,_) ->
 140     let (name,_,arity,cons_list) = List.nth tys typeno in
 141     (*we suppose there is only one inductiveType, so typeno=0 identically *)
 142     (name,nleft,arity,cons_list)
 143   |_ -> assert false
 144  in
 145  (*check if there are right parameters, else return void*)
 146  if List.length (list_of_prod arity) = (nleft + 1) then
 147   None
 148  else
 149   begin
 150    let arity_l = cut_last (list_of_prod arity) in
 151    let rightparam_tys = cut_first nleft arity_l in
 152    let theorem = build_theorem rightparam_tys arity_l arity cons_list
 153    [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in
 154    (*DEBUG*) debug_print (lazy ("theorem prima di refine: " ^ (CicPp.ppterm
 155     theorem)));
 156    let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem
 157    CicUniv.empty_ugraph in
 158    (*DEBUG*) debug_print (lazy ("theorem dopo refine: " ^ (CicPp.ppterm
 159     ref_theorem)));
 160    let buri = UriManager.buri_of_uri uri in
 161    let inversor_uri =
 162     UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
 163    let goal = CicMkImplicit.new_meta metasenv [] in
 164    let metasenv' = (goal,[],ref_theorem)::metasenv in
 165    let proof= (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem) in
 166    let _,applies =
 167     List.fold_right
 168      (fun _ (i,applies) ->
 169       i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies)
 170      cons_list (2,[])
 171    in
 172    let proof1,gl1 =
 173     PET.apply_tactic
 174      (Tacticals.then_
 175       ~start:(PrimitiveTactics.intros_tac ())
 176       (*if the number of applies is 1, we cannot use thens, but then_*)
 177       ~continuation:
 178        (match (List.length applies) with
 179         0 -> (Inversion.private_inversion_tac (Cic.Rel 1))
 180       | 1 -> (Tacticals.then_
 181          ~start:(Inversion.private_inversion_tac (Cic.Rel 1))
 182          ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
 183          )
 184       | _ -> (Tacticals.thens
 185          ~start:(Inversion.private_inversion_tac (Cic.Rel 1))
 186          ~continuations:applies
 187         )
 188    ))
 189    (proof,goal)
 190    in
 191    let metasenv,bo,ty =
 192     match proof1 with (_,metasenv,bo,ty) -> metasenv,bo,ty
 193    in
 194    assert (metasenv = []);
 195    Some
 196     (inversor_uri,
 197     Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
 198   end
 199 ;;
 200
 201 let init () = ();;
 202
 203 LibrarySync.build_inversion_principle := build_inversion;;