## Stream: Coq users

### Topic: exact vs apply tactic?

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