feat: add specialize tactic

src/Init/Notation.lean

@@ -408,6 +408,14 @@ syntax "trivial" : tactic
 
 syntax (name := split) "split " (colGt term)? (location)? : tactic
 
+/--
+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.
+-/
+syntax (name := specialize) "specialize " term : tactic
+
 macro_rules | `(tactic| trivial) => `(tactic| assumption)
 macro_rules | `(tactic| trivial) => `(tactic| rfl)
 macro_rules | `(tactic| trivial) => `(tactic| contradiction)

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -98,6 +98,21 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
   | `(tactic| refine' $e) => refineCore e `refine' (allowNaturalHoles := true)
   | _                     => throwUnsupportedSyntax
 
+@[builtinTactic «specialize»] def evalSpecialize : Tactic := fun stx => withMainContext do
+  match stx with
+  | `(tactic| specialize $e:term) =>
+    let (e, mvarIds') ← elabTermWithHoles e (← getMainTarget) `specialize (allowNaturalHoles := true)
+    let h := e.getAppFn
+    if h.isFVar then
+      let localDecl ← getLocalDecl h.fvarId!
+      let mvarId ← assert (← getMainGoal) localDecl.userName (← inferType e).headBeta e
+      let (_, mvarId) ← intro1P mvarId
+      let mvarId ← tryClear mvarId h.fvarId!
+      replaceMainGoal (mvarId :: mvarIds')
+    else
+      throwError "'specialize' requires a term of the form `h x_1 .. x_n` where `h` appears in the local context"
+  | _ => throwUnsupportedSyntax
+
 /--
    Given a tactic
    ```

tests/lean/run/specialize1.lean

@@ -0,0 +1,28 @@
+example (x y z : Prop) (f : x → y → z) (xp : x) (yp : y) : z := by
+  specialize f xp yp
+  assumption
+
+example (B C : Prop) (f : forall (A : Prop), A → C) (x : B) : C := by
+  specialize f _ x
+  exact f
+
+example (B C : Prop) (f : forall {A : Prop}, A → C) (x : B) : C := by
+  specialize f x
+  exact f
+
+example (B C : Prop) (f : forall {A : Prop}, A → C) (x : B) : C := by
+  specialize @f _ x
+  exact f
+
+example (X : Type) [Add X] (f : forall {A : Type} [Add A], A → A → A) (x : X) : X := by
+  specialize f x x
+  assumption
+
+def ex (f : Nat → Nat → Nat) : Nat := by
+  specialize f _ _
+  exact f
+  exact 10
+  exact 2
+
+example : ex (. - .) = 8 :=
+  rfl