ACL2中:explain-near-miss针对重写定理执行失败的原因排查

使用ACL2的:explain-near-miss命令排查被拒绝应用的引理时，触发规则类不兼容报错，但涉事引理problem-41属于:rewrite规则类，符合该命令的前提条件。

具体场景：引理problem-41无法应用于表达式(app (rev b) nil)，原因是证明器无法推导(rev x)是proper的——而能证明该事实的引理problem-44b被故意禁用。预期:explain-near-miss会提示这一依赖缺失，但实际报错。

相关定义与定理代码 #

(defun app (x y) (if (consp x) (cons (car x) (app (cdr x) y)) y))
(defun rev (l) (if (consp l) (app (rev (cdr l)) (list (car l))) l))
(defun proper (x) (if (consp x) (proper (cdr x)) (equal x nil)))

(defthm problem-41 (implies (proper x) (equal (app x nil) x)))
(defthm problem-44b (implies (proper x) (proper (rev x))))

(thm 
    (implies (and (proper a) (proper b))
             (equal (rev (app a b))
                    (app (rev b) (rev a))))
  :hints (("Goal"
           :in-theory (disable problem-44b))))

操作步骤与报错信息 #

ACL2 !>(ld "./f.lisp")
...
ACL2 !>:monitor problem-41 t
((:REWRITE PROBLEM-41) (:CONDITION QUOTE T))
ACL2 !>:brr t
...
ACL2 !>(ld "./f.lisp")
...
Subgoal *1/3
(1 Breaking (:REWRITE PROBLEM-41) on (APP (REV B) 'NIL):
1 ACL2 >:explain-near-miss
ACL2 Error in EXPLAIN-NEAR-MISS: Explain-near-miss is meant to be
invoked when (brr@ :lemma) is a lemma of rule-class :rewrite, :linear,
or :rewrite-quoted-constant and the current value of (brr@ :lemma)
is none of these.

brr检查结果 #

1 ACL2 > (brr@ :lemma)
(REWRITE-RULE (:REWRITE PROBLEM-41)
5619 ((PROPER X))
EQUAL (APP X 'NIL)
X BACKCHAIN NIL NIL T)

1 ACL2 >(@ acl2-version)
"ACL2 Version 8.6"

内容的提问来源于stack exchange，提问作者Daniil Iaitskov