refine
Summary
The refine
tactic is “exact
with holes”. You can use an incomplete term containing one or more underscores ?_
and Lean will give you these terms as new goals.
Examples
Faced with (amongst other things)
hQ : Q
⊢ P ∧ Q ∧ R
you can see that we already have a proof of Q
, but we might still need to do some work to prove P
and R
. The tactic refine ⟨?_, hQ, ?_⟩
replaces this goal with two new goals ⊢ P
and ⊢ R
.
As well as being a generalization of the
exact
tactic,refine
is also a generalization of theapply
tactic. If your tactic state is
h : P → Q
⊢ Q
then you can change the goal to ⊢ P
with refine h ?_
.
refine ?_
does nothing at all; it leaves the goal unchanged.Faced with
⊢ ∃ (n : ℕ), n ^ 4 = 16
, the tacticrefine ⟨2, ?_⟩
turns the goal into⊢ 2 ^ 4 = 16
, so it does the same asuse 2
. In fact here, because⊢ 2 ^ 4 = 16
can be solved withnorm_num
, the entire goal can be closed withexact ⟨2, by norm_num⟩
.If your tactic state looks (in part) like this:
f : ℝ → ℝ
x y ε : ℝ
hε : 0 < ε
⊢ ∃ δ > 0, |f y - f x| < δ
then refine ⟨ε^2, by positivity, ?_⟩
changes the goal to ⊢ |f y - f x| < ε ^ 2
. Here we use the positivity tactic to prove ε^2 > 0
from the hypothesis 0 < ε
.
Further notes
refine
works up to definitional equality.