From 58930a5cb5e011da1ef50a793b48e2ec4856491f Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 14 Aug 2021 11:16:29 +0900
Subject: pigeonhole: Update.

---
 pigeonhole.lisp | 40 +++++++++++++++++++++++++---------------
 1 file changed, 25 insertions(+), 15 deletions(-)

diff --git a/pigeonhole.lisp b/pigeonhole.lisp
index 58f44cd..bda4cfc 100644
--- a/pigeonhole.lisp
+++ b/pigeonhole.lisp
@@ -76,12 +76,21 @@
 
 (defthm blood-types-are-duplicates
   (implies (and (subsetp x '(A B O AB))
-                (< 4 (len x)))
+                (<= 5 (len x)))
            (not (no-duplicatesp x)))
   :hints (("Goal" :use (:instance pigeonhole-for-list
                                   (s '(A B O AB))
                                   (x x)))))
 
+(defthm birth-months-are-duplicates
+  (let ((birth-months '(1 2 3 4 5 6 7 8 9 10 11 12)))
+    (implies (and (subsetp x birth-months)
+                  (<= 13 (len x)))
+             (not (no-duplicatesp x))))
+  :hints (("Goal" :use (:instance pigeonhole-for-list
+                                  (s '(1 2 3 4 5 6 7 8 9 10 11 12))
+                                  (x x)))))
+
 (defun nats-below (n)
   (if (zp n)
       nil
@@ -104,35 +113,36 @@
            (all-under-p x n)))
 
 (defthm all-under-p-nats-below
-  (implies (natp n)
-           (all-under-p (nats-below n) n)))
+  (all-under-p (nats-below n) n))
 
 (defthm all-under-p-not-member
   (implies (all-under-p x n)
            (not (member n x))))
 
 (defthm not-member-nats-below
-  (implies (natp n)
-           (not (member n (nats-below n)))))
+  (not (member n (nats-below n))))
 
 (defthm no-duplicatesp-nats-below
   (no-duplicatesp (nats-below n)))
 
 (defthm duplicates-nats
-  (implies (and (natp n)
+  (implies (and (posp n)
                 (subsetp x (nats-below n))
-                (<= n m)
-                (< m (len x)))
+                (< n m)
+                (<= m (len x)))
            (not (no-duplicatesp x)))
   :hints (("Goal" :use (:instance pigeonhole-for-list
                                   (s (nats-below n))
                                   (x x)))))
+(in-theory (disable duplicates-nats))
 
 (defthm number-of-hairs-are-duplicates-in-gunma
-  (let ((gunma-population 2000000)
-        (max-number-of-hairs 250000))
-    (implies (and (natp n)
-                  (<= n max-number-of-hairs)
-                  (subsetp x (nats-below n))
-                  (<= gunma-population (len x)))
-             (not (no-duplicatesp x)))))
+  (let ((max-number-of-hairs 250000)
+        (gunma-population 2000000))
+    (implies (and (subsetp x (nats-below max-number-of-hairs))
+                  (= gunma-population (len x)))
+             (not (no-duplicatesp x))))
+  :hints (("Goal" :use (:instance duplicates-nats
+                                  (n 250000)
+                                  (m 2000000)
+                                  (x x)))))
-- 
cgit v1.2.3