(in-package "ACL2")

;; 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)
                              (posp i)
                              (< (1- i) (len x)))))
  (if (zp (1- i))
      (car x)
      (element-at (cdr x) (1- i))))

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

(defthm elment-at-equal-nth
  (implies (posp i)
           (equal (element-at x i)
                  (nth (1- 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)
  (if (endp x)
      nil
      (cons (list (len (car x)) (caar x))
            (encode-1 (cdr x)))))

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

;; P11 (*) Modified run-length encoding.
(defun encode-modified-1 (x)
  (cond
    ((endp x) nil)
    ((equal (caar x) 1)
     (cons (cadar x)
           (encode-modified-1 (cdr x))))
    (t
     (cons (car x)
           (encode-modified-1 (cdr x))))))

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

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

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

(defthm car-repeat
  (equal (car (repeat x n))
         (if (zp n)
             nil
             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 repeat-1-list
  (equal (repeat y 1) (list y))
  :hints (("Goal" :expand ((repeat y 1)))))


(defthm decode-encode-1-pack-1-lemma-1
  (implies (and (consp y)
                (true-listp x)
                (true-listp y)
                (consp y)
                (seqp y))
           (equal (decode (encode-1 (pack-1 x y)))
                  (cons (car y) (decode (encode-1 (pack-1 x (cdr y))))))))

(defthm decode-encode-1
  (implies (and (true-listp x)
                (true-listp y)
                (seqp y))
           (equal (decode (encode-1 (pack-1 x y)))
                  (app y x))))

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

(defthm decode-encode-modified-1-lemma-1
  (implies (and (atom-listp x)
                (atom-listp y)
                (consp y)
                (seqp y))
           (equal (decode (encode-modified-1 (encode-1 (pack-1 x y))))
                  (cons (car y)
                        (decode (encode-modified-1 (encode-1 (pack-1 x (cdr
                                                                        y)))))))))

(defthm decode-encode-modified-1
  (implies (and (atom-listp x)
                (atom-listp y)
                (seqp y))
           (equal (decode (encode-modified-1 (encode-1 (pack-1 x y))))
                  (app y x))))

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

;; P13 (**) Run-length encoding of a list (direct solution).
(defun encode-direct-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-direct-1 (cdr x) (car x) (1+ n)))
    ((equal n 1)
     (cons prev (encode-direct-1 (cdr x) (car x) 1)))
    (t  (cons (list n prev)
              (encode-direct-1 (cdr x) (car x) 1)))))

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

(defthm app-repeat-1
  (implies (and (natp n)
                (consp x))
           (equal (app (repeat (car x) n) x)
                  (cons (car x)
                        (app (repeat (car x) n) (cdr x))))))

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

(defthm decode-encode-direct
  (implies (atom-listp x)
           (equal (decode (encode-direct x))
                  x)))

(defthm not-zp-car-repeat
  (implies (not (zp n))
           (equal (car (repeat sym n)) sym)))

(defthm consp-repeat
  (implies (posp n)
           (consp (repeat x n))))

(defthm encode-direct-equal-encode-modified-1
  (implies (and (atom-listp x)
                (atom sym)
                (natp n))
           (equal (encode-direct-1 x sym n)
                  (encode-modified-1 (encode-1 (pack-1 x (repeat sym n)))))))

(defthm encode-direct-equal-encode-modified
  (implies (atom-listp x)
           (equal (encode-direct x)
                  (encode-modified x))))

;; P14 (*) Duplicate the elements of a list.
(defun dupli (x)
  (if (endp x)
      nil
      (cons (car x)
            (cons (car x)
                  (dupli (cdr x))))))

(defthm len-dupli
  (equal (len (dupli x))
         (* 2 (len x))))

;; P15 (**) Replicate the elements of a list a given number of times.
(defun repli (x n)
  (if (endp x)
      nil
      (app (repeat (car x) n)
           (repli (cdr x) n))))

(defthm repli-2-equal-dupli
  (equal (repli x 2)
         (dupli x)))

(defthm len-repli
  (implies (natp n)
           (equal (len (repli x n))
                  (* n (len x)))))

;; P16 (**) Drop every N'th element from a list.
(defun drop-1 (x n i)
  (cond
    ((endp x) nil)
    ((zp (- i 1))
     (drop-1 (cdr x) n n))
    (t (cons (car x)
             (drop-1 (cdr x)
                     n
                     (1- i))))))

(defmacro drop (x n)
  `(drop-1 ,x ,n ,n))

;; P17 (*) Split a list into two parts; the length of the first part is given.
(defun split-1 (x n acc)
  (if (or (zp n) (endp x))
      (list (rev acc) x)
      (split-1 (cdr x)
               (1- n)
               (cons (car x) acc))))

(defthm cadr-split-1-equal-nthcdr
  (implies (and (natp n)
                (< n (len x)))
           (equal (cadr (split-1 x n acc))
                  (nthcdr n x))))

(defthm car-split-1-equal-take
  (implies (and (natp n)
                (< n (len x))
                (true-listp acc))
           (equal (car (split-1 x n acc))
                  (revapp acc (take n x)))))

(defmacro split (x n)
  `(split-1 ,x ,n nil))

(defthm car-split-equal-take
  (implies (and (natp n)
                (< n (len x)))
           (equal (car (split x n))
                  (take n x))))

(defthm cadr-split-equal-nthcdr
  (implies (and (natp n)
                (< n (len x)))
           (equal (cadr (split x n))
                  (nthcdr n x))))

(defthm split-1-car+cadr
  (equal (split-1 x n acc)
         (list (car (split-1 x n acc))
               (cadr (split-1 x n acc)))))
(in-theory (disable split-1-car+cadr))

(defun split/easy (x n)
  (list (take n x) (nthcdr n x)))

(defthm split-1-equal-split-easy
  (implies (and (true-listp x)
                (natp n)
                (< n (len x)))
           (equal (split-1 x n nil)
                  (split/easy x n)))
  :hints (("Goal" :do-not-induct t
                  :use ((:instance split-1-car+cadr
                                   (x x)
                                   (n n)
                                   (acc nil))))))
(in-theory (disable split-1))

;; P18 (**) Extract a slice from a list.
(defun slice (x i k)
  (take (1+ (- k i)) (nthcdr (1- i) x)))

;; P19 (**) Rotate a list N places to the left.
(defun rotate (x n)
  (let ((splited (split x (if (natp n)
                              n
                              (+ (len x) n)))))
    (app (cadr splited) (car splited))))

(defthm subsetp-take
  (implies (and (true-listp x)
                (natp n)
                (< n (len x)))
           (subsetp (take n x) x)))

(defthm subsetp-reflexive-lemma
  (implies (subsetp x (cdr y))
           (subsetp x y)))

(defthm subsetp-reflexive
  (subsetp x x))

(defthm subsetp-nthcdr
  (implies (true-listp x)
           (subsetp (nthcdr n x) x)))

(defthm subsetp-rotate-left
  (implies (and (true-listp x)
                (natp n)
                (< n (len x)))
           (subsetp (rotate x n) x)))

(defthm member-app
  (iff (member e (app a b))
       (or (member e a)
           (member e b))))

(defthm subsetp-app-commutative
  (equal (subsetp x (app a b))
         (subsetp x (app b a))))

(defthm subsetp-rotate-right
  (implies (and (true-listp x)
                (natp n)
                (< n (len x)))
           (subsetp x (rotate x n))))

;; P20 (*) Remove the K'th element from a list.
(defun remove-at (x n)
  (cond
    ((endp x) nil)
    ((zp (1- n)) (cdr x))
    (t (cons (car x)
             (remove-at (cdr x) (1- n))))))

(defun count/list (e x)
  (cond ((endp x) 0)
        ((equal (car x) e) (+ 1 (count/list e (cdr x))))
        (t (count/list e (cdr x)))))

(defthm count-to-count/list
 (implies (consp x)
          (equal (count e x) (count/list e x))))

(defthm posp-len-implies-consp
  (implies (posp (len x))
           (consp x)))

(defthm len-remove-at
  (implies (and (posp i)
                (<= i (len x)))
           (equal (len (remove-at x i))
                  (- (len x) 1))))

(defthm not-member-element-at-remove-at-implies-only-one
  (implies (and (posp i)
                (<= i (len x))
                (not (member (element-at x i) (remove-at x i))))
           (equal (count (element-at x i) x) 1)))