feat: add constructor tactic

src/Init/Notation.lean

@@ -214,6 +214,7 @@ syntax (name := apply) "apply " term : tactic
 syntax (name := exact) "exact " term : tactic
 syntax (name := refine) "refine " term : tactic
 syntax (name := refine') "refine' " term : tactic
+syntax (name := constructor) "constructor" : tactic
 syntax (name := case) "case " ident (ident <|> "_")* " => " tacticSeq : tactic
 syntax (name := allGoals) "allGoals " tacticSeq : tactic
 syntax (name := focus) "focus " tacticSeq : tactic

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -115,6 +115,12 @@ def evalApplyLikeTactic (tac : MVarId → Expr → MetaM (List MVarId)) (e : Syn
   | `(tactic| apply $e) => evalApplyLikeTactic Meta.apply e
   | _ => throwUnsupportedSyntax
 
+@[builtinTactic Lean.Parser.Tactic.constructor] def evalConstructor : Tactic := fun stx =>
+  withMainContext do
+    let mvarIds'  ← Meta.constructor (← getMainGoal)
+    Term.synthesizeSyntheticMVarsNoPostponing
+    replaceMainGoal mvarIds'
+
 @[builtinTactic Lean.Parser.Tactic.existsIntro] def evalExistsIntro : Tactic := fun stx =>
   match stx with
   | `(tactic| exists $e) => evalApplyLikeTactic (fun mvarId e => return [(← Meta.existsIntro mvarId e)]) e

src/Lean/Meta/Tactic/Constructor.lean

@@ -9,6 +9,20 @@ import Lean.Meta.Tactic.Apply
 
 namespace Lean.Meta
 
+def constructor (mvarId : MVarId) : MetaM (List MVarId) := do
+  withMVarContext mvarId do
+    checkNotAssigned mvarId `constructor
+    let target ← getMVarType' mvarId
+    matchConstInduct target.getAppFn
+      (fun _ => throwTacticEx `constructor mvarId "target is not an inductive datatype")
+      fun ival us => do
+        for ctor in ival.ctors do
+          try
+            return ← apply mvarId (Lean.mkConst ctor us)
+          catch _ =>
+            pure ()
+        throwTacticEx `constructor mvarId "no applicable constructor found"
+
 def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do
   withMVarContext mvarId do
     checkNotAssigned mvarId `exists

tests/lean/constructorTac.lean

@@ -0,0 +1,8 @@
+inductive Le (m : Nat) : Nat → Prop
+  | base : Le m m
+  | succ : (n : Nat) → Le m n → Le m n.succ
+
+example : Le n n := by constructor
+example : Le n m := by constructor
+example : Le n n.succ := by constructor; constructor
+example : Type := by constructor

tests/lean/constructorTac.lean.expected.out

@@ -0,0 +1,5 @@
+constructorTac.lean:6:23-6:34: error: tactic 'constructor' failed, no applicable constructor found
+n m : Nat
+⊢ Le n m
+constructorTac.lean:8:21-8:32: error: tactic 'constructor' failed, target is not an inductive datatype
+⊢ Type