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