• Top
  • Documentation
  • Books
  • 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
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • 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
      • Std/lists/add-to-set
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • 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

All-equalp

(all-equalp a x) determines if every member of x is equal to a.

Signature

(all-equalp a x) → *

In the logic, we define all-equalp in terms of repeat.

We usually leave this enabled and prefer to reason about repeat instead. On the other hand, we also sometimes disable it and reason about it recursively, so we do prove a few theorems about it.

For better execution speed, we use a recursive definition that does no consing.

Function: all-equalp

(defun all-equalp (a x)
  (declare (xargs :guard t))
  (let ((__function__ 'all-equalp))
    (declare (ignorable __function__))
    (mbe :logic
         (equal (list-fix x) (repeat (len x) a))
         :exec
         (if (consp x)
             (and (equal a (car x))
                  (all-equalp a (cdr x)))
           t))))

Definitions and Theorems

Theorem: all-equalp-when-atom

(defthm all-equalp-when-atom
  (implies (atom x) (all-equalp a x)))

Theorem: all-equalp-of-cons

(defthm all-equalp-of-cons
  (equal (all-equalp a (cons b x))
         (and (equal a b) (all-equalp a x))))

Theorem: car-when-all-equalp

(defthm car-when-all-equalp
  (implies (all-equalp a x)
           (equal (car x) (if (consp x) a nil)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: all-equalp-of-cdr-when-all-equalp

(defthm all-equalp-of-cdr-when-all-equalp
  (implies (all-equalp a x)
           (all-equalp a (cdr x))))

Theorem: member-equal-when-all-equalp

(defthm member-equal-when-all-equalp
  (implies (all-equalp a x)
           (iff (member-equal b x)
                (and (consp x) (equal a b)))))

Theorem: all-equalp-by-superset

(defthm all-equalp-by-superset
  (implies (and (all-equalp a y)
                (subsetp-equal x y))
           (all-equalp a x)))

Theorem: set-equiv-implies-equal-all-equalp-2

(defthm set-equiv-implies-equal-all-equalp-2
  (implies (set-equiv x x-equiv)
           (equal (all-equalp a x)
                  (all-equalp a x-equiv)))
  :rule-classes (:congruence))

Theorem: all-equalp-of-append

(defthm all-equalp-of-append
  (equal (all-equalp a (append x y))
         (and (all-equalp a x)
              (all-equalp a y))))

Theorem: all-equalp-of-list-fix

(defthm all-equalp-of-list-fix
  (equal (all-equalp a (list-fix x))
         (all-equalp a x)))

Theorem: all-equalp-of-rev

(defthm all-equalp-of-rev
  (equal (all-equalp a (rev x))
         (all-equalp a x)))

Theorem: all-equalp-of-repeat

(defthm all-equalp-of-repeat
  (equal (all-equalp a (repeat n b))
         (or (equal a b) (zp n))))

Theorem: all-equalp-of-take

(defthm all-equalp-of-take
  (implies (all-equalp a x)
           (equal (all-equalp a (take n x))
                  (or (not a) (<= (nfix n) (len x))))))

Theorem: all-equalp-of-nthcdr

(defthm all-equalp-of-nthcdr
  (implies (all-equalp a x)
           (all-equalp a (nthcdr n x))))