diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-13 23:33:52 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-13 23:33:52 +0900 |
commit | d1cf027f4247f01a3d4781ec7f751c67da96e923 (patch) | |
tree | fa0d20276e6f01b0ce49e3ed357ec084a6db974a | |
parent | 22e1d6c1abc5c7c825364658deab9969190586a6 (diff) |
pigeonhole: Rename from count/list to list-count.
-rw-r--r-- | pigeonhole.lisp | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/pigeonhole.lisp b/pigeonhole.lisp index c2fb779..69fe8ab 100644 --- a/pigeonhole.lisp +++ b/pigeonhole.lisp @@ -13,10 +13,10 @@ (implies (< (len x) (sum x)) (member-if-over-1 x))) -(defun count/list (e x) +(defun list-count (e x) (cond ((endp x) 0) - ((equal e (car x)) (1+ (count/list e (cdr x)))) - (t (count/list e (cdr x))))) + ((equal e (car x)) (1+ (list-count e (cdr x)))) + (t (list-count e (cdr x))))) (defthm member-remove (implies (not (equal x y)) @@ -27,45 +27,45 @@ (implies (no-duplicatesp x) (no-duplicatesp (remove e x)))) -(defun map-count/list (x s) +(defun map-list-count (x s) (if (endp s) nil - (cons (count/list (car s) x) - (map-count/list (remove (car s) x) (cdr s))))) + (cons (list-count (car s) x) + (map-list-count (remove (car s) x) (cdr s))))) -(defthm len-map-count/list - (equal (len (map-count/list x s)) +(defthm len-map-list-count + (equal (len (map-list-count x s)) (len s))) (defthm len-remove (equal (len (remove e x)) - (- (len x) (count/list e x)))) + (- (len x) (list-count e x)))) (defthm not-subsetp-remove (implies (not (subsetp (remove e x) y)) (not (subsetp x (cons e y))))) -(defthm sum-map-count/list +(defthm sum-map-list-count (implies (and (no-duplicatesp s) (subsetp x s)) - (equal (sum (map-count/list x s)) + (equal (sum (map-list-count x s)) (len x))) - :hints (("Goal" :induct (map-count/list x s)))) + :hints (("Goal" :induct (map-list-count x s)))) -(defthm not-no-duplicatesp-count/list - (implies (< 1 (count/list e x)) +(defthm not-no-duplicatesp-list-count + (implies (< 1 (list-count e x)) (not (no-duplicatesp x)))) (defthm not-no-duplicatesp-remove (implies (not (no-duplicatesp (remove e x))) (not (no-duplicatesp x)))) -(defthm member-if-over-1-map-count/list-is-duplicated +(defthm member-if-over-1-map-list-count-is-duplicated (implies (and (no-duplicatesp s) (subsetp x s) - (member-if-over-1 (map-count/list x s))) + (member-if-over-1 (map-list-count x s))) (not (no-duplicatesp x))) - :hints (("Goal" :induct (map-count/list x s)))) + :hints (("Goal" :induct (map-list-count x s)))) (defthm pigeonhole-for-list (implies (and (no-duplicatesp s) |