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 same_type_as_conclusion 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 same_type_as_conclusion 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 same_type_as_conclusion 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   distribute_tac (fun status goal ->
 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 (exec (bydone wrappedjust) status goal)
 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' (Some ty) status goal (exec (block_tac [change_tac
 300                                                                 ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; bydone
 301                                                                 wrappedjust]) status goal)
 302            with
 303            | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion")
 304            | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
 305          )
 306       )
 307     | Some id ->
 308       (
 309         match ty' with
 310         | None -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac
 311                                id; merge_tac ]) status goal
 312         | Some ty' -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac
 313                                    id; change_tac ~where:("",0,(None,[id,Ast.UserInput],None))
 314                                    ~with_what:ty'; merge_tac]) status goal
 315       )
 316   )
 317 ;;
 318
 319 let thesisbecomes t1 t2 status = we_need_to_prove t1 None t2 status
 320 ;;
 321
 322 let existselim just id1 t1 t2 id2 (*status*) =
 323   distribute_tac (fun status goal ->
 324     let (_,_,t1) = t1 in
 325     let (_,_,t2) = t2 in
 326     let just = mk_just status goal just in
 327     exec (block_tac [
 328       cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
 329                                                                                  (id1,None), Some t1),t2)]));
 330       branch_tac ~force:false;
 331       just;
 332       shift_tac;
 333       case1_tac "_";
 334       intros_tac ~names_ref:(ref []) [id1;id2];
 335       merge_tac
 336     ]) status goal
 337   )
 338 ;;
 339
 340 let andelim just t1 id1 t2 id2 (*status*) =
 341 (*   let goal = extract_first_goal_from_status status in *)
 342   distribute_tac (fun status goal ->
 343     let (_,_,t1) = t1 in
 344     let (_,_,t2) = t2 in
 345     let just = mk_just status goal just in
 346     exec (block_tac [
 347       cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
 348       branch_tac ~force:false;
 349       just;
 350       shift_tac;
 351       case1_tac "_";
 352       intros_tac ~names_ref:(ref []) [id1;id2];
 353       merge_tac
 354     ]) status goal
 355   )
 356 ;;
 357
 358 let type_of_tactic_term status ctx t =
 359   let status,cicterm = disambiguate status ctx t `XTNone in
 360   let (_,cicty) = typeof status ctx cicterm in
 361   cicty
 362
 363 let rewritingstep lhs rhs just last_step status =
 364   let goal = extract_first_goal_from_status status in
 365   let cicgty = get_goalty status goal in
 366   let ctx = ctx_of cicgty in
 367   let _,gty = term_of_cic_term status cicgty ctx in
 368   let cicty = type_of_tactic_term status ctx rhs in
 369   let _,ty = term_of_cic_term status cicty ctx in
 370   let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
 371     match just with
 372       `Auto (univ, params) ->
 373       let params =
 374         if not (List.mem_assoc "timeout" params) then
 375           ("timeout","3")::params
 376         else params
 377       in
 378       let params' =
 379         if not (List.mem_assoc "paramodulation" params) then
 380           ("paramodulation","1")::params
 381         else params
 382       in
 383       if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
 384       else
 385         first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
 386                      ~params:(univ, params') status goal]
 387     | `Term just -> apply_tac just
 388     | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
 389     | `Proof -> id_tac
 390   in
 391   let plhs,prhs,prepare =
 392     match lhs with
 393       None -> (* = E2 *)
 394       let plhs,prhs =
 395         match gty with (* Extracting the lhs and rhs of the previous equality *)
 396           NCic.Appl [_;_;plhs;prhs] -> plhs,prhs
 397         | _ -> fail (lazy "You are not building an equaility chain")
 398       in
 399       plhs,prhs,
 400       (fun continuation -> continuation status)
 401     | Some (None,lhs) -> (* conclude *)
 402       let plhs,prhs =
 403         match gty with
 404           NCic.Appl [_;_;plhs;prhs] -> plhs,prhs
 405         | _ -> fail (lazy "You are not building an equaility chain")
 406       in
 407       (*TODO*)
 408       (*CSC: manca check plhs convertibile con lhs *)
 409       plhs,prhs,
 410       (fun continuation -> continuation status)
 411     | Some (Some name,lhs) -> (* obtain *)
 412       fail (lazy "Not implemented")
 413         (*
 414       let plhs = lhs in
 415       let prhs = Cic.Meta(newmeta,irl) in
 416       plhs,prhs,
 417       (fun continuation ->
 418          let metasenv = (newmeta, ctx, ty)::metasenv in
 419          let mk_fresh_name_callback =
 420            fun metasenv ctx _ ~typ ->
 421              FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv ctx
 422                (Cic.Name name) ~typ
 423          in
 424          let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
 425          let proof,goals =
 426            ProofEngineTypes.apply_tactic
 427              (Tacticals.thens
 428                 ~start:(Tactics.cut ~mk_fresh_name_callback
 429                           (Cic.Appl [eq ; ty ; lhs ; prhs]))
 430                 ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
 431          in
 432          let goals =
 433            match just,goals with
 434              `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1]
 435            | _, [g1;g2] -> [g2;newmeta;g1]
 436            | _, l ->
 437              prerr_endline (String.concat "," (List.map string_of_int l));
 438              prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
 439              assert false
 440          in
 441          proof,goals)
 442            *)
 443   in
 444   let continuation =
 445     if last_step then
 446       (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
 447       let todo = [just'] in
 448       let todo = if mustdot status then List.append todo [dot_tac] else todo
 449       in
 450         block_tac todo
 451     else
 452       let (_,_,rhs) = rhs in
 453       block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
 454                                            rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
 455   in
 456     prepare continuation
 457 ;;
 458
 459 let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
 460
 461 (* vim: ts=2: sw=0: et:
 462  * *)