如何在 Isabelle 中调试无限 simpl 循环

Question

有没有一种很好的方法来打印简化器（例如，

apply clarsimp

）在进入无限循环时正在做什么？

Answer 1

using [[simp_trace]]

记录简化器正在做什么（非常难以阅读，但您只是在寻找在循环中应用哪些定理”。

示例

lemma "Q (f b) ⟹ b = f a ⟹ a = b ⟹ Q a"
  using [[simp_trace, simp_trace_depth_limit = 5]]
  apply simp
  done

快速浏览一下日志后，您可以看到日志始终循环应用

b = f a

和

b = a

。

即使 simp 不发散，它也能工作。

simp_trace_depth_limit 将 simp_trace 的效果限制在给定深度 递归简化器调用（当解决重写条件时 规则）。

--- https://www.isabelle.in.tum.de/website-Isabelle2024/dist/Isabelle2024/doc/isar-ref.pdf