From d973652d95b95537f424dfa2b02323a19bb12150 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 24 Jul 2021 16:09:16 +0900
Subject: L-99: Solve P11 and P12 problems.

---
 L-99.lisp | 78 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)

(limited to 'L-99.lisp')

diff --git a/L-99.lisp b/L-99.lisp
index efd9e15..c7e1bb8 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -269,3 +269,81 @@
   (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)))
-- 
cgit v1.2.3