		Search-engine friendly clone of the ACL2 documentation.

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