diff options
| -rw-r--r-- | L-99.lisp | 72 |
1 files changed, 67 insertions, 5 deletions
@@ -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))) |