L-99: Solve problems from P01 to P07.

1 files changed, 143 insertions, 0 deletions

diff --git a/L-99.lisp b/L-99.lisp
new file mode 100644
index 0000000..3bfaa94
--- /dev/null
+++ b/L-99.lisp
@@ -0,0 +1,143 @@
+;; 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))))))