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/Equality/eq.ind")) ->
  74          PrimitiveTactics.apply_tac ~status:(proof,goal)
  75           ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/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/Equality_is_a_congruence/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 Tl = 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/Equality/eq.ind")) ->
  94          Tl.thens
  95           ~start:(PrimitiveTactics.apply_tac
  96             ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/trans_eq.con", [])))
  97           ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac]
  98           ~status
  99
 100       | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
 101          Tl.thens
 102           ~start:(PrimitiveTactics.apply_tac
 103             ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/trans_eqT.con", [])))
 104           ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac]
 105           ~status
 106
 107       | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
 108 ;;
 109
 110
 111 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
 112
 113 let assumption_tac ~status:((proof,goal) as status) =
 114   let module C = Cic in
 115   let module R = CicReduction in
 116   let module T = CicTypeChecker in
 117    let _,metasenv,_,_ = proof in
 118     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 119      let rec find n = function
 120         hd::tl ->
 121 (*         (let hdd = hd in
 122           match hdd with
 123              Some (name, termine) -> prerr_endline("####" ^ name ^ CicPp.ppterm termine)
 124            | None -> prerr_endline("#### None")
 125          );
 126 *)         (match hd with
 127              (Some (_, C.Decl t)) when (R.are_convertible context t ty) -> n
 128            | (Some (_, C.Def t)) when (R.are_convertible context (T.type_of_aux' metasenv context t) ty) -> n
 129            | _ -> find (n+1) tl
 130          )
 131       | [] -> raise (ProofEngineTypes.Fail "No such assumption")
 132      in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
 133 ;;
 134
 135 (*
 136 let generalize_tac ~term ~status:((proof,goal) as status) =
 137   let module C = Cic in
 138   let module R = CicReduction in
 139   let module T = CicTypeChecker in
 140   let module P = PrimitiveTactics in
 141   let module Tl = Tacticals in
 142    let _,metasenv,_,_ = proof in
 143     let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
 144      Tl.thens
 145       ~start:(P.cut_tac ~term:(C.Lambda ("dummy_for_gen", (T.type_of_aux' metasenv context term), (R.replace ?????? (C.Name "dummy_for_gen") term )))
 146       ~continuations: [(P.apply_tac (C.Appl [(C.Rel 1); term])); Tl.id_tac]     (* in quest'ordine o viceversa? provare *)
 147       ~status
 148 ;;
 149
 150
 151 let absurd_tac ~term ~status:((proof,goal) as status) =
 152   PrimitiveTactics.cut_tac
 153 ;;
 154 *)
 155