Stream: Coq users

Topic: make auto fail if it does not solve?


view this post on Zulip Roger Bosman (Apr 20 2021 at 15:55):

Quick question, I often have something like try (inverts H; auto) that handles some of my cases. However, auto never fails, so the inverts (or whatever else) before the auto is not rolled back for the unsolved goals. How can I force this rollback? I have tried to add trivial after auto but not sure if that is the best solution

view this post on Zulip Théo Winterhalter (Apr 20 2021 at 15:59):

Do you want solve [ auto ]?

view this post on Zulip Théo Winterhalter (Apr 20 2021 at 16:01):

I usually do things like

some_tactic.
all: try solve [ complicated_tactic_that_might_succeed_without_closing_the_goal ].

view this post on Zulip Cody Roux (Apr 20 2021 at 16:05):

is now still supported? now auto.

view this post on Zulip Théo Winterhalter (Apr 20 2021 at 16:09):

Yes, but now auto does more than ensure that auto will succeed, it will try to solve the goal left by auto using easy.

view this post on Zulip Théo Winterhalter (Apr 20 2021 at 16:12):

See https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:tacn.now and https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.solve

view this post on Zulip Roger Bosman (Apr 21 2021 at 07:53):

solve does exactly what I need, thank you! easy looks interesting as well because by the description it seems to do exactly what I usually cover with my initial try before going to the "real" cases, so I will check that out as well :)


Last updated: Jan 31 2023 at 14:03 UTC