search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.85k stars 649 forks source link

Hint Cut in auto and eauto #19580

Open radrow opened 1 month ago

radrow commented 1 month ago

Is your feature request related to a problem?

I think there is little to explain. My hints are quite abundant and often the proof search repeats nodes in search paths. Additionally, I often get hit by the diamond problem where for example given A -> B, B -> C and A -> C with no proof for A, leads to A being attempted twice while proving C. This explodes quite quickly leading to massive and pointless waste of time. This situation happens to me very commonly when I use "alias" or "wrapper" predicates, often for hiding exists behind blackboxes.

Hint Immediate does not always solve the problem, because those paths can get longer, and predicates may have parameters generalized to different extents. With Hint Immediate I would either have to give up on many only-valid search paths, or force myself to manually chain resolution with immediates.

Proposed solution

Add an option to apply Hint Cut (or equivalent) for auto and eauto. For example, the diamond problem above could be optimized by banning [ ( _ * ) C ( _ * ) B ( _ * ) A ] (insert hint names) since you can always show C from A without need of exploring B.

Alternative solutions

An option to mark hints as checkpoints, so their results can be cached?

Additional context

I couldn't find anyone requesting that, though I find it hard to believe I am the first one

mrhaandi commented 1 month ago

As a heavy auto user myself, I have good experience using Hint Extern for better guidance. This way, one can specify what happens on expected patterns.

Zimmi48 commented 1 month ago

The recommended solution is generally to use typeclasses eauto with <hint db name> as a replacement for auto / eauto. Is there something preventing you from doing that? (Note that there are some discrepancies, as this PR #721 trying to replace the implementation of auto and eauto by the one of typeclasses eauto confirmed.)

radrow commented 1 month ago

One reason is that I don't always want evars to be involved. Another thing is that, as far as I understand, typeclasses eauto runs in proof mode which would slow it down (correct me if I am wrong).

Zimmi48 commented 1 month ago

One reason is that I don't always want evars to be involved.

Indeed, one of my main regrets with #721 is not having extracted valuable pieces like a mode to run typeclasses eauto with the behavior of auto.

Another thing is that, as far as I understand, typeclasses eauto runs in proof mode which would slow it down (correct me if I am wrong).

Not sure what is meant here.