• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
      • Lispfloat
      • Arithmetic-1
      • Number-theory
      • Proof-by-arith
      • Arith-equivs
        • Nat-equiv
          • Nats-equiv
        • Bit->bool
        • Bit-equiv
        • Int-equiv
        • Negp
        • Bool->bit
      • Include-an-arithmetic-book
      • Number-theory
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra
  • 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))