From b5d930724b689d122f23d92cd1fa1433009bc619 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 14 Aug 2021 01:42:41 +0900
Subject: pigeonhole: Add examples.

---
 pigeonhole.lisp | 64 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

(limited to 'pigeonhole.lisp')

diff --git a/pigeonhole.lisp b/pigeonhole.lisp
index 69fe8ab..58f44cd 100644
--- a/pigeonhole.lisp
+++ b/pigeonhole.lisp
@@ -72,3 +72,67 @@
                 (subsetp x s)
                 (< (len s) (len x)))
            (not (no-duplicatesp x))))
+(in-theory (disable pigeonhole-for-list))
+
+(defthm blood-types-are-duplicates
+  (implies (and (subsetp x '(A B O AB))
+                (< 4 (len x)))
+           (not (no-duplicatesp x)))
+  :hints (("Goal" :use (:instance pigeonhole-for-list
+                                  (s '(A B O AB))
+                                  (x x)))))
+
+(defun nats-below (n)
+  (if (zp n)
+      nil
+      (cons (- n 1)
+            (nats-below (- n 1)))))
+
+(defthm len-nats-below
+  (implies (natp n)
+           (equal (len (nats-below n)) n)))
+
+(defun all-under-p (x n)
+  (if (endp x)
+      t
+      (and (< (car x) n)
+           (all-under-p (cdr x) n))))
+
+(defthm all-under-p-lemma
+  (implies (and (posp n)
+                (all-under-p x (+ -1 n)))
+           (all-under-p x n)))
+
+(defthm all-under-p-nats-below
+  (implies (natp 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)))))
+
+(defthm no-duplicatesp-nats-below
+  (no-duplicatesp (nats-below n)))
+
+(defthm duplicates-nats
+  (implies (and (natp n)
+                (subsetp x (nats-below n))
+                (<= n m)
+                (< m (len x)))
+           (not (no-duplicatesp x)))
+  :hints (("Goal" :use (:instance pigeonhole-for-list
+                                  (s (nats-below n))
+                                  (x x)))))
+
+(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)))))
-- 
cgit v1.2.3