specialize @foo x

Stream: mathlib4

[Mario Carneiro]

Lean 3 and lean 4 parse specialize differently. In Lean 3, it is a term headed by a local constant, while in lean 4 it is ident expr*. The difference comes up around uses of @ to change which variables are being provided implicitly; in lean 4 there is no place for this marker to go, and I would assume that it ignores binder modes and always acts like @ is used.

[Leonardo de Moura]

@Mario Carneiro Are you referring to the specialize tactic in Lean 3?

/--
The tactic `specialize h a₁ ... aₙ` works on local hypothesis `h`. The premises of this hypothesis, either universal quantifications or non-dependent implications, are instantiated by concrete terms coming either from arguments `a₁` ... `aₙ`. The tactic adds a new hypothesis with the same name `h := h a₁ ... aₙ` and tries to clear the previous one.
-/
meta def specialize (p : parse texpr) : tactic unit :=
focus1 $
do e ← i_to_expr p,
   let h := expr.get_app_fn e,
   if h.is_local_constant
   then tactic.note h.local_pp_name none e >> try (tactic.clear h) >> rotate 1
   else tactic.fail "specialize requires a term of the form `h x_1 .. x_n` where `h` appears in the local context"

If yes, we can add this tactic to Lean 4. We can use a similar parser when we add it.

[Leonardo de Moura]

Just added the specialize tactic to Lean 4:
https://github.com/leanprover/lean4/blob/master/tests/lean/run/specialize1.lean

[Kevin Buzzard]

It's great to see the tactics slowly appearing, especially the ones I tell to the undergraduates!