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