From b729e723d88a3f07320f6c5a6527747f8f668870 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 25 Jul 2021 10:42:58 +0900
Subject: L-99: Fix P10-12 problems.

---
 L-99.lisp | 114 +++++++++++++++++++++++++++++++++-----------------------------
 1 file changed, 60 insertions(+), 54 deletions(-)

diff --git a/L-99.lisp b/L-99.lisp
index c7e1bb8..5848ae9 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -239,54 +239,28 @@
          (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)
+(defun encode-1 (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)))))
+      nil
+      (cons (list (len (car x)) (caar x))
+            (encode-1 (cdr x)))))
 
-(defthm sum-of-cars-encode
-  (equal (sum-of-cars (encode x))
-         (len x)))
+(defmacro encode (x)
+  `(encode-1 (pack ,x)))
 
 ;; P11 (*) Modified run-length encoding.
-(defun encode-modified-1 (x prev n)
+(defun encode-modified-1 (x)
   (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)))))
+    ((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 ,x nil 0))
+  `(encode-modified-1 (encode ,x)))
 
 ;; P12 (**) Decode a run-length encoded list.
 (defun repeat (x n)
@@ -300,9 +274,10 @@
                   n)))
 
 (defthm car-repeat
-  (implies (posp n)
-           (equal (car (repeat x n))
-                  x))
+  (equal (car (repeat x n))
+         (if (zp n)
+             nil
+             x))
   :hints (("Goal" :expand (REPEAT X 1))))
 
 (defthm seqp-repeat
@@ -319,24 +294,55 @@
     (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 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)
-                (natp n))
-           (equal (decode (encode-1 x sym n))
-                  (app (repeat sym n) x))))
+                (true-listp y)
+                (seqp y))
+           (equal (decode (encode-1 (pack-1 x y)))
+                  (app y x))))
 
 (defthm decode-encode
-  (implies (true-listp x)
+  (implies (and (true-listp x)
+                (true-listp y))
            (equal (decode (encode x))
                   x)))
 
-(defthm decode-encode-mofified-1
+(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)))
+
   (implies (and (atom-listp x)
                 (atom sym)
                 (natp n))
-- 
cgit v1.2.3