Andrea Vezzosi (Jan 08 2024 at 09:48): Andrea Vezzosi (Jan 08 2024 at 09:48):A lot of proof methods like auto and simp have a corresponding tactic, but is there a way to generally get a tactic from an input proof method? e.g. one defined with Eisbach method command.
Alteranatively, is there something like Goal.prove that accepts a method instead of a tactic?
Hanno Becker (May 02 2024 at 04:37):Very late reply, but just in case it still matters...:
You cannot do this without loosing information, because a method can change the proof context, while a tactic cannot. If that is not a concern for you, you can convert a method into a context-tactic (i.e. Proof.context -> tactic) using Context_Tactic.NO_CONTEXT_TACTIC
Hanno Becker (May 02 2024 at 04:39): fun method_to_context_tactic (m : Method.method) (ctxt : Proof.context) : tactic =
Context_Tactic.NO_CONTEXT_TACTIC ctxt (m [])
(And if you have an Eisbach method text, you can evaluate it to get a Method.method using Method.evaluate)
Andrea Vezzosi (May 02 2024 at 08:58):Thanks! Should still be useful!
Last updated: May 04 2024 at 20:16 UTC