		Search-engine friendly clone of the ACL2 documentation.

Svex-env

Svex-envs-similar

(svex-envs-similar x y) is like alist equivalence for svex-envs: environments are similar if they bind all variables to the same values, in the sense of svex-env-lookup.

Recall that svex-env-lookup treats any unbound variables as being bound to an infinite X vector. Accordingly, two environments need not have the same bound variables to be regarded as equal.

This is an important equivalence relation that is satisfied by, e.g., svex-eval. It is used more than is apparent because of the congruences it provides.

Function: svex-envs-similar

(defun svex-envs-similar (x y)
  (declare (xargs :non-executable t))
  (declare (xargs :guard t))
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'svex-envs-similar
                                     (list x y))
          (let ((k (svex-envs-similar-witness x y)))
            (and (equal (svex-env-lookup k x)
                        (svex-env-lookup k y))))))

Definitions and Theorems

Theorem: svex-envs-similar-necc

(defthm svex-envs-similar-necc
  (implies (not (and (equal (svex-env-lookup k x)
                            (svex-env-lookup k y))))
           (not (svex-envs-similar x y))))

Theorem: svex-envs-similar-witnessing-witness-rule-correct

(defthm svex-envs-similar-witnessing-witness-rule-correct
  (implies (not ((lambda (k y x)
                   (not (equal (svex-env-lookup k x)
                               (svex-env-lookup k y))))
                 (svex-envs-similar-witness x y)
                 y x))
           (svex-envs-similar x y))
  :rule-classes nil)

Theorem: svex-envs-similar-instancing-instance-rule-correct

(defthm svex-envs-similar-instancing-instance-rule-correct
  (implies (not (equal (svex-env-lookup k x)
                       (svex-env-lookup k y)))
           (not (svex-envs-similar x y)))
  :rule-classes nil)

Theorem: svex-envs-similar-is-an-equivalence

(defthm svex-envs-similar-is-an-equivalence
  (and (booleanp (svex-envs-similar x y))
       (svex-envs-similar x x)
       (implies (svex-envs-similar x y)
                (svex-envs-similar y x))
       (implies (and (svex-envs-similar x y)
                     (svex-envs-similar y z))
                (svex-envs-similar x z)))
  :rule-classes (:equivalence))

Theorem: svex-envs-similar-implies-equal-svex-env-lookup-2

(defthm svex-envs-similar-implies-equal-svex-env-lookup-2
  (implies (svex-envs-similar x x-equiv)
           (equal (svex-env-lookup k x)
                  (svex-env-lookup k x-equiv)))
  :rule-classes (:congruence))

Theorem: svex-eval-env-congruence

(defthm svex-eval-env-congruence
  (implies (svex-envs-similar env env2)
           (equal (svex-eval x env)
                  (svex-eval x env2)))
  :rule-classes :congruence)

Theorem: svexlist-eval-env-congruence

(defthm svexlist-eval-env-congruence
  (implies (svex-envs-similar env env2)
           (equal (svexlist-eval x env)
                  (svexlist-eval x env2)))
  :rule-classes :congruence)

Theorem: svex-envs-similar-implies-equal-svex-alist-eval-2

(defthm svex-envs-similar-implies-equal-svex-alist-eval-2
  (implies (svex-envs-similar env env-equiv)
           (equal (svex-alist-eval x env)
                  (svex-alist-eval x env-equiv)))
  :rule-classes (:congruence))

Theorem: append-of-svex-env-fix-a-under-svex-env-equiv

(defthm acl2::append-of-svex-env-fix-a-under-svex-env-equiv
  (svex-env-equiv (append (svex-env-fix a) b)
                  (append a b)))

Theorem: append-svex-env-equiv-congruence-on-a-under-svex-env-equiv

(defthm
   acl2::append-svex-env-equiv-congruence-on-a-under-svex-env-equiv
  (implies (svex-env-equiv a acl2::a-equiv)
           (svex-env-equiv (append a b)
                           (append acl2::a-equiv b)))
  :rule-classes :congruence)

Theorem: append-of-svex-env-fix-b-under-svex-env-equiv

(defthm acl2::append-of-svex-env-fix-b-under-svex-env-equiv
  (svex-env-equiv (append a (svex-env-fix b))
                  (append a b)))

Theorem: append-svex-env-equiv-congruence-on-b-under-svex-env-equiv

(defthm
   acl2::append-svex-env-equiv-congruence-on-b-under-svex-env-equiv
  (implies (svex-env-equiv b acl2::b-equiv)
           (svex-env-equiv (append a b)
                           (append a acl2::b-equiv)))
  :rule-classes :congruence)

Theorem: svex-env-equiv-refines-svex-envs-similar

(defthm svex-env-equiv-refines-svex-envs-similar
  (implies (svex-env-equiv x y)
           (svex-envs-similar x y))
  :rule-classes (:refinement))

Theorem: svex-envs-similar-implies-equal-svex-env-extract-2

(defthm svex-envs-similar-implies-equal-svex-env-extract-2
  (implies (svex-envs-similar x x-equiv)
           (equal (svex-env-extract keys x)
                  (svex-env-extract keys x-equiv)))
  :rule-classes (:congruence))