I'm trying to automate some proofs, I'm using a
repeat (match goal with ...) loop but want to use hints instead, my problem is that auto will restore the goal if it can't completely proove it and I'm looking for something that goes as far as possible but leave the remaining goals so I can finish it manually. Is there any tatic like auto but that doesn't restore the goal when one of the subgoals fails?
One trick is to use auto with a Hint Extern that shelves the goal. I.e. something like
Local Hint Extern 1000 => shelve : test_db. Axiom P : Prop. Axiom proof_of_P : P. Goal P /\ True. unshelve auto with test_db. apply proof_of_P.
Last updated: Feb 06 2023 at 13:03 UTC