		Search-engine friendly clone of the ACL2 documentation.

Proof-automation

Rewrite-equiv-hint

A hint to induce ACL2 to perform substitutions using equivalence relations from the hypothesis

Rewrite-equiv-hint is a clause-processor hint that leverages rewrite-equiv to induce ACL2 to perform substitution using equivalence relations in the hypothesis. (rewrite-equiv-hint equiv) will apply rewrite-equiv to any equivalence relation involving equiv appearing in the hypothesis. Without an argument, (rewrite-equiv-hint), it will apply rewrite-equiv to any equality in the hypothesis.

Example Usage:

(include-book "coi/util/rewrite-equiv" :dir :system)

(defstub foo (x) nil)
(defstub goo (x) nil)
(defstub hoo (x) nil)

(encapsulate
 (
  ((fred *) => *)
  )

 (local
  (defun fred (x)
    (declare (ignore x))
    t))

 (defthm fred-goo
   (fred (+ 3 (goo x))))

 )

 (defun equiv (x y) (equal x y))
 
 (defequiv equiv)
 
 (defcong equiv equal (fred x) 1)
 
 (defcong equiv equal (binary-+ x y) 1)
 
 (defcong equiv equal (binary-+ x y) 2)
 
 (in-theory (disable equiv))

;;
;; This theorem does not prove without rewrite-equiv-hint ..
;;
(defthm simple-example
  (implies
   (and
    (integerp x)
    (equiv (foo x) (goo x))
    (equiv (hoo x) (+ 3 (foo x))))
   (fred (hoo x)))
  :hints ((rewrite-equiv-hint equiv)))