英文:
Trace tauto, finish
问题
有办法在Lean中追踪tauto、finish策略（或其他不适用于simp的策略）吗？
例如：
example (P Q : Prop) : a → b ↔ ¬a ∨ b := by tauto
我希望能够看到证明目标所应用的必要重写或定理，以便在更复杂的情况下可以明确使用它们。
英文:
Is there a way to trace tauto, finish tactics (or others that don't fall into simp) in Lean?
E.g.
example (P Q : Prop) : a → b ↔ ¬a ∨ b := by tauto
I'd like to see the neccesary rewritings or theorems that are applied to the terms to prove the goal, in order to use them explicitly in more complex situations.
答案1
得分: 2
import tactic
theorem foo (a b : Prop) : a → b ↔ ¬a ∨ b := by tauto!
#print foo
英文:
import tactic
theorem foo (a b : Prop) : a → b ↔ ¬a ∨ b := by tauto!
#print foo
shows you the term that the tactic created. But high-powered tactics are not designed to produce readable terms, so your mileage may vary.
答案2
得分: 0
有一个通用的 show_term { tauto }，它将打印一个显示由 tauto（或您使用的任何其他策略）构建的术语的消息。
正如Kevin在上面指出的，一些策略会产生难以理解和/或庞大的术语。
英文:
There is also the general purpose show_term { tauto } which will print a message showing the term that tauto (or whatever tactic you used) constructed.
As Kevin points out above, some tactics produce inscrutable and/or enormous terms.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论