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

  1. 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.

  1. As well as being a generalization of the exact tactic, refine is also a generalization of the apply tactic. If your tactic state is

h : P  Q
 Q

then you can change the goal to P with refine h ?_.

  1. refine ?_ does nothing at all; it leaves the goal unchanged.

  2. Faced with (n : ℕ), n ^ 4 = 16, the tactic refine ⟨2, ?_⟩ turns the goal into 2 ^ 4 = 16, so it does the same as use 2. In fact here, because 2 ^ 4 = 16 can be solved with norm_num, the entire goal can be closed with exact ⟨2, by norm_num⟩.

  3. If your tactic state looks (in part) like this:

f :   
x y ε : 
 : 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.