Stream: Equations devs & users

Topic: Address all obligations at once


view this post on Zulip Yves Bertot (Jul 03 2020 at 10:45):

Hello, this example contains a function defined using Equations and a measure function. All recursive calls can be proved using the same tactic. Is there a way to tell the system I want to apply this tactic on all obligations?

view this post on Zulip Paolo Giarrusso (Jul 03 2020 at 10:53):

There's Solve All Obligations with tactic. However, for equivalent results, you'll need to prepend the current default obligation tactic — which Show Obligation Tactic. should show.

https://coq.inria.fr/refman/addendum/program.html?highlight=solve%20all%20obligations#coq:cmd.solve-all-obligations

view this post on Zulip Jakob Botsch Nielsen (Jul 03 2020 at 10:53):

You can also change Equations to Equations? which will allow you to prove all obligations in a single proof mode, where you can use a goal selector, eg. all: <tactics>


Last updated: Sep 25 2023 at 12:01 UTC