Anders Larsson (Oct 16 2022 at 09:23): Anders Larsson (Oct 16 2022 at 09:23):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?
walker (Oct 16 2022 at 12:49):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.
Karl Palmskog (Oct 16 2022 at 12:56):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++
Karl Palmskog (Oct 16 2022 at 12:58):it's seemingly not documented that now/easy fail when not being able to solve a goal, but they do
walker (Oct 16 2022 at 13:06):actually that is how I learned about the exact tactic from the ssreflect.
Paolo Giarrusso (Oct 16 2022 at 13:43):exact: and 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.
Paolo Giarrusso (Oct 16 2022 at 13:43):exact: a is instead by apply: a
Paolo Giarrusso (Oct 16 2022 at 13:45):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