什么时候‘in’战术在精益完成证明？

Question

我正在学习在自然数博弈中用精益证明定理，我很难理解rw策略的行为。

在不平等世界中的第1/17级中，我编写了以下代码：

use 1,
rw add_comm,

然后精益完成了证明。在这里，我没有使用refl战术。另一方面，在不平等世界中的第2/17级中，类似的代码

use 0,
rw add_zero,

不完整的证据。我怀疑以下代码会起作用：

use 0,
symmetry,
rw add_zero,

但是，这段代码仍然没有完成验证；在这些情况下，我需要使用refl策略。我该如何理解这些不同之处？

Answer 1

这很可能是NNG中的一个bug；普通精益中的rw策略总是在完成所有重写之后尝试(弱版本) refl，但是这种行为在NNG中被禁用了，因为它对教学不太好。然而，关闭这种行为并不容易，有时它会从裂缝中滑出来。