• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
      • Maybe-stringp
      • Maybe-natp
      • Two-nats-measure
      • Impossible
      • Bytep
      • Nat-list-measure
      • Maybe-posp
      • Nibblep
      • Organize-symbols-by-pkg
      • Organize-symbols-by-name
      • Lnfix
      • Good-valuep
      • Streqv
      • Chareqv
      • Symbol-package-name-non-cl
      • Arith-equivs
        • Nat-equiv
          • Nats-equiv
        • Bit->bool
        • Bit-equiv
        • Int-equiv
        • Negp
        • Bool->bit
      • Induction-schemes
      • Maybe-integerp
      • Char-fix
      • Pos-fix
      • Symbol-package-name-lst
      • Mbt$
      • Maybe-bitp
      • Good-pseudo-termp
      • Str-fix
      • Maybe-string-fix
      • Nonkeyword-listp
      • Lifix
      • Bfix
      • Std/basic/if*
      • Impliez
      • Tuplep
      • Std/basic/intern-in-package-of-symbol
      • Lbfix
      • Std/basic/symbol-name-lst
      • True
      • Std/basic/rfix
      • Std/basic/realfix
      • Std/basic/member-symbol-name
      • Std/basic/fix
      • False
      • Std/basic/nfix
      • Std/basic/ifix
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/lists
• Nat-equiv

Nats-equiv

Recognizer for lists that are the same length and that are pairwise equivalent up to nfix.

Definitions and Theorems

Function: nats-equiv

(defun nats-equiv (x y)
  (if (and (atom x) (atom y))
      t
    (and (nat-equiv (car x) (car y))
         (nats-equiv (cdr x) (cdr y)))))

This is an equivalence relation:

Theorem: nats-equiv-is-an-equivalence

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

It is also a refinement of list-equiv:

Theorem: list-equiv-refines-nats-equiv

(defthm list-equiv-refines-nats-equiv
  (implies (list-equiv x y)
           (nats-equiv x y))
  :rule-classes (:refinement))

It also enjoys several basic congruences:

Theorem: nats-equiv-implies-nat-equiv-car-1

(defthm nats-equiv-implies-nat-equiv-car-1
  (implies (nats-equiv x x-equiv)
           (nat-equiv (car x) (car x-equiv)))
  :rule-classes (:congruence))

Theorem: nats-equiv-implies-nats-equiv-cdr-1

(defthm nats-equiv-implies-nats-equiv-cdr-1
  (implies (nats-equiv x x-equiv)
           (nats-equiv (cdr x) (cdr x-equiv)))
  :rule-classes (:congruence))

Theorem: nats-equiv-implies-nats-equiv-cons-2

(defthm nats-equiv-implies-nats-equiv-cons-2
  (implies (nats-equiv x x-equiv)
           (nats-equiv (cons a x)
                       (cons a x-equiv)))
  :rule-classes (:congruence))

Theorem: nats-equiv-of-cons

(defthm nats-equiv-of-cons
  (equal (nats-equiv (cons a x) z)
         (and (nat-equiv a (car z))
              (nats-equiv x (cdr z)))))

Theorem: nats-equiv-implies-nat-equiv-nth-2

(defthm nats-equiv-implies-nat-equiv-nth-2
  (implies (nats-equiv x x-equiv)
           (nat-equiv (nth n x) (nth n x-equiv)))
  :rule-classes (:congruence))

Theorem: nats-equiv-implies-nats-equiv-update-nth-3

(defthm nats-equiv-implies-nats-equiv-update-nth-3
  (implies (nats-equiv x x-equiv)
           (nats-equiv (update-nth n v x)
                       (update-nth n v x-equiv)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-nats-equiv-update-nth-2

(defthm nat-equiv-implies-nats-equiv-update-nth-2
  (implies (nat-equiv v v-equiv)
           (nats-equiv (update-nth n v x)
                       (update-nth n v-equiv x)))
  :rule-classes (:congruence))

Theorem: nats-equiv-implies-nats-equiv-append-2

(defthm nats-equiv-implies-nats-equiv-append-2
  (implies (nats-equiv y y-equiv)
           (nats-equiv (append x y)
                       (append x y-equiv)))
  :rule-classes (:congruence))

Theorem: nats-equiv-implies-nats-equiv-revappend-2

(defthm nats-equiv-implies-nats-equiv-revappend-2
  (implies (nats-equiv y y-equiv)
           (nats-equiv (revappend x y)
                       (revappend x y-equiv)))
  :rule-classes (:congruence))

Theorem: nats-equiv-implies-nats-equiv-take-2

(defthm nats-equiv-implies-nats-equiv-take-2
  (implies (nats-equiv x x-equiv)
           (nats-equiv (take n x)
                       (take n x-equiv)))
  :rule-classes (:congruence))

Theorem: nats-equiv-implies-nats-equiv-nthcdr-2

(defthm nats-equiv-implies-nats-equiv-nthcdr-2
  (implies (nats-equiv x x-equiv)
           (nats-equiv (nthcdr n x)
                       (nthcdr n x-equiv)))
  :rule-classes (:congruence))

Theorem: nats-equiv-implies-nats-equiv-make-list-ac-3

(defthm nats-equiv-implies-nats-equiv-make-list-ac-3
  (implies (nats-equiv ac ac-equiv)
           (nats-equiv (make-list-ac n val ac)
                       (make-list-ac n val ac-equiv)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-nats-equiv-replicate-2

(defthm nat-equiv-implies-nats-equiv-replicate-2
  (implies (nat-equiv x x-equiv)
           (nats-equiv (replicate n x)
                       (replicate n x-equiv)))
  :rule-classes (:congruence))