From f45671c05282ccb6b02dcb4386a0042b669e1a8b Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sun, 1 Aug 2021 13:46:52 +0900 Subject: L-99: Fix P16 problem. --- L-99.lisp | 48 +++++++++++++++++++++--------------------------- 1 file changed, 21 insertions(+), 27 deletions(-) diff --git a/L-99.lisp b/L-99.lisp index 820e741..3c8dc71 100644 --- a/L-99.lisp +++ b/L-99.lisp @@ -431,37 +431,18 @@ (* n (len x))))) ;; P16 (**) Drop every N'th element from a list. -(defun drop (x n) +(defun drop-1 (x n i) (cond ((endp x) nil) - ((zp (1- n)) (cdr x)) + ((zp (- i 1)) + (drop-1 (cdr x) n n)) (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))) + (drop-1 (cdr x) + n + (1- i)))))) -(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))) +(defmacro drop (x n) + `(drop-1 ,x ,n ,n)) ;; P17 (*) Split a list into two parts; the length of the first part is given. (defun split-1 (x n acc) @@ -578,6 +559,19 @@ (t (cons (car x) (remove-at (cdr x) (1- n)))))) +(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 len-remove-at (implies (and (posp i) (<= i (len x))) -- cgit v1.2.3