Stream: Coq users

Topic: Avoiding loops with auto

Patrick Nicodemus (Sep 24 2022 at 03:09):

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?

Patrick Nicodemus (Sep 24 2022 at 03:14):

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.

Patrick Nicodemus (Sep 24 2022 at 03:16):

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.

Karl Palmskog (Sep 24 2022 at 08:28):

if it's 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.

Paolo Giarrusso (Sep 24 2022 at 11:14):

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 trivial and done

Paolo Giarrusso (Sep 24 2022 at 11:14):

FWIW, I'm not sure if (e)auto is actually discouraged, I just never saw it in use

Paolo Giarrusso (Sep 24 2022 at 11:16):

Viceversa, if you're building fancy enough automation, using ltnW as a "forward hint" on hypotheses is perfectly fine.

Paolo Giarrusso (Sep 24 2022 at 11:18):

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

Paolo Giarrusso (Sep 24 2022 at 11:20):

I'm probably biased by working mostly with unbounded typeclass search and not relying on eauto's limits, but limits don't really compose.

Paolo Giarrusso (Sep 24 2022 at 11:22):

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.

Paolo Giarrusso (Sep 24 2022 at 11:28):

@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:

1. (typeclasses) eauto can use Hint Cut, which isn't inspired by Prolog's cut and lets you say some such things to eauto; it might help if you're rewriting in hint externs (which sounds fragile to me), but I suspect you'd need named hint externs.
2. Autorewrite supports no such thing, but rewrite_strat supports more expressive "rewrite strategies". rewrite_strat is also pretty buggy and/underdocumented, but I've seen at least two uses that worked at all (tho both were replaced with better tools).

Last updated: Oct 13 2024 at 01:02 UTC