在acl2中给出最小列表的证明函数

Question

我需要试着展示一个找到最小列表的函数，我感觉我就快得到它了，但实际上却无法得到它。

讲师为我们提供了以下功能：

(defun minlist (l)
  (if (<= (len l) 1)
    (first l)
    (if (<= (first l) (minlist (rest l)))
      (first l)
      (minlist (rest l)))))

然后说

;;; TODO: Write a little theory that verifies that the minlist of a list is 
;;; less than or equal to any element of the list
;;; Hint: Use this declaration to generate a non-empty list
;;;  (n :value (random-between 1 10)
;;;   l :value (random-natural-list-of-length n))    

然后我就这么做了：

(defproperty-program minlist-<=-member (n)
    (if ((n :value (random-between 1 10) 
          l :value (random-natural-list-of-length n)))
          (<= (min-list l) (first l))
          (nil)))

在Proof Pad中，它给了我一个错误，我无法找出我做错了什么。

错误是：

HARD ACL2错误:缺少:N的值参数

顶级中的ACL2错误:在尝试宏展开表单时

(EXPAND-VARS (N)
             (IF ((N :VALUE (RANDOM-BETWEEN 1 10)
                     L
                     :VALUE (RANDOM-NATURAL-LIST-OF-LENGTH N)))
                 (<= (MIN-LIST L) (FIRST L))
                 (NIL))),

对宏主体的求值导致以下错误：

评估已中止。要进行调试，请参阅:DOC print-gv，请参阅:DOC trace，并请参阅:DOC wet。

Answer 1

如果这篇文章来得太晚，我很抱歉。

所以我发现你的defproperty有一些“结构”问题，一个是你调用了min-list (<= (MIN-LIST L)，但是定义的函数是不带破折号的minlist。另外，(n :value (random-between 1 10) l :value (random-natural-list-of-length n))部分

构造要使用的列表，并且根本不应该在if语句中。它应该在它上面。此外，该语句声明了n值，并且您不需要已有的(n)。在这些更改之后，您最终会得到

   (defproperty-program minlist-<=-member
(n :value (random-between 1 10) 
          l :value (random-natural-list-of-length n))
    (if (<= (minlist l) (first l))
          (nil)))

但这会使if语句没有足够的参数。此外，您拥有的语句'(<= (minlist l) (first l))‘只检查列表的第一个元素是否小于或等于minlist元素。这并不能证明它比其他可能存在的元素更小。

我希望这能帮到你。