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