From abd9e5cfa8e7b6923e0664a4813a0a842f5c4e76 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 17 Jun 2005 14:58:48 +0000 Subject: [PATCH] added support for goal patterns --- helm/ocaml/tactics/discriminationTactics.ml | 5 +- helm/ocaml/tactics/equalityTactics.ml | 69 +++++++---- helm/ocaml/tactics/equalityTactics.mli | 20 +++- helm/ocaml/tactics/fourierR.ml | 2 +- helm/ocaml/tactics/primitiveTactics.ml | 2 +- helm/ocaml/tactics/proofEngineHelpers.ml | 43 +++++++ helm/ocaml/tactics/proofEngineHelpers.mli | 8 ++ helm/ocaml/tactics/proofEngineTypes.ml | 3 + helm/ocaml/tactics/proofEngineTypes.mli | 8 ++ helm/ocaml/tactics/reductionTactics.ml | 122 +++++++++++--------- helm/ocaml/tactics/reductionTactics.mli | 16 +-- helm/ocaml/tactics/tactics.ml | 12 +- helm/ocaml/tactics/tactics.mli | 32 ++--- 13 files changed, 226 insertions(+), 116 deletions(-) diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 96822d8e8..f39ee677d 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -184,7 +184,7 @@ and injection1_tac ~term ~i = )) ~continuation: (T.then_ - ~start:(EqualityTactics.rewrite_simpl_tac ~term) + ~start:(EqualityTactics.rewrite_simpl_tac ~term ()) ~continuation:EqualityTactics.reflexivity_tac ) ]) @@ -316,7 +316,8 @@ let discriminate'_tac ~term = ~continuation: ( T.then_ - ~start:(EqualityTactics.rewrite_back_simpl_tac ~term) + ~start:(EqualityTactics.rewrite_back_simpl_tac + ~term ()) ~continuation:(IntroductionTactics.constructor_tac ~n:1) )) (proof',goal') diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 52ea4054d..e1a4c6849 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -22,11 +22,14 @@ * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) + -let rewrite ~term:equality ?(direction=`Left) (proof,goal) = +let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) = let module C = Cic in let module U = UriManager in let module PET = ProofEngineTypes in + let module PER = ProofEngineReduction in + let module PEH = ProofEngineHelpers in let module PT = PrimitiveTactics in let module HLO = HelmLibraryObjects in let if_left a b = @@ -53,10 +56,36 @@ let rewrite ~term:equality ?(direction=`Left) (proof,goal) = (* now we always do as if direction was `Left *) let gty' = CicSubstitution.lift 1 gty in let t1' = CicSubstitution.lift 1 t1 in + let eq_kind, what = + match where with + | None + | Some ([], None) -> + PER.alpha_equivalence, [t1'] + | Some (hp_paths, goal_path) -> + assert (hp_paths = []); + match goal_path with + | None -> assert false (* (==), [t1'] *) + | Some path -> + let roots = CicUtil.select ~term:gty' ~context:path in + let subterms = + List.fold_left ( + fun acc (i, r) -> + let wanted = CicSubstitution.lift i t1' in + PEH.find_subterms ~eq:PER.alpha_equivalence ~wanted r @ acc + ) [] roots + in + (==), subterms + in + let with_what = + let rec aux = function + | 0 -> [] + | n -> C.Rel 1 :: aux (n-1) + in + aux (List.length what) + in let gty'' = ProofEngineReduction.replace_lifting - ~equality:ProofEngineReduction.alpha_equivalence - ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty' + ~equality:eq_kind ~what ~with_what ~where:gty' in let gty_red = CicSubstitution.subst t2 gty'' in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in @@ -78,37 +107,37 @@ let rewrite ~term:equality ?(direction=`Left) (proof,goal) = (proof',[fresh_meta]) -let rewrite_tac ~term = - let rewrite_tac ~term status = - rewrite ~term ~direction:`Right status +let rewrite_tac ?where ~term () = + let rewrite_tac ?where ~term status = + rewrite ?where ~term ~direction:`Right status in - ProofEngineTypes.mk_tactic (rewrite_tac ~term) + ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term) -let rewrite_simpl_tac ~term = - let rewrite_simpl_tac ~term status = +let rewrite_simpl_tac ?where ~term () = + let rewrite_simpl_tac ?where ~term status = ProofEngineTypes.apply_tactic (Tacticals.then_ - ~start:(rewrite_tac ~term) + ~start:(rewrite_tac ?where ~term ()) ~continuation: - (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)) + (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern)) status in ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term) ;; -let rewrite_back_tac ~term = - let rewrite_back_tac ~term status = - rewrite ~term ~direction:`Left status +let rewrite_back_tac ?where ~term () = + let rewrite_back_tac ?where ~term status = + rewrite ?where ~term ~direction:`Left status in - ProofEngineTypes.mk_tactic (rewrite_back_tac ~term) + ProofEngineTypes.mk_tactic (rewrite_back_tac ?where ~term) -let rewrite_back_simpl_tac ~term = - let rewrite_back_simpl_tac ~term status = +let rewrite_back_simpl_tac ?where ~term () = + let rewrite_back_simpl_tac ?where ~term status = ProofEngineTypes.apply_tactic (Tacticals.then_ - ~start:(rewrite_back_tac ~term) + ~start:(rewrite_back_tac ?where ~term ()) ~continuation: - (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)) + (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern)) status in ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term) @@ -139,7 +168,7 @@ let replace_tac ~what ~with_what = with_what])) ~continuations:[ - T.then_ ~start:(rewrite_simpl_tac ~term:(C.Rel 1)) + T.then_ ~start:(rewrite_simpl_tac ~term:(C.Rel 1) ()) ~continuation:( ProofEngineStructuralRules.clear ~hyp:(List.hd context)) ; diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli index 7d57a0c11..698b34e9c 100644 --- a/helm/ocaml/tactics/equalityTactics.mli +++ b/helm/ocaml/tactics/equalityTactics.mli @@ -23,11 +23,21 @@ * 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 rewrite_tac: + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic +val rewrite_simpl_tac: + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic +val rewrite_back_tac: + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic +val rewrite_back_simpl_tac: + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic + +val replace_tac: + what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic val reflexivity_tac: ProofEngineTypes.tactic val symmetry_tac: ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 3556a85f2..2ee088edb 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -885,7 +885,7 @@ let equality_replace a b = let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); let (proof,goals) = apply_tactic - (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))) + (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ()) ((curi,metasenv',pbo,pty),goal) in let new_goals = fresh_meta::goals in diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index c155d81cc..2f1d7be47 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -586,7 +586,7 @@ let elim_intros_simpl_tac ~term = (Tacticals.thens ~start:(intros_tac ()) ~continuations: - [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None]) + [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern]) ;; exception NotConvertible diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index d78b94afa..c1f4ebc3c 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -107,3 +107,46 @@ let compare_metasenvs ~oldmetasenv ~newmetasenv = (function (i,_,_) -> not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv) ;; + +(** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *) +let find_subterms ~eq ~wanted t = + let rec find wanted t = + if eq wanted t then + [t] + else + match t with + | Cic.Sort _ + | Cic.Rel _ -> [] + | Cic.Meta (_, ctx) -> + List.fold_left ( + fun acc e -> + match e with + | None -> acc + | Some t -> find wanted t @ acc + ) [] ctx + | Cic.Lambda (_, t1, t2) + | Cic.Prod (_, t1, t2) + | Cic.LetIn (_, t1, t2) -> + find wanted t1 @ find (CicSubstitution.lift 1 wanted) t2 + | Cic.Appl l -> + List.fold_left (fun acc t -> find wanted t @ acc) [] l + | Cic.Cast (t, ty) -> find wanted t @ find wanted ty + | Cic.Implicit _ -> assert false + | Cic.Const (_, esubst) + | Cic.Var (_, esubst) + | Cic.MutInd (_, _, esubst) + | Cic.MutConstruct (_, _, _, esubst) -> + List.fold_left (fun acc (_, t) -> find wanted t @ acc) [] esubst + | Cic.MutCase (_, _, outty, indterm, patterns) -> + find wanted outty @ find wanted indterm @ + List.fold_left (fun acc p -> find wanted p @ acc) [] patterns + | Cic.Fix (_, funl) -> + List.fold_left ( + fun acc (_, _, ty, bo) -> find wanted ty @ find wanted bo @ acc + ) [] funl + | Cic.CoFix (_, funl) -> + List.fold_left ( + fun acc (_, ty, bo) -> find wanted ty @ find wanted bo @ acc + ) [] funl + in + find wanted t diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index b0e390940..5cf58999c 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -40,3 +40,11 @@ val subst_meta_and_metasenv_in_proof : oldmetasenv *) val compare_metasenvs : oldmetasenv:Cic.metasenv -> newmetasenv:Cic.metasenv -> int list + +(** Finds the _pointers_ to subterms that are alpha-equivalent to wanted in t. + * wanted is properly lifted when binders are crossed *) +val find_subterms : + eq:(Cic.term -> Cic.term -> bool) -> + wanted:Cic.term -> Cic.term -> + Cic.term list + diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index e90e43807..7d1a53d73 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -56,6 +56,9 @@ type tactic = status -> proof * goal list (** creates an opaque tactic from a status->proof*goal list function *) let mk_tactic t = t +type pattern = (string * Cic.term) list * Cic.term option +let goal_pattern = [],None + (** tactic failure *) exception Fail of string diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli index af5daf5dc..6d2bae11e 100644 --- a/helm/ocaml/tactics/proofEngineTypes.mli +++ b/helm/ocaml/tactics/proofEngineTypes.mli @@ -44,6 +44,14 @@ val initial_status: Cic.term -> Cic.metasenv -> status type tactic val mk_tactic: (status -> proof * goal list) -> tactic +(** the type of a tactic application domain + * [ hypothesis_name * path ] * goal_path + *) +type pattern = (string * Cic.term) list * Cic.term option + +(** the pattern for the whole goal *) +val goal_pattern : pattern + (** tactic failure *) exception Fail of string diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index d3d36ca6e..975333fa9 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -42,70 +42,86 @@ let reduction_tac ~reduction (proof,goal) = *) (* The default of term is the thesis of the goal to be prooved *) -let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let terms = - match terms with None -> [ty] | Some l -> l - in +let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in (* We don't know if [term] is a subterm of [ty] or a subterm of *) (* the type of one metavariable. So we replace it everywhere. *) (*CSC: Il vero problema e' che non sapendo dove sia il term non *) (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) (*CSC: e' meglio prima cercare il termine e scoprirne il *) (*CSC: contesto, poi ridurre e infine rimpiazzare. *) - let replace context where= -(*CSC: Per il momento se la riduzione fallisce significa solamente che *) -(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) -(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) - try - let terms' = List.map (reduction context) terms in - ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' - ~where:where - with - _ -> where - in - let ty' = replace context ty in - let context' = - if also_in_hypotheses then - List.fold_right - (fun entry context -> - match entry with - Some (name,Cic.Def (t,None)) -> - (Some (name,Cic.Def ((replace context t),None)))::context - | Some (name,Cic.Decl t) -> - (Some (name,Cic.Decl (replace context t)))::context - | None -> None::context - | Some (_,Cic.Def (_,Some _)) -> assert false - ) context [] - else - context - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [metano] + let replace context where terms = + (*CSC: Per il momento se la riduzione fallisce significa solamente che *) + (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) + (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) + try + let terms' = List.map (reduction context) terms in + ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' + ~where:where + with + _ -> where + in + let find_pattern_for name = + try Some (snd(List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) + with Not_found -> None + in + let ty' = + match goal_pattern with + | None -> replace context ty [ty] + | Some pat -> + let terms = CicUtil.select ~term:ty ~context:pat in + let terms = List.map snd terms in + replace context ty terms + in + let context' = + if hyp_patterns <> [] then + List.fold_right + (fun entry context -> + match entry with + | Some (name,Cic.Decl term) -> + (match find_pattern_for name with + | None -> entry::context + | Some pat -> + let terms = CicUtil.select ~term ~context:pat in + let terms = List.map snd terms in + let where = replace context term terms in + let entry = Some (name,Cic.Decl where) in + entry::context) + | Some (name,Cic.Def (term, None)) -> + (match find_pattern_for name with + | None -> entry::context + | Some pat -> + let terms = CicUtil.select ~term ~context:pat in + let terms = List.map snd terms in + let where = replace context term terms in + let entry = Some (name,Cic.Def (where,None)) in + entry::context) + | _ -> entry::context + ) context [] + else + context + in + let metasenv' = + List.map (function + | (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [metano] ;; -let simpl_tac ~also_in_hypotheses ~terms = - mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.simpl - ~also_in_hypotheses ~terms);; +let simpl_tac ~pattern = + mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);; -let reduce_tac ~also_in_hypotheses ~terms = - mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.reduce - ~also_in_hypotheses ~terms);; +let reduce_tac ~pattern = + mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);; -let whd_tac ~also_in_hypotheses ~terms = - mk_tactic ( reduction_tac ~reduction:CicReduction.whd - ~also_in_hypotheses ~terms);; +let whd_tac ~pattern = + mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);; -let normalize_tac ~also_in_hypotheses ~terms = - mk_tactic ( reduction_tac ~reduction:CicReduction.normalize - ~also_in_hypotheses ~terms);; +let normalize_tac ~pattern = + mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );; let fold_tac ~reduction ~also_in_hypotheses ~term = let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) = diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index e1b3f9107..bb4ca3c70 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -24,18 +24,10 @@ *) (* The default of term is the thesis of the goal to be prooved *) -val simpl_tac: - also_in_hypotheses:bool -> terms:(Cic.term list option) -> - ProofEngineTypes.tactic -val reduce_tac: - also_in_hypotheses:bool -> terms:(Cic.term list option) -> - ProofEngineTypes.tactic -val whd_tac: - also_in_hypotheses:bool -> terms:(Cic.term list option) -> - ProofEngineTypes.tactic -val normalize_tac: - also_in_hypotheses:bool -> terms:(Cic.term list option) -> - ProofEngineTypes.tactic +val simpl_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val fold_tac: reduction:(Cic.context -> Cic.term -> Cic.term) -> diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml index 5bbb01645..60c60c7ff 100644 --- a/helm/ocaml/tactics/tactics.ml +++ b/helm/ocaml/tactics/tactics.ml @@ -36,33 +36,33 @@ let cut = PrimitiveTactics.cut_tac let decide_equality = DiscriminationTactics.decide_equality_tac let decompose = EliminationTactics.decompose_tac let discriminate = DiscriminationTactics.discriminate_tac -let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac let elim_intros = PrimitiveTactics.elim_intros_tac +let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac let elim_type = EliminationTactics.elim_type_tac let exact = PrimitiveTactics.exact_tac let exists = IntroductionTactics.exists_tac let fold = ReductionTactics.fold_tac let fourier = FourierR.fourier_tac +let fwd_simpl = FwdSimplTactic.fwd_simpl_tac let generalize = VariousTactics.generalize_tac -let set_goal = VariousTactics.set_goal let injection = DiscriminationTactics.injection_tac let intros = PrimitiveTactics.intros_tac +let lapply = FwdSimplTactic.lapply_tac let left = IntroductionTactics.left_tac let letin = PrimitiveTactics.letin_tac +let normalize = ReductionTactics.normalize_tac let reduce = ReductionTactics.reduce_tac let reflexivity = EqualityTactics.reflexivity_tac let replace = EqualityTactics.replace_tac +let rewrite = EqualityTactics.rewrite_tac let rewrite_back = EqualityTactics.rewrite_back_tac let rewrite_back_simpl = EqualityTactics.rewrite_back_simpl_tac -let rewrite = EqualityTactics.rewrite_tac let rewrite_simpl = EqualityTactics.rewrite_simpl_tac let right = IntroductionTactics.right_tac let ring = Ring.ring_tac +let set_goal = VariousTactics.set_goal let simpl = ReductionTactics.simpl_tac let split = IntroductionTactics.split_tac let symmetry = EqualityTactics.symmetry_tac let transitivity = EqualityTactics.transitivity_tac let whd = ReductionTactics.whd_tac -let normalize = ReductionTactics.normalize_tac -let fwd_simpl = FwdSimplTactic.fwd_simpl_tac -let lapply = FwdSimplTactic.lapply_tac diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 8938b99f3..5eb66704f 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -45,29 +45,29 @@ val left : ProofEngineTypes.tactic val letin : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> ProofEngineTypes.tactic -val reduce : - also_in_hypotheses:bool -> - terms:Cic.term list option -> ProofEngineTypes.tactic +val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic val replace : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic -val rewrite_back : term:Cic.term -> ProofEngineTypes.tactic -val rewrite_back_simpl : term:Cic.term -> ProofEngineTypes.tactic -val rewrite : term:Cic.term -> ProofEngineTypes.tactic -val rewrite_simpl : term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back : + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic +val rewrite_back_simpl : + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic +val rewrite : + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic +val rewrite_simpl : + ?where:ProofEngineTypes.pattern -> + term:Cic.term -> unit -> ProofEngineTypes.tactic val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic -val simpl : - also_in_hypotheses:bool -> - terms:Cic.term list option -> ProofEngineTypes.tactic +val simpl : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic -val whd : - also_in_hypotheses:bool -> - terms:Cic.term list option -> ProofEngineTypes.tactic -val normalize : - also_in_hypotheses:bool -> - terms:Cic.term list option -> ProofEngineTypes.tactic +val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val normalize : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val fwd_simpl : hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic val lapply : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> -- 2.39.2