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?

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: Jun 23 2024 at 23:01 UTC