(in-package "ACL2")

(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 list-count (e x)
  (cond ((endp x) 0)
        ((equal e (car x)) (1+ (list-count e (cdr x))))
        (t (list-count 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-list-count (x s)
  (if (endp s)
      nil
      (cons (list-count (car s) x)
            (map-list-count (remove (car s) x) (cdr s)))))

(defthm len-map-list-count
  (equal (len (map-list-count x s))
         (len s)))

(defthm len-remove
  (equal (len (remove e x))
         (- (len x) (list-count e x))))

(defthm not-subsetp-remove
  (implies (not (subsetp (remove e x) y))
           (not (subsetp x (cons e y)))))

(defthm sum-map-list-count
  (implies (and (no-duplicatesp s)
                (subsetp x s))
           (equal (sum (map-list-count x s))
                  (len x)))
  :hints (("Goal" :induct (map-list-count x s))))

(defthm not-no-duplicatesp-list-count
  (implies (< 1 (list-count e x))
           (not (no-duplicatesp x)))
  :rule-classes ((:rewrite :match-free :all)))

(defthm not-no-duplicatesp-remove
  (implies (not (no-duplicatesp (remove e x)))
           (not (no-duplicatesp x)))
  :rule-classes ((:rewrite :match-free :all)))

(defthm member-if-over-1-map-list-count-is-duplicated
  (implies (and (no-duplicatesp s)
                (subsetp x s)
                (member-if-over-1 (map-list-count x s)))
           (not (no-duplicatesp x)))
  :hints (("Goal" :induct (map-list-count x s)))
  :rule-classes ((:rewrite :match-free :all)))

(defthm pigeonhole-for-list
  (implies (and (no-duplicatesp s)
                (subsetp x s)
                (< (len s) (len x)))
           (not (no-duplicatesp x)))
  :rule-classes ((:rewrite :match-free :all)))
(in-theory (disable pigeonhole-for-list))

(defthm blood-types-are-duplicates
  (implies (and (subsetp x '(A B O AB))
                (<= 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
      (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
  (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
  (not (member n (nats-below n))))

(defthm no-duplicatesp-nats-below
  (no-duplicatesp (nats-below n)))

(defthm duplicates-nats
  (implies (and (integerp n)
                (<= 0 n)
                (subsetp x (nats-below n))
                (< n m)
                (<= m (len x)))
           (not (no-duplicatesp x)))
  :rule-classes ((:rewrite :match-free :all))
  :hints (("Goal" :use (:instance pigeonhole-for-list
                                  (s (nats-below n))
                                  (x x)))))
(in-theory (disable duplicates-nats))

(defthm numbers-of-hairs-are-duplicates-in-gunma
  (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)))))