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