From 7999d486dba9e8229957fa7e355ca04db776aef1 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Tue, 22 Mar 2022 12:09:54 +0900 Subject: L-99: Solve P21. --- L-99.lisp | 34 ++++++++++++++++++++++++++++++++-- 1 file 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))) + -- cgit v1.2.3