exact¶
The exact
tactic can be used to close a goal.
Example¶
If the local context is
P : Prop,
HP : P
⊢ P
then the tactic exact HP
(note: not exact P
) will close the goal.
In this case, because the goal is one of the hypotheses, the assumption
tactic would also work fine. However exact
is more general, because it takes an arbitrary term. For example, the goal here is not precisely one of the assumptions, it is built from two of them.
example (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
begin
/-
P Q : Prop,
HP : P,
HPQ : P → Q
⊢ Q
-/
exact (HPQ HP)
end
In fact, for proofs of the form begin exact X, end
there is no point entering tactic mode at all:
example (P Q : Prop) (HP : P) (HPQ : P → Q) : Q := HPQ HP