EqualityTactics, IntroductionTactics and NegationTactics.
--- /dev/null
+(* 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
+;;
+
+
--- /dev/null
+(* 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
--- /dev/null
+(* 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")
+;;
+
+
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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
+;;
+
--- /dev/null
+(* 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
--- /dev/null
+(* 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)
+;;
+*)
+
+
--- /dev/null
+(* 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
+
(* 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
~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
;;
projects / helm.git / commitdiff