From db8de2e5c6141cc67a7c524d52c328760b8b47cf Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 13 Aug 2021 16:08:08 +0900
Subject: pigenhole: Add pigenhole.lisp.

---
 pigenhole.lisp | 106 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 106 insertions(+)
 create mode 100644 pigenhole.lisp

diff --git a/pigenhole.lisp b/pigenhole.lisp
new file mode 100644
index 0000000..2aabfed
--- /dev/null
+++ b/pigenhole.lisp
@@ -0,0 +1,106 @@
+(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)))))
+
+(defmacro finite-natp (x n)
+  `(and (natp ,x) (< ,x ,n)))
+
+(defun finite-nat-listp (x n)
+  (if (endp x)
+      (null x)
+      (and (finite-natp (car x) n)
+           (finite-nat-listp (cdr x) n))))
+
+(defun duplicatedp (x)
+  (cond ((endp x) nil)
+        ((member (car x) (cdr x)) t)
+        (t (duplicatedp (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)))))
+
+(defun map-count/list (x n)
+  (if (zp n)
+      nil
+      (cons (count/list (1- n) x)
+            (map-count/list (remove-equal (1- n) x) (1- n)))))
+
+(defthm finite-nat-listp-remove-equal
+  (implies (and (not (zp n))
+                (finite-nat-listp x n))
+           (and (finite-nat-listp (remove-equal (1- n) x) (1- n))
+                (finite-nat-listp (remove-equal (1- n) x) n))))
+
+(defthm len-map-count/list
+  (implies (natp n)
+           (equal (len (map-count/list x n)) n)))
+
+(defthm sum-map-count/list-nil
+  (equal (sum (map-count/list nil n)) 0))
+
+(defun sum-map-count/list-induction (x n)
+  (declare (xargs :measure (nfix n)))
+  (if (zp n)
+      x
+      (sum-map-count/list-induction (remove-equal (1- n) x) (1- n))))
+
+(defthm len-remove-equal
+  (equal (len (remove-equal e x))
+         (- (len x) (count/list e x))))
+
+(defthm sum-map-count/list
+  (implies (and (natp n)
+                (finite-nat-listp x n))
+           (equal (sum (map-count/list x n))
+                  (len x)))
+  :hints (("Goal" :induct (sum-map-count/list-induction x n))))
+
+(defun map-count/list* (x n)
+  (if (zp n)
+      nil
+      (cons (count/list (1- n) x)
+            (map-count/list* x (1- n)))))
+
+(defun nat-induction (n)
+  (if (zp n)
+      1
+      (nat-induction (- n 1))))
+
+(defthm duplicatedp-count/list
+  (implies (< 1 (count/list e x))
+           (duplicatedp x)))
+
+(defthm member-remove-equal
+  (implies (not (equal x y))
+           (iff (member x (remove-equal y z))
+                (member x z))))
+
+(defthm duplicatedp-remove-equal
+  (implies (duplicatedp (remove-equal e x))
+           (duplicatedp x)))
+
+(defthm member-if-over-1-map-count/list-is-duplicated
+  (implies (and (natp n)
+                (finite-nat-listp x n)
+                (member-if-over-1 (map-count/list x n)))
+           (duplicatedp x))
+  :hints (("Goal" :induct (sum-map-count/list-induction x n))))
+
+(defthm pigeonhole-for-finite-nat-list
+  (implies (and (natp n)
+                (finite-nat-listp x n)
+                (< n (len x)))
+           (duplicatedp x)))
-- 
cgit v1.2.3