From eee26e12e82d2ac1b63a1787c7d3671c096a55d1 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 13 Aug 2021 19:44:56 +0900
Subject: pigeonhole: Rename pigenhole from to pigeonhole.

---
 pigenhole.lisp  | 74 ---------------------------------------------------------
 pigeonhole.lisp | 74 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 74 insertions(+), 74 deletions(-)
 delete mode 100644 pigenhole.lisp
 create mode 100644 pigeonhole.lisp

diff --git a/pigenhole.lisp b/pigenhole.lisp
deleted file mode 100644
index c2fb779..0000000
--- a/pigenhole.lisp
+++ /dev/null
@@ -1,74 +0,0 @@
-(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))))
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))))
-- 
cgit v1.2.3