no-duplicatesp

(in-package "ACL2")

(defsection duplicity-badguy1
  :parents (duplicity-badguy)
  :short "@(call duplicity-badguy1) finds the first element of @('dom') whose
duplicity in @('x') exceeds 1, if such a member exists."
  (defund duplicity-badguy1
    (dom x)
    (declare (xargs :guard t))
    (if (consp dom)
      (if (> (duplicity (car dom) x) 1)
        (list (car dom))
        (duplicity-badguy1 (cdr dom) x))
      nil))
  (defthm duplicity-badguy1-exists-in-list
    (implies (duplicity-badguy1 dom x)
      (member-equal (car (duplicity-badguy1 dom x)) x))
    :hints (("Goal" :in-theory (enable duplicity-badguy1))))
  (defthm duplicity-badguy1-exists-in-dom
    (implies (duplicity-badguy1 dom x)
      (member-equal (car (duplicity-badguy1 dom x)) dom))
    :hints (("Goal" :in-theory (enable duplicity-badguy1))))
  (defthm duplicity-badguy1-has-high-duplicity
    (implies (duplicity-badguy1 dom x)
      (< 1 (duplicity (car (duplicity-badguy1 dom x)) x)))
    :hints (("Goal" :in-theory (enable duplicity-badguy1))))
  (defthm duplicity-badguy1-is-complete-for-domain
    (implies (and (member-equal a dom) (< 1 (duplicity a x)))
      (duplicity-badguy1 dom x))
    :hints (("Goal" :in-theory (enable duplicity-badguy1))))
  (defthm duplicity-badguy1-need-only-consider-the-list
    (implies (duplicity-badguy1 dom x) (duplicity-badguy1 x x))
    :hints (("Goal" :in-theory (disable duplicity-badguy1-exists-in-dom
         duplicity-badguy1-exists-in-list)
       :use ((:instance duplicity-badguy1-exists-in-dom) (:instance duplicity-badguy1-exists-in-list)))))
  (encapsulate nil
    (local (defthm lemma1
        (implies (duplicity-badguy1 dom x)
          (duplicity-badguy1 dom (cons a x)))
        :hints (("Goal" :in-theory (enable duplicity-badguy1)))))
    (local (defthm lemma2
        (implies (and (member-equal a x) (member-equal a dom))
          (duplicity-badguy1 dom (cons a x)))
        :hints (("Goal" :in-theory (enable duplicity-badguy1)))))
    (defthm no-duplicatesp-equal-when-duplicity-badguy1
      (implies (and (not (duplicity-badguy1 dom x)) (subsetp-equal x dom))
        (no-duplicatesp-equal x))
      :hints (("Goal" :in-theory (enable duplicity-badguy1))))))

(defsection duplicity-badguy
  :parents (duplicity no-duplicatesp-equal-same-by-duplicity)
  :short "@(call duplicity-badguy) finds an element that occurs multiple times
in the list @('x'), if one exists."
  :long "<p>This function is central to our proof of @(see
no-duplicatesp-equal-same-by-duplicity), a pick-a-point style strategy for
proving that @(see no-duplicatesp) holds of a list by reasoning about duplicity
of an arbitrary element.</p>"
  (defund duplicity-badguy
    (x)
    (declare (xargs :guard t))
    (duplicity-badguy1 x x))
  (defthm duplicity-badguy-exists
    (implies (duplicity-badguy x)
      (member-equal (car (duplicity-badguy x)) x))
    :hints (("Goal" :in-theory (enable duplicity-badguy))))
  (defthm duplicity-badguy-has-high-duplicity
    (implies (duplicity-badguy x)
      (< 1 (duplicity (car (duplicity-badguy x)) x)))
    :hints (("Goal" :in-theory (e/d (duplicity-badguy) (duplicity-when-member-equal)))))
  (defthm duplicity-badguy-is-complete
    (implies (< 1 (duplicity a x)) (duplicity-badguy x))
    :hints (("Goal" :in-theory (enable duplicity-badguy)
       :use ((:instance duplicity-badguy1-is-complete-for-domain (dom x))))))
  (local (defthm lemma
      (implies (subsetp-equal a (cdr x)) (subsetp-equal a x))))
  (local (defthm lemma2
      (subsetp-equal x x)
      :hints (("Goal" :induct (len x)))))
  (local (defthm lemma3
      (implies (not (duplicity-badguy x))
        (no-duplicatesp-equal x))
      :hints (("Goal" :in-theory (enable duplicity-badguy)))))
  (local (defthm lemma5
      (implies (duplicity-badguy x)
        (not (no-duplicatesp-equal x)))
      :hints (("Goal" :in-theory (disable no-duplicatesp-equal)
         :use ((:instance no-duplicatesp-equal-when-high-duplicity
            (a (car (duplicity-badguy x)))))))))
  (defthm duplicity-badguy-under-iff
    (iff (duplicity-badguy x) (not (no-duplicatesp-equal x)))))

(defsection no-duplicatesp-equal-same-by-duplicity
  :parents (no-duplicatesp-equal duplicity)
  :short "Proof strategy: show that a list satisfies @(see no-duplicatesp-equal)
because it has no element whose @(see duplicity) is over 1."
  :long "<p>This is often a good way to prove @(see no-duplicatesp).  This is a
basic pick-a-point style theorem that you can (manually) <see topic='@(url
functional-instantiation-example)'>functionally instantiate</see>.</p>"
  (encapsulate (((duplicity-hyp) => *) ((duplicity-lhs) => *)
      ((duplicity-rhs) => *))
    (local (defun duplicity-hyp nil nil))
    (local (defun duplicity-lhs nil nil))
    (local (defun duplicity-rhs nil nil))
    (defthm duplicity-constraint
      (implies (duplicity-hyp)
        (equal (duplicity a (duplicity-lhs))
          (duplicity a (duplicity-rhs))))))
  (local (defthm lemma1
      (implies (and (duplicity-hyp) (no-duplicatesp-equal (duplicity-lhs)))
        (no-duplicatesp-equal (duplicity-rhs)))
      :hints (("goal" :in-theory (disable duplicity-constraint
           duplicity-badguy-has-high-duplicity)
         :use ((:instance duplicity-badguy-has-high-duplicity
            (x (duplicity-rhs))) (:instance duplicity-constraint
             (a (car (duplicity-badguy (duplicity-rhs))))))))))
  (local (defthm lemma2
      (implies (and (duplicity-hyp) (no-duplicatesp-equal (duplicity-rhs)))
        (no-duplicatesp-equal (duplicity-lhs)))
      :hints (("goal" :in-theory (disable duplicity-constraint
           duplicity-badguy-has-high-duplicity)
         :use ((:instance duplicity-badguy-has-high-duplicity
            (x (duplicity-lhs))) (:instance duplicity-constraint
             (a (car (duplicity-badguy (duplicity-lhs))))))))))
  (defthm no-duplicatesp-equal-same-by-duplicity
    (implies (duplicity-hyp)
      (equal (no-duplicatesp-equal (duplicity-lhs))
        (no-duplicatesp-equal (duplicity-rhs))))
    :hints (("goal" :use ((:instance lemma1) (:instance lemma2))))))