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 NnAuto.auto_params ]
  31
  32 let mk_just =
  33     function
  34           `Auto (l,params) -> distribute_tac (fun status goal -> NnAuto.auto_lowtac
  35           ~params:(l,params) status goal)
  36         | `Term t -> apply_tac t
  37
  38 exception NotAProduct
  39 exception FirstTypeWrong
  40 exception NotEquivalentTypes
  41
  42 let extract_conclusion_type status goal =
  43     let gty = get_goalty status goal in
  44     let ctx = ctx_of gty in
  45     let status,gty = term_of_cic_term status gty ctx in
  46     gty
  47 ;;
  48
  49 let same_type_as_conclusion ty t status goal =
  50     let gty = get_goalty status goal in
  51     let ctx = ctx_of gty in
  52     let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
  53     let (_,_,metasenv,subst,_) = status#obj in
  54     let status,ty = term_of_cic_term status cicterm ctx in
  55     if NCicReduction.alpha_eq status metasenv subst ctx t ty then
  56         true
  57     else
  58         false
  59 ;;
  60
  61 let are_convertible ty1 ty2 status goal =
  62     let gty = get_goalty status goal in
  63     let ctx = ctx_of gty in
  64     let status,cicterm1 = disambiguate status ctx ty1 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
  65     let status,cicterm2 = disambiguate status ctx ty2 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
  66     NTacStatus.are_convertible status ctx cicterm1 cicterm2
  67
  68 (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
  69 the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
  70 \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
  71 *)
  72 let lambda_abstract_tac id t1 t2 status goal =
  73     match extract_conclusion_type status goal with
  74     | NCic.Prod (_,t,_) ->
  75         if same_type_as_conclusion t1 t status goal then
  76             match t2 with
  77             | None ->
  78                     let (_,_,t1) = t1 in
  79                     exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
  80                     `JustOne)))) status goal
  81
  82             | Some t2 ->
  83                 let status,res = are_convertible t1 t2 status goal in
  84                 if res then
  85                 let (_,_,t2) = t2 in
  86                     exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
  87                     `JustOne)))) status goal
  88                 else
  89                     raise NotEquivalentTypes
  90         else
  91             raise FirstTypeWrong
  92     | _ -> raise NotAProduct
  93
  94 let assume name ty eqty =
  95     distribute_tac (fun status goal ->
  96         try lambda_abstract_tac name ty eqty status goal
  97         with
  98         | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
  99         | FirstTypeWrong ->  fail (lazy "The assumed type is wrong")
 100         | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
 101      )
 102 ;;
 103
 104 let suppose t1 id t2 =
 105     distribute_tac (fun status goal ->
 106         try lambda_abstract_tac id t1 t2 status goal
 107         with
 108         | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
 109         | FirstTypeWrong ->  fail (lazy "The supposed proposition is different from the premise")
 110         | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
 111      )
 112 ;;
 113
 114 let assert_tac t1 t2 status goal continuation =
 115     let t = extract_conclusion_type status goal in
 116     if same_type_as_conclusion t1 t status goal then
 117         match t2 with
 118         | None -> exec continuation status goal
 119         | Some t2 ->
 120             let status,res = are_convertible t1 t2 status goal in
 121             if res then
 122                 exec continuation status goal
 123             else
 124                 raise NotEquivalentTypes
 125     else
 126         raise FirstTypeWrong
 127
 128 let we_need_to_prove t id t1 =
 129     distribute_tac (fun status goal ->
 130         match id with
 131         | None ->
 132             (
 133                 match t1 with
 134                 | None ->  (* We need to prove t *)
 135                     (
 136                     try
 137                         assert_tac t None status goal id_tac
 138                     with
 139                     | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
 140                     )
 141                 | Some t1 -> (* We need to prove t or equivalently t1 *)
 142                     (
 143                         try
 144                             assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1)
 145                         with
 146                         | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
 147                         | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
 148                     )
 149             )
 150         | Some id ->
 151             (
 152                 match t1 with
 153                 | None -> (* We need to prove t (id) *)
 154                     exec (block_tac [cut_tac t; branch_tac ~force:false; shift_tac; intro_tac id;
 155                     (*merge_tac*)]) status goal
 156                 | Some t1 -> (* We need to prove t (id) or equivalently t1 *)
 157                     exec (block_tac [cut_tac t; branch_tac ~force:false; change_tac ~where:("",0,(None,[],Some Ast.UserInput))
 158                     ~with_what:t1; shift_tac; intro_tac id; merge_tac]) status goal
 159             )
 160     )
 161 ;;
 162
 163 let by_just_we_proved just ty id ty' =
 164     distribute_tac (fun status goal ->
 165         let just = mk_just just in
 166             match id with
 167             | None ->
 168                 (match ty' with
 169                      | None -> (* just we proved P done *)
 170                         (
 171                             try
 172                                 assert_tac ty None status goal just
 173                             with
 174                             | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
 175                             | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
 176                         )
 177                      | Some ty' -> (* just we proved P that is equivalent to P' done *)
 178                         (
 179                             try
 180                                 assert_tac ty' (Some ty) status goal (block_tac [change_tac
 181                                 ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; just])
 182                             with
 183                             | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion")
 184                             | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
 185                         )
 186                  )
 187             | Some id ->
 188                 (
 189                     match ty' with
 190                     | None -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac
 191                     id; merge_tac ]) status goal
 192                     | Some ty' -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac
 193                     id; change_tac ~where:("",0,(None,[id,Ast.UserInput],None))
 194                     ~with_what:ty'; merge_tac]) status goal
 195                 )
 196     )
 197 ;;
 198
 199 let thesisbecomes t1 t2 = we_need_to_prove t1 None t2 ;;
 200
 201 let bydone just =
 202     mk_just just
 203 ;;
 204
 205 let existselim just id1 t1 t2 id2 =
 206     let (_,_,t1) = t1 in
 207     let (_,_,t2) = t2 in
 208     let just = mk_just just in
 209     block_tac [
 210         cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
 211         (id1,None), Some t1),t2)]));
 212         branch_tac ~force:false;
 213         just;
 214         shift_tac;
 215         case1_tac "_";
 216         intros_tac ~names_ref:(ref []) [id1;id2];
 217         merge_tac
 218     ]
 219
 220 let andelim just t1 id1 t2 id2 =
 221     let (_,_,t1) = t1 in
 222     let (_,_,t2) = t2 in
 223     let just = mk_just just in
 224     block_tac [
 225         cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
 226         branch_tac ~force:false;
 227         just;
 228         shift_tac;
 229         case1_tac "_";
 230         intros_tac ~names_ref:(ref []) [id1;id2];
 231         merge_tac
 232     ]
 233 ;;
 234
 235
 236
 237 let rewritingstep lhs rhs just last_step = fail (lazy "Not implemented");
 238  (*
 239  let aux ((proof,goal) as status) =
 240   let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
 241   let _,context,gty = CicUtil.lookup_meta goal metasenv in
 242   let eq,trans =
 243    match LibraryObjects.eq_URI () with
 244       None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
 245     | Some uri ->
 246       Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
 247   in
 248   let ty,_ =
 249    CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in
 250   let just' =
 251    match just with
 252       `Auto (univ, params) ->
 253         let params =
 254          if not (List.exists (fun (k,_) -> k = "timeout") params) then
 255           ("timeout","3")::params
 256          else params
 257         in
 258         let params' =
 259          if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
 260           ("paramodulation","1")::params
 261          else params
 262         in
 263          if params = params' then
 264           Tactics.auto ~dbd ~params:(univ, params) ~automation_cache
 265          else
 266           Tacticals.first
 267            [Tactics.auto ~dbd ~params:(univ, params) ~automation_cache ;
 268             Tactics.auto ~dbd ~params:(univ, params') ~automation_cache]
 269     | `Term just -> Tactics.apply just
 270     | `SolveWith term ->
 271                     Tactics.demodulate ~automation_cache ~dbd
 272                     ~params:(Some [term],
 273                       ["all","1";"steps","1"; "use_context","false"])
 274     | `Proof ->
 275         Tacticals.id_tac
 276   in
 277    let plhs,prhs,prepare =
 278     match lhs with
 279        None ->
 280         let plhs,prhs =
 281          match gty with
 282             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
 283           | _ -> assert false
 284         in
 285          plhs,prhs,
 286           (fun continuation ->
 287             ProofEngineTypes.apply_tactic continuation status)
 288      | Some (None,lhs) ->
 289         let plhs,prhs =
 290          match gty with
 291             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
 292           | _ -> assert false
 293         in
 294          (*CSC: manca check plhs convertibile con lhs *)
 295          plhs,prhs,
 296           (fun continuation ->
 297             ProofEngineTypes.apply_tactic continuation status)
 298      | Some (Some name,lhs) ->
 299         let newmeta = CicMkImplicit.new_meta metasenv [] in
 300         let irl =
 301          CicMkImplicit.identity_relocation_list_for_metavariable context in
 302         let plhs = lhs in
 303         let prhs = Cic.Meta(newmeta,irl) in
 304          plhs,prhs,
 305           (fun continuation ->
 306             let metasenv = (newmeta, context, ty)::metasenv in
 307             let mk_fresh_name_callback =
 308              fun metasenv context _ ~typ ->
 309               FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
 310                (Cic.Name name) ~typ
 311             in
 312             let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
 313             let proof,goals =
 314              ProofEngineTypes.apply_tactic
 315               (Tacticals.thens
 316                 ~start:(Tactics.cut ~mk_fresh_name_callback
 317                  (Cic.Appl [eq ; ty ; lhs ; prhs]))
 318                 ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
 319             in
 320              let goals =
 321               match just,goals with
 322                  `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1]
 323                | _, [g1;g2] -> [g2;newmeta;g1]
 324                | _, l ->
 325                  prerr_endline (String.concat "," (List.map string_of_int l));
 326                  prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
 327                  assert false
 328              in
 329               proof,goals)
 330    in
 331     let continuation =
 332      if last_step then
 333       (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
 334       just'
 335      else
 336       Tacticals.thens
 337        ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs]))
 338        ~continuations:[just' ; Tacticals.id_tac]
 339     in
 340      prepare continuation
 341  in
 342   ProofEngineTypes.mk_tactic aux
 343 ;;
 344   *)