pigeonhole: Rename pigenhole from to pigeonhole.

1 files changed, 74 insertions, 0 deletions

diff --git a/pigeonhole.lisp b/pigeonhole.lisp
new file mode 100644
index 0000000..c2fb779
--- /dev/null
+++ b/pigeonhole.lisp
@@ -0,0 +1,74 @@
+(defun member-if-over-1 (x)
+  (cond ((endp x) nil)
+        ((< 1 (car x)) x)
+        (t (member-if-over-1 (cdr x)))))
+
+(defun sum (x)
+  (if (endp x)
+      0
+      (+ (car x)
+         (sum (cdr x)))))
+
+(defthm pigeonhole
+  (implies (< (len x) (sum x))
+           (member-if-over-1 x)))
+
+(defun count/list (e x)
+  (cond ((endp x) 0)
+        ((equal e (car x)) (1+ (count/list e (cdr x))))
+        (t (count/list e (cdr x)))))
+
+(defthm member-remove
+  (implies (not (equal x y))
+           (iff (member x (remove y z))
+                (member x z))))
+
+(defthm no-duplicatesp-remove
+  (implies (no-duplicatesp x)
+           (no-duplicatesp (remove e x))))
+
+(defun map-count/list (x s)
+  (if (endp s)
+      nil
+      (cons (count/list (car s) x)
+            (map-count/list (remove (car s) x) (cdr s)))))
+
+(defthm len-map-count/list
+  (equal (len (map-count/list x s))
+         (len s)))
+
+(defthm len-remove
+  (equal (len (remove e x))
+         (- (len x) (count/list e x))))
+
+(defthm not-subsetp-remove
+  (implies (not (subsetp (remove e x) y))
+           (not (subsetp x (cons e y)))))
+
+(defthm sum-map-count/list
+  (implies (and (no-duplicatesp s)
+                (subsetp x s))
+           (equal (sum (map-count/list x s))
+                  (len x)))
+  :hints (("Goal" :induct (map-count/list x s))))
+
+(defthm not-no-duplicatesp-count/list
+  (implies (< 1 (count/list 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
+  (implies (and (no-duplicatesp s)
+                (subsetp x s)
+                (member-if-over-1 (map-count/list x s)))
+           (not (no-duplicatesp x)))
+  :hints (("Goal" :induct (map-count/list x s))))
+
+(defthm pigeonhole-for-list
+  (implies (and (no-duplicatesp s)
+                (subsetp x s)
+                (< (len s) (len x)))
+           (not (no-duplicatesp x))))