equality

(in-package "ACL2")

(local (include-book "tools/flag" :dir :system))

(defconst *esc-disables*
  '(disjoin disjoin2 conjoin conjoin2))

(make-event (prog2$ (cw "Note (from clause-processors/equality): disabling ~&0.~%~%"
      *esc-disables*)
    '(value-triple :invisible))
  :check-expansion t)

(in-theory (set-difference-theories (current-theory :here)
    *esc-disables*))

(defund iff-list
  (x y)
  (if (and (consp x) (consp y))
    (and (iff (car x) (car y)) (iff-list (cdr x) (cdr y)))
    (and (not (consp x)) (not (consp y)))))

(local (in-theory (enable iff-list)))

(encapsulate nil
  (defthm iff-list-reflexive (iff-list x x))
  (defthm iff-list-symmetric
    (implies (iff-list x y) (iff-list y x)))
  (defthm iff-list-transitive
    (implies (and (iff-list x y) (iff-list y z)) (iff-list x z)))
  (defequiv iff-list))

(defcong iff-list equal (or-list x) 1)

(defcong iff-list equal (and-list x) 1)

(defevaluator esc-eval
  esc-eval-list
  ((if x
     y
     z) (equal x y)
    (not x)))

(local (defthm esc-eval-of-arbitrary-function
    (implies (and (symbolp fn)
        (not (equal fn 'quote))
        (equal (esc-eval-list args1 env) (esc-eval-list args2 env)))
      (equal (esc-eval (cons fn args1) env)
        (esc-eval (cons fn args2) env)))
    :hints (("goal" :use ((:instance esc-eval-constraint-0
          (x (cons fn args1))
          (a env)) (:instance esc-eval-constraint-0
           (x (cons fn args2))
           (a env)))))))

(defthm esc-eval-of-disjoin2
  (iff (esc-eval (disjoin2 t1 t2) env)
    (or (esc-eval t1 env) (esc-eval t2 env)))
  :hints (("Goal" :in-theory (enable disjoin2))))

(defthm esc-eval-of-disjoin
  (iff (esc-eval (disjoin x) env)
    (or-list (esc-eval-list x env)))
  :hints (("Goal" :in-theory (enable disjoin))))

(defthm esc-eval-of-conjoin2
  (iff (esc-eval (conjoin2 t1 t2) env)
    (and (esc-eval t1 env) (esc-eval t2 env)))
  :hints (("Goal" :in-theory (enable conjoin2))))

(defthm esc-eval-of-conjoin
  (iff (esc-eval (conjoin x) env)
    (and-list (esc-eval-list x env)))
  :hints (("Goal" :in-theory (enable conjoin))))

(defund esc-alist-p
  (x)
  "Recognizes an alist whose keys and values are all pseudo-terms."
  (declare (xargs :guard t))
  (if (atom x)
    (not x)
    (and (consp (car x))
      (pseudo-termp (car (car x)))
      (pseudo-termp (cdr (car x)))
      (esc-alist-p (cdr x)))))

(defthm esc-alist-p-when-atom
  (implies (atom x) (equal (esc-alist-p x) (not x)))
  :hints (("Goal" :in-theory (enable esc-alist-p))))

(defthm esc-alist-p-of-cons
  (equal (esc-alist-p (cons a x))
    (and (consp a)
      (pseudo-termp (car a))
      (pseudo-termp (cdr a))
      (esc-alist-p x)))
  :hints (("Goal" :in-theory (enable esc-alist-p))))

(defthmd alistp-when-esc-alist-p
  (implies (esc-alist-p x) (alistp x))
  :hints (("Goal" :induct (len x))))

(local (in-theory (enable alistp-when-esc-alist-p)))

(defund esc-alist-to-equalities
  (x)
  "Convert an esc-alist-p into a list of (equal key val) terms."
  (declare (xargs :guard (esc-alist-p x)))
  (if (atom x)
    nil
    (cons `(equal ,(CAR (CAR X)) ,(CDR (CAR X)))
      (esc-alist-to-equalities (cdr x)))))

(defthm esc-alist-to-equalities-when-atom
  (implies (atom x) (equal (esc-alist-to-equalities x) nil))
  :hints (("Goal" :in-theory (enable esc-alist-to-equalities))))

(defthm esc-alist-to-equalities-of-cons
  (equal (esc-alist-to-equalities (cons a x))
    (cons `(equal ,(CAR A) ,(CDR A))
      (esc-alist-to-equalities x)))
  :hints (("Goal" :in-theory (enable esc-alist-to-equalities))))

(defthm pseudo-term-listp-of-esc-alist-to-equalities
  (implies (force (esc-alist-p x))
    (equal (pseudo-term-listp (esc-alist-to-equalities x)) t))
  :hints (("Goal" :induct (len x))))

(encapsulate nil
  (local (defthm lemma1
      (implies (consp (assoc-equal a x))
        (member `(equal ,A ,(CDR (ASSOC-EQUAL A X)))
          (esc-alist-to-equalities x)))
      :hints (("Goal" :induct (len x)))))
  (local (defthm lemma2
      (implies (and (and-list (esc-eval-list x env)) (member a x))
        (iff (esc-eval a env) t))
      :hints (("Goal" :induct (len x)))))
  (local (defthm lemma3
      (implies (and (and-list (esc-eval-list (esc-alist-to-equalities x) env))
          (consp (assoc-equal a x)))
        (iff (esc-eval `(equal ,A ,(CDR (ASSOC-EQUAL A X))) env) t))))
  (defthm esc-eval-of-binding
    (implies (and (and-list (esc-eval-list (esc-alist-to-equalities x) env))
        (consp (assoc-equal a x)))
      (equal (esc-eval (cdr (assoc-equal a x)) env)
        (esc-eval a env)))))

(mutual-recursion (defund esc-substitute
    (x alist)
    "Substitute an esc-alist-p into a pseudo-term-p."
    (declare (xargs :guard (and (pseudo-termp x) (esc-alist-p alist))))
    (let ((binding (assoc-equal x alist)))
      (cond ((consp binding) (cdr binding))
        ((atom x) x)
        ((eq (car x) 'quote) x)
        (t (cons (car x) (esc-substitute-list (cdr x) alist))))))
  (defund esc-substitute-list
    (x alist)
    (declare (xargs :guard (and (pseudo-term-listp x) (esc-alist-p alist))))
    (if (atom x)
      nil
      (cons (esc-substitute (car x) alist)
        (esc-substitute-list (cdr x) alist)))))

(defthm esc-substitute-list-when-atom
  (implies (atom x) (equal (esc-substitute-list x alist) nil))
  :hints (("Goal" :in-theory (enable esc-substitute-list))))

(defthm esc-substitute-list-of-cons
  (equal (esc-substitute-list (cons a x) alist)
    (cons (esc-substitute a alist)
      (esc-substitute-list x alist)))
  :hints (("Goal" :in-theory (enable esc-substitute-list))))

(encapsulate nil
  (local (make-flag flag-pseudo-termp
      pseudo-termp
      :flag-mapping ((pseudo-termp term) (pseudo-term-listp list))))
  (local (defthm-flag-pseudo-termp lemma
      (term (implies (and (pseudo-termp x)
            (esc-alist-p alist)
            (and-list (esc-eval-list (esc-alist-to-equalities alist) env)))
          (equal (esc-eval (esc-substitute x alist) env)
            (esc-eval x env))))
      (list (implies (and (pseudo-term-listp lst)
            (esc-alist-p alist)
            (and-list (esc-eval-list (esc-alist-to-equalities alist) env)))
          (equal (esc-eval-list (esc-substitute-list lst alist) env)
            (esc-eval-list lst env))))
      :hints (("goal" :induct (flag-pseudo-termp flag x lst)
         :expand ((esc-substitute x alist))
         :do-not '(generalize fertilize)
         :do-not-induct t))))
  (defthm esc-eval-of-esc-substitute
    (implies (and (pseudo-termp x)
        (esc-alist-p alist)
        (and-list (esc-eval-list (esc-alist-to-equalities alist) env)))
      (equal (esc-eval (esc-substitute x alist) env)
        (esc-eval x env))))
  (defthm esc-eval-list-of-esc-substitute-list
    (implies (and (pseudo-term-listp lst)
        (esc-alist-p alist)
        (and-list (esc-eval-list (esc-alist-to-equalities alist) env)))
      (equal (esc-eval-list (esc-substitute-list lst alist) env)
        (esc-eval-list lst env)))))

(defund weaken-clause-with-each-term
  (terms clause)
  (declare (xargs :guard (and (pseudo-term-listp terms) (pseudo-term-listp clause))))
  (if (atom terms)
    nil
    (cons (cons (car terms) clause)
      (weaken-clause-with-each-term (cdr terms) clause))))

(defthm pseudo-term-list-listp-of-weaken-clause-with-each-term
  (implies (and (force (pseudo-term-listp terms))
      (force (pseudo-term-listp clause)))
    (pseudo-term-list-listp (weaken-clause-with-each-term terms clause)))
  :hints (("Goal" :in-theory (enable weaken-clause-with-each-term))))

(defthm soundness-of-weaken-clause-with-each-term
  (implies (not (or-list (esc-eval-list clause env)))
    (iff-list (esc-eval-list (disjoin-lst (weaken-clause-with-each-term terms clause))
        env)
      (esc-eval-list terms env)))
  :hints (("Goal" :in-theory (enable weaken-clause-with-each-term))))

(defund equality-substitute-clause
  (clause alist state)
  (declare (xargs :guard (and (state-p state) (pseudo-term-listp clause))
      :stobjs state))
  (cond ((not (esc-alist-p alist)) (prog2$ (cw "equality-substitute-clause invoked with bad alist: ~x0~%"
          alist)
        (mv t nil state)))
    (t (value (cons (esc-substitute-list clause alist)
          (weaken-clause-with-each-term (esc-alist-to-equalities alist)
            clause))))))

(defthm correctness-of-equality-substitute-clause
  (implies (and (pseudo-term-listp clause)
      (alistp env)
      (esc-eval (conjoin-clauses (clauses-result (equality-substitute-clause clause alist state)))
        env))
    (esc-eval (disjoin clause) env))
  :rule-classes :clause-processor :hints (("Goal" :in-theory (enable equality-substitute-clause))))