1 (* Copyright (C) 2002, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
27 let constructor_tac ~n ~status:(proof, goal) =
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")
41 let exists_tac ~status =
42 constructor_tac ~n:1 ~status
46 let split_tac ~status =
47 constructor_tac ~n:1 ~status
51 let left_tac ~status =
52 constructor_tac ~n:1 ~status
56 let right_tac ~status =
57 constructor_tac ~n:2 ~status
66 let symmetry_tac ~status:(proof, goal) =
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", []))
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", []))
81 | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
85 let transitivity_tac ~term ~status:((proof, goal) as status) =
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")) ->
95 ~start:(PrimitiveTactics.apply_tac
96 ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", [])))
98 [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term]
101 | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
103 ~start:(PrimitiveTactics.apply_tac
104 ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", [])))
106 [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term]
109 | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
113 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
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
126 Some (name, termine) -> prerr_endline("####" ^ name ^ CicPp.ppterm termine)
127 | None -> prerr_endline("#### None")
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
137 | [] -> raise (ProofEngineTypes.Fail "No such assumption")
138 in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
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
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 *)
157 let absurd_tac ~term ~status:((proof,goal) as status) =
158 PrimitiveTactics.cut_tac