Patrick Nicodemus (Jan 13 2022 at 18:27): Patrick Nicodemus (Jan 13 2022 at 18:27):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.
Théo Winterhalter (Jan 13 2022 at 18:31):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.
Patrick Nicodemus (Jan 13 2022 at 18:32):Interesting solution! Thanks!
Last updated: Oct 01 2023 at 19:01 UTC