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 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/eq.ind")) ->
  94          Tl.thens
  95           ~start:(PrimitiveTactics.apply_tac
  96             ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", [])))
  97           ~continuations:
  98             [Tl.id_tac ; Tl.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          Tl.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             [Tl.id_tac ; Tl.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 T = CicTypeChecker in
 119   let module S = CicSubstitution in
 120    let _,metasenv,_,_ = proof in
 121     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 122      let rec find n = function
 123         hd::tl ->
 124 (*         (let hdd = hd in
 125           match hdd with
 126              Some (name, termine) -> prerr_endline("####" ^ name ^ CicPp.ppterm termine)
 127            | None -> prerr_endline("#### None")
 128          );
 129 *)         (match hd with
 130              (Some (_, C.Decl t)) when
 131                (R.are_convertible context (S.lift n t) ty) -> n
 132            | (Some (_, C.Def t)) when
 133                (R.are_convertible context
 134                 (T.type_of_aux' metasenv context (S.lift n t)) ty) -> n
 135            | _ -> find (n+1) tl
 136          )
 137       | [] -> raise (ProofEngineTypes.Fail "No such assumption")
 138      in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
 139 ;;
 140
 141 (*
 142 let generalize_tac ~term ~status:((proof,goal) as status) =
 143   let module C = Cic in
 144   let module R = CicReduction in
 145   let module T = CicTypeChecker in
 146   let module P = PrimitiveTactics in
 147   let module Tl = Tacticals in
 148    let _,metasenv,_,_ = proof in
 149     let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
 150      Tl.thens
 151       ~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 )))
 152       ~continuations: [(P.apply_tac (C.Appl [(C.Rel 1); term])); Tl.id_tac]     (* in quest'ordine o viceversa? provare *)
 153       ~status
 154 ;;
 155
 156
 157 let absurd_tac ~term ~status:((proof,goal) as status) =
 158   PrimitiveTactics.cut_tac
 159 ;;
 160 *)
 161