Hello fellow forum members,

I am struggling to understand what I am supposed to be doing with ACL2.

So I am given these axioms that define a function called up, and I just need to translate these into ACL2.
-- axioms for predicate for increasing lists of numbers

``````(up nil) = T                                                     {up0}
(up (cons x nil)) = T                                            {up1}
(up (cons x1 (cons x2 xs))) = (and (<= x1 x2) (up (cons x2 xs))) {up2}
``````

Here is what I have... but it does not work.

``````(defun problem1up (xs)
(if (> (len xs) 1)
(problem1up (cons (first xs) (cons (second xs) xs)))
(if (> (len xs) 0)
(problem1up (cons (first xs) nil))
(problem1up nil))))
``````

Any help would be definitely appreciated. I just need a kick in the right direction.

Thank you :)

Disclaimer: I'm not familiar with the acl2 dialect.

Clearly, your base case is `(if (< (len xs) 2) #t ...)`. That is saying, if your list has 1 or 0 elements, return true (I'm not sure if it's #t in acl, but you get the …

## All 2 Replies

``````(defun problem1up (xs)                  ;<------- Problem 1
(if (>= (len xs) 2)
(up (cons (first xs) (cons (second xs) xs))) ; {up2}
(if (>= (len xs) 1)
(up (cons (first xs) nil))               ; {up1}
nil)))                                   ; {up0}
``````

This works in Proof Pad. Does this seem correct? Thanks!

Disclaimer: I'm not familiar with the acl2 dialect.

Clearly, your base case is `(if (< (len xs) 2) #t ...)`. That is saying, if your list has 1 or 0 elements, return true (I'm not sure if it's #t in acl, but you get the idea).
Now we need to REDUCE the problem, which is already given to you. `(and (<= (first xs) (second xs)) (up (rest xs)))`.
The idea is that the input is broken down at each call, until the problem is trivial. Notice that your `(up (cons (first xs) (cons (second xs) xs)))` and `(up (cons (first xs) nil))` is actually making the input GROW. Your adding the first and second element onto the list, never reaching the base case, and eating all of your memory.