path: root/L-99.lisp

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