如何修复重写证明中的循环

Question

我正在尝试在 ACL2 中用一元符号（O、(S O)、(S (S O))、...）对自然数建模并证明加法的交换性。这是我的尝试：

; a NATURAL is 'O or a list ('S n') where n' is a NATURAL
(defun naturalp (n)
  (cond ((equal n 'O) t)
        (t (and (true-listp n)
                (equal (length n) 2)
                (equal (first n) 'S)
                (naturalp (second n))))))

(defun pred (n)
  (cond ((equal n 'O) 'O)
        ((naturalp n) (second n))))

(defun succ (n)
  (list 'S n))

(defun plus (n m)
  (cond ((equal n 'O) m)
        ((naturalp n) (succ (plus (pred n) m)))))

; FIXME: cannot prove this because rewriting loops...
(defthm plus_comm                                 
  (implies (and (naturalp n) (naturalp m))
           (iff (equal (plus n m) (plus m n)) t)))

这可能不是最 LISPy 的方式，我已经习惯了带有模式匹配的语言。

我的问题正如评论所暗示的那样：证明者循环，试图证明同一事物的嵌套越来越深的版本。我该如何阻止呢？该手册确实简要提到了循环重写规则，但没有说明如何处理它们。

我的预期是这个证明会失败，给我提示需要什么辅助引理来完成它。我可以使用循环证明的输出来找出可能停止循环的引理吗？

Answer 1

ACL2 最终可能会进入不同类型的循环。一种常见的类型是重写器循环，这通常非常明显。例如，以下内容：

(defun f (x) x)
(defun g (x) x)
(defthm f-is-g (implies (consp x) (equal (f x) (g x))))
(defthm g-is-f (implies (consp x) (equal (g x) (f x))))
(in-theory (disable f g))
(defthm loop (equal (f (cons a b)) (cons a b)))

引发重写循环，并提供信息性调试消息：

HARD ACL2 ERROR in REWRITE:  The call depth limit of 1000 has been
exceeded in the ACL2 rewriter.  To see why the limit was exceeded,
first execute
  :brr t
and then try the proof again, and then execute the form (cw-gstack)
or, for less verbose output, instead try (cw-gstack :frames 30).  You
will then probably notice a loop caused by some set of enabled rules,
some of which you can then disable; see :DOC disable.  Also see :DOC
rewrite-stack-limit.

不幸的是，您的示例进入了另一种循环。特别是，看起来 ACL2 正在进入循环

它归纳，但随后到达一个无法通过重写证明的子目标，所以
它归纳，但随后到达一个无法通过重写证明的子目标，所以
...

很难看出这是怎么回事。我所做的只是运行 (set-gag-mode nil) 在提交定理之前，然后检查中断证明程序后打印的输出。

避免这种情况的一种方法是给出提示，特别是您可以告诉 ACL2 不要像这样引入：

(defthm plus_comm
  (implies (and (naturalp n) (naturalp m))
           (iff (equal (plus n m) (plus m n)) t))
  :hints(("Goal" :do-not-induct t)))

但如果你这样做，它就会立即卡住，因为你可能真的想要归纳来证明这个定理。所以你真正想告诉它的是："induct once, but don't induct more than that." 语法有点傻：

(defthm plus_comm
  (implies (and (naturalp n) (naturalp m))
           (iff (equal (plus n m) (plus m n)) t))
  :hints(("Goal"
          :induct t          ;; Induct once.
          :do-not-induct t   ;; But don't induct more than once.
      )))

这应该会给您留下一个合理的检查点，然后您可以尝试通过添加重写规则或提供进一步的提示来进行调试。

祝你好运！

如何修复重写证明中的循环

How to fix loop in rewriting proof

acl2