From be426f930462ffa7f54a0d775a0c8a6adaf5e3b4 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Thu, 29 Jul 2021 20:33:58 +0900
Subject: L-99: Solve P17, P18 and P19 problems.

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

diff --git a/L-99.lisp b/L-99.lisp
index 4ed6841..ff9e1c6 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -462,3 +462,110 @@
                 (<= i (len x))
                 (not (member (element-at x i) (drop x i))))
            (equal (count (element-at x i) x) 1)))
+
+;; 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))))
-- 
cgit v1.2.3