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
Do you want solve [ auto ]
?
I usually do things like
some_tactic.
all: try solve [ complicated_tactic_that_might_succeed_without_closing_the_goal ].
is now
still supported? now auto
.
Yes, but now auto
does more than ensure that auto
will succeed, it will try to solve the goal left by auto
using easy
.
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: Oct 13 2024 at 01:02 UTC