From b420ce87ceae55123e1780a7eddec7eea5388ab7 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 13 Aug 2021 16:50:01 +0900
Subject: pigenhole: Remove finite-nat.

---
 pigenhole.lisp | 115 ++++++++++++++++++++++-----------------------------------
 1 file changed, 44 insertions(+), 71 deletions(-)

diff --git a/pigenhole.lisp b/pigenhole.lisp
index 2aabfed..0536656 100644
--- a/pigenhole.lisp
+++ b/pigenhole.lisp
@@ -9,20 +9,6 @@
       (+ (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)))
@@ -32,75 +18,62 @@
         ((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 member-remove
+  (implies (not (equal x y))
+           (iff (member x (remove y z))
+                (member x z))))
 
-(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 no-duplicatesp-remove
+  (implies (no-duplicatesp x)
+           (no-duplicatesp (remove e x))))
 
-(defthm len-map-count/list
-  (implies (natp n)
-           (equal (len (map-count/list x n)) n)))
+(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 sum-map-count/list-nil
-  (equal (sum (map-count/list nil n)) 0))
+(defthm len-map-count/list
+  (equal (len (map-count/list x s))
+         (len s)))
 
-(defun sum-map-count/list-induction (x n)
-  (declare (xargs :measure (nfix n)))
-  (if (zp n)
+(defun sum-map-count/list-induction (x s)
+  (if (endp s)
       x
-      (sum-map-count/list-induction (remove-equal (1- n) x) (1- n))))
+      (sum-map-count/list-induction (remove (car s) x) (cdr s))))
 
-(defthm len-remove-equal
-  (equal (len (remove-equal e x))
+(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 (natp n)
-                (finite-nat-listp x n))
-           (equal (sum (map-count/list x n))
+  (implies (and (no-duplicatesp s)
+                (subsetp x s))
+           (equal (sum (map-count/list x s))
                   (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))))
+  :hints (("Goal" :induct (sum-map-count/list-induction x s))))
 
-(defthm duplicatedp-count/list
+(defthm not-no-duplicatesp-count/list
   (implies (< 1 (count/list e x))
-           (duplicatedp x)))
+           (not (no-duplicatesp 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 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 (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)))
+  (implies (and (no-duplicatesp s)
+                (subsetp x s)
+                (member-if-over-1 (map-count/list x s)))
+           (not (no-duplicatesp x)))
+  :hints (("Goal" :induct (sum-map-count/list-induction 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