• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
          • 4v-sexpr-alist-equiv
          • 4v-env-equiv
          • 4v-sexpr-list-equiv
          • 4v-sexpr-equiv
          • 4v-alists-agree
          • Key-and-env-equiv
          • 4v-sexpr-alist-equiv-alt
          • 4v-sexpr-alist-pair-equiv
          • 4v-cdr-consp-equiv
          • 4v-cdr-equiv
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Sexpr-equivs

4v-sexpr-list-equiv

X === Y in the sense of sexpr lists if they are equal lengths and Xi evaluates to the same thing as Yi for all i and for all environments.

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

Function: 4v-sexpr-list-equiv

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

Definitions and Theorems

Theorem: 4v-sexpr-list-equiv-necc

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

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

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

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

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

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

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

Theorem: 4v-sexpr-list-equiv-alt-def

(defthm 4v-sexpr-list-equiv-alt-def
        (equal (4v-sexpr-list-equiv x y)
               (if (atom x)
                   (atom y)
                   (and (consp y)
                        (4v-sexpr-equiv (car x) (car y))
                        (4v-sexpr-list-equiv (cdr x) (cdr y)))))
        :rule-classes :definition)

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

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

Theorem: 4v-sexpr-list-equiv-implies-4v-sexpr-equiv-cons-2

(defthm 4v-sexpr-list-equiv-implies-4v-sexpr-equiv-cons-2
        (implies (4v-sexpr-list-equiv a a-equiv)
                 (4v-sexpr-equiv (cons x a)
                                 (cons x a-equiv)))
        :rule-classes (:congruence))

Theorem: 4v-sexpr-equiv-implies-4v-sexpr-list-equiv-cons-1

(defthm 4v-sexpr-equiv-implies-4v-sexpr-list-equiv-cons-1
        (implies (4v-sexpr-equiv a a-equiv)
                 (4v-sexpr-list-equiv (cons a b)
                                      (cons a-equiv b)))
        :rule-classes (:congruence))

Theorem: 4v-sexpr-list-equiv-implies-4v-sexpr-list-equiv-cons-2

(defthm 4v-sexpr-list-equiv-implies-4v-sexpr-list-equiv-cons-2
        (implies (4v-sexpr-list-equiv b b-equiv)
                 (4v-sexpr-list-equiv (cons a b)
                                      (cons a b-equiv)))
        :rule-classes (:congruence))