L-99: Solve P21.develop

1 files changed, 32 insertions, 2 deletions

diff --git a/L-99.lisp b/L-99.lisp
index b1854fc..bb84d4c 100644
--- a/L-99.lisp
+++ b/L-99.lisp
@@ -33,7 +33,7 @@
 (defun element-at (x i)
   (declare (xargs :guard (and (true-listp x)
                               (posp i)
-                              (< (1- i) (len x)))))
+                              (<= i (len x)))))
   (if (zp (1- i))
       (car x)
       (element-at (cdr x) (1- i))))
@@ -45,7 +45,8 @@
 (defthm elment-at-equal-nth
   (implies (posp i)
            (equal (element-at x i)
-                  (nth (1- i) x))))
+                  (nth (1- i) x)))
+  :rule-classes nil)
 
 ;; P04 (*) Find the number of elements of a list.
 (defun my-len (x)
@@ -585,3 +586,32 @@
                 (<= i (len x))
                 (not (member (element-at x i) (remove-at x i))))
            (equal (count (element-at x i) x) 1)))
+
+;; P21: Insert an element at a given position into a list.
+(defun insert-at (e x i)
+  (declare (xargs :guard (and (true-listp x)
+                              (posp i)
+                              (<= i (1+ (len x))))))
+  (cond
+    ((zp (1- i)) (cons e x))
+    ((endp x) (list e))
+    (t (cons (car x)
+             (insert-at e (cdr x) (1- i))))))
+
+(defthm insert-at-nil
+  (equal (insert-at x nil n) (cons x nil)))
+
+(defthm element-at-insert-at
+  (implies (<= i (1+ (len x)))
+           (equal (element-at (insert-at e x i) i)
+                  e)))
+
+(defthm len-insert-at
+  (equal (len (insert-at e x n))
+         (+ 1 (len x))))
+
+(defthm remove-at-insert-at
+  (implies (<= i (1+ (len x)))
+           (equal (remove-at (insert-at e x i) i)
+                  x)))
+