From: marangon Date: Thu, 15 Dec 2005 16:02:48 +0000 (+0000) Subject: New tactic: inversion. X-Git-Tag: make_still_working~7992 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=059c1bb4766e823aa53b39fed7d3dd55b4a06101;p=helm.git New tactic: inversion. - only first phase implemented (no cleaning) - code in inversion.ml to be improved/cleaned up --- diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml index e1ae5865d..810e54140 100644 --- a/helm/ocaml/grafite/grafiteAst.ml +++ b/helm/ocaml/grafite/grafiteAst.ml @@ -70,6 +70,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | IdTac of loc | Injection of loc * 'term | Intros of loc * int option * 'ident list + | Inversion of loc * 'term | LApply of loc * int option * 'term list * 'term * 'ident option | Left of loc | LetIn of loc * 'term * 'ident diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml index 617a6d563..7be8c816e 100644 --- a/helm/ocaml/grafite/grafiteAstPp.ml +++ b/helm/ocaml/grafite/grafiteAstPp.ml @@ -117,6 +117,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | IdTac _ -> "id" | Injection (_, term) -> "injection " ^ term_pp term | Intros (_, None, []) -> "intro" + | Inversion (_, term) -> "inversion " ^ term_pp term | Intros (_, num, idents) -> sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml index 1fa272b22..4a851e77b 100644 --- a/helm/ocaml/grafite2/grafiteEngine.ml +++ b/helm/ocaml/grafite2/grafiteEngine.ml @@ -118,6 +118,8 @@ let tactic_of_ast ast = | GrafiteAst.Intros (_, Some num, names) -> PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) () + | GrafiteAst.Inversion (_, term) -> + Tactics.inversion term | GrafiteAst.LApply (_, how_many, to_what, what, ident) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml index 7b6b69d44..e6cc064a5 100644 --- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml +++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml @@ -170,6 +170,9 @@ let disambiguate_tactic status goal tactic = let term = disambiguate_term status_ref goal term in GrafiteAst.Injection (loc,term) | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names) + | GrafiteAst.Inversion (loc, term) -> + let term = disambiguate_term status_ref goal term in + GrafiteAst.Inversion (loc, term) | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> let f term to_what = let term = disambiguate_term status_ref goal term in diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml index aa60c87c4..5b9cea37a 100644 --- a/helm/ocaml/grafite_parser/grafiteParser.ml +++ b/helm/ocaml/grafite_parser/grafiteParser.ml @@ -183,6 +183,8 @@ EXTEND GrafiteAst.Intros (loc, Some 1, idents) | IDENT "intros"; (num, idents) = intros_spec -> GrafiteAst.Intros (loc, num, idents) + | IDENT "inversion"; t = tactic_term -> + GrafiteAst.Inversion (loc, t) | IDENT "lapply"; depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; what = tactic_term; diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 9ff04ffec..5d1ceb1d0 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -12,11 +12,11 @@ eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi equalityTactics.cmi: proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi +inversion.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi -tactics.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi @@ -85,6 +85,12 @@ discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ proofEngineTypes.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi +inversion.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \ + inversion.cmi +inversion.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \ + inversion.cmi ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \ primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \ @@ -111,11 +117,11 @@ statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.cmi tactics.cmo: variousTactics.cmi tacticals.cmi ring.cmi reductionTactics.cmi \ proofEngineStructuralRules.cmi primitiveTactics.cmi negationTactics.cmi \ - introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ + inversion.cmi introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ autoTactic.cmi tactics.cmi tactics.cmx: variousTactics.cmx tacticals.cmx ring.cmx reductionTactics.cmx \ proofEngineStructuralRules.cmx primitiveTactics.cmx negationTactics.cmx \ - introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ + inversion.cmx introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ autoTactic.cmx tactics.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 88372bf04..1595fb337 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -8,9 +8,9 @@ INTERFACE_FILES = \ primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ variousTactics.mli autoTactic.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ - equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \ - fourierR.mli fwdSimplTactic.mli history.mli statefulProofEngine.mli \ - tactics.mli + equalityTactics.mli discriminationTactics.mli inversion.mli ring.mli \ + fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ + statefulProofEngine.mli tactics.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) all: diff --git a/helm/ocaml/tactics/inversion.ml b/helm/ocaml/tactics/inversion.ml new file mode 100644 index 000000000..3bedf006a --- /dev/null +++ b/helm/ocaml/tactics/inversion.ml @@ -0,0 +1,320 @@ +(* 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/. + *) + +exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple +exception NotAnInductiveTypeToEliminate + +let debug = false;; +let debug_print = + fun msg -> if debug then prerr_endline (Lazy.force msg) else () + +let inside_obj = function + | Cic.InductiveDefinition (l,params, nleft, _) -> + (l,params,nleft) + | _ -> raise (Invalid_argument "Errore in inside_obj") + +let term_to_list = function + | Cic.Appl l -> l + | _ -> raise (Invalid_argument "Errore in term_to_list") + + +let rec baseuri_of_term = function + | Cic.Appl l -> baseuri_of_term (List.hd l) + | Cic.MutInd (baseuri, tyno, []) -> baseuri + | _ -> raise (Invalid_argument "baseuri_of_term") + + +(*prende il numero dei parametri sinistri, la lista dei parametri, la lista dei tipi dei parametri, +il tipo del GOAL e costruisce il termine per la cut ossia DX1 = DX1 -> ... DXn=DXn -> GOALTY *) +let rec foo_cut nleft l param_ty_l body uri_of_eq = + + if nleft >0 then foo_cut (nleft-1) (List.tl l) (List.tl param_ty_l) body uri_of_eq + else match l with + | hd::tl -> Cic.Prod (Cic.Anonymous, + Cic.Appl[Cic.MutInd (uri_of_eq ,0,[]); + (List.hd param_ty_l) ; + hd; + hd], + foo_cut nleft (List.map (CicSubstitution.lift 1) tl) (List.tl param_ty_l) (CicSubstitution.lift 1 body) uri_of_eq + ) + | [] -> body + ;; + +(* da una catena di prod costruisce una lista dei termini che lo compongono.*) +let rec list_of_prod term = +match term with + | Cic.Prod (Cic.Anonymous,src,tgt) -> [src] @ (list_of_prod tgt) + | _ -> [term] + +;; + + +let rec cut_first n l = + if n>0 then + match l with + | hd::tl -> cut_first (n-1) tl + | [] -> [] + else l +;; + + +let rec cut_last l = +match l with + | hd::tl when tl != [] -> hd:: (cut_last tl) + | _ -> [] +;; + + +let foo_appl nleft nright_consno term uri = + let l = [] in + let a = ref l in + + for n = 1 to nleft do + a := !a @ [(Cic.Implicit None)] + + done; + a:= !a @ [term]; + + for n = 1 to nright_consno do + a := !a @ [(Cic.Implicit None)] + done; + Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1]) (*L'ipotesi e' sempre Rel 1. (?) *) +;; + + + +let rec foo_prod nright param_ty_l l l2 base_rel body uri_of_eq nleft termty isSetType term = + match param_ty_l with + | hd::tl -> Cic.Prod (Cic.Anonymous, + Cic.Appl[Cic.MutInd(uri_of_eq,0,[]); + hd; + (List.hd l); + Cic.Rel base_rel + ], + foo_prod (nright-1) tl (List.map (CicSubstitution.lift 1) (List.tl l)) + (List.map (CicSubstitution.lift 1) l2) + base_rel + (CicSubstitution.lift 1 body) + uri_of_eq nleft + (CicSubstitution.lift 1 termty) + isSetType + (CicSubstitution.lift 1 term)) + + + | [] -> ProofEngineReduction.replace_lifting ~equality:(ProofEngineReduction.alpha_equivalence) + ~what: (if isSetType then ((cut_first (1+nleft) (term_to_list termty) ) @ [term] ) + else (cut_first (1+nleft) (term_to_list termty) ) ) + ~with_what: (List.map (CicSubstitution.lift (-1)) l2) + ~where:body + (*TODO lo stesso sottotermine di body puo' essere sia sx che dx!*) +;; + + +let rec foo_lambda nright param_ty_l nright_ param_ty_l_ l l2 base_rel body uri_of_eq nleft termty isSetType ty_indty term = + (*assert nright >0 *) + match param_ty_l with + | hd::tl ->Cic.Lambda ((Cic.Name ("lambda" ^ (string_of_int nright))), + hd, (* typ *) + foo_lambda (nright-1) tl + nright_ param_ty_l_ + (List.map (CicSubstitution.lift 1) l) + (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) + base_rel + (CicSubstitution.lift 1 body) + uri_of_eq nleft + (CicSubstitution.lift 1 termty) + isSetType ty_indty + (CicSubstitution.lift 1 term)) + | [] when isSetType -> Cic.Lambda ( + (Cic.Name ("lambda" ^ (string_of_int nright))), + (ProofEngineReduction.replace_lifting ~equality:(ProofEngineReduction.alpha_equivalence) + ~what: (cut_first (1+nleft) (term_to_list termty) ) + ~with_what: (List.map (CicSubstitution.lift (-1)) l2) + ~where:termty), (* tipo di H con i parametri destri sostituiti *) + foo_prod nright_ param_ty_l_ + (List.map (CicSubstitution.lift 1) l) + (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) + (base_rel+1) (CicSubstitution.lift 1 body) + uri_of_eq nleft + (CicSubstitution.lift 1 termty) isSetType + (CicSubstitution.lift 1 term)) + | [] -> foo_prod nright_ param_ty_l_ l l2 + base_rel body uri_of_eq + nleft termty isSetType term +;; + + + +let inversion_tac ~term = + let module T = CicTypeChecker in + let module R = CicReduction in + let module C = Cic in + let module P = PrimitiveTactics in + let module PET = ProofEngineTypes in + let inversion_tac ~term (proof, goal) = + let (_,metasenv,_,_) = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let (newproof, metasenv') = ProofEngineHelpers.subst_meta_in_proof proof metano term [] in + let uri_of_eq = HelmLibraryObjects.Logic.eq_URI in + +(* dall'indice che indentifica il goal nel metasenv, ritorna il suo tipo, che e' la terza componente +della relativa congettura *) +let (_,_,body) = CicUtil.lookup_meta goal metasenv in + +(* estrae il tipo del termine oggetto di inversion, di solito un Cic.Appl list, ma..*) + + let termty,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let uri = baseuri_of_term termty in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let l,params,nleft = inside_obj o in + let (_,_,typeno,_) = + 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 NotAnInductiveTypeToEliminate + in + + let eliminator_uri = + + let buri = UriManager.buri_of_uri uri in + let name = + match o with + C.InductiveDefinition (tys,_,_,_) -> + let (name,_,_,_) = List.nth tys typeno in + name + |_ -> assert false + in + + +(* let ty_ty,_ = T.type_of_aux' metasenv context termty CicUniv.empty_ugraph in + let ext = + match ty_ty with + C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort C.CProp -> "_rec" + | C.Sort (C.Type _)-> "_rect" + | C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple + | _ -> assert false + in +*) + + let ext = "_ind" in + UriManager.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") +in + + (* il tipo del tipo induttivo oggetto di inversione *) + + let (_,_,ty_indty,cons_list) = (List.hd l) in + (*la lista ricavata dal tipo del tipo induttivo. *) + let param_ty_l = list_of_prod ty_indty in + let consno = List.length cons_list in + let nright= (List.length param_ty_l)- (nleft+1) in + + let isSetType = ((Pervasives.compare + (List.nth param_ty_l ((List.length param_ty_l)-1)) + (Cic.Sort Cic.Prop) + ) != 0) in + + + + +(* eliminiamo la testa di termty, in quanto e' il nome del predicato e non un parametro.*) +let cut_term = foo_cut nleft (List.tl (term_to_list termty)) (list_of_prod ty_indty) body uri_of_eq in + + + +(* cut DXn=DXn \to GOAL *) +let proof1,gl1 = PET.apply_tactic (P.cut_tac cut_term) (proof,goal) in + +(* apply Hcut ; reflexivity (su tutti i goals aperti da apply_tac) *) +let proof2, gl2 = PET.apply_tactic + (Tacticals.then_ + ~start: (P.apply_tac (C.Rel 1) + ) (* apply Hcut *) + ~continuation: (EqualityTactics.reflexivity_tac + ) + ) + (proof1, (List.hd gl1)) + + in + + + +(* apply (ledx_ind( lambda x. lambda y, ...)) *) + +let (t1,metasenv,t3,t4) = proof2 in +let goal2 = List.hd (List.tl gl1) in +let (metano,context,_) = CicUtil.lookup_meta goal2 metasenv in + +let cut_param_ty_l = (cut_first nleft (cut_last param_ty_l)) in + +(* la lista dei soli parametri destri *) +let l= cut_first (1+nleft) (term_to_list termty) in + +let lambda_t = foo_lambda nright cut_param_ty_l nright cut_param_ty_l l [] nright body uri_of_eq nleft termty isSetType ty_indty term in +let t = foo_appl nleft (nright+consno) lambda_t eliminator_uri in + +debug_print (lazy ("Lambda_t: " ^ (CicPp.ppterm t))); +prerr_endline ("Term: " ^ (CicPp.ppterm termty)); +prerr_endline ("Body: " ^ (CicPp.ppterm body)); +prerr_endline ("Right param: " ^ (CicPp.ppterm (Cic.Appl l))); + + + + + + +let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t CicUniv.empty_ugraph in + +let proof2 = (t1,metasenv'',t3,t4) in + +let proof3,gl3 = PET.apply_tactic (P.apply_tac ref_t) + (proof2, goal2) in + +let new_goals = + ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:metasenv'' + in + +let patched_new_goals = + let (_,metasenv''',_,_) = proof3 in + List.filter + (function i -> List.exists (function (j,_,_) -> j=i) metasenv''' + ) new_goals @ gl3 + in + + + + +(*prerr_endline ("METASENV: " ^ CicMetaSubst.ppmetasenv metasenv []); DEBUG*) + + +(proof3, patched_new_goals) + +in + +ProofEngineTypes.mk_tactic (inversion_tac ~term) +;; diff --git a/helm/ocaml/tactics/inversion.mli b/helm/ocaml/tactics/inversion.mli new file mode 100644 index 000000000..50bdf58f2 --- /dev/null +++ b/helm/ocaml/tactics/inversion.mli @@ -0,0 +1,26 @@ +(* 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 inversion_tac: term: Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml index e75677caf..ee59af349 100644 --- a/helm/ocaml/tactics/tactics.ml +++ b/helm/ocaml/tactics/tactics.ml @@ -50,6 +50,7 @@ let generalize = VariousTactics.generalize_tac let id = Tacticals.id_tac let injection = DiscriminationTactics.injection_tac let intros = PrimitiveTactics.intros_tac +let inversion = Inversion.inversion_tac let lapply = FwdSimplTactic.lapply_tac let left = IntroductionTactics.left_tac let letin = PrimitiveTactics.letin_tac diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 9d5bc4753..cc2498577 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -1,89 +1 @@ (* GENERATED FILE, DO NOT EDIT *) -val absurd : term:Cic.term -> ProofEngineTypes.tactic -val apply : term:Cic.term -> ProofEngineTypes.tactic -val assumption : ProofEngineTypes.tactic -val auto : - ?depth:int -> - ?width:int -> - ?paramodulation:string -> - ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic -val change : - pattern:ProofEngineTypes.lazy_pattern -> - ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic -val clear : hyp:string -> ProofEngineTypes.tactic -val clearbody : hyp:string -> ProofEngineTypes.tactic -val compare : term:Cic.term -> ProofEngineTypes.tactic -val constructor : n:int -> ProofEngineTypes.tactic -val contradiction : ProofEngineTypes.tactic -val cut : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - Cic.term -> ProofEngineTypes.tactic -val decide_equality : ProofEngineTypes.tactic -val decompose : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?user_types:(UriManager.uri * int) list -> - dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic -val discriminate : term:Cic.term -> ProofEngineTypes.tactic -val elim_intros : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic -val elim_intros_simpl : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic -val elim_type : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic -val exact : term:Cic.term -> ProofEngineTypes.tactic -val exists : ProofEngineTypes.tactic -val fail : ProofEngineTypes.tactic -val fold : - reduction:ProofEngineTypes.lazy_reduction -> - term:ProofEngineTypes.lazy_term -> - pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val fourier : ProofEngineTypes.tactic -val fwd_simpl : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic -val generalize : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val id : ProofEngineTypes.tactic -val injection : term:Cic.term -> ProofEngineTypes.tactic -val intros : - ?howmany:int -> - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - unit -> ProofEngineTypes.tactic -val lapply : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?how_many:int -> - ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic -val left : ProofEngineTypes.tactic -val letin : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - Cic.term -> ProofEngineTypes.tactic -val normalize : - pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val reflexivity : ProofEngineTypes.tactic -val replace : - pattern:ProofEngineTypes.lazy_pattern -> - with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic -val rewrite : - direction:[ `LeftToRight | `RightToLeft ] -> - pattern:ProofEngineTypes.lazy_pattern -> - Cic.term -> ProofEngineTypes.tactic -val rewrite_simpl : - direction:[ `LeftToRight | `RightToLeft ] -> - pattern:ProofEngineTypes.lazy_pattern -> - Cic.term -> ProofEngineTypes.tactic -val right : ProofEngineTypes.tactic -val ring : ProofEngineTypes.tactic -val set_goal : int -> ProofEngineTypes.tactic -val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val split : ProofEngineTypes.tactic -val symmetry : ProofEngineTypes.tactic -val transitivity : term:Cic.term -> ProofEngineTypes.tactic -val unfold : - ProofEngineTypes.lazy_term option -> - pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic