用ACL2编写select()函数

Question

我试图用ACL2 (特别是ACL2s)编写一个函数，它接受一个列表和一个自然数，并在给定的索引处返回列表中的项。因此(选择(列表12，3) 2)将返回3。

这是我的代码：

;; select: List x Nat -> All
(defunc select (l n)
  :input-contract (and (listp l) (natp n))
  :output-contract t
  (if (equal 0 n)
    (first l)
    (select (rest l) (- n 1))))

我收到以下错误：

Query: Testing body contracts ... 

**Summary of Cgen/testing**
We tested 50 examples across 1 subgoals, of which 48 (48 unique) satisfied
the hypotheses, and found 1 counterexamples and 47 witnesses.

We falsified the conjecture. Here are counterexamples:
 [found in : "top"]
 -- ((L NIL) (N 0))

Test? found a counterexample.
Body contract falsified in: 
 -- (ACL2::EXTRA-INFO '(:GUARD (:BODY SELECT)) '(FIRST L))

任何帮助都是非常感谢的！

Answer 1

在我看来，这个信息非常清楚:您正在尝试获取一个空列表的第一个元素，这与您的规范相冲突。

基于本参考，first似乎需要一个非空列表，而car则在输入为nil时返回nil。

要么用nil测试来解释endp案例，要么使用car而不是first。