;; P01 (*) Find the last box of a list.
(defun my-last (x)
  (declare (xargs :guard (and (true-listp x)
                              (consp x))))
  (if (endp (cdr x))
      x
      (my-last (cdr x))))

(defthm theorem-of-my-last
  (implies (and (true-listp x)
                (consp x))
           (equal (list (nth (1- (len x)) x))
                  (my-last x))))

;; P02 (*) Find the last but one box of a list.
(defun my-butlast (x)
  (declare (xargs :guard (and (true-listp x)
                              (consp x))))
  (if (endp (cdr x))
      nil
      (cons (car x)
            (my-butlast (cdr x)))))

(defthm my-butlast-my-last
  (implies (and (true-listp x)
                (consp x))
           (equal (append (my-butlast x) (my-last x))
                  x)))

;; P03 (*) Find the K'th element of a list.
(defun element-at (x i)
  (declare (xargs :guard (and (true-listp x)
                              (natp i)
                              (< i (len x)))))
  (if (zp i)
      (car x)
      (element-at (cdr x) (1- i))))

(defthm element-at-nil
  (equal (element-at nil i)
         nil))

(defthm elment-at-equal-nth
  (equal (element-at x i)
         (nth i x)))

;; P04 (*) Find the number of elements of a list.
(defun my-len (x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      0
      (+ 1 (my-len (cdr x)))))

(defun rev-iota (n)
  (if (zp n)
      nil
      (cons (1- n) (rev-iota (1- n)))))

(defthm my-len-rev-iota
  (implies (natp n)
           (equal (my-len (rev-iota n))
                  n)))

;; P05 (*) Reverse a list.
(defun app (x y)
  (declare (xargs :guard (and (true-listp x)
                              (true-listp y))))
  (if (endp x)
      y
      (cons (car x)
            (app (cdr x) y))))

(defthm true-listp-app
  (implies (true-listp y)
           (true-listp (app x y))))

(defun rev (x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      nil
      (app (rev (cdr x))
           (list (car x)))))

(defun revapp (x y)
  (declare (xargs :guard (and (true-listp x)
                              (true-listp y))))
  (if (endp x)
      y
      (revapp (cdr x)
              (cons (car x) y))))

(defmacro my-reverse (x)
  `(revapp ,x nil))

(defthm associativity-of-app
  (equal (app (app x y) z)
         (app x (app y z))))

(defthm app-rev-equal-revapp
  (equal (revapp x y)
         (app (rev x) y)))

(defthm my-reverse-equal-rev
  (equal (my-reverse x)
         (rev x)))

;; P06 (*) Find out whether a list is a palindrome.
(defmacro palindromep (x)
  `(equal (my-reverse ,x) ,x))

(defthm app-nil
  (implies (true-listp x)
           (equal (app x nil)
                  x)))

(defthm true-listp-rev
  (implies (true-listp x)
           (true-listp (rev x))))

(defthm rev-app
  (implies (true-listp y)
           (equal (rev (app x y))
                  (app (rev y) (rev x)))))

(defthm rev-rev
  (implies (true-listp x)
           (equal (rev (rev x))
                  x)))

(defthm sandwich-palindrome
  (implies (and (true-listp y)
                (palindromep x))
           (palindromep (app y (app x (rev y))))))

;; P07 (**) Flatten a nested list structure.
(defun flatten (x)
  (cond
    ((endp x) x)
    ((consp (car x))
     (app (flatten (car x))
          (flatten (cdr x))))
    (t (cons (car x)
             (flatten (cdr x))))))