helm/software/components/tactics/declarative.ml

   1 (* Copyright (C) 2006, 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 assume id t =
  27   Tacticals.then_
  28      ~start:
  29        (Tactics.intros ~howmany:1
  30         ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
  31      ~continuation:
  32        (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  33          (fun _ metasenv ugraph -> t,metasenv,ugraph))
  34 ;;
  35
  36 let suppose t id ty =
  37 (*BUG: check on t missing *)
  38  let ty = match ty with None -> t | Some ty -> ty in
  39  Tacticals.then_
  40    ~start:
  41      (Tactics.intros ~howmany:1
  42        ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
  43    ~continuation:
  44      (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  45       (fun _ metasenv ugraph -> ty,metasenv,ugraph))
  46 ;;
  47
  48 let by_term_we_proved ~dbd t ty id ty' =
  49 match id with None -> assert false | Some id ->
  50  let just =
  51   match t with
  52      None -> Tactics.auto ~dbd ~params:[]
  53    | Some t -> Tactics.apply t
  54  in
  55   let continuation =
  56    match ty' with
  57       None -> Tacticals.id_tac
  58     | Some ty' ->
  59         Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  60          (fun _ metasenv ugraph -> ty',metasenv,ugraph)
  61   in
  62    Tacticals.thens
  63    ~start:
  64      (Tactics.cut ty
  65        ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
  66    ~continuations:[ continuation ; just ]
  67 ;;
  68
  69 let bydone ~dbd t =
  70  let just =
  71   match t with
  72      None -> Tactics.auto ~dbd ~params:[]
  73    | Some t -> Tactics.apply t
  74  in
  75   just
  76 ;;
  77
  78 let we_need_to_prove t id ty =
  79 match id with None -> assert false | Some id ->
  80  let aux status =
  81   let cont,cutted =
  82    match ty with
  83       None -> Tacticals.id_tac,t
  84     | Some ty ->
  85        Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  86          (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
  87   let proof,goals =
  88    ProofEngineTypes.apply_tactic
  89     (Tacticals.thens
  90       ~start:
  91        (Tactics.cut cutted
  92          ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
  93       ~continuations:[cont])
  94     status
  95   in
  96    let goals' =
  97     match goals with
  98        [fst; snd] -> [snd; fst]
  99      | _ -> assert false
 100    in
 101     proof,goals'
 102  in
 103   ProofEngineTypes.mk_tactic aux
 104 ;;
 105
 106 let existselim t id1 t1 id2 t2 =
 107 (*BUG: t1 and t2 not used *)
 108 (*PARSING BUG: t2 is parsed in the current context, but it may
 109   have occurrences of id1 in it *)
 110  Tactics.elim_intros t
 111   ~mk_fresh_name_callback:
 112     (let i = ref 0 in
 113       fun _ _ _  ~typ ->
 114        incr i;
 115        if !i = 1 then Cic.Name id1 else Cic.Name id2)
 116
 117 let andelim = existselim;;
 118
 119 let rewritingstep ~dbd lhs rhs just conclude =
 120  let aux ((proof,goal) as status) =
 121   let (curi,metasenv,proofbo,proofty) = proof in
 122   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 123   let eq,trans =
 124    match LibraryObjects.eq_URI () with
 125       None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
 126     | Some uri ->
 127       Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
 128   in
 129   let ty,_ =
 130    CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
 131   let just =
 132    match just with
 133       None ->
 134        Tactics.auto ~dbd
 135         ~params:["paramodulation","1"; "timeout","3"]
 136     | Some just -> Tactics.apply just
 137   in
 138    match lhs with
 139       None ->
 140        let plhs,prhs =
 141         match
 142          fst
 143           (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1)
 144             CicUniv.empty_ugraph)
 145         with
 146            Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
 147          | _ -> assert false in
 148        let last_hyp_name =
 149         match context with
 150            (Some (Cic.Name id,_))::_ -> id
 151          | _ -> assert false
 152        in
 153         (match conclude with
 154             None ->
 155              ProofEngineTypes.apply_tactic
 156               (Tacticals.thens
 157                 ~start:(Tactics.apply ~term:trans)
 158                 ~continuations:
 159                   [ Tactics.apply prhs ;
 160                     Tactics.apply (Cic.Rel 1) ;
 161                     just]) status
 162           | Some name ->
 163              let mk_fresh_name_callback =
 164               fun metasenv context _ ~typ ->
 165                 FreshNamesGenerator.mk_fresh_name ~subst:[]
 166                  metasenv context name ~typ
 167              in
 168               ProofEngineTypes.apply_tactic
 169                (Tacticals.thens
 170                  ~start:(Tactics.cut ~mk_fresh_name_callback
 171                   (Cic.Appl [eq ; ty ; plhs ; rhs]))
 172                  ~continuations:
 173                    [ Tactics.clear ~hyps:[last_hyp_name] ;
 174                      Tacticals.thens
 175                       ~start:(Tactics.apply ~term:trans)
 176                       ~continuations:
 177                         [ Tactics.apply prhs ;
 178                           Tactics.apply (Cic.Rel 1) ;
 179                           just]
 180                    ]) status)
 181     | Some lhs ->
 182        match conclude with
 183           None -> ProofEngineTypes.apply_tactic just status
 184         | Some name ->
 185             let mk_fresh_name_callback =
 186              fun metasenv context _ ~typ ->
 187                FreshNamesGenerator.mk_fresh_name ~subst:[]
 188                 metasenv context name ~typ
 189             in
 190              ProofEngineTypes.apply_tactic
 191               (Tacticals.thens
 192                 ~start:
 193                   (Tactics.cut ~mk_fresh_name_callback
 194                     (Cic.Appl [eq ; ty ; lhs ; rhs]))
 195                 ~continuations:[ Tacticals.id_tac ; just ]) status
 196  in
 197   ProofEngineTypes.mk_tactic aux
 198 ;;
 199
 200 let we_proceed_by_induction_on t pat =
 201  (*BUG here: pat unused *)
 202  Tactics.elim_intros ~depth:0 t
 203 ;;
 204
 205 let case id ~params =
 206  (*BUG here: id unused*)
 207  (*BUG here: it does not verify that the previous branch is closed *)
 208  (*BUG here: the params should be parsed telescopically*)
 209  (*BUG here: the tactic_terms should be terms*)
 210  let rec aux ~params ((proof,goal) as status) =
 211   match params with
 212      [] -> proof,[goal]
 213    | (id,t)::tl ->
 214       match ProofEngineTypes.apply_tactic (assume id t) status with
 215          proof,[goal] -> aux tl (proof,goal)
 216        | _ -> assert false
 217  in
 218   ProofEngineTypes.mk_tactic (aux ~params)
 219 ;;
 220
 221 let thesisbecomes t =
 222 let ty = None in
 223  (*BUG here: missing check on t *)
 224  match ty with
 225     None -> Tacticals.id_tac
 226   | Some ty ->
 227      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
 228       (fun _ metasenv ugraph -> ty,metasenv,ugraph)
 229 ;;
 230
 231 let byinduction t id  = suppose t id None;;