Subtleties of :type prescription rules - acl2/acl2 GitHub Wiki

Taken from a conversation between Rager and Kaufmann. This should probably be made into a :doc topic at some point (and we should also check that it isn't covered already).

Rager says:

I have a simple type rule that when converted to a :type-prescription rule causes some of my high-level proofs to go out to lunch. My question is: do you think I should care why? In general it seems like type-prescription rules work well -- should I bother to learn the reason that the type-prescription rule is failing to be used in this case? Would such knowledge help me in future proofs?

Here's the rule:

(defrule ash-natp-type :short "Ash returns a natp when given a natp for x" (implies (natp x) (natp (ash x y))))

BTW, natp is disabled.

Matt says:

That's a good question, but I'm not sure I have a particularly good (complete) answer. Here are some thoughts. It might be helpful for you to send the question to acl2-help. Feel free to include my reply if you like, in case it triggers a helpful thought in someone.

I'm assuming from your wording that "out to lunch" is being caused because rules are no longer being applied. If "out to lunch" is instead caused by excessive application of type-prescription rules, that's another story.

I think it's a good goal to use a type-prescription rule here, since there might be cases where knowing (natp (ash x y)) is helpful but no natp call is present. In particular, this could happen when linear arithmetic cares whether (ash x y) is rational.

One thing you could do -- I think I often have done this -- is to force hypotheses on such type-prescription rules, IF you believe that they'll always be true. Of course (ash x y) might occur where you've only assumed (integerp x), say, and then the forced hypothesis wouldn't be provable. But I'm guessing that you're dealing with natural numbers, in which case forcing (natp x) might be good.

The reason forcing could help is that you might have other natp rules around that aren't type-prescription rules. For example, suppose we have this rule, natp-foo:

(natp (foo x))

Now suppose ACL2 encounters the term (ash (foo a) b). With your new type-prescription rule ash-natp-type, the hypothesis (natp (foo a)) would need to be relieved using only type-set reasoning, not rewriting. If natp-foo is a type-prescription rule, it will be used to relieve that hypothesis, but not if natp-foo is a rewrite rule.

Suppose natp-foo is a rewrite rule and you haven't yet discovered why ash-natp-type fails to fire. If you instead had this (pardon the probably-bad syntax)

(defrule ash-natp-type :short "Ash returns a natp when given a natp for x" (implies (force (natp x)) (natp (ash x y))) :rule-classes :type-prescription)

then natp-foo would apply in the forcing round. When you see that happen, you can say "OOOOH, let's make natp-foo a :type-prescription rule", and maybe then you won't even need the FORCE call above.

Rager says:

Great answer. I suspect this is the underlying cause of my "problem":

"The reason forcing could help is that you might have other natp rules around that aren't type-prescription rules."

In your response, was the following a typo? I thought the point was that without the force, the rule wouldn't be able to apply.

"and maybe then you won't even need the FORCE call above."

Matt says:

Nope, that wasn't a typo. My point was that once you decide to make natp-foo a type-prescription rule, it will be used in relieving the hypothesis of ash-natp-type in the manner I described, avoiding the creation of a forcing round to deal with that. Does that make sense?

Rager says:

The moral of the story is: always make natp rules have at least the :type-prescription rule class (also having them as rewrite rules may not hurt too much)!

This will be good, as I can go through and search my codebase for natp rules that aren't type-prescription rules.