matita/components/ng_tactics/declarative.ml

   1 (* Copyright (C) 2019, 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 module Ast = NotationPt
  27 open NTactics
  28 open NTacStatus
  29
  30 type just = [ `Term of NTacStatus.tactic_term | `Auto of NTacStatus.tactic_term GrafiteAst.aauto_params ]
  31
  32 let mk_just =
  33     function
  34           `Auto (l,params) -> NnAuto.auto_tac ~params:(l,params) ?trace_ref:None
  35         | `Term t -> apply_tac t
  36
  37 let extract_conclusion_type status goal =
  38     let gty = get_goalty status goal in
  39     let ctx = ctx_of gty in
  40     let status,gty = term_of_cic_term status gty ctx in
  41     gty
  42 ;;
  43
  44 let same_type_as_conclusion ty t status goal =
  45     let gty = get_goalty status goal in
  46     let ctx = ctx_of gty in
  47     let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
  48     let (_,_,metasenv,subst,_) = status#obj in
  49     let status,ty = term_of_cic_term status cicterm ctx in
  50     if NCicReduction.alpha_eq status metasenv subst ctx t ty then
  51         true
  52     else
  53         false
  54 ;;
  55
  56 let same_type t1 t2 status goal =
  57     let gty = get_goalty status goal in
  58     let ctx = ctx_of gty in
  59     let status1,cicterm1 = disambiguate status ctx t1 `XTNone in
  60     let status1,term1 = term_of_cic_term status cicterm1 (ctx_of cicterm1) in
  61     let status2,cicterm2 = disambiguate status ctx t2 `XTNone in
  62     let status2,term2 = term_of_cic_term status cicterm2 (ctx_of cicterm2) in
  63     let (_,_,metasenv,subst,_) = status#obj in
  64     if NCicReduction.alpha_eq status1 metasenv subst ctx term1 term2 then
  65         true
  66     else
  67         false
  68 ;;
  69
  70 let assume name ty eqty =
  71     distribute_tac (fun status goal ->
  72         match extract_conclusion_type status goal with
  73         | NCic.Prod (_,t,_) ->
  74             if same_type_as_conclusion ty t status goal then
  75                 match eqty with
  76                 | None ->
  77                         let (_,_,ty) = ty in
  78                         exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit
  79                         `JustOne)))) status goal
  80
  81                 | Some eqty ->
  82                     if same_type ty eqty status goal then
  83                     let (_,_,eqty) = eqty in
  84                         exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some eqty),Ast.Implicit
  85                         `JustOne)))) status goal
  86                     else
  87                         fail (lazy "The two given types are not equivalent")
  88             else
  89                 fail (lazy "The assumed type is wrong")
  90         | _ -> fail (lazy "You can't assume without an universal quantification")
  91     )
  92 ;;
  93
  94 let suppose t1 id t2 =
  95     distribute_tac (fun status goal ->
  96         match extract_conclusion_type status goal with
  97         | NCic.Prod (_,t,_) ->
  98             if same_type_as_conclusion t1 t status goal then
  99                 match t2 with
 100                 | None ->
 101                         let (_,_,t1) = t1 in
 102                         exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
 103                         `JustOne)))) status goal
 104
 105                 | Some t2 ->
 106                     if same_type t1 t2 status goal then
 107                     let (_,_,t2) = t2 in
 108                         exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
 109                         `JustOne)))) status goal
 110                     else
 111                         fail (lazy "The two given proposition are not equivalent")
 112             else
 113                 fail (lazy "The supposed proposition is different from the premise")
 114         | _ -> fail (lazy "You can't suppose without a logical implication")
 115     )
 116
 117 let we_need_to_prove t id t1 =
 118     distribute_tac (fun status goal ->
 119         match id with
 120         | None ->
 121             (
 122                 match t1 with
 123                 (* Change the conclusion of the sequent with t *)
 124                 (* Is the pattern correct? Probably not *)
 125                 | None ->  (* We need to prove t *)
 126                     exec (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t) status goal
 127                 | Some t1 -> (* We need to prove t or equivalently t1 *)
 128                     if same_type t1 t status goal then
 129                         exec (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1) status goal
 130                     else
 131                         fail (lazy "The two conclusions are not equivalent")
 132             )
 133         | Some id ->
 134             (
 135                 let (_,_,npt_t) = t in
 136                 match t1 with
 137                 | None -> (* We need to prove t (id) *)
 138                     exec (block_tac [cut_tac t; exact_tac ("",0,(Ast.LetIn ((Ast.Ident
 139                     (id,None),None),npt_t,Ast.Implicit
 140                     `JustOne)))]) status goal
 141                 | Some t1 -> (* We need to prove t (id) or equivalently t1 *)
 142                     exec (block_tac [cut_tac t; change_tac ~where:("",0,(None,[],Some Ast.UserInput))
 143                     ~with_what:t1; exact_tac ("",0,(Ast.LetIn ((Ast.Ident (id,None),None),npt_t,Ast.Implicit
 144                     `JustOne)))]) status goal
 145             )
 146     )
 147 ;;
 148
 149 let by_just_we_proved just ty id ty' =
 150     let just = mk_just just in
 151         match id with
 152         | None ->
 153             (match ty' with
 154                  | None -> (* just we proved P done *)
 155                      just
 156                  | Some ty' -> (* just we proved P that is equivalent to P' done *)
 157                     (* I should probably check that ty' is the same thing as the conclusion of the
 158                     sequent of the open goal and that ty and ty' are equivalent *)
 159                      block_tac [ change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; just]
 160              )
 161         | Some id ->
 162             let ty',continuation =
 163                 match ty' with
 164                     | None -> ty,just
 165                     | Some ty' -> ty', block_tac [change_tac ~where:("",0,(None,[id,Ast.Implicit `JustOne],None))
 166                     ~with_what:ty; just]
 167             in block_tac [cut_tac ty'; continuation ]
 168 ;;
 169
 170 let bydone just =
 171     mk_just just
 172 ;;
 173
 174 (*
 175 let existselim just id1 t1 t2 id2 =
 176  let aux (proof, goal) =
 177   let (n,metasenv,_subst,bo,ty,attrs) = proof in
 178   let metano,context,_ = CicUtil.lookup_meta goal metasenv in
 179   let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
 180   let proof' = (n,metasenv,_subst,bo,ty,attrs) in
 181    ProofEngineTypes.apply_tactic (
 182    Tacticals.thens
 183     ~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)]))
 184     ~continuations:
 185      [ Tactics.elim_intros (Cic.Rel 1)
 186         ~mk_fresh_name_callback:
 187           (let i = ref 0 in
 188             fun _ _ _  ~typ ->
 189              incr i;
 190              if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
 191        (mk_just ~dbd ~automation_cache just)
 192      ]) (proof', goal)
 193  in
 194   ProofEngineTypes.mk_tactic aux
 195 ;;
 196
 197 let andelim just t1 id1 t2 id2 =
 198    Tacticals.thens
 199     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2]))
 200     ~continuations:
 201      [ Tactics.elim_intros (Cic.Rel 1)
 202         ~mk_fresh_name_callback:
 203           (let i = ref 0 in
 204             fun _ _ _  ~typ ->
 205              incr i;
 206              if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
 207        (mk_just ~dbd ~automation_cache just) ]
 208 ;;
 209         *)