specialize
Summary
The specialize
tactic can be used specialize hypotheses which are function types, by giving some or all of the inputs to the function. Its two main uses are with hypotheses of type P → Q
and of type ∀ x, ...
(that is, hypotheses where you might use intro
if their type was the goal).
Examples
If you have a hypothesis
h : P → Q
and another hypothesishP : P
(that is, a proof ofP
) thenspecialize h hP
will change the type ofh
toh : Q
.
Note: h
is a function from proofs of P
to proofs of Q
so if you just want to quickly access a proof of Q
for use elsewhere, then you don’t have to use specialize
at all, you can make a proof of Q
with the term h (hP)
or, as the functional programmers would prefer us to write, h hP
.
If you have a hypothesis
h : ∀ x, f x = 37
saying that the functionf (x)
is a constant function with value 37, thenspecialize h 10
will changeh
toh : f 10 = 37
.
Note that h
has now become a weaker statement; you have lost the hypothesis that ∀ x, f x = 37
after this application of the specialize
tactic. If you want to keep it around, you could make a copy by running have h2 := h
beforehand.
You can specialize more than one variable at once. For example if you have a hypothesis
h : ∀ (x y : ℕ), ...
thenspecialize h 37 42
setsx = 37
andy = 42
inh
.If you have a hypothesis
h : ∀ ε > 0, ∃ δ > 0, ...
, it turns out that internally this is∀ (ε : ℝ), ε > 0 → ...
. If you also have variablesε : ℝ
andhε : ε > 0
then you can dospecialize h ε hε
in which caseh
will change to∃ δ > 0, ...
.If again you have a hypothesis
h : ∀ ε > 0, ∃ δ > 0, ...
but you would like to useh
in the case whereε = 37
then you canspecialize h 37
and this will changeh
toh : 37 > 0 → (∃ δ...
. Now obviously37 > 0
buth
still wants a proof of this as its next input. You could make this proof in a couple of ways. For example (assuming that37
is the real number37 : ℝ
, which it probably is if you’re doing epsilon-delta arguments) this would work:
have h37 : (37 : ℝ) > 0 -- two goals now
· positivity
specialize h h37
However you could just drop the proof in directly:
specialize h (by positivity)
or
specialize h (by norm_num)
or
specialize h (by linarith)
In fact going back to the original hypothesis h : ∀ ε > 0, ∃ δ > 0, ...
, and remembering that Lean actually stores this as h : ∀ (ε : ℝ), ε > 0 → ∃ δ ...
, you could specialize to ε = 37
in one line with specialize h 37 (by positivity)
.
Further notes
You don’t always have to specialize
. For example if you have h : ∀ ε > 0, ∃ N, some_fact
where some_fact
is some proposition which depends on ε
and N
, and you also have ε : ℝ
and hε : ε > 0
in your tactic state, you can just get straight to N
and the fact with cases' h ε hε with N hN
or obtain ⟨N, hN⟩ : some_fact := h ε hε
.