]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/equalityTactics.ml
s/List.find.../CicUtil.lookup_meta/
[helm.git] / helm / ocaml / tactics / equalityTactics.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 rewrite_tac ~term:equality ~status:(proof,goal) =
28  let module C = Cic in
29  let module U = UriManager in
30   let curi,metasenv,pbo,pty = proof in
31   let metano,context,gty = CicUtil.lookup_meta goal metasenv in
32    let eq_ind_r,ty,t1,t2 =
33     match CicTypeChecker.type_of_aux' metasenv context equality with
34        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
35         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
36          let eq_ind_r =
37           C.Const
38            (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
39          in
40           eq_ind_r,ty,t1,t2
41      | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
42         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
43          let eqT_ind_r =
44           C.Const
45            (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
46          in
47           eqT_ind_r,ty,t1,t2
48      | _ ->
49        raise
50         (ProofEngineTypes.Fail
51           "Rewrite: the argument is not a proof of an equality")
52    in
53     let pred =
54      let gty' = CicSubstitution.lift 1 gty in
55      let t1' = CicSubstitution.lift 1 t1 in
56      let gty'' =
57       ProofEngineReduction.replace_lifting
58        ~equality:ProofEngineReduction.alpha_equivalence
59        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
60      in
61       C.Lambda
62        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
63     in
64     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
65     let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
66     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
67
68      let (proof',goals) =
69       PrimitiveTactics.exact_tac
70        ~term:(C.Appl
71          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
72         ~status:((curi,metasenv',pbo,pty),goal)
73      in
74       assert (List.length goals = 0) ;
75       (proof',[fresh_meta])
76 ;;
77
78
79 let rewrite_simpl_tac ~term ~status =
80  Tacticals.then_ 
81   ~start:(rewrite_tac ~term)
82   ~continuation:
83    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
84   ~status
85 ;;
86
87
88 let rewrite_back_tac ~term:equality ~status:(proof,goal) =
89  let module C = Cic in
90  let module U = UriManager in
91   let curi,metasenv,pbo,pty = proof in
92   let metano,context,gty = CicUtil.lookup_meta goal metasenv in
93    let eq_ind_r,ty,t1,t2 =
94     match CicTypeChecker.type_of_aux' metasenv context equality with
95        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
96         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
97          let eq_ind_r =
98           C.Const
99            (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[])
100          in
101           eq_ind_r,ty,t2,t1
102      | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
103         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
104          let eqT_ind_r =
105           C.Const
106            (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con",[])
107          in
108           eqT_ind_r,ty,t2,t1
109      | _ ->
110        raise
111         (ProofEngineTypes.Fail
112           "Rewrite: the argument is not a proof of an equality")
113    in
114     let pred =
115      let gty' = CicSubstitution.lift 1 gty in
116      let t1' = CicSubstitution.lift 1 t1 in
117      let gty'' =
118       ProofEngineReduction.replace_lifting
119        ~equality:ProofEngineReduction.alpha_equivalence
120        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
121      in
122       C.Lambda
123        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
124     in
125     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
126     let irl =
127      CicMkImplicit.identity_relocation_list_for_metavariable context in
128     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
129
130      let (proof',goals) =
131       PrimitiveTactics.exact_tac
132        ~term:(C.Appl
133          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
134         ~status:((curi,metasenv',pbo,pty),goal)
135      in
136       assert (List.length goals = 0) ;
137       (proof',[fresh_meta])
138
139 ;;
140
141
142 let rewrite_back_simpl_tac ~term ~status =
143  Tacticals.then_ 
144   ~start:(rewrite_back_tac ~term)
145   ~continuation:
146    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
147   ~status
148 ;;
149
150
151 let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
152   let module C = Cic in
153   let module U = UriManager in
154   let module P = PrimitiveTactics in
155   let module T = Tacticals in
156    let _,metasenv,_,_ = proof in
157     let _,context,_ = CicUtil.lookup_meta goal metasenv in
158      let wty = CicTypeChecker.type_of_aux' metasenv context what in
159       try
160       if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
161        then
162         let equality =
163          match CicTypeChecker.type_of_aux' metasenv context wty with
164             C.Sort C.Set -> "cic:/Coq/Init/Logic/eq.ind"
165           | C.Sort C.Type
166           | C.Sort C.CProp
167           | C.Sort C.Prop -> "cic:/Coq/Init/Logic_Type/eqT.ind"
168           | _ -> assert false
169         in
170          T.thens
171           ~start:(
172             P.cut_tac 
173              (C.Appl [
174                (C.MutInd ((U.uri_of_string equality), 0, [])) ;
175                  wty ; 
176                  what ; 
177                  with_what]))
178           ~continuations:[
179             T.then_
180                ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
181                ~continuation:(
182                  ProofEngineStructuralRules.clear
183                   ~hyp:(List.hd context)) ;
184             T.id_tac]
185           ~status
186        else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
187        with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context")
188 ;;
189
190
191 (* All these tacs do is applying the right constructor/theorem *)
192
193 let reflexivity_tac =
194   IntroductionTactics.constructor_tac ~n:1
195 ;;
196
197
198 let symmetry_tac ~status:(proof, goal) =
199   let module C = Cic in
200   let module R = CicReduction in
201   let module U = UriManager in
202    let (_,metasenv,_,_) = proof in
203     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
204      match (R.whd context ty) with
205         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
206          PrimitiveTactics.apply_tac ~status:(proof,goal)
207           ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", []))
208
209       | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
210          PrimitiveTactics.apply_tac ~status:(proof,goal)
211           ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", []))
212
213       | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
214 ;;
215
216
217 let transitivity_tac ~term ~status:((proof, goal) as status) =
218   let module C = Cic in
219   let module R = CicReduction in
220   let module U = UriManager in
221   let module T = Tacticals in
222    let (_,metasenv,_,_) = proof in
223     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
224      match (R.whd context ty) with
225         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
226          T.thens
227           ~start:(PrimitiveTactics.apply_tac
228             ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", [])))
229           ~continuations:
230             [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]
231           ~status
232
233       | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
234          T.thens
235           ~start:(PrimitiveTactics.apply_tac
236             ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", [])))
237           ~continuations:
238             [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term]
239           ~status
240
241       | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
242 ;;
243
244