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