• 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
    • Equal-by-nths

    Equal-by-nths-hint

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

    This is a computed hint that looks for goals of the form

    (implies (and hyp1 ... hypN) (equal lhs rhs))

    If the goal has the right form, we functionally instantiate equal-by-nths with the hyps, lhs, and rhs above, which should effectively reduce the goal to showing that the nth element of lhs and rhs are always the same, and that their length is the same.

    Typical usage would be something like:

    (defthm foo ... :hints((equal-by-nths-hint)))

    or perhaps:

    (defthm foo ... :hints((and stable-under-simplificationp
                                (equal-by-nths-hint))))

    Definitions and Theorems

    Function: equal-by-nths-hint-fn

    (defun
     equal-by-nths-hint-fn (clause)
     (b*
      ((lit (car (last clause)))
       ((unless (and (consp lit) (eq (car lit) 'equal)))
        nil)
       (hyps (dumb-negate-lit-lst (butlast clause 1)))
       ((list x y) (cdr lit)))
      (cons
       ':use
       (cons
        (cons
         (cons
          ':functional-instance
          (cons
           'equal-by-nths
           (cons
            (cons 'equal-by-nths-lhs
                  (cons (cons 'lambda (cons 'nil (cons x 'nil)))
                        'nil))
            (cons
             (cons 'equal-by-nths-rhs
                   (cons (cons 'lambda (cons 'nil (cons y 'nil)))
                         'nil))
             (cons
                  (cons 'equal-by-nths-hyp
                        (cons (cons 'lambda
                                    (cons 'nil
                                          (cons (cons 'and hyps) 'nil)))
                              'nil))
                  'nil)))))
         'nil)
        'nil))))