equal-by-g-help - ACL2 Book

Included Books

records

other

(in-package "ACL2")

include-book

(include-book "records")

local

(local (defthm rcdp-of-cdr (implies (rcdp x) (rcdp (cdr x)))))

g-badguyfunction

(defun g-badguy
  (x y)
  (cond ((atom x) (if (atom y)
        nil
        (cons :extra-in-y (car y))))
    ((atom y) (cons :extra-in-x (car x)))
    ((equal (car x) (car y)) (g-badguy (cdr x) (cdr y)))
    ((<< (caar x) (caar y)) (cons :extra-in-x (car x)))
    ((equal (caar x) (caar y)) (cons :mismatch (car x)))
    (t (cons :extra-in-y (car y)))))

g-badguy-lookup-in-x-when-extra-in-xencapsulate

(encapsulate nil
  (local (defthm l0
      (implies (and (<< (cadr (g-badguy x y)) a)
          (equal (car (g-badguy x y)) :extra-in-x)
          (rcdp x)
          (<< b (caar x)))
        (not (<< a b)))))
  (defthm g-badguy-lookup-in-x-when-extra-in-x
    (implies (and (equal (car (g-badguy x y)) :extra-in-x)
        (rcdp x)
        (rcdp y))
      (g-aux (cadr (g-badguy x y)) x))
    :hints (("Goal" :do-not '(generalize fertilize)))))

g-badguy-lookup-in-y-when-extra-in-xencapsulate

(encapsulate nil
  (local (defthm l0
      (implies (and (equal (car (g-badguy x y)) :extra-in-x)
          (<< a (caar x))
          (<< (cadr (g-badguy x y)) a)
          (rcdp x))
        (not (<< a (caar y))))))
  (defthm g-badguy-lookup-in-y-when-extra-in-x
    (implies (and (equal (car (g-badguy x y)) :extra-in-x)
        (rcdp x)
        (rcdp y))
      (and (not (g-aux (cadr (g-badguy x y)) y))))
    :hints (("Goal" :do-not '(generalize fertilize)))))

g-badguy-lookup-in-y-when-extra-in-yencapsulate

(encapsulate nil
  (local (defthm l0
      (implies (and (<< (cadr (g-badguy x y)) a)
          (equal (car (g-badguy x y)) :extra-in-y)
          (<< b (caar x))
          (rcdp y)
          (<< b (caar y)))
        (not (<< a b)))))
  (defthm g-badguy-lookup-in-y-when-extra-in-y
    (implies (and (equal (car (g-badguy x y)) :extra-in-y)
        (rcdp x)
        (rcdp y))
      (g-aux (cadr (g-badguy x y)) y))
    :hints (("Goal" :do-not '(generalize fertilize)))))

g-badguy-lookup-in-x-when-extra-in-yencapsulate

(encapsulate nil
  (local (defthm l0
      (implies (and (equal (car (g-badguy x y)) :extra-in-y)
          (<< a (caar x))
          (<< (cadr (g-badguy x y)) a)
          (rcdp y))
        (not (<< a (caar y))))))
  (defthm g-badguy-lookup-in-x-when-extra-in-y
    (implies (and (equal (car (g-badguy x y)) :extra-in-y)
        (rcdp x)
        (rcdp y))
      (not (g-aux (cadr (g-badguy x y)) x)))
    :hints (("Goal" :do-not '(generalize fertilize)))))

g-badguy-mismatch-when-mismatchencapsulate

(encapsulate nil
  (local (defthm l0
      (implies (and (<< (cadr (g-badguy x y)) a)
          (equal (car (g-badguy x y)) :mismatch)
          (rcdp x)
          (rcdp y)
          (<< b (caar x))
          (<< b (caar y)))
        (not (<< a b)))))
  (local (defthm l1
      (implies (and (equal (car (g-badguy x y)) :mismatch)
          (rcdp x)
          (rcdp y)
          (<< a (caar x))
          (<< (cadr (g-badguy x y)) a))
        (not (<< a (caar y))))))
  (defthm g-badguy-mismatch-when-mismatch
    (implies (and (equal (car (g-badguy x y)) :mismatch)
        (rcdp x)
        (rcdp y))
      (equal (equal (g-aux (cadr (g-badguy x y)) x)
          (g-aux (cadr (g-badguy x y)) y))
        nil))
    :hints (("goal" :do-not '(generalize fertilize)))))

g-badguy-casestheorem

(defthm g-badguy-cases
  (or (not (g-badguy x y))
    (equal (car (g-badguy x y)) :mismatch)
    (equal (car (g-badguy x y)) :extra-in-x)
    (equal (car (g-badguy x y)) :extra-in-y))
  :rule-classes nil)

g-aux-of-g-badguytheorem

(defthm g-aux-of-g-badguy
  (implies (and (g-badguy x y) (rcdp x) (rcdp y))
    (not (equal (g-aux (cadr (g-badguy x y)) x)
        (g-aux (cadr (g-badguy x y)) y))))
  :hints (("Goal" :do-not-induct t
     :do-not '(eliminate-destructors generalize fertilize)
     :use ((:instance g-badguy-cases)))))

g-badguy-unless-equaltheorem

(defthm g-badguy-unless-equal
  (implies (and (not (equal x y)) (rcdp x) (rcdp y))
    (g-badguy x y)))

g-worseguyfunction

(defun g-worseguy
  (x y)
  (g-badguy (acl2->rcd x) (acl2->rcd y)))

acl2->rcd-returns-rcdptheorem

(defthm acl2->rcd-returns-rcdp
  (rcdp (acl2->rcd x))
  :hints (("Goal" :in-theory (enable acl2->rcd))))

g-worseguy-finds-counterexampletheorem

(defthm g-worseguy-finds-counterexample
  (implies (g-worseguy x y)
    (not (equal (g (cadr (g-worseguy x y)) x)
        (g (cadr (g-worseguy x y)) y))))
  :hints (("Goal" :in-theory (enable g))))

g-worseguy-unless-equalencapsulate

(encapsulate nil
  (local (defthm rcdp-unless-ifrp (implies (not (ifrp x)) (rcdp x))))
  (local (defthm main-lemma-for-case-3
      (implies (and (not (ifrp x)) (ifrp y))
        (not (equal x (list (cons nil y)))))))
  (local (defthm corollary-for-case-3
      (implies (and (not (ifrp x)) (ifrp y))
        (g-badguy x (list (cons nil y))))
      :hints (("Goal" :in-theory (disable g-badguy-unless-equal)
         :use ((:instance g-badguy-unless-equal
            (x x)
            (y (list (cons nil y)))))))))
  (defthm g-worseguy-unless-equal
    (implies (not (equal x y)) (g-worseguy x y))
    :hints (("Goal" :in-theory (enable acl2->rcd ifrp)
       :do-not-induct t
       :do-not '(generalize fertilize)))))