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 `now`

/`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:`

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.

`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: Jun 18 2024 at 07:01 UTC