Stream: Coq users

Topic: Prevent Program Fixpoint from auto-proving obligations


view this post on Zulip Ana de Almeida Borges (Sep 27 2020 at 19:03):

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?

view this post on Zulip Yannick Zakowski (Sep 27 2020 at 19:06):

You can change the tactic that gets run to solve the obligations, so I guess setting it locally to idtac would do the trick?
https://coq.github.io/doc/v8.12/refman/addendum/program.html?highlight=program%20fixpoint#coq:cmd.obligation-tactic

view this post on Zulip Kenji Maillard (Sep 27 2020 at 19:06):

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.

view this post on Zulip Ana de Almeida Borges (Sep 27 2020 at 19:10):

Cool! Setting 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