在 acl2 中给出最少列表的证明函数答案

【问题标题】：Proving function that gives minimum of lists in acl2在 acl2 中给出最少列表的证明函数
【发布时间】：2017-10-16 16:18:36
【问题描述】：

我需要尝试展示一个可以找到列表最小值的函数，我觉得我快要得到它但实际上无法得到它。

导师给我们这个功能：

(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 缺少 :value 参数

TOP-LEVEL 中的 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 跟踪，以及请参阅：DOC 湿。

【问题讨论】：

为了帮助人们回答您的问题，您需要更具体地说明错误。请edit 您的帖子包含您从minimal reproducible example 获得的确切错误（最好使用复制+粘贴以避免转录错误）。
@TobySpeight 我已经添加了错误

标签： acl2

【解决方案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) 。在这些更改之后，您最终会得到 p>

   (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 语句没有足够的参数。另外，您的声明 '(

我希望这会有所帮助。

【讨论】：