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 open Continuationals.Stack
  27 module Ast = NotationPt
  28 open NTactics
  29 open NTacStatus
  30
  31 type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ]
  32
  33 let mk_just status goal =
  34   function
  35     `Auto (l,params) -> NnAuto.auto_lowtac ~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_first_goal_from_status status =
  43   let s = status#stack in
  44   match s with
  45   | [] -> fail (lazy "There's nothing to prove")
  46   | (g1, _, k, tag1) :: tl ->
  47     let goals = filter_open g1 in
  48     let (loc::tl) = goals in
  49     let goal = goal_of_loc (loc) in
  50     goal ;;
  51
  52 let extract_conclusion_type status goal =
  53   let gty = get_goalty status goal in
  54   let ctx = ctx_of gty in
  55   let status,gty = term_of_cic_term status gty ctx in
  56   gty
  57 ;;
  58
  59 let alpha_eq_tacterm_kerterm ty t status goal =
  60   let gty = get_goalty status goal in
  61   let ctx = ctx_of gty in
  62   let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
  63   let (_,_,metasenv,subst,_) = status#obj in
  64   let status,ty = term_of_cic_term status cicterm ctx in
  65   if NCicReduction.alpha_eq status metasenv subst ctx t ty then
  66     true
  67   else
  68     false
  69 ;;
  70
  71 let are_convertible ty1 ty2 status goal =
  72   let gty = get_goalty status goal in
  73   let ctx = ctx_of gty in
  74   let status,cicterm1 = disambiguate status ctx ty1 `XTNone in
  75   let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
  76   NTacStatus.are_convertible status ctx cicterm1 cicterm2
  77
  78 (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
  79    the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
  80    \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
  81 *)
  82 let lambda_abstract_tac id t1 t2 status goal =
  83   match extract_conclusion_type status goal with
  84   | NCic.Prod (_,t,_) ->
  85     if alpha_eq_tacterm_kerterm t1 t status goal then
  86       match t2 with
  87       | None ->
  88         let (_,_,t1) = t1 in
  89         exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
  90                                        `JustOne))) (*status*)
  91       | Some t2 ->
  92         let status,res = are_convertible t1 t2 status goal in
  93         if res then
  94           let (_,_,t2) = t2 in
  95           exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
  96                                          `JustOne))) (*status*)
  97         else
  98           raise NotEquivalentTypes
  99     else
 100       raise FirstTypeWrong
 101   | _ -> raise NotAProduct
 102
 103 let assume name ty eqty =
 104   distribute_tac (fun status goal ->
 105       try exec (lambda_abstract_tac name ty eqty status goal) status goal
 106       with
 107       | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
 108       | FirstTypeWrong ->  fail (lazy "The assumed type is wrong")
 109       | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
 110     )
 111 ;;
 112
 113 let suppose t1 id t2 =
 114   distribute_tac (fun status goal ->
 115       try exec (lambda_abstract_tac id t1 t2 status goal) status goal
 116       with
 117       | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
 118       | FirstTypeWrong ->  fail (lazy "The supposed proposition is different from the premise")
 119       | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
 120     )
 121 ;;
 122
 123 let assert_tac t1 t2 status goal continuation =
 124   let t = extract_conclusion_type status goal in
 125   if alpha_eq_tacterm_kerterm t1 t status goal then
 126     match t2 with
 127     | None -> continuation
 128     | Some t2 ->
 129       let status,res = are_convertible t1 t2 status goal in
 130       if res then continuation
 131       else
 132         raise NotEquivalentTypes
 133   else
 134     raise FirstTypeWrong
 135
 136 let mustdot status =
 137   let s = status#stack in
 138   match s with
 139   | [] -> fail (lazy "No goals to dot")
 140   | (_, _, k, _) :: tl ->
 141     if List.length k > 0 then
 142       true
 143     else
 144       false
 145
 146 let bydone just status =
 147   let goal = extract_first_goal_from_status status in
 148   let mustdot = mustdot status in
 149   let l = [mk_just status goal just] in
 150   let l =
 151     if mustdot then List.append l [dot_tac] else l
 152   in
 153   block_tac l status
 154 ;;
 155
 156 let we_need_to_prove t id t1 status =
 157   let goal = extract_first_goal_from_status status in
 158   match id with
 159   | None ->
 160     (
 161       match t1 with
 162       | None ->  (* We need to prove t *)
 163         (
 164           try assert_tac t None status goal (id_tac status)
 165           with
 166           | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
 167         )
 168       | Some t1 -> (* We need to prove t or equivalently t1 *)
 169         (
 170           try assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some
 171                                                                              Ast.UserInput)) ~with_what:t1 status)
 172           with
 173           | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
 174           | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
 175         )
 176     )
 177   | Some id ->
 178     (
 179       match t1 with
 180       (* We need to prove t (id) *)
 181       | None -> block_tac [cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac;
 182                            dot_tac
 183                           ] status
 184       (* We need to prove t (id) or equivalently t1 *)
 185       | Some t1 ->  block_tac [cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some
 186                                                                                   Ast.UserInput))
 187                                  ~with_what:t1; shift_tac; intro_tac id; merge_tac;
 188                                dot_tac
 189                               ]
 190                       status
 191     )
 192 ;;
 193
 194 let by_just_we_proved just ty id ty' status =
 195   let goal = extract_first_goal_from_status status in
 196   let wrappedjust = just in
 197   let just = mk_just status goal just in
 198   match id with
 199   | None ->
 200     (match ty' with
 201      | None -> (* just we proved P done *)
 202        (
 203          try
 204            assert_tac ty None status goal (bydone wrappedjust status)
 205          with
 206          | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
 207          | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
 208        )
 209      | Some ty' -> (* just we proved P that is equivalent to P' done *)
 210        (
 211          try
 212            assert_tac ty' None status goal (block_tac [change_tac ~where:("",0,(None,[],Some
 213                                                                                   Ast.UserInput))
 214                                                          ~with_what:ty; bydone wrappedjust]
 215                                               status )
 216          with
 217          | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion")
 218          | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
 219        )
 220     )
 221   | Some id ->
 222     (
 223       match ty' with
 224       | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac ] status
 225       | Some ty' -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; change_tac
 226                                  ~where:("",0,(None,[id,Ast.UserInput],None)) ~with_what:ty';
 227                                merge_tac] status
 228     )
 229 ;;
 230
 231 let existselim just id1 t1 t2 id2 =
 232   distribute_tac (fun status goal ->
 233       let (_,_,t1) = t1 in
 234       let (_,_,t2) = t2 in
 235       let just = mk_just status goal just in
 236       exec (block_tac [
 237           cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
 238                                                                                      (id1,None), Some t1),t2)]));
 239           branch_tac ~force:false;
 240           just;
 241           shift_tac;
 242           case1_tac "_";
 243           intros_tac ~names_ref:(ref []) [id1;id2];
 244           merge_tac
 245         ]) status goal
 246     )
 247 ;;
 248
 249 let andelim just t1 id1 t2 id2  =
 250   distribute_tac (fun status goal ->
 251       let (_,_,t1) = t1 in
 252       let (_,_,t2) = t2 in
 253       let just = mk_just status goal just in
 254       exec (block_tac [
 255           cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
 256           branch_tac ~force:false;
 257           just;
 258           shift_tac;
 259           case1_tac "_";
 260           intros_tac ~names_ref:(ref []) [id1;id2];
 261           merge_tac
 262         ]) status goal
 263     )
 264 ;;
 265
 266 let type_of_tactic_term status ctx t =
 267   let status,cicterm = disambiguate status ctx t `XTNone in
 268   let (_,cicty) = typeof status ctx cicterm in
 269   cicty
 270
 271 let swap_first_two_goals_tac status =
 272   let gstatus =
 273     match status#stack with
 274     | [] -> assert false
 275     | (g,t,k,tag) :: s ->
 276       match g with
 277       | (loc1) :: (loc2) :: tl ->
 278         ([loc2;loc1] @+ tl,t,k,tag) :: s
 279       | _ -> assert false
 280   in
 281   status#set_stack gstatus
 282
 283 let thesisbecomes t1 t2 = we_need_to_prove t1 None t2
 284 ;;
 285
 286 let obtain id t1 status =
 287   let goal = extract_first_goal_from_status status in
 288   let cicgty = get_goalty status goal in
 289   let ctx = ctx_of cicgty in
 290   let cicty = type_of_tactic_term status ctx t1 in
 291   let _,ty = term_of_cic_term status cicty ctx in
 292   let (_,_,t1) = t1 in
 293   block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
 294                                          `JustOne]));
 295               swap_first_two_goals_tac;
 296               branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; dot_tac;
 297             ]
 298     status
 299 ;;
 300
 301 let conclude t1 =
 302   distribute_tac (fun status goal ->
 303       let cicgty = get_goalty status goal in
 304       let ctx = ctx_of cicgty in
 305       let _,gty = term_of_cic_term status cicgty ctx in
 306       match gty with
 307         NCic.Appl [_;_;plhs;_] ->
 308         if alpha_eq_tacterm_kerterm t1 plhs status goal then
 309           exec id_tac status goal
 310         else
 311           fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
 312       | _ -> fail (lazy "Your conclusion needs to be an equality")
 313     )
 314 ;;
 315
 316 let rewritingstep rhs just last_step status =
 317   let goal = extract_first_goal_from_status status in
 318   let cicgty = get_goalty status goal in
 319   let ctx = ctx_of cicgty in
 320   let _,gty = term_of_cic_term status cicgty ctx in
 321   let cicty = type_of_tactic_term status ctx rhs in
 322   let _,ty = term_of_cic_term status cicty ctx in
 323   let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
 324     match just with
 325       `Auto (univ, params) ->
 326       let params =
 327         if not (List.mem_assoc "timeout" params) then
 328           ("timeout","3")::params
 329         else params
 330       in
 331       let params' =
 332         if not (List.mem_assoc "paramodulation" params) then
 333           ("paramodulation","1")::params
 334         else params
 335       in
 336       if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
 337       else
 338         first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
 339                      ~params:(univ, params') status goal]
 340     | `Term just -> apply_tac just
 341     | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
 342     | `Proof -> id_tac
 343   in
 344   let plhs,prhs,prepare =
 345     match gty with (* Extracting the lhs and rhs of the previous equality *)
 346       NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
 347     | _ -> fail (lazy "You are not building an equaility chain")
 348   in
 349   let continuation =
 350     if last_step then
 351       (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
 352       let todo = [just'] in
 353       let todo = if mustdot status then List.append todo [dot_tac] else todo
 354       in
 355       block_tac todo
 356     else
 357       let (_,_,rhs) = rhs in
 358       block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
 359                                            rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
 360   in
 361   prepare continuation
 362 ;;
 363
 364 let rec pp_metasenv_names (metasenv:NCic.metasenv) =
 365   match metasenv with
 366     [] -> ""
 367   | hd :: tl ->
 368     let n,conj = hd in
 369     let meta_attrs,_,_ = conj in
 370     let rec find_name_aux meta_attrs = match meta_attrs with
 371         [] -> "Anonymous"
 372       | hd :: tl -> match hd with
 373           `Name n -> n
 374         | _ -> find_name_aux tl
 375     in
 376     let name = find_name_aux meta_attrs
 377     in
 378     "[Goal: " ^ (string_of_int n) ^ ", Name: " ^ name ^ "]; " ^ (pp_metasenv_names tl)
 379 ;;
 380
 381 let print_goals_names_tac s (status:#NTacStatus.tac_status) =
 382   let (_,_,metasenv,_,_) = status#obj in
 383   prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
 384
 385 let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
 386   let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
 387   let rec remove_name_from_metaattrs mattrs =
 388     match mattrs with
 389       [] -> []
 390     | hd :: tl ->
 391       match hd with
 392         `Name n -> remove_name_from_metaattrs tl
 393       | _ as it -> it :: (remove_name_from_metaattrs tl)
 394   in
 395   let rec add_names_to_metasenv cl metasenv =
 396     match cl with
 397       [] -> metasenv
 398     | hd :: tl ->
 399       let _,consname,_ = hd
 400       in match metasenv with
 401         [] -> []
 402       | mhd :: mtl ->
 403         let gnum,conj = mhd in
 404         let mattrs,ctx,t = conj in
 405         let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
 406         in
 407         let newconj = mattrs,ctx,t in
 408         let newmeta = gnum,newconj in
 409         newmeta :: (add_names_to_metasenv tl mtl)
 410   in
 411   let newmetasenv = add_names_to_metasenv !cl metasenv in
 412   status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
 413
 414 let we_proceed_by_induction_on t1 t2 status =
 415   let goal = extract_first_goal_from_status status in
 416   let txt,len,t1 = t1 in
 417   let t1 = txt, len, Ast.Appl [t1; Ast.Implicit `Vector] in
 418   let indtyinfo = ref None in
 419   let sort = ref (NCic.Rel 1) in
 420   let cl = ref [] in
 421   try
 422     assert_tac t2 None status goal (block_tac [
 423         analyze_indty_tac ~what:t1 indtyinfo;
 424         sort_of_goal_tac sort;
 425         (fun status ->
 426            let ity = HExtlib.unopt !indtyinfo in
 427            let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
 428            let name =
 429              NUri.name_of_uri uri ^ "_" ^
 430              snd (NCicElim.ast_of_sort
 431                     (match !sort with NCic.Sort x -> x | _ -> assert false))
 432            in
 433            let eliminator =
 434              let l = [Ast.Ident (name,None); Ast.Implicit `JustOne] in
 435              (* Generating as many implicits as open goals *)
 436              let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) ity.consno in
 437              let _,_,t1 = t1 in
 438              let l = l @ [t1] in
 439              Ast.Appl l
 440            in
 441            cl := ity.cl;
 442            exact_tac ("",0,eliminator) status);
 443         add_names_to_goals_tac cl; dot_tac] status)
 444   with
 445   | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
 446 ;;
 447
 448 let we_proceed_by_cases_on ((txt,len,ast1) as t1)  t2 status =
 449   let goal = extract_first_goal_from_status status in
 450   let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in
 451   let indtyinfo = ref None in
 452   let cl = ref [] in
 453   try
 454     assert_tac t2 None status goal (block_tac [
 455         analyze_indty_tac ~what:npt1 indtyinfo;
 456         cases_tac ~what:t1 ~where:("",0,(None,[],Some
 457                                            Ast.UserInput));
 458         print_goals_names_tac "Pre Adding";
 459         (
 460           fun status ->
 461             let ity = HExtlib.unopt !indtyinfo in
 462             cl := ity.cl; add_names_to_goals_tac cl status
 463         );
 464         print_goals_names_tac "Post Adding";
 465         dot_tac] status)
 466   with
 467   | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
 468 ;;
 469
 470 let byinduction t1 id = suppose t1 id None ;;
 471
 472 let name_of_conj conj =
 473   let mattrs,_,_ = conj in
 474   let rec search_name mattrs =
 475     match mattrs with
 476       [] -> "Anonymous"
 477     | hd::tl ->
 478       match hd with
 479         `Name n -> n
 480       | _ -> search_name tl
 481   in
 482   search_name mattrs
 483
 484 let rec loc_of_goal goal l =
 485   match l with
 486     [] -> fail (lazy "Reached the end")
 487   | hd :: tl ->
 488     let _,sw = hd in
 489     let g = goal_of_switch sw in
 490     if g = goal then hd
 491     else loc_of_goal goal tl
 492 ;;
 493
 494 let focus_on_case_tac case status =
 495   let goal = extract_first_goal_from_status status in
 496   let (_,_,metasenv,_,_) = status#obj in
 497   let rec goal_of_case case metasenv =
 498     match metasenv with
 499       [] -> fail (lazy "The given case does not exist")
 500     | (goal,conj) :: tl ->
 501       if name_of_conj conj = case then goal
 502       else goal_of_case case tl
 503   in
 504   let goal_to_focus = goal_of_case case metasenv in
 505   let gstatus =
 506     match status#stack with
 507       [] -> fail (lazy "There is nothing to prove")
 508     | (g,t,k,tag) :: s ->
 509       let loc = loc_of_goal goal_to_focus k in
 510       let curloc = loc_of_goal goal g in
 511       (((g @- [curloc]) @+ [loc]),t,([curloc] @+ (k @- [loc])),tag) :: s
 512   in status#set_stack gstatus
 513
 514 let case id l status =
 515   let goal = extract_first_goal_from_status status in
 516   let (_,_,metasenv,_,_) = status#obj in
 517   let conj = NCicUtils.lookup_meta goal metasenv in
 518   let name = name_of_conj conj in
 519   let continuation =
 520     let rec aux l =
 521       match l with
 522         [] -> [id_tac]
 523       | (id,ty)::tl ->
 524         (try_tac (assume id ("",0,ty) None)) :: (aux tl)
 525     in
 526     aux l
 527   in
 528   if name = id then block_tac continuation status
 529   else block_tac ([focus_on_case_tac id] @ continuation) status
 530 ;;
 531
 532 let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
 533
 534 (* vim: ts=2: sw=0: et:
 535  * *)