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

(defthm flatten-flatten
  (equal (flatten (flatten x))
         (flatten x)))

(defthm flatten-app
  (equal (flatten (app x y))
         (app (flatten x)
              (flatten y))))

;; P08 (**) Eliminate consecutive duplicates of list elements.
(defun compress (x)
  (cond
    ((endp x) nil)
    ((endp (cdr x)) (list (car x)))
    ((equal (car x) (cadr x)) (compress (cdr x)))
    (t (cons (car x) (compress (cdr x))))))

(defthm car-compress
  (implies (consp x)
           (equal (car (compress x))
                  (car x))))

(defthm compress-compress
  (equal (compress (compress x))
         (compress x)))

;; P09 (**) Pack consecutive duplicates of list elements into sublists.
(defun pack-1 (x acc)
  (cond
    ((endp x)
     (if (endp acc)
         nil
         (list acc)))
    ((or (endp acc)
         (equal (car acc) (car x)))
     (pack-1 (cdr x) (cons (car x) acc)))
    (t (cons acc (pack-1 (cdr x) (list (car x)))))))

(defmacro pack (x)
  `(pack-1 ,x nil))

(defun collect-cars (x)
  (if (endp x)
      nil
      (cons (caar x)
            (collect-cars (cdr x)))))

(defthm collect-cars-pack-lemma-1
  (implies (endp (collect-cars (pack-1 x y)))
           (endp x)))

(defthm collect-cars-pack-lemma-2
  (implies (consp y)
           (equal (collect-cars (pack-1 nil y))
                  (list (car y)))))

(defun seqp (x)
  (cond
    ((endp x) t)
    ((endp (cdr x)) t)
    ((equal (car x) (cadr x))
     (seqp (cdr x)))
    (t nil)))

(defthm collect-cars-pack-1-lemma-1
  (implies (and (seqp y)
                (consp x)
                (consp y)
                (equal (car x) (car y)))
           (equal (collect-cars (pack-1 x y))
                  (collect-cars (pack-1 x (cdr y))))))

(defthm collect-cars-pack-1-lemma-2
  (implies (and (consp y)
                (endp (cdr y))
                (not (equal (car x) (car y))))
           (equal (collect-cars (pack-1 x y))
                  (cons (car y) (collect-cars (pack-1 x nil))))))

(defthm collect-cars-pack-1-lemma-3
  (implies (and (consp y)
                (consp (cdr y))
                (equal (car y) (cadr y)))
           (equal (collect-cars (pack-1 x y))
                  (collect-cars (pack-1 x (cdr y))))))

(defthm collect-cars-pack-1
  (implies (and (seqp y)
                (true-listp y))
           (equal (collect-cars (pack-1 x y))
                  (compress (app y x)))))

(defthm collect-cars-pack
  (equal (collect-cars (pack x))
         (compress x)))

;; P10 (*) Run-length encoding of a list.
(defun encode-1 (x prev n)
  (cond
    ((endp x)
     (if (zp n)
         nil
         (list (list n prev))))
    ((or (zp n)
         (equal (car x) prev))
     (encode-1 (cdr x) (car x) (1+ n)))
    (t (cons (list n prev)
             (encode-1 (cdr x) (car x) 1)))))

(defmacro encode (x)
  `(encode-1 ,x nil 0))

(defun sum-of-cars (x)
  (if (endp x)
      0
      (+ (caar x)
         (sum-of-cars (cdr x)))))

(defthm sum-of-cars-encode-1
  (implies (natp n)
           (equal (sum-of-cars (encode-1 x sym n))
                  (+ n (len x)))))

(defthm sum-of-cars-encode
  (equal (sum-of-cars (encode x))
         (len x)))

;; P11 (*) Modified run-length encoding.
(defun encode-modified-1 (x prev n)
  (cond
    ((endp x)
     (cond
       ((zp n) nil)
       ((equal n 1) (list prev))
       (t (list (list n prev)))))
    ((or (zp n)
         (equal (car x) prev))
     (encode-modified-1 (cdr x) (car x) (1+ n)))
    ((equal n 1)
     (cons prev (encode-modified-1 (cdr x) (car x) 1)))
    (t  (cons (list n prev)
              (encode-modified-1 (cdr x) (car x) 1)))))

(defmacro encode-modified (x)
  `(encode-modified-1 ,x nil 0))

;; P12 (**) Decode a run-length encoded list.
(defun repeat (x n)
  (if (zp n)
      nil
      (cons x (repeat x (1- n)))))

(defthm repeat-len
  (implies (natp n)
           (equal (len (repeat x n))
                  n)))

(defthm car-repeat
  (implies (posp n)
           (equal (car (repeat x n))
                  x))
  :hints (("Goal" :expand (REPEAT X 1))))

(defthm seqp-repeat
  (implies (natp n)
           (seqp (repeat x n)))
  :hints (("Goal" :expand (repeat x (+ -1 n)))))

(defun decode (x)
  (cond
    ((endp x) nil)
    ((atom (car x))
     (cons (car x)
           (decode (cdr x))))
    (t (app (repeat (cadar x) (caar x))
            (decode (cdr x))))))

(defthm app-repeat-lemma
  (implies (consp x)
           (equal (app (repeat (car x) n) x)
                  (cons (car x)
                        (app (repeat (car x) n) (cdr x))))))

(defthm decode-encode-1
  (implies (and (true-listp x)
                (natp n))
           (equal (decode (encode-1 x sym n))
                  (app (repeat sym n) x))))

(defthm decode-encode
  (implies (true-listp x)
           (equal (decode (encode x))
                  x)))

(defthm decode-encode-mofified-1
  (implies (and (atom-listp x)
                (atom sym)
                (natp n))
           (equal (decode (encode-modified-1 x sym n))
                  (app (repeat sym n) x))))

(defthm decode-encode-mofified
  (implies (atom-listp x)
           (equal (decode (encode-modified x))
                  x)))