ACL2 and unification during rewrite - acl2/acl2 GitHub Wiki

What to do when ACL2 picks the wrong substitution

#Introduction

Often ACL2 will pick a substitution scheme for your rewrite rule that allows it to be used in your proof attempt. That being said, sometimes ACL2 will pick a substitution for your rewrite rule that prevents the rewrite rule from being used in your proof attempt, because the hypotheses of the rewrite rule can't be relieved under the chosen substitution (but they could be relieved under another substitution). Automatically picking the "right" substitution is difficult and a long-studied research topic.

This topic describes the options available for guiding ACL2 to an effective substitution.

Please edit this and make it better

#Details

Here are some possible solutions I've found:

  • Provide a :use hint. This will often work but due to the reasons I mentioned in the "Gotchas" section of https://code.google.com/p/acl2-books/wiki/TipsAndTricksForACL2 , isn't fool proof. Also, if the substitutions are long, then the :use hint is also long.

  • Create a lemma that contains an instance of the rewrite rule with enough information so that ACL2 will pick the right substitutions. For example, suppose ACL2 couldn't prove:

(implies (equal (foo (binary-* x 7)) (bar (binary-* y 10))) 
         (equal (+ (foo (binary-* x 7)) (bar (binary-* y 10)))
                (binary-* 2 (foo (binary-* x 7))))

and if for whatever reason ACL2 instantiates the rewrite rule (in practice, I doubt this would occur in this particular example, but it makes the point)

(implies (equal a b) 
         (equal (+ a b)
                (binary-* 2 a))

as

(implies (equal (bar (binary-* y 10)) (foo (binary-* x 7)))
                (equal (+ (bar (binary-* y 10)) (foo (binary-* x 7)))
                       (* 2 (bar (binary-* y 10)))))

then your conclusion will be about (bar (binary-* y 10)), not (foo (binary-* x 7)). But that isn't what you want. So, you can prove a lemma that looks like the following, and ACL2 will be "guided" towards picking better substitutions, because it must match the calls of foo and bar.

(implies (equal (foo a) (bar b))
                (equal (+ (foo a) (bar b))
                       (binary-* 2 (foo a)))))

  • Consider using syntaxp and mfc-rw together. I don't quite understand this idea yet

  • Use bind-free. There's some trick for making free variables, even when there aren't free variables in the formula, which would allow one to use bind-free. I don't understand that trick yet, either.