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 ~universe t ty id ty' =
  49  let just =
  50   match t with
  51      None -> Tactics.auto ~dbd ~params:[] ~universe
  52    | Some t -> Tactics.apply t
  53  in
  54   match id with
  55      None ->
  56       (match ty' with
  57           None -> assert false
  58         | Some ty' ->
  59            Tacticals.then_
  60             ~start:(Tactics.change
  61               ~pattern:(ProofEngineTypes.conclusion_pattern None)
  62               (fun _ metasenv ugraph -> ty,metasenv,ugraph))
  63             ~continuation:just
  64       )
  65    | Some id ->
  66        let continuation =
  67         match ty' with
  68            None -> Tacticals.id_tac
  69          | Some ty' ->
  70              Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  71               (fun _ metasenv ugraph -> ty',metasenv,ugraph)
  72        in
  73         Tacticals.thens
  74         ~start:
  75           (Tactics.cut ty
  76             ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
  77         ~continuations:[ continuation ; just ]
  78 ;;
  79
  80 let bydone ~dbd ~universe t =
  81  let just =
  82   match t with
  83      None -> Tactics.auto ~dbd ~params:[] ~universe
  84    | Some t -> Tactics.apply t
  85  in
  86   just
  87 ;;
  88
  89 let we_need_to_prove t id ty =
  90  match id with
  91     None ->
  92      (match ty with
  93          None -> Tacticals.id_tac (*BUG: check missing here *)
  94        | Some ty ->
  95           Tactics.change ~pattern:(ProofEngineTypes.conclusion_pattern None)
  96            (fun _ metasenv ugraph -> ty,metasenv,ugraph))
  97   | Some id ->
  98      let aux status =
  99       let cont,cutted =
 100        match ty with
 101           None -> Tacticals.id_tac,t
 102         | Some ty ->
 103            Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
 104              (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
 105       let proof,goals =
 106        ProofEngineTypes.apply_tactic
 107         (Tacticals.thens
 108           ~start:
 109            (Tactics.cut cutted
 110              ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
 111           ~continuations:[cont])
 112         status
 113       in
 114        let goals' =
 115         match goals with
 116            [fst; snd] -> [snd; fst]
 117          | _ -> assert false
 118        in
 119         proof,goals'
 120      in
 121       ProofEngineTypes.mk_tactic aux
 122 ;;
 123
 124 let existselim ~dbd ~universe t id1 t1 id2 t2 =
 125  let aux (proof, goal) =
 126   let (n,metasenv,bo,ty,attrs) = proof in
 127   let metano,context,_ = CicUtil.lookup_meta goal metasenv in
 128   let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
 129   let proof' = (n,metasenv,bo,ty,attrs) in
 130    let pattern = ProofEngineTypes.conclusion_pattern (Some (Cic.Rel 1)) in
 131    ProofEngineTypes.apply_tactic (
 132    Tacticals.thens
 133     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
 134     ~continuations:
 135      [ Tactics.elim_intros pattern
 136         ~mk_fresh_name_callback:
 137           (let i = ref 0 in
 138             fun _ _ _  ~typ ->
 139              incr i;
 140              if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
 141        (match t with
 142           None -> Tactics.auto ~dbd ~params:[] ~universe
 143         | Some t -> Tactics.apply t)
 144      ]) (proof', goal)
 145  in
 146   ProofEngineTypes.mk_tactic aux
 147 ;;
 148
 149 let andelim t id1 t1 id2 t2 =
 150  Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t))
 151       ~mk_fresh_name_callback:
 152         (let i = ref 0 in
 153           fun _ _ _  ~typ ->
 154            incr i;
 155            if !i = 1 then Cic.Name id1 else Cic.Name id2)
 156
 157 let rewritingstep ~dbd ~universe lhs rhs just last_step =
 158  let aux ((proof,goal) as status) =
 159   let (curi,metasenv,proofbo,proofty, attrs) = proof in
 160   let _,context,gty = CicUtil.lookup_meta goal metasenv in
 161   let eq,trans =
 162    match LibraryObjects.eq_URI () with
 163       None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
 164     | Some uri ->
 165       Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
 166   in
 167   let ty,_ =
 168    CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
 169   let just =
 170    match just with
 171       `Auto params ->
 172         let params =
 173          if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
 174           ("paramodulation","1")::params
 175          else params in
 176         let params =
 177          if not (List.exists (fun (k,_) -> k = "timeout") params) then
 178           ("timeout","3")::params
 179          else params
 180         in
 181          Tactics.auto ~dbd ~params ~universe
 182     | `Term just -> Tactics.apply just
 183   in
 184    let plhs,prhs,prepare =
 185     match lhs with
 186        None ->
 187         let plhs,prhs =
 188          match gty with
 189             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
 190           | _ -> assert false
 191         in
 192          plhs,prhs,
 193           (fun continuation ->
 194             ProofEngineTypes.apply_tactic continuation status)
 195      | Some (None,lhs) ->
 196         let plhs,prhs =
 197          match gty with
 198             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
 199           | _ -> assert false
 200         in
 201          (*CSC: manca check plhs convertibile con lhs *)
 202          plhs,prhs,
 203           (fun continuation ->
 204             ProofEngineTypes.apply_tactic continuation status)
 205      | Some (Some name,lhs) ->
 206         let newmeta = CicMkImplicit.new_meta metasenv [] in
 207         let irl =
 208          CicMkImplicit.identity_relocation_list_for_metavariable context in
 209         let plhs = lhs in
 210         let prhs = Cic.Meta(newmeta,irl) in
 211          plhs,prhs,
 212           (fun continuation ->
 213             let metasenv = (newmeta, context, ty)::metasenv in
 214             let mk_fresh_name_callback =
 215              fun metasenv context _ ~typ ->
 216               FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
 217                (Cic.Name name) ~typ
 218             in
 219             let proof = curi,metasenv,proofbo,proofty, attrs in
 220             let proof,goals =
 221              ProofEngineTypes.apply_tactic
 222               (Tacticals.thens
 223                 ~start:(Tactics.cut ~mk_fresh_name_callback
 224                  (Cic.Appl [eq ; ty ; lhs ; prhs]))
 225                 ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
 226             in
 227              let goals =
 228               match goals with
 229                  [g1;g2] -> [g2;newmeta;g1]
 230                | _ -> assert false
 231              in
 232               proof,goals)
 233    in
 234     let continuation =
 235      if last_step then
 236       (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
 237       just
 238      else
 239       Tacticals.thens
 240        ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs]))
 241        ~continuations:[just ; Tacticals.id_tac]
 242     in
 243      prepare continuation
 244  in
 245   ProofEngineTypes.mk_tactic aux
 246 ;;
 247
 248 let we_proceed_by_cases_on t pat =
 249  (*BUG here: pat unused *)
 250  Tactics.cases_intros t
 251 ;;
 252
 253 let we_proceed_by_induction_on t pat =
 254  let pattern = Some (fun c m u -> t, m, u), [], Some pat in
 255  Tactics.elim_intros ~depth:0 pattern
 256 ;;
 257
 258 let case id ~params =
 259  (*BUG here: id unused*)
 260  (*BUG here: it does not verify that the previous branch is closed *)
 261  (*BUG here: the params should be parsed telescopically*)
 262  (*BUG here: the tactic_terms should be terms*)
 263  let rec aux ~params ((proof,goal) as status) =
 264   match params with
 265      [] -> proof,[goal]
 266    | (id,t)::tl ->
 267       match ProofEngineTypes.apply_tactic (assume id t) status with
 268          proof,[goal] -> aux tl (proof,goal)
 269        | _ -> assert false
 270  in
 271   ProofEngineTypes.mk_tactic (aux ~params)
 272 ;;
 273
 274 let thesisbecomes t =
 275 let ty = None in
 276  match ty with
 277     None ->
 278      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
 279       (fun _ metasenv ugraph -> t,metasenv,ugraph)
 280   | Some ty ->
 281      (*BUG here: missing check on t *)
 282      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
 283       (fun _ metasenv ugraph -> ty,metasenv,ugraph)
 284 ;;
 285
 286 let byinduction t id  = suppose t id None;;