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

  1. If you have a hypothesis h : P → Q and another hypothesis hP : P (that is, a proof of P) then specialize h hP will change the type of h to h : 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.

  1. If you have a hypothesis h : ∀ x, f x = 37 saying that the function f(x) is a constant function with value 37, then specialize h 10 will change h to h : 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.

  1. You can specialize more than one variable at once. For example if you have a hypothesis h : ∀ (x y : ℕ), ... then specialize h 37 42 sets x = 37 and y = 42 in h.

  2. If you have a hypothesis h : ∀ ε > 0, ∃ δ > 0, ... then looking at your tactic state more carefully you might find that it actually says something like ∀ (ε : ℝ), ε > 0 → .... If you also have variables ε : ℝ and hε : ε > 0 then you can do specialize h ε hε in which case h will change to ∃ δ > 0, ... .

  3. If again you have a hypothesis h : ∀ ε > 0, ∃ δ > 0, ... but you would like to use h in the case where ε = 37 then you can specialize h 37 and this will change h to h : 37 > 0 → (∃ δ.... Now obviously 37 > 0 but h still wants a proof of this as its next input. You could make this proof in a couple of ways. For example (assuming that 37 is the real number 37 : ℝ, which it probably is if you’re doing epsilon-delta arguments) this would work:

have h37 : (37 : ℝ) > 0 -- two goals now
{ norm_num }, -- `h37` now proved
specialize h h37

However you could just drop the proof in directly:

specialize h (begin norm_num end)

There is special notation by for tactic blocks with just one tactic in, so in fact the following variants would also work

have h37 : (37 : ℝ) > 0 := by norm_num, -- still only one goal
specialize h h37

or even

specialize h (by norm_num)

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 norm_num).

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.