• 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-alist-equiv

X === Y in the sense of sexpr alists if X[k] === Y[k] in the sense of sexprs for all keys k.

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

Function: 4v-sexpr-alist-equiv

(defun
 4v-sexpr-alist-equiv (x y)
 (declare (xargs :non-executable t))
 (declare (xargs :guard t))
 (declare (xargs :non-executable t))
 (prog2$ (throw-nonexec-error '4v-sexpr-alist-equiv
                              (list x y))
         (let ((k (4v-sexpr-alist-equiv-witness x y)))
              (and (iff (hons-assoc-equal k x)
                        (hons-assoc-equal k y))
                   (4v-sexpr-equiv (cdr (hons-assoc-equal k x))
                                   (cdr (hons-assoc-equal k y)))))))

Definitions and Theorems

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

(defthm
  4v-sexpr-alist-equiv-necc
  (implies (not (and (iff (hons-assoc-equal k x)
                          (hons-assoc-equal k y))
                     (4v-sexpr-equiv (cdr (hons-assoc-equal k x))
                                     (cdr (hons-assoc-equal k y)))))
           (not (4v-sexpr-alist-equiv x y))))

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

(defthm
 4v-sexpr-alist-equiv-witnessing-witness-rule-correct
 (implies
  (not
     ((lambda (k y x)
              (not (if (iff (hons-assoc-equal k x)
                            (hons-assoc-equal k y))
                       (4v-sexpr-equiv (cdr (hons-assoc-equal k x))
                                       (cdr (hons-assoc-equal k y)))
                       'nil)))
      (4v-sexpr-alist-equiv-witness x y)
      y x))
  (4v-sexpr-alist-equiv x y))
 :rule-classes nil)

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

(defthm
     4v-sexpr-alist-equiv-instancing-instance-rule-correct
     (implies (not (if (iff (hons-assoc-equal k x)
                            (hons-assoc-equal k y))
                       (4v-sexpr-equiv (cdr (hons-assoc-equal k x))
                                       (cdr (hons-assoc-equal k y)))
                       'nil))
              (not (4v-sexpr-alist-equiv x y)))
     :rule-classes nil)

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

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

Theorem: alist-equiv-refines-4v-sexpr-alist-equiv

(defthm alist-equiv-refines-4v-sexpr-alist-equiv
        (implies (alist-equiv x y)
                 (4v-sexpr-alist-equiv x y))
        :rule-classes (:refinement))

Theorem: 4v-sexpr-alist-equiv-refines-keys-equiv

(defthm 4v-sexpr-alist-equiv-refines-keys-equiv
        (implies (4v-sexpr-alist-equiv x y)
                 (keys-equiv x y))
        :rule-classes (:refinement))

Theorem: 4v-sexpr-alist-pair-equiv-implies-4v-sexpr-alist-equiv-cons-1

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

Theorem: 4v-sexpr-alist-equiv-implies-4v-sexpr-alist-pair-equiv-hons-assoc-equal-2

(defthm
 4v-sexpr-alist-equiv-implies-4v-sexpr-alist-pair-equiv-hons-assoc-equal-2
 (implies (4v-sexpr-alist-equiv al al-equiv)
          (4v-sexpr-alist-pair-equiv (hons-assoc-equal x al)
                                     (hons-assoc-equal x al-equiv)))
 :rule-classes (:congruence))

Theorem: 4v-sexpr-equiv-cdr-hons-assoc-equal-when-4v-sexpr-alist-equiv

(defthm
     4v-sexpr-equiv-cdr-hons-assoc-equal-when-4v-sexpr-alist-equiv
     (implies (and (4v-sexpr-alist-equiv a b)
                   (syntaxp (and (term-order a b)
                                 (not (equal a b)))))
              (4v-sexpr-equiv (cdr (hons-assoc-equal k a))
                              (cdr (hons-assoc-equal k b)))))

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

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

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

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

Theorem: 4v-sexpr-equiv-implies-4v-sexpr-alist-equiv-acons-2

(defthm 4v-sexpr-equiv-implies-4v-sexpr-alist-equiv-acons-2
        (implies (4v-sexpr-equiv b b-equiv)
                 (4v-sexpr-alist-equiv (acons a b c)
                                       (acons a b-equiv c)))
        :rule-classes (:congruence))

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

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

Theorem: 4v-sexpr-alist-equiv-implies-4v-sexpr-alist-equiv-append-1

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

Theorem: 4v-sexpr-alist-equiv-implies-4v-sexpr-alist-equiv-append-2

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

Theorem: 4v-sexpr-alist-equiv-implies-4v-sexpr-equiv-4v-sexpr-restrict-2

(defthm
     4v-sexpr-alist-equiv-implies-4v-sexpr-equiv-4v-sexpr-restrict-2
     (implies (4v-sexpr-alist-equiv al1 al2)
              (4v-sexpr-equiv (4v-sexpr-restrict x al1)
                              (4v-sexpr-restrict x al2)))
     :rule-classes :congruence)

Theorem: 4v-sexpr-alist-equiv-implies-4v-sexpr-list-equiv-4v-sexpr-restrict-list-2

(defthm
 4v-sexpr-alist-equiv-implies-4v-sexpr-list-equiv-4v-sexpr-restrict-list-2
 (implies (4v-sexpr-alist-equiv al1 al2)
          (4v-sexpr-list-equiv (4v-sexpr-restrict-list x al1)
                               (4v-sexpr-restrict-list x al2)))
 :rule-classes :congruence)

Theorem: 4v-sexpr-alist-equiv-implies-4v-env-equiv-4v-sexpr-eval-alist-1

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

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

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

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

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

Theorem: 4v-sexpr-alist-equiv-alt-necc

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

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

(defthm
 4v-sexpr-alist-equiv-alt-witnessing-witness-rule-correct
 (implies
   (not ((lambda (env y x)
                 (not (if (keys-equiv x y)
                          (4v-env-equiv (4v-sexpr-eval-alist x env)
                                        (4v-sexpr-eval-alist y env))
                          'nil)))
         (4v-sexpr-alist-equiv-alt-witness x y)
         y x))
   (4v-sexpr-alist-equiv-alt x y))
 :rule-classes nil)

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

(defthm 4v-sexpr-alist-equiv-alt-instancing-instance-rule-correct
        (implies (not (if (keys-equiv x y)
                          (4v-env-equiv (4v-sexpr-eval-alist x env)
                                        (4v-sexpr-eval-alist y env))
                          'nil))
                 (not (4v-sexpr-alist-equiv-alt x y)))
        :rule-classes nil)

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

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

Theorem: 4v-sexpr-alist-equiv-is-alt

(defthm 4v-sexpr-alist-equiv-is-alt
        (iff (4v-sexpr-alist-equiv a b)
             (4v-sexpr-alist-equiv-alt a b)))

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

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

Theorem: 4v-sexpr-alist-equiv-implies-4v-sexpr-alist-equiv-4v-sexpr-restrict-alist-2

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

Theorem: 4v-sexpr-alist-equiv-implies-4v-sexpr-alist-equiv-4v-sexpr-alist-extract-2

(defthm
 4v-sexpr-alist-equiv-implies-4v-sexpr-alist-equiv-4v-sexpr-alist-extract-2
 (implies
      (4v-sexpr-alist-equiv al al-equiv)
      (4v-sexpr-alist-equiv (4v-sexpr-alist-extract keys al)
                            (4v-sexpr-alist-extract keys al-equiv)))
 :rule-classes (:congruence))