Auto does not change the goal when it fails to solve it completely. Are there any alternate tactics which do basically the same thing as auto, but which change the goal as much as they can before giving up?
My imagined use case is something like this - there are certain goals i have where i know i always want to perform a certain step, there's no other choice I would make, so I always want that step to be taken, and I would create a database with these special goals where the proof step is uniquely determined. In that case I wouldn't want auto to backtrack and undo the work when it succeeds.
My current solution is just to put all of these in a big "repeat match goal" but I would like to know if there's a better way.
Here is what I did after asking a similar question here: https://github.com/SSProve/ssprove/blob/main/theories/Crypt/package/pkg_tactics.v#L339
#[export] Hint Extern 100 => shelve : ssprove_valid_db. Ltac ssprove_valid := (unshelve typeclasses eauto with ssprove_valid_db) ; shelve_unifiable.
The idea is that it will "succeed" by shelving the goal, so afterward you
unshelve what has been shelved.
Interesting solution! Thanks!
Last updated: Jan 27 2023 at 02:04 UTC