		Search-engine friendly clone of the ACL2 documentation.

Sexpr-equivs

4v-sexpr-equiv

X === Y in the sense of sexprs if they always evaluate to the same thing under any possible environment.

This is a universal equivalence, introduced using def-universal-equiv.

Function: 4v-sexpr-equiv

(defun 4v-sexpr-equiv (x y)
       (declare (xargs :non-executable t))
       (declare (xargs :guard t))
       (declare (xargs :non-executable t))
       (prog2$ (throw-nonexec-error '4v-sexpr-equiv
                                    (list x y))
               (let ((env (4v-sexpr-equiv-witness x y)))
                    (and (equal (4v-sexpr-eval x env)
                                (4v-sexpr-eval y env))))))

Definitions and Theorems

Theorem: 4v-sexpr-equiv-necc

(defthm 4v-sexpr-equiv-necc
        (implies (not (and (equal (4v-sexpr-eval x env)
                                  (4v-sexpr-eval y env))))
                 (not (4v-sexpr-equiv x y))))

Theorem: 4v-sexpr-equiv-witnessing-witness-rule-correct

(defthm 4v-sexpr-equiv-witnessing-witness-rule-correct
        (implies (not ((lambda (env y x)
                               (not (equal (4v-sexpr-eval x env)
                                           (4v-sexpr-eval y env))))
                       (4v-sexpr-equiv-witness x y)
                       y x))
                 (4v-sexpr-equiv x y))
        :rule-classes nil)

Theorem: 4v-sexpr-equiv-instancing-instance-rule-correct

(defthm 4v-sexpr-equiv-instancing-instance-rule-correct
        (implies (not (equal (4v-sexpr-eval x env)
                             (4v-sexpr-eval y env)))
                 (not (4v-sexpr-equiv x y)))
        :rule-classes nil)

Theorem: 4v-sexpr-equiv-is-an-equivalence

(defthm 4v-sexpr-equiv-is-an-equivalence
        (and (booleanp (4v-sexpr-equiv x y))
             (4v-sexpr-equiv x x)
             (implies (4v-sexpr-equiv x y)
                      (4v-sexpr-equiv y x))
             (implies (and (4v-sexpr-equiv x y)
                           (4v-sexpr-equiv y z))
                      (4v-sexpr-equiv x z)))
        :rule-classes (:equivalence))

Theorem: 4v-sexpr-equiv-implies-equal-4v-sexpr-eval-1

(defthm 4v-sexpr-equiv-implies-equal-4v-sexpr-eval-1
        (implies (4v-sexpr-equiv x x-equiv)
                 (equal (4v-sexpr-eval x env)
                        (4v-sexpr-eval x-equiv env)))
        :rule-classes (:congruence))

Theorem: 4v-sexpr-equiv-implies-iff-4v-sexpr-<=-2

(defthm 4v-sexpr-equiv-implies-iff-4v-sexpr-<=-2
        (implies (4v-sexpr-equiv b b-equiv)
                 (iff (4v-sexpr-<= a b)
                      (4v-sexpr-<= a b-equiv)))
        :rule-classes (:congruence))

Theorem: 4v-sexpr-equiv-implies-iff-4v-sexpr-<=-1

(defthm 4v-sexpr-equiv-implies-iff-4v-sexpr-<=-1
        (implies (4v-sexpr-equiv a a-equiv)
                 (iff (4v-sexpr-<= a b)
                      (4v-sexpr-<= a-equiv b)))
        :rule-classes (:congruence))

Theorem: 4v-sexpr-equiv-implies-4v-sexpr-equiv-4v-sexpr-restrict-1

(defthm 4v-sexpr-equiv-implies-4v-sexpr-equiv-4v-sexpr-restrict-1
        (implies (4v-sexpr-equiv x x-equiv)
                 (4v-sexpr-equiv (4v-sexpr-restrict x al)
                                 (4v-sexpr-restrict x-equiv al)))
        :rule-classes (:congruence))

Theorem: 4v-sexpr-equiv-implies-4v-sexpr-equiv-4v-sexpr-compose-1

(defthm 4v-sexpr-equiv-implies-4v-sexpr-equiv-4v-sexpr-compose-1
        (implies (4v-sexpr-equiv x x-equiv)
                 (4v-sexpr-equiv (4v-sexpr-compose x al)
                                 (4v-sexpr-compose x-equiv al)))
        :rule-classes (:congruence))