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
auto but not sure if that is the best solution
Do you want
solve [ auto ]?
I usually do things like
some_tactic. all: try solve [ complicated_tactic_that_might_succeed_without_closing_the_goal ].
now still supported?
now auto does more than ensure that
auto will succeed, it will try to solve the goal left by
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
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