I have a Program Fixpoint definition that generates two obligations and is able to automatically prove one of them.
However, it takes a long time to do so, and I could probably prove it manually without much effort.
Is there a way to prevent Program Fixpoint to try to automatically prove the obligations?
You can change the tactic that gets run to solve the obligations, so I guess setting it locally to
idtac would do the trick?
Set the obligation tactic so that it gives up eagerly on your goal, for instance
Obligation Tactic := idtac.; if you want to prevent only some of the goals from being solved by the obligation tactic, you can also use a variation of what's presented there.
Local Obligation Tactic := intros. is slightly more useful than
idtac and does the trick. Thank you :)
Last updated: Jan 27 2023 at 00:03 UTC