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_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
 163     ~status
 164 ;;
 165
 166 let absurd_tac ~term ~status:((proof,goal) as status) =
 167   let module C = Cic in
 168   let module U = UriManager in
 169   let module P = PrimitiveTactics in
 170    let _,metasenv,_,_ = proof in
 171     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 172      if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop))
 173       then P.apply_tac ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status
 174       else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
 175 ;;
 176
 177
 178 let contradiction_tac ~status =
 179   let module C = Cic in
 180   let module U = UriManager in
 181   let module P = PrimitiveTactics in
 182   let module T = Tacticals in
 183    T.then_
 184       ~start:P.intros_tac
 185       ~continuation:(
 186         T.then_
 187            ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ))
 188            ~continuation: assumption_tac)
 189     ~status
 190 ;;
 191
 192 (* Questa era in fourierR.ml
 193 (* !!!!! fix !!!!!!!!!! *)
 194 let contradiction_tac ~status:(proof,goal)=
 195         Tacticals.then_
 196                 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
 197                 ~continuation:(Tacticals.then_
 198                         ~start:(VariousTactics.elim_type_tac ~term:_False)
 199                         ~continuation:(assumption_tac))
 200         ~status:(proof,goal)
 201 ;;
 202 *)
 203
 204
 205 (* IN FASE DI IMPLEMENTAZIONE *)
 206
 207
 208 let generalize_tac ~term ~status:((proof,goal) as status) =
 209   let module C = Cic in
 210   let module P = PrimitiveTactics in
 211   let module T = Tacticals in
 212   let struct_equality t a = (t == a) in
 213    let _,metasenv,_,_ = proof in
 214     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 215      T.thens
 216       ~start:(P.cut_tac
 217        ~term:(
 218          C.Lambda (
 219           (C.Name "dummy_for_gen"),
 220           (CicTypeChecker.type_of_aux' metasenv context term),
 221           (ProofEngineReduction.replace
 222             ~equality:(==)
 223             ~with_what:(C.Rel 1)(* (C.Name "dummy_for_gen") *)
 224             ~what:term
 225             ~where:ty))))        (* dove?? nel goal va bene?*)
 226       ~continuations:
 227        [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac]      (* in quest'ordine o viceversa? provare *)
 228       ~status
 229 ;;
 230
 231 (* PROVE DI DECOMPOSE
 232
 233 (* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *)
 234 let decompose_tac ~what ~where ~status:((proof,goal) as status) =
 235   let module C = Cic in
 236   let module R = CicReduction in
 237   let module P = PrimitiveTactics in
 238   let module T = Tacticals in
 239   let module S = ProofEngineStructuralRules in
 240
 241    let rec decomposing ty what =
 242     match (what) with
 243        [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *)
 244      | hd::tl as what ->
 245         match ty with
 246            (C.Appl (hd::_)) -> hd
 247          | _ -> decomposing ty tl
 248     in
 249
 250    let (_,metasenv,_,_) = proof in
 251     let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
 252      T.repeat_tactic
 253        ~tactic:(T.then_
 254                    ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what))
 255                    ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where))))                (* ma che ipotesi sto cancellando??? *)
 256                )
 257        ~status
 258 ;;
 259
 260
 261 let decompose_tac ~clist ~status:((proof,goal) as status) =
 262   let module C = Cic in
 263   let module R = CicReduction in
 264   let module P = PrimitiveTactics in
 265   let module T = Tacticals in
 266   let module S = ProofEngineStructuralRules in
 267    let (_,metasenv,_,_) = proof in
 268     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 269
 270      let rec repeat_elim ~term ~status =                (* term -> status -> proof * (goal list) *)
 271       try
 272        let (proof, goallist) =
 273         T.then_
 274            ~start:(P.elim_simpl_intros_tac ~term)
 275            ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty))))                (* non so che ipotesi sto cancellando??? *)
 276            ~status
 277         in
 278          let rec step proof goallist =
 279           match goallist with
 280              [] -> (proof, [])
 281            | hd::tl ->
 282               let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in
 283                let (proof'', goallist'') = step proof' tl in
 284                 proof'', goallist'@goallist''
 285           in
 286            step proof goallist
 287        with
 288         (Fail _) -> T.id_tac
 289
 290     in
 291      let rec decomposing ty clist =             (* term -> (term list) -> bool *)
 292       match (clist) with
 293         [] -> false
 294       | hd::tl as clist ->
 295          match ty with
 296            (C.Appl (hd::_)) -> true
 297          | _ -> decomposing ty tl
 298
 299       in
 300        let term = decomposing (R.whd context ty) clist in
 301         if (term == C.Implicit)
 302          then (Fail "Decompose: nothing to decompose or no application")
 303          else repeat_elim ~term ~status
 304 ;;
 305 *)
 306
 307 let decompose_tac ~clist ~status =
 308   let module C = Cic in
 309   let module R = CicReduction in
 310   let module P = PrimitiveTactics in
 311   let module T = Tacticals in
 312   let module S = ProofEngineStructuralRules in
 313
 314    let rec choose ty =
 315     function
 316        [] -> C.Implicit (* a cosa serve? *)
 317      | hd::tl ->
 318         match ty with
 319            (C.Appl (hd::_)) -> hd
 320          | _ -> choose ty tl
 321      in
 322
 323     let decompose_one_tac ~clist ~status:((proof,goal) as status) =
 324      let (_,metasenv,_,_) = proof in
 325       let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 326        let term = choose (R.whd context ty) clist in
 327         if (term == C.Implicit)
 328          then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
 329          else T.then_
 330                  ~start:(P.elim_intros_simpl_tac ~term)
 331                  ~continuation:(S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty))))                (* ma che ipotesi sto cancellando??? *)
 332                  ~status
 333      in
 334       T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status
 335 ;;
 336
 337
 338 let decide_equality_tac =
 339   Tacticals.id_tac
 340 ;;
 341
 342 (*
 343 let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
 344   let module C = Cic in
 345   let module U = UriManager in
 346   let module P = PrimitiveTactics in
 347   let module T = Tacticals in
 348    let _,metasenv,_,_ = proof in
 349     let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 350      if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
 351        (* controllo che i due termini siano comparabili *)
 352       then
 353        T.thens
 354          ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
 355          ~continuations:[split_tac ; intros_tac ~name:"FOO"]
 356       else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
 357 ;;
 358 *)
 359
 360
 361 let rewrite_tac ~term:equality ~status:(proof,goal) =
 362  let module C = Cic in
 363  let module U = UriManager in
 364   let curi,metasenv,pbo,pty = proof in
 365   let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 366    let eq_ind_r,ty,t1,t2 =
 367     match CicTypeChecker.type_of_aux' metasenv context equality with
 368        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
 369         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
 370          let eq_ind_r =
 371           C.Const
 372            (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
 373          in
 374           eq_ind_r,ty,t1,t2
 375      | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
 376         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
 377          let eqT_ind_r =
 378           C.Const
 379            (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
 380          in
 381           eqT_ind_r,ty,t1,t2
 382      | _ ->
 383        raise
 384         (ProofEngineTypes.Fail
 385           "Rewrite: the argument is not a proof of an equality")
 386    in
 387     let pred =
 388      let gty' = CicSubstitution.lift 1 gty in
 389      let t1' = CicSubstitution.lift 1 t1 in
 390      let gty'' =
 391       ProofEngineReduction.replace_lifting
 392        ~equality:ProofEngineReduction.alpha_equivalence
 393        ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
 394      in
 395       C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
 396     in
 397 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
 398     let fresh_meta = ProofEngineHelpers.new_meta proof in
 399     let irl =
 400      ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 401     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
 402
 403      let (proof',goals) =
 404       PrimitiveTactics.exact_tac
 405        ~term:(C.Appl
 406          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
 407         ~status:((curi,metasenv',pbo,pty),goal)
 408      in
 409       assert (List.length goals = 0) ;
 410       (proof',[fresh_meta])
 411 ;;
 412
 413
 414 let rewrite_simpl_tac ~term ~status =
 415  Tacticals.then_ ~start:(rewrite_tac ~term)
 416   ~continuation:
 417    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
 418   ~status
 419 ;;
 420
 421
 422 let rewrite_back_tac ~term:equality ~status:(proof,goal) =
 423  let module C = Cic in
 424  let module U = UriManager in
 425   let curi,metasenv,pbo,pty = proof in
 426   let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 427    let eq_ind_r,ty,t1,t2 =
 428     match CicTypeChecker.type_of_aux' metasenv context equality with
 429        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
 430         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
 431          let eq_ind_r =
 432           C.Const
 433            (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[])
 434          in
 435           eq_ind_r,ty,t1,t2
 436      | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
 437         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
 438          let eqT_ind_r =
 439           C.Const
 440            (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con",[])
 441          in
 442           eqT_ind_r,ty,t1,t2
 443      | _ ->
 444        raise
 445         (ProofEngineTypes.Fail
 446           "Rewrite: the argument is not a proof of an equality")
 447    in
 448     let pred =
 449      let gty' = CicSubstitution.lift 1 gty in
 450      let t1' = CicSubstitution.lift 1 t1 in
 451      let gty'' =
 452       ProofEngineReduction.replace_lifting
 453        ~equality:ProofEngineReduction.alpha_equivalence
 454        ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
 455      in
 456       C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
 457     in
 458 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
 459     let fresh_meta = ProofEngineHelpers.new_meta proof in
 460     let irl =
 461      ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 462     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
 463
 464      let (proof',goals) =
 465       PrimitiveTactics.exact_tac
 466        ~term:(C.Appl
 467          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
 468         ~status:((curi,metasenv',pbo,pty),goal)
 469      in
 470       assert (List.length goals = 0) ;
 471       (proof',[fresh_meta])
 472
 473 ;;
 474
 475
 476 let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
 477   let module C = Cic in
 478   let module U = UriManager in
 479   let module P = PrimitiveTactics in
 480   let module T = Tacticals in
 481    let _,metasenv,_,_ = proof in
 482     let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
 483      let wty = CicTypeChecker.type_of_aux' metasenv context what in
 484       if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
 485        then T.thens
 486               ~start:(P.cut_tac ~term:(C.Appl [(C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; wty ; what ; with_what]))
 487                                                         (* quale uguaglianza usare, eq o eqT ? *)
 488               ~continuations:[
 489                 T.then_
 490                    ~start:P.intros_tac
 491                    ~continuation:(T.then_
 492                                      ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
 493                                      ~continuation:(ProofEngineStructuralRules.clear
 494                                                      ~hyp:(Some((C.Name "dummy_for_replace") , (C.Def C.Implicit) (* NO!! tipo di dummy *) ))
 495                                                    )
 496                                  ) ;
 497                 T.id_tac]
 498              ~status
 499       else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
 500 ;;
 501