helm/gTopLevel/variousTactics.ml

   1 (* Copyright (C) 2002, 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
  27 let constructor_tac ~n ~status:(proof, goal) =
  28   let module C = Cic in
  29   let module R = CicReduction in
  30    let (_,metasenv,_,_) = proof in
  31     let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  32      match (R.whd context ty) with
  33         (C.MutInd (uri, typeno, exp_named_subst))
  34       | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
  35          PrimitiveTactics.apply_tac ~status:(proof, goal)
  36           ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
  37       | _ -> raise (ProofEngineTypes.Fail "Constructor failed")
  38 ;;
  39
  40
  41 let exists_tac ~status =
  42   constructor_tac ~n:1 ~status
  43 ;;
  44
  45
  46 let split_tac ~status =
  47   constructor_tac ~n:1 ~status
  48 ;;
  49
  50
  51 let left_tac ~status =
  52   constructor_tac ~n:1 ~status
  53 ;;
  54
  55
  56 let right_tac ~status =
  57   constructor_tac ~n:2 ~status
  58 ;;
  59
  60
  61 let reflexivity_tac =
  62   constructor_tac ~n:1
  63 ;;
  64
  65
  66 let symmetry_tac ~status:(proof, goal) =
  67   let module C = Cic in
  68   let module R = CicReduction in
  69   let module U = UriManager in
  70    let (_,metasenv,_,_) = proof in
  71     let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  72      match (R.whd context ty) with
  73         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
  74          PrimitiveTactics.apply_tac ~status:(proof,goal)
  75           ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", []))
  76
  77       | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
  78          PrimitiveTactics.apply_tac ~status:(proof,goal)
  79           ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", []))
  80
  81       | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
  82 ;;
  83
  84
  85 let transitivity_tac ~term ~status:((proof, goal) as status) =
  86   let module C = Cic in
  87   let module R = CicReduction in
  88   let module U = UriManager in
  89   let module T = Tacticals in
  90    let (_,metasenv,_,_) = proof in
  91     let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  92      match (R.whd context ty) with
  93         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
  94          T.thens
  95           ~start:(PrimitiveTactics.apply_tac
  96             ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", [])))
  97           ~continuations:
  98             [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term]
  99           ~status
 100
 101       | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
 102          T.thens
 103           ~start:(PrimitiveTactics.apply_tac
 104             ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", [])))
 105           ~continuations:
 106             [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term]
 107           ~status
 108
 109       | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
 110 ;;
 111
 112
 113 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
 114
 115 let assumption_tac ~status:((proof,goal) as status) =
 116   let module C = Cic in
 117   let module R = CicReduction in
 118   let module S = CicSubstitution in
 119    let _,metasenv,_,_ = proof in
 120     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 121      let rec find n = function
 122         hd::tl ->
 123          (match hd with
 124              (Some (_, C.Decl t)) when
 125                (R.are_convertible context (S.lift n t) ty) -> n
 126            | (Some (_, C.Def t)) when
 127                (R.are_convertible context
 128                 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
 129            | _ -> find (n+1) tl
 130          )
 131       | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
 132      in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
 133 ;;
 134
 135 (* Questa invece era in fourierR.ml
 136 let assumption_tac ~status:(proof,goal)=
 137   let curi,metasenv,pbo,pty = proof in
 138   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 139   let num = ref 0 in
 140   let tac_list = List.map
 141         ( fun x -> num := !num + 1;
 142                 match x with
 143                   Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
 144                   | _ -> ("fake",tcl_fail 1)
 145         )
 146         context
 147   in
 148   Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
 149 ;;
 150 *)
 151
 152
 153 (* ANCORA DA DEBUGGARE *)
 154
 155
 156 let elim_type_tac ~term ~status =
 157   let module C = Cic in
 158   let module P = PrimitiveTactics in
 159   let module T = Tacticals in
 160    T.thens
 161     ~start: (P.cut_tac ~term)
 162     ~continuations:[ P.elim_simpl_intros_tac ~term:(C.Rel 1) ; T.id_tac ]
 163     ~status
 164 ;;
 165
 166 (* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-)
 167 let elim_type_tac ~term ~status =
 168   warn "in Ring.elim_type_tac";
 169   Tacticals.thens ~start:(cut_tac ~term)
 170    ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
 171 *)
 172
 173
 174 let absurd_tac ~term ~status:((proof,goal) as status) =
 175   let module C = Cic in
 176   let module U = UriManager in
 177   let module P = PrimitiveTactics in
 178    let _,metasenv,_,_ = proof in
 179     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 180      if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop))
 181       then P.apply_tac ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status
 182       else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
 183 ;;
 184
 185
 186 let contradiction_tac ~status =
 187   let module C = Cic in
 188   let module U = UriManager in
 189   let module P = PrimitiveTactics in
 190   let module T = Tacticals in
 191    T.then_
 192       ~start: (P.intros_tac ~mknames:(function () -> "FOO"))
 193       ~continuation:(
 194         T.then_
 195            ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ))
 196            ~continuation: assumption_tac)
 197     ~status
 198 ;;
 199
 200 (* Questa era in fourierR.ml
 201 (* !!!!! fix !!!!!!!!!! *)
 202 let contradiction_tac ~status:(proof,goal)=
 203         Tacticals.then_
 204                 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
 205                 ~continuation:(Tacticals.then_
 206                         ~start:(VariousTactics.elim_type_tac ~term:_False)
 207                         ~continuation:(assumption_tac))
 208         ~status:(proof,goal)
 209 ;;
 210 *)
 211
 212
 213 (* IN FASE DI IMPLEMENTAZIONE *)
 214
 215
 216 let generalize_tac ~term ~status:((proof,goal) as status) =
 217   let module C = Cic in
 218   let module P = PrimitiveTactics in
 219   let module T = Tacticals in
 220   let struct_equality t a = (t == a) in
 221    let _,metasenv,_,_ = proof in
 222     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 223      T.thens
 224       ~start:(P.cut_tac
 225        ~term:(
 226          C.Lambda (
 227           (C.Name "dummy_for_gen"),
 228           (CicTypeChecker.type_of_aux' metasenv context term),
 229           (ProofEngineReduction.replace
 230             ~equality:(==)
 231             ~with_what:(C.Rel 1)(* (C.Name "dummy_for_gen") *)
 232             ~what:term
 233             ~where:ty))))        (* dove?? nel goal va bene?*)
 234       ~continuations:
 235        [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac]      (* in quest'ordine o viceversa? provare *)
 236       ~status
 237 ;;
 238
 239 (* PROVE DI DECOMPOSE
 240
 241 (* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *)
 242 let decompose_tac ~what ~where ~status:((proof,goal) as status) =
 243   let module C = Cic in
 244   let module R = CicReduction in
 245   let module P = PrimitiveTactics in
 246   let module T = Tacticals in
 247   let module S = ProofEngineStructuralRules in
 248
 249    let rec decomposing ty what =
 250     match (what) with
 251        [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *)
 252      | hd::tl as what ->
 253         match ty with
 254            (C.Appl (hd::_)) -> hd
 255          | _ -> decomposing ty tl
 256     in
 257
 258    let (_,metasenv,_,_) = proof in
 259     let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
 260      T.repeat_tactic
 261        ~tactic:(T.then_
 262                    ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what))
 263                    ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where))))                (* ma che ipotesi sto cancellando??? *)
 264                )
 265        ~status
 266 ;;
 267
 268
 269 let decompose_tac ~clist ~status:((proof,goal) as status) =
 270   let module C = Cic in
 271   let module R = CicReduction in
 272   let module P = PrimitiveTactics in
 273   let module T = Tacticals in
 274   let module S = ProofEngineStructuralRules in
 275    let (_,metasenv,_,_) = proof in
 276     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 277
 278      let rec repeat_elim ~term ~status =                (* term -> status -> proof * (goal list) *)
 279       try
 280        let (proof, goallist) =
 281         T.then_
 282            ~start:(P.elim_simpl_intros_tac ~term)
 283            ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty))))                (* non so che ipotesi sto cancellando??? *)
 284            ~status
 285         in
 286          let rec step proof goallist =
 287           match goallist with
 288              [] -> (proof, [])
 289            | hd::tl ->
 290               let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in
 291                let (proof'', goallist'') = step proof' tl in
 292                 proof'', goallist'@goallist''
 293           in
 294            step proof goallist
 295        with
 296         (Fail _) -> T.id_tac
 297
 298     in
 299      let rec decomposing ty clist =             (* term -> (term list) -> bool *)
 300       match (clist) with
 301         [] -> false
 302       | hd::tl as clist ->
 303          match ty with
 304            (C.Appl (hd::_)) -> true
 305          | _ -> decomposing ty tl
 306
 307       in
 308        let term = decomposing (R.whd context ty) clist in
 309         if (term == C.Implicit)
 310          then (Fail "Decompose: nothing to decompose or no application")
 311          else repeat_elim ~term ~status
 312 ;;
 313 *)
 314
 315 let decompose_tac ~clist ~status =
 316   let module C = Cic in
 317   let module R = CicReduction in
 318   let module P = PrimitiveTactics in
 319   let module T = Tacticals in
 320   let module S = ProofEngineStructuralRules in
 321
 322    let rec choose ty =
 323     function
 324        [] -> C.Implicit (* a cosa serve? *)
 325      | hd::tl ->
 326         match ty with
 327            (C.Appl (hd::_)) -> hd
 328          | _ -> choose ty tl
 329      in
 330
 331     let decompose_one_tac ~clist ~status:((proof,goal) as status) =
 332      let (_,metasenv,_,_) = proof in
 333       let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 334        let term = choose (R.whd context ty) clist in
 335         if (term == C.Implicit)
 336          then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
 337          else T.then_
 338                  ~start:(P.elim_simpl_intros_tac ~term)
 339                  ~continuation:(S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty))))                (* ma che ipotesi sto cancellando??? *)
 340                  ~status
 341      in
 342       T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status
 343 ;;
 344
 345
 346 let decide_equality_tac =
 347   Tacticals.id_tac
 348 ;;
 349
 350 (*
 351 let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
 352   let module C = Cic in
 353   let module U = UriManager in
 354   let module P = PrimitiveTactics in
 355   let module T = Tacticals in
 356    let _,metasenv,_,_ = proof in
 357     let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 358      if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
 359        (* controllo che i due termini siano comparabili *)
 360       then
 361        T.thens
 362          ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
 363          ~continuations:[split_tac ; intros_tac ~name:"FOO"]
 364       else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
 365 ;;
 366 *)
 367
 368
 369 let rewrite_tac ~term:equality ~status:(proof,goal) =
 370  let module C = Cic in
 371  let module U = UriManager in
 372   let curi,metasenv,pbo,pty = proof in
 373   let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 374    let eq_ind_r,ty,t1,t2 =
 375     match CicTypeChecker.type_of_aux' metasenv context equality with
 376        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
 377         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
 378          let eq_ind_r =
 379           C.Const
 380            (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
 381          in
 382           eq_ind_r,ty,t1,t2
 383      | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
 384         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
 385          let eqT_ind_r =
 386           C.Const
 387            (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
 388          in
 389           eqT_ind_r,ty,t1,t2
 390      | _ ->
 391        raise
 392         (ProofEngineTypes.Fail
 393           "Rewrite: the argument is not a proof of an equality")
 394    in
 395     let pred =
 396      let gty' = CicSubstitution.lift 1 gty in
 397      let t1' = CicSubstitution.lift 1 t1 in
 398      let gty'' =
 399       ProofEngineReduction.replace_lifting
 400        ~equality:ProofEngineReduction.alpha_equivalence
 401        ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
 402      in
 403       C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
 404     in
 405 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
 406     let fresh_meta = ProofEngineHelpers.new_meta proof in
 407     let irl =
 408      ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 409     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
 410
 411      let (proof',goals) =
 412       PrimitiveTactics.exact_tac
 413        ~term:(C.Appl
 414          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
 415         ~status:((curi,metasenv',pbo,pty),goal)
 416      in
 417       assert (List.length goals = 0) ;
 418       (proof',[fresh_meta])
 419 ;;
 420
 421
 422 let rewrite_simpl_tac ~term ~status =
 423  Tacticals.then_ ~start:(rewrite_tac ~term)
 424   ~continuation:
 425    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
 426   ~status
 427 ;;
 428
 429
 430 let rewrite_back_tac ~term:equality ~status:(proof,goal) =
 431  let module C = Cic in
 432  let module U = UriManager in
 433   let curi,metasenv,pbo,pty = proof in
 434   let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 435    let eq_ind_r,ty,t1,t2 =
 436     match CicTypeChecker.type_of_aux' metasenv context equality with
 437        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
 438         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
 439          let eq_ind_r =
 440           C.Const
 441            (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[])
 442          in
 443           eq_ind_r,ty,t1,t2
 444      | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
 445         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
 446          let eqT_ind_r =
 447           C.Const
 448            (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con",[])
 449          in
 450           eqT_ind_r,ty,t1,t2
 451      | _ ->
 452        raise
 453         (ProofEngineTypes.Fail
 454           "Rewrite: the argument is not a proof of an equality")
 455    in
 456     let pred =
 457      let gty' = CicSubstitution.lift 1 gty in
 458      let t1' = CicSubstitution.lift 1 t1 in
 459      let gty'' =
 460       ProofEngineReduction.replace_lifting
 461        ~equality:ProofEngineReduction.alpha_equivalence
 462        ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
 463      in
 464       C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
 465     in
 466 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
 467     let fresh_meta = ProofEngineHelpers.new_meta proof in
 468     let irl =
 469      ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 470     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
 471
 472      let (proof',goals) =
 473       PrimitiveTactics.exact_tac
 474        ~term:(C.Appl
 475          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
 476         ~status:((curi,metasenv',pbo,pty),goal)
 477      in
 478       assert (List.length goals = 0) ;
 479       (proof',[fresh_meta])
 480
 481 ;;
 482
 483
 484 let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
 485   let module C = Cic in
 486   let module U = UriManager in
 487   let module P = PrimitiveTactics in
 488   let module T = Tacticals in
 489    let _,metasenv,_,_ = proof in
 490     let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
 491      let wty = CicTypeChecker.type_of_aux' metasenv context what in
 492       if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
 493        then T.thens
 494               ~start:(P.cut_tac ~term:(C.Appl [(C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; wty ; what ; with_what]))
 495                                                         (* quale uguaglianza usare, eq o eqT ? *)
 496               ~continuations:[
 497                 T.then_
 498                    ~start:
 499                      (P.intros_tac ~mknames:(function () ->"dummy_for_replace"))
 500                    ~continuation:(T.then_
 501                                      ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
 502                                      ~continuation:(ProofEngineStructuralRules.clear
 503                                                      ~hyp:(Some((C.Name "dummy_for_replace") , (C.Def C.Implicit) (* NO!! tipo di dummy *) ))
 504                                                    )
 505                                  ) ;
 506                 T.id_tac]
 507              ~status
 508       else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
 509 ;;
 510