• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
        • Equal-by-nths
          • Equal-by-nths-hint
      • 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/nth
• Nth

Equal-by-nths

Proof technique: show two lists are equal by showing that their nth elements are always the same.

This is a powerful rule that can be functionally instantiated to prove that two lists are equal when their nth elements are always the same. The theorem to instantiate is:

Theorem: equal-by-nths

(defthm equal-by-nths
        (implies (and (equal-by-nths-hyp)
                      (true-listp (equal-by-nths-lhs))
                      (true-listp (equal-by-nths-rhs)))
                 (equal (equal (equal-by-nths-lhs)
                               (equal-by-nths-rhs))
                        (equal (len (equal-by-nths-lhs))
                               (len (equal-by-nths-rhs))))))

Where the hyp, lhs, and rhs must satisfy the encapsulated constraint, essentially that the nth element of lhs is always the same as the nth element of rhs when the hyp is satisfied:

Definition: equal-by-nths-hyp

(encapsulate
     (((equal-by-nths-hyp) => *)
      ((equal-by-nths-lhs) => *)
      ((equal-by-nths-rhs) => *))
     (local (value-triple :elided))
     (local (value-triple :elided))
     (local (value-triple :elided))
     (defthmd equal-by-nths-constraint
              (implies (and (equal-by-nths-hyp)
                            (natp n)
                            (< n (len (equal-by-nths-lhs))))
                       (equal (nth n (equal-by-nths-lhs))
                              (nth n (equal-by-nths-rhs))))))

For some bare-bones automation, see also equal-by-nths-hint.

Subtopics

Equal-by-nths-hint

A computed-hint that automates basic applications of equal-by-nths.