proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \
primitiveTactics.cmi
primitiveTactics.cmi: proofEngineTypes.cmo
+variousTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticals.cmi \
+ variousTactics.cmi
+variousTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticals.cmx \
+ variousTactics.cmi
+variousTactics.cmi: proofEngineTypes.cmo
ring.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \
- proofEngineTypes.cmo tacticals.cmi ring.cmi
+ proofEngineTypes.cmo tacticals.cmi variousTactics.cmi ring.cmi
ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \
- proofEngineTypes.cmx tacticals.cmx ring.cmi
+ proofEngineTypes.cmx tacticals.cmx variousTactics.cmx ring.cmi
ring.cmi: proofEngineTypes.cmo
fourierR.cmo: fourier.cmo primitiveTactics.cmi proofEngineHelpers.cmi \
- proofEngineReduction.cmi proofEngineTypes.cmo ring.cmi tacticals.cmi \
- fourierR.cmi
+ proofEngineReduction.cmi proofEngineTypes.cmo reductionTactics.cmi \
+ ring.cmi tacticals.cmi fourierR.cmi
fourierR.cmx: fourier.cmx primitiveTactics.cmx proofEngineHelpers.cmx \
- proofEngineReduction.cmx proofEngineTypes.cmx ring.cmx tacticals.cmx \
- fourierR.cmi
+ proofEngineReduction.cmx proofEngineTypes.cmx reductionTactics.cmx \
+ ring.cmx tacticals.cmx fourierR.cmi
fourierR.cmi: proofEngineTypes.cmo
proofEngine.cmo: fourierR.cmi primitiveTactics.cmi proofEngineHelpers.cmi \
proofEngineReduction.cmi proofEngineStructuralRules.cmi \
- proofEngineTypes.cmo ring.cmi proofEngine.cmi
+ proofEngineTypes.cmo ring.cmi tacticals.cmi variousTactics.cmi \
+ proofEngine.cmi
proofEngine.cmx: fourierR.cmx primitiveTactics.cmx proofEngineHelpers.cmx \
proofEngineReduction.cmx proofEngineStructuralRules.cmx \
- proofEngineTypes.cmx ring.cmx proofEngine.cmi
+ proofEngineTypes.cmx ring.cmx tacticals.cmx variousTactics.cmx \
+ proofEngine.cmi
proofEngine.cmi: proofEngineTypes.cmo
doubleTypeInference.cmo: doubleTypeInference.cmi
doubleTypeInference.cmx: doubleTypeInference.cmi
proofEngineReduction.ml proofEngineReduction.mli \
proofEngineStructuralRules.ml proofEngineStructuralRules.mli \
tacticals.ml tacticals.mli reductionTactics.ml reductionTactics.mli \
- primitiveTactics.ml primitiveTactics.mli \
+ primitiveTactics.ml primitiveTactics.mli variousTactics.ml variousTactics.mli \
ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\
proofEngine.ml proofEngine.mli \
doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \
proofEngineReduction.cmo proofEngineStructuralRules.cmo \
tacticals.cmo reductionTactics.cmo primitiveTactics.cmo \
+ variousTactics.cmo \
ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \
doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \
logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \
--- /dev/null
+
+!n:nat.(eq nat n n)
+
+!n:nat.!m:nat.(eq nat n m)->(eq nat m n)
+
+!n:nat.!m:nat.!p:nat.(eq nat n p)->(eq nat p m)->(eq nat n m)
+
" disequazioni\n");
let res=fourier_lineq (!lineq) in
- let tac=ref Ring.id_tac in
+ let tac=ref Tacticals.id_tac in
if res=[] then
(print_string "Tactic Fourier fails.\n";flush stdout;
failwith "fourier_tac fails")
let r = Ring.ring_tac ~status in
debug ("end RING\n");
r)
- ; "id", Ring.id_tac]
+ ; "id", Tacticals.id_tac]
])
(* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *)
;tac2]))
(*
let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
-*)
let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
+*)
+
+let prooffile = "/home/galata/miohelm/currentproof";;
+let prooffiletype = "/home/galata/miohelm/currentprooftype";;
+
(*CSC: the getter should handle the innertypes, not the FS *)
(*
let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
-*)
let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
+*)
+
+let innertypesfile = "/home/galata/miohelm/innertypes";;
+let constanttypefile = "/home/galata/miohelm/constanttype";;
+
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
let rewritesimpl rendering_window =
call_tactic_with_input ProofEngine.rewrite_simpl rendering_window
;;
-
+let reflexivity rendering_window =
+ call_tactic ProofEngine.reflexivity rendering_window
+;;
+let symmetry rendering_window =
+ call_tactic ProofEngine.symmetry rendering_window
+;;
+let transitivity rendering_window =
+ call_tactic_with_input ProofEngine.transitivity rendering_window
+;;
+let left rendering_window =
+ call_tactic ProofEngine.left rendering_window
+;;
+let right rendering_window =
+ call_tactic ProofEngine.right rendering_window
+;;
+let assumption rendering_window =
+ call_tactic ProofEngine.assumption rendering_window
+;;
+(*
+let prova_tatticali rendering_window =
+ call_tactic ProofEngine.prova_tatticali rendering_window
+;;
+*)
let whd_in_scratch scratch_window =
let rewritesimplb =
GButton.button ~label:"RewriteSimpl ->"
~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let reflexivityb =
+ GButton.button ~label:"Reflexivity"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let symmetryb =
+ GButton.button ~label:"Symmetry"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let transitivityb =
+ GButton.button ~label:"Transitivity"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let leftb =
+ GButton.button ~label:"Left"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let rightb =
+ GButton.button ~label:"Right"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let assumptionb =
+ GButton.button ~label:"Assumption"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let prova_tatticalib =
+ GButton.button ~label:"Prova_tatticali"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
let outputhtml =
GHtml.xmhtml
~source:"<html><body bgColor=\"white\"></body></html>"
ignore(clearb#connect#clicked (clear self)) ;
ignore(fourierb#connect#clicked (fourier self)) ;
ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ;
+ ignore(reflexivityb#connect#clicked (reflexivity self)) ;
+ ignore(symmetryb#connect#clicked (symmetry self)) ;
+ ignore(transitivityb#connect#clicked (transitivity self)) ;
+ ignore(leftb#connect#clicked (left self)) ;
+ ignore(rightb#connect#clicked (right self)) ;
+ ignore(assumptionb#connect#clicked (assumption self)) ;
+(*
+ ignore(prova_tatticalib#connect#clicked (prova_tatticali self)) ;
+*)
ignore(introsb#connect#clicked (intros self)) ;
Logger.log_callback :=
(Logger.log_to_html ~print_and_flush:(output_html outputhtml))
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term)
+
+let reflexivity () = apply_tactic VariousTactics.reflexivity_tac
+let symmetry () = apply_tactic VariousTactics.symmetry_tac
+let transitivity term = apply_tactic (VariousTactics.transitivity_tac ~term)
+
+let left () = apply_tactic VariousTactics.left_tac
+let right () = apply_tactic VariousTactics.right_tac
+
+let assumption () = apply_tactic VariousTactics.assumption_tac
+(*
+let prova_tatticali () = apply_tactic Tacticals.prova_tac
+*)
+
val ring : unit -> unit
val fourier : unit -> unit
val rewrite_simpl : Cic.term -> unit
+
+val reflexivity : unit -> unit
+val symmetry : unit -> unit
+val transitivity : Cic.term -> unit
+
+val left : unit -> unit
+val right : unit -> unit
+
+val assumption : unit -> unit
+
+(*
+val prova_tatticali : unit -> unit
+*)
Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t]
) aterms
-let id_tac ~status:(proof,goal) =
- (proof,[goal])
let status_of_single_goal_tactic_result =
function
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) ; id_tac] ~status
+ ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
(**
auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
let elim_type2_tac ~term ~proof ~status =
warn "in Ring.elim_type2";
Tacticals.thens ~start:(elim_type_tac ~term)
- ~continuations:[id_tac ; exact_tac ~term:proof] ~status
+ ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
+(* spostata in variousTactics.ml
(**
Reflexivity tactic, try to solve current goal using "refl_eqT"
Warning: this isn't equale to the coq's Reflexivity because this one tries
with (Fail _) as e ->
let e_str = Printexc.to_string e in
raise (Fail ("Reflexivity failed with exception: " ^ e_str))
+*)
(** lift an 8-uple of debrujins indexes of n *)
let lift ~n (a,b,c,d,e,f,g,h) =
Tacticals.try_tactics
~status
~tactics:[
- "reflexivity", reflexivity_tac ;
+ "reflexivity", VariousTactics.reflexivity_tac ;
"exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
"exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
"exact sym_eqt su t1 ...", exact_tac
in
try (* try to solve main goal *)
warn "trying reflexivity ....";
- reflexivity_tac ~status:status'
+ VariousTactics.reflexivity_tac ~status:status'
with (Fail _) -> (* leave conclusion to the user *)
warn "reflexivity failed, solution's left as an ex :-)";
purge_hyps_tac ~count:!new_hyps ~status:status')]
(* auxiliary tactics *)
val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
+
+(* spostata in variousTactics.ml
val reflexivity_tac: ProofEngineTypes.tactic
-val id_tac : ProofEngineTypes.tactic
+*)
if debug then
prerr_endline ("TACTICALS WARNING: " ^ s)
-(** AUX TACTIC{,AL}S *)
+
+(** TACTIC{,AL}S *)
+
+ (* not a tactical, but it's used only here (?) *)
+
+let id_tac ~status:(proof,goal) =
+ (proof,[goal])
+
(**
naive implementation of ORELSE tactical, try a sequence of tactics in turn:
if one fails pass to the next one and so on, eventually raises (failure "no
tactics left")
TODO warning: not tail recursive due to "try .. with" boxing
+
+ Galla: is this exactly Coq's "First"?
+
*)
let rec try_tactics ~(tactics: (string * tactic) list) ~status =
- warn "in Ring.try_tactics";
+ warn "in Tacticals.try_tactics";
match tactics with
| (descr, tac)::tactics ->
- warn ("Ring.try_tactics IS TRYING " ^ descr);
+ warn ("Tacticals.try_tactics IS TRYING " ^ descr);
(try
let res = tac ~status in
- warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!");
+ warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!");
res
with
e ->
| (CicTypeChecker.NotWellTyped _)
| (CicUnification.UnificationFailed) ->
warn (
- "Ring.try_tactics failed with exn: " ^
+ "Tacticals.try_tactics failed with exn: " ^
Printexc.to_string e);
try_tactics ~tactics ~status
| _ -> raise e (* [e] must not be caught ; let's re-raise it *)
)
| [] -> raise (Fail "try_tactics: no tactics left")
+
+
let thens ~start ~continuations ~status =
let (proof,new_goals) = start ~status in
try
with
Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+
+
let then_ ~start ~continuation ~status =
let (proof,new_goals) = start ~status in
List.fold_left
let (proof',new_goals') = continuation ~status:(proof,goal) in
(proof',goals@new_goals')
) (proof,[]) new_goals
+
+
+(* Galla *)
+(* si suppone che tutte le tattiche sollevano solamente Fail? *)
+
+(* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
+
+(* This keep on appling tactic until it fails *)
+(* When <tactic> generates more than one goal, you have a tree of
+ application on the tactic, repeat_tactic works in depth on this tree *)
+
+let rec repeat_tactic ~tactic ~status =
+ warn "in repeat_tactic";
+ try let (proof, goallist) = tactic ~status in
+ let rec step proof goallist =
+ match goallist with
+ [] -> (proof, [])
+ | head::tail ->
+ let (proof', goallist') = repeat_tactic ~tactic ~status:(proof, head) in
+ let (proof'', goallist'') = step proof' tail in
+ proof'', goallist'@goallist''
+ in
+ step proof goallist
+ with
+ (Fail _) as e ->
+ warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+ id_tac ~status
+;;
+
+
+
+(* This tries to apply tactic n times *)
+
+let rec do_tactic ~n ~tactic ~status =
+ warn "in do_tactic";
+ try
+ let (proof, goallist) =
+ if (n>0) then tactic ~status
+ else id_tac ~status in
+(* else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *)
+ let rec step proof goallist =
+ match goallist with
+ [] -> (proof, [])
+ | head::tail ->
+ let (proof', goallist') = do_tactic ~n:(n-1) ~tactic ~status:(proof, head) in
+ let (proof'', goallist'') = step proof' tail in
+ proof'', goallist'@goallist''
+ in
+ step proof goallist
+ with
+ (Fail _) as e ->
+ warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+ id_tac ~status
+;;
+
+
+
+(* This applies tactic and catches its possible failure *)
+
+let rec try_tactic ~tactic ~status =
+ warn "in Tacticals.try_tactic";
+ try
+ tactic ~status
+ with
+ (Fail _) as e ->
+ warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
+ id_tac ~status
+;;
+
+
+(* This tries tactics until one of them doesn't _solve_ the goal *)
+(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
+
+let rec solve_tactics ~(tactics: (string * tactic) list) ~status =
+ warn "in Tacticals.solve_tactics";
+ match tactics with
+ | (descr, currenttactic)::moretactics ->
+ warn ("Tacticals.solve_tactics is trying " ^ descr);
+ (try
+ let (proof, goallist) = currenttactic ~status in
+ match goallist with
+ [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!");
+(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *)
+(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
+ (proof, goallist)
+ | _ -> warn ("Tacticals.solve_tactics: try the next tactic");
+ solve_tactics ~tactics:(moretactics) ~status
+ with
+ (Fail _) as e ->
+ warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e);
+ solve_tactics ~tactics ~status
+ )
+ | [] -> raise (Fail "solve_tactics cannot solve the goal");
+ id_tac ~status
+;;
+
+
+
+
+
+
+ (** tattica di prova per debuggare i tatticali *)
+(*
+let thens' ~start ~continuations ~status =
+ let (proof,new_goals) = start ~status in
+ try
+ List.fold_left2
+ (fun (proof,goals) goal tactic ->
+ let (proof',new_goals') = tactic ~status:(proof,goal) in
+ (proof',goals@new_goals')
+ ) (proof,[]) new_goals continuations
+ with
+ Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+
+let prova_tac =
+ let apply_T_tac ~status:((proof,goal) as status) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let rel =
+ let rec find n =
+ function
+ [] -> assert false
+ | (Some (Cic.Name name,_))::_ when name = "T" -> n
+ | _::tl -> find (n+1) tl
+ in
+ prerr_endline ("eseguo find");
+ find 1 context
+ in
+ prerr_endline ("eseguo apply");
+ apply_tac ~term:(Cic.Rel rel) ~status
+ in
+(* do_tactic ~n:2 *)
+ repeat_tactic
+ ~tactic:
+ (then_
+ ~start:(intros_tac ~name:"pippo")
+ ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)]))
+(* id_tac *)
+;;
+*)
+
+
* http://cs.unibo.it/helm/.
*)
+
+val id_tac : ProofEngineTypes.tactic
+
+
+
(* pseudo tacticals *)
val try_tactics:
tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
+
val thens:
start: ProofEngineTypes.tactic ->
continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
+
val then_:
start: ProofEngineTypes.tactic ->
continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+
+
+val repeat_tactic:
+ tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+
+val do_tactic:
+ n: int ->
+ tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+
+val try_tactic:
+ tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+
+val solve_tactics:
+ tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
+
+
+
+(*
+val prova_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 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
+;;
+
+
+let reflexivity_tac =
+ 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/Equality/eq.ind")) ->
+ PrimitiveTactics.apply_tac ~status:(proof,goal)
+ ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/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/Equality_is_a_congruence/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 Tl = 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/Equality/eq.ind")) ->
+ Tl.thens
+ ~start:(PrimitiveTactics.apply_tac
+ ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/trans_eq.con", [])))
+ ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac]
+ ~status
+
+ | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
+ Tl.thens
+ ~start:(PrimitiveTactics.apply_tac
+ ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/trans_eqT.con", [])))
+ ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac]
+ ~status
+
+ | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
+;;
+
+
+(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
+
+let assumption_tac ~status:((proof,goal) as status) =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module T = CicTypeChecker in
+ let _,metasenv,_,_ = proof in
+ let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let rec find n = function
+ hd::tl ->
+(* (let hdd = hd in
+ match hdd with
+ Some (name, termine) -> prerr_endline("####" ^ name ^ CicPp.ppterm termine)
+ | None -> prerr_endline("#### None")
+ );
+*) (match hd with
+ (Some (_, C.Decl t)) when (R.are_convertible context t ty) -> n
+ | (Some (_, C.Def t)) when (R.are_convertible context (T.type_of_aux' metasenv context t) ty) -> n
+ | _ -> find (n+1) tl
+ )
+ | [] -> raise (ProofEngineTypes.Fail "No such assumption")
+ in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
+;;
+
+(*
+let generalize_tac ~term ~status:((proof,goal) as status) =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module T = CicTypeChecker in
+ let module P = PrimitiveTactics in
+ let module Tl = Tacticals in
+ let _,metasenv,_,_ = proof in
+ let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ Tl.thens
+ ~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 )))
+ ~continuations: [(P.apply_tac (C.Appl [(C.Rel 1); term])); Tl.id_tac] (* in quest'ordine o viceversa? provare *)
+ ~status
+;;
+
+
+let absurd_tac ~term ~status:((proof,goal) as status) =
+ PrimitiveTactics.cut_tac
+;;
+*)
+
--- /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 reflexivity_tac: ProofEngineTypes.tactic
+val symmetry_tac: ProofEngineTypes.tactic
+val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic
+
+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
+
+val assumption_tac: ProofEngineTypes.tactic
+
+(*
+val generalize_tac: Cic.term -> ProofEnginrTypes.tactic
+*)
projects / helm.git / commitdiff