1 files changed, 114 insertions, 0 deletions
diff --git a/L-99.lisp b/L-99.lisp
index 3bfaa94..a4e5a59 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -141,3 +141,117 @@
           (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 prev n))))
+    ((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))
+
+