From: Michele Galatà Date: Fri, 13 Dec 2002 09:27:05 +0000 (+0000) Subject: Rearranged tactics in VariousTactics into new modules EliminationTactics, X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c47727977f13d6e4946fb78bad8d25e8a22a10c;p=helm.git Rearranged tactics in VariousTactics into new modules EliminationTactics, EqualityTactics, IntroductionTactics and NegationTactics. --- diff --git a/helm/gTopLevel/eliminationTactics.cmi b/helm/gTopLevel/eliminationTactics.cmi new file mode 100644 index 000000000..6283bd6b3 Binary files /dev/null and b/helm/gTopLevel/eliminationTactics.cmi differ diff --git a/helm/gTopLevel/eliminationTactics.cmx b/helm/gTopLevel/eliminationTactics.cmx new file mode 100644 index 000000000..4cf93fd85 Binary files /dev/null and b/helm/gTopLevel/eliminationTactics.cmx differ diff --git a/helm/gTopLevel/eliminationTactics.ml b/helm/gTopLevel/eliminationTactics.ml new file mode 100644 index 000000000..d2ed74810 --- /dev/null +++ b/helm/gTopLevel/eliminationTactics.ml @@ -0,0 +1,190 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* +let induction_tac ~term ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + let module U = UriManager in + let (_,metasenv,_,_) = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let termty = T.type_of_aux' metasenv context term in + let uri,exp_named_subst,typeno,args = + match termty with + C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) + | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> (uri,exp_named_subst,typeno,args) + | _ -> raise (ProofEngineTypes.Fail "Induction: Not an Inductive Type to Eliminate") + in + let eliminator_uri = + let base = U.buri_of_uri uri in + let name = + match CicEnvironment.get_obj uri with + C.InductiveDefinition (tys,_,_) -> + let (name,_,_,_) = List.nth tys typeno in + name + | _ -> assert false + in + let ext = + match T.type_of_aux' metasenv context ty with + C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort C.Type -> "_rect" + | _ -> assert false + in + U.uri_of_string (base ^ "/" ^ name ^ ext ^ ".con") + in + apply_tac ~term:(C.Const (eliminator_uri , exp_named_subst)) (* come mi devo comportare con gli args??? *) +;; +*) + +let elim_type_tac ~term ~status = + let module C = Cic in + let module P = PrimitiveTactics in + let module T = Tacticals in + T.thens + ~start: (P.cut_tac ~term) + ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ] + ~status +;; + +(* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-) +let elim_type_tac ~term ~status = + warn "in Ring.elim_type_tac"; + Tacticals.thens ~start:(cut_tac ~term) + ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status +*) + + +(* PROVE DI DECOMPOSE + +(* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *) +let decompose_tac ~what ~where ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + + let rec decomposing ty what = + match (what) with + [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *) + | hd::tl as what -> + match ty with + (C.Appl (hd::_)) -> hd + | _ -> decomposing ty tl + in + + let (_,metasenv,_,_) = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + T.repeat_tactic + ~tactic:(T.then_ + ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what)) + ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where)))) (* ma che ipotesi sto cancellando??? *) + ) + ~status +;; + + +let decompose_tac ~clist ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + let (_,metasenv,_,_) = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + + let rec repeat_elim ~term ~status = (* term -> status -> proof * (goal list) *) + try + let (proof, goallist) = + T.then_ + ~start:(P.elim_simpl_intros_tac ~term) + ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty)))) (* non so che ipotesi sto cancellando??? *) + ~status + in + let rec step proof goallist = + match goallist with + [] -> (proof, []) + | hd::tl -> + let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in + let (proof'', goallist'') = step proof' tl in + proof'', goallist'@goallist'' + in + step proof goallist + with + (Fail _) -> T.id_tac + + in + let rec decomposing ty clist = (* term -> (term list) -> bool *) + match (clist) with + [] -> false + | hd::tl as clist -> + match ty with + (C.Appl (hd::_)) -> true + | _ -> decomposing ty tl + + in + let term = decomposing (R.whd context ty) clist in + if (term == C.Implicit) + then (Fail "Decompose: nothing to decompose or no application") + else repeat_elim ~term ~status +;; +*) + +let decompose_tac ~clist ~status = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + + let rec choose ty = + function + [] -> C.Implicit (* a cosa serve? *) + | hd::tl -> + match ty with + (C.Appl (hd::_)) -> hd + | _ -> choose ty tl + in + + let decompose_one_tac ~clist ~status:((proof,goal) as status) = + let (_,metasenv,_,_) = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let term = choose (R.whd context ty) clist in + if (term == C.Implicit) + then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application") + else T.then_ + ~start:(P.elim_intros_simpl_tac ~term) + ~continuation:(S.clear ~hyp:(List.hd context)) +(* (S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty)))) (* ma che ipotesi sto cancellando??? *)*) + ~status + in + T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status +;; + + diff --git a/helm/gTopLevel/eliminationTactics.mli b/helm/gTopLevel/eliminationTactics.mli new file mode 100644 index 000000000..00ccedd64 --- /dev/null +++ b/helm/gTopLevel/eliminationTactics.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic + +val decompose_tac: clist:(Cic.term list) -> ProofEngineTypes.tactic diff --git a/helm/gTopLevel/eliminationTactics.o b/helm/gTopLevel/eliminationTactics.o new file mode 100644 index 000000000..ad369ef75 Binary files /dev/null and b/helm/gTopLevel/eliminationTactics.o differ diff --git a/helm/gTopLevel/equalityTactics.cmi b/helm/gTopLevel/equalityTactics.cmi new file mode 100644 index 000000000..645ab0f51 Binary files /dev/null and b/helm/gTopLevel/equalityTactics.cmi differ diff --git a/helm/gTopLevel/equalityTactics.cmx b/helm/gTopLevel/equalityTactics.cmx new file mode 100644 index 000000000..e2d282757 Binary files /dev/null and b/helm/gTopLevel/equalityTactics.cmx differ diff --git a/helm/gTopLevel/equalityTactics.ml b/helm/gTopLevel/equalityTactics.ml new file mode 100644 index 000000000..afa210119 --- /dev/null +++ b/helm/gTopLevel/equalityTactics.ml @@ -0,0 +1,236 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +let rewrite_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[]) + in + eq_ind_r,ty,t1,t2 + | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[]) + in + eqT_ind_r,ty,t1,t2 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.alpha_equivalence + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ~status:((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) +;; + + +let rewrite_simpl_tac ~term ~status = + Tacticals.then_ + ~start:(rewrite_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~status +;; + + +let rewrite_back_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[]) + in + eq_ind_r,ty,t2,t1 + | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con",[]) + in + eqT_ind_r,ty,t2,t1 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.alpha_equivalence + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ~status:((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) + +;; + + +let rewrite_back_simpl_tac ~term ~status = + Tacticals.then_ + ~start:(rewrite_back_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~status +;; + + +let replace_tac ~what ~with_what ~status:((proof, goal) as status) = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + let _,metasenv,_,_ = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let wty = CicTypeChecker.type_of_aux' metasenv context what in + try + if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what)) + then T.thens + ~start:( + P.cut_tac + ~term:( + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; (* quale uguaglianza usare, eq o eqT ? *) + wty ; + what ; + with_what])) + ~continuations:[ + T.then_ + ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *) + ~continuation:( + ProofEngineStructuralRules.clear + ~hyp:(List.hd context)) ; +(* (Some(C.Name "dummy_for_replace" , C.Def (CicTypeChecker.type_of_aux' metasenv context (C.Rel 1)) (* NOOOO!!!!! tipo di dummy *) )))) ; *) + T.id_tac] + ~status + else raise (ProofEngineTypes.Fail "Replace: terms not replaceable") + with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context") +;; + + +let reflexivity_tac = + IntroductionTactics.constructor_tac ~n:1 +;; + + +let symmetry_tac ~status:(proof, goal) = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> + PrimitiveTactics.apply_tac ~status:(proof,goal) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", [])) + + | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + PrimitiveTactics.apply_tac ~status:(proof,goal) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", [])) + + | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") +;; + + +let transitivity_tac ~term ~status:((proof, goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let module T = Tacticals in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> + T.thens + ~start:(PrimitiveTactics.apply_tac + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", []))) + ~continuations: + [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac] + ~status + + | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + T.thens + ~start:(PrimitiveTactics.apply_tac + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", []))) + ~continuations: + [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term] + ~status + + | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") +;; + + diff --git a/helm/gTopLevel/equalityTactics.mli b/helm/gTopLevel/equalityTactics.mli new file mode 100644 index 000000000..7d57a0c11 --- /dev/null +++ b/helm/gTopLevel/equalityTactics.mli @@ -0,0 +1,35 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +val replace_tac: what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic + +val reflexivity_tac: ProofEngineTypes.tactic +val symmetry_tac: ProofEngineTypes.tactic +val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic + diff --git a/helm/gTopLevel/equalityTactics.o b/helm/gTopLevel/equalityTactics.o new file mode 100644 index 000000000..7686b7d23 Binary files /dev/null and b/helm/gTopLevel/equalityTactics.o differ diff --git a/helm/gTopLevel/introductionTactics.cmi b/helm/gTopLevel/introductionTactics.cmi new file mode 100644 index 000000000..957cd311a Binary files /dev/null and b/helm/gTopLevel/introductionTactics.cmi differ diff --git a/helm/gTopLevel/introductionTactics.cmx b/helm/gTopLevel/introductionTactics.cmx new file mode 100644 index 000000000..bf2bb17cf Binary files /dev/null and b/helm/gTopLevel/introductionTactics.cmx differ diff --git a/helm/gTopLevel/introductionTactics.ml b/helm/gTopLevel/introductionTactics.ml new file mode 100644 index 000000000..bd29f4f5a --- /dev/null +++ b/helm/gTopLevel/introductionTactics.ml @@ -0,0 +1,59 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +let constructor_tac ~n ~status:(proof, goal) = + let module C = Cic in + let module R = CicReduction in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.MutInd (uri, typeno, exp_named_subst)) + | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) -> + PrimitiveTactics.apply_tac ~status:(proof, goal) + ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)) + | _ -> raise (ProofEngineTypes.Fail "Constructor failed") +;; + + +let exists_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let split_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let left_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let right_tac ~status = + constructor_tac ~n:2 ~status +;; + diff --git a/helm/gTopLevel/introductionTactics.mli b/helm/gTopLevel/introductionTactics.mli new file mode 100644 index 000000000..c3a12720b --- /dev/null +++ b/helm/gTopLevel/introductionTactics.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val constructor_tac: n:int -> ProofEngineTypes.tactic + +val exists_tac: ProofEngineTypes.tactic +val split_tac: ProofEngineTypes.tactic +val left_tac: ProofEngineTypes.tactic +val right_tac: ProofEngineTypes.tactic diff --git a/helm/gTopLevel/introductionTactics.o b/helm/gTopLevel/introductionTactics.o new file mode 100644 index 000000000..0f67a4174 Binary files /dev/null and b/helm/gTopLevel/introductionTactics.o differ diff --git a/helm/gTopLevel/negationTactics.cmi b/helm/gTopLevel/negationTactics.cmi new file mode 100644 index 000000000..2bb6540d2 Binary files /dev/null and b/helm/gTopLevel/negationTactics.cmi differ diff --git a/helm/gTopLevel/negationTactics.cmx b/helm/gTopLevel/negationTactics.cmx new file mode 100644 index 000000000..bb9034294 Binary files /dev/null and b/helm/gTopLevel/negationTactics.cmx differ diff --git a/helm/gTopLevel/negationTactics.ml b/helm/gTopLevel/negationTactics.ml new file mode 100644 index 000000000..d55f04556 --- /dev/null +++ b/helm/gTopLevel/negationTactics.ml @@ -0,0 +1,67 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +let absurd_tac ~term ~status:((proof,goal) as status) = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let _,metasenv,_,_ = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) + then P.apply_tac + ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status + else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition") +;; + + +let contradiction_tac ~status = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + T.then_ + ~start: P.intros_tac + ~continuation:( + T.then_ + ~start: (EliminationTactics.elim_type_tac + ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )) + ~continuation: VariousTactics.assumption_tac) + ~status +;; + +(* Questa era in fourierR.ml +(* !!!!! fix !!!!!!!!!! *) +let contradiction_tac ~status:(proof,goal)= + Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*) + ~continuation:(Tacticals.then_ + ~start:(VariousTactics.elim_type_tac ~term:_False) + ~continuation:(assumption_tac)) + ~status:(proof,goal) +;; +*) + + diff --git a/helm/gTopLevel/negationTactics.mli b/helm/gTopLevel/negationTactics.mli new file mode 100644 index 000000000..bfa3e8d5d --- /dev/null +++ b/helm/gTopLevel/negationTactics.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val absurd_tac: term:Cic.term -> ProofEngineTypes.tactic +val contradiction_tac: ProofEngineTypes.tactic + diff --git a/helm/gTopLevel/negationTactics.o b/helm/gTopLevel/negationTactics.o new file mode 100644 index 000000000..2c872a7df Binary files /dev/null and b/helm/gTopLevel/negationTactics.o differ diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml index 615cf43b4..604307cd3 100644 --- a/helm/gTopLevel/variousTactics.ml +++ b/helm/gTopLevel/variousTactics.ml @@ -65,6 +65,9 @@ let assumption_tac ~status:(proof,goal)= (* ANCORA DA DEBUGGARE *) +(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda +e li aggiunga nel context, poi si conta la lunghezza di questo nuovo +contesto e si lifta *) let generalize_tac ~term ~status:((proof,goal) as status) = let module C = Cic in let module P = PrimitiveTactics in @@ -82,7 +85,7 @@ let generalize_tac ~term ~status:((proof,goal) as status) = ~what:term ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) ~where:ty) - ))) + ))) ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] ~status ;;