• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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))