This is a general design question which i'm sure comes up all the time on this forum.
When trying to automate or script proofs, what are some of the best ways to stop from repeated application of the same theorems many times in a row? For example the lemma
ltnW : S n <= m -> n <= m in the SSReflect library (and in the core hint database)
can be applied repeatedly. Therefore if I inspect "debug auto" on an inequality, the proof tree tends to have almost all of the steps be 'apply ltnW" at any given point. What is a good way to get around this problem?
A complementary question - Suppose I have an equation
Lemma my_eq1 : A = B, sometimes I want to run
rewrite -> my_eq1 and sometimes
rewrite <- my_eq1. Is there a way to tell
auto, "Don't try
rewrite -> my_eq1 if `rewrite <- my_eq1' has been tried above this node in the proof tree.
It doesn't have to be directly a question about auto, I think in general i'm asking what the easiest/most common techniques are in recursive proof search for the parent function to pass supplementary information to the child when it calls it.
auto, you can manually set the depth of
auto. For rewrites, you can manually set the number of times to rewrite (ssreflect encourages this). I don't think there's a general solution here, there is no way to know beforehand how many times you want to apply or rewrite something.
To me, the basic design principle is to not make ltnW a backwards hint, since it's not "structurally recursive"; I suspect ssreflect only does it because they don't really use
auto, and it's fine for
FWIW, I'm not sure if (e)auto is actually discouraged, I just never saw it in use
Viceversa, if you're building fancy enough automation, using ltnW as a "forward hint" on hypotheses is perfectly fine.
In both cases, the point is that hints that decrease context size won't cause loops on their own; in general, you can think about termination of proof search similarly to how you think about termination of functional programs, using fancier termination metrics etc
I'm probably biased by working mostly with unbounded typeclass search and not relying on eauto's limits, but limits don't really compose.
Also, using ltnW "inversely" has the advantage of being syntax-directed: the number of applications is limited by occurrences of S in the goal/hypothesis that you're simplifying, which means automation can be fairly predictable.
@Patrick Nicodemus on your second question, I don't know an answer but I know two somewhat related tools. There isn't an immediate way to deploy them, but I don't think there's an easy answer doing all you want:
Last updated: Oct 03 2023 at 20:01 UTC