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 typeno = 0 in
 136  let name,nleft,arity,cons_list =
 137   match obj with
 138    Cic.InductiveDefinition (tys,_,nleft,_) ->
 139     let (name,_,arity,cons_list) = List.nth tys typeno in
 140     (*we suppose there is only one inductiveType, so typeno=0 identically *)
 141     (name,nleft,arity,cons_list)
 142   |_ -> assert false
 143  in
 144  (*check if there are right parameters, else return void*)
 145  if List.length (list_of_prod arity) = (nleft + 1) then
 146   None
 147  else
 148   try
 149    let arity_l = cut_last (list_of_prod arity) in
 150    let rightparam_tys = cut_first nleft arity_l in
 151    let theorem = build_theorem rightparam_tys arity_l arity cons_list
 152    [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in
 153    (*DEBUG*) debug_print (lazy ("theorem prima di refine: " ^ (CicPp.ppterm
 154     theorem)));
 155    let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem
 156    CicUniv.empty_ugraph in
 157    (*DEBUG*) debug_print (lazy ("theorem dopo refine: " ^ (CicPp.ppterm
 158     ref_theorem)));
 159    let buri = UriManager.buri_of_uri uri in
 160    let inversor_uri =
 161     UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
 162    let goal = CicMkImplicit.new_meta metasenv [] in
 163    let metasenv' = (goal,[],ref_theorem)::metasenv in
 164    let proof= (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem) in
 165    let _,applies =
 166     List.fold_right
 167      (fun _ (i,applies) ->
 168       i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies)
 169      cons_list (2,[])
 170    in
 171    let proof1,gl1 =
 172     PET.apply_tactic
 173      (Tacticals.then_
 174       ~start:(PrimitiveTactics.intros_tac ())
 175       (*if the number of applies is 1, we cannot use thens, but then_*)
 176       ~continuation:
 177        (match (List.length applies) with
 178         0 -> (Inversion.private_inversion_tac (Cic.Rel 1))
 179       | 1 -> (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         )
 187    ))
 188    (proof,goal)
 189    in
 190    let metasenv,bo,ty =
 191     match proof1 with (_,metasenv,bo,ty) -> metasenv,bo,ty
 192    in
 193    assert (metasenv = []);
 194    Some
 195     (inversor_uri,
 196     Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
 197   with
 198    Inversion.EqualityNotDefinedYet -> None
 199 ;;
 200
 201 let init () = ();;
 202
 203 LibrarySync.build_inversion_principle := build_inversion;;