Stream: Coq users

Topic: exact vs apply tactic?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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++

view this post on Zulip 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

view this post on Zulip walker (Oct 16 2022 at 13:06):

actually that is how I learned about the exact tactic from the ssreflect.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 16 2022 at 13:43):

exact: a is instead by apply: a

view this post on Zulip 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: Feb 08 2023 at 22:03 UTC