Sometimes both exact and apply can complete a proof. What is the big picture here. Could I expect exact to be faster as it seems to be more specific?
As per my understanding, the
exact tactic fails if the goal is not completely solved:
Consider the following simple example:
Lemma foo : forall A B, A -> (A -> B) -> B. Proof. intros A B HA HAB. Fail exact HAB. apply HAB. exact HA. Qed.
This is useful to write robust proofs that are easier to maintain.
on the other hand, if you want proof robustness, you might as well use a finisher tactical like now or
by in ssreflect or Std++
it's seemingly not documented that
easy fail when not being able to solve a goal, but they do
actually that is how I learned about the exact tactic from the ssreflect.
exact are rather different tho: they're both closing tactics, but
exact a is just
solve [refine a] so it only succeeds if
a and the goal have the same type.
exact: a is instead
by apply: a
I think the intended informal reading is that
done does entirely trivial work that is not worth bothering the reader about
Last updated: Sep 28 2023 at 09:01 UTC