From 8902e2807da9cfce8a50147968bdd4a90b7606e9 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Thu, 29 Jul 2021 16:43:39 +0900
Subject: L-99: Solve P14, P15 and P16.

---
 L-99.lisp | 72 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 67 insertions(+), 5 deletions(-)

diff --git a/L-99.lisp b/L-99.lisp
index 26bb663..4ed6841 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -30,9 +30,9 @@
 ;; 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)
+                              (posp i)
+                              (< (1- i) (len x)))))
+  (if (zp (1- i))
       (car x)
       (element-at (cdr x) (1- i))))
 
@@ -41,8 +41,9 @@
          nil))
 
 (defthm elment-at-equal-nth
-  (equal (element-at x i)
-         (nth i x)))
+  (implies (posp i)
+           (equal (element-at x i)
+                  (nth (1- i) x))))
 
 ;; P04 (*) Find the number of elements of a list.
 (defun my-len (x)
@@ -400,3 +401,64 @@
   (implies (atom-listp x)
            (equal (encode-direct x)
                   (encode-modified x))))
+
+;; P14 (*) Duplicate the elements of a list.
+(defun dupli (x)
+  (if (endp x)
+      nil
+      (cons (car x)
+            (cons (car x)
+                  (dupli (cdr x))))))
+
+(defthm len-dupli
+  (equal (len (dupli x))
+         (* 2 (len x))))
+
+;; P15 (**) Replicate the elements of a list a given number of times.
+(defun repli (x n)
+  (if (endp x)
+      nil
+      (app (repeat (car x) n)
+           (repli (cdr x) n))))
+
+(defthm repli-2-equal-dupli
+  (equal (repli x 2)
+         (dupli x)))
+
+(defthm len-repli
+  (implies (natp n)
+           (equal (len (repli x n))
+                  (* n (len x)))))
+
+;; P16 (**) Drop every N'th element from a list.
+(defun drop (x n)
+  (cond
+    ((endp x) nil)
+    ((zp (1- n)) (cdr x))
+    (t (cons (car x)
+             (drop (cdr x) (1- n))))))
+
+(defthm len-drop
+  (implies (and (posp i)
+                (<= i (len x)))
+           (equal (len (drop x i))
+                  (- (len x) 1))))
+
+(defun count/list (e x)
+  (cond ((endp x) 0)
+        ((equal (car x) e) (+ 1 (count/list e (cdr x))))
+        (t (count/list e (cdr x)))))
+
+(defthm count-to-count/list
+ (implies (consp x)
+          (equal (count e x) (count/list e x))))
+
+(defthm posp-len-implies-consp
+  (implies (posp (len x))
+           (consp x)))
+
+(defthm not-member-element-at-drop-implies-only-one
+  (implies (and (posp i)
+                (<= i (len x))
+                (not (member (element-at x i) (drop x i))))
+           (equal (count (element-at x i) x) 1)))
-- 
cgit v1.2.3