Designing a Lisp Function (ACL2)

[VengefulToast]

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 :)

[VengefulToast]

(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!

[Hiroshe]

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

Your answer seems too complicated.

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.