From 9ed8db4bc364569c1c9878709fe4ad1277a9982e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 6 May 2021 12:28:57 +0200
Subject: [PATCH] feat: add `constructor` tactic

---
 src/Init/Notation.lean                      |  1 +
 src/Lean/Elab/Tactic/ElabTerm.lean          |  6 ++++++
 src/Lean/Meta/Tactic/Constructor.lean       | 14 ++++++++++++++
 tests/lean/constructorTac.lean              |  8 ++++++++
 tests/lean/constructorTac.lean.expected.out |  5 +++++
 5 files changed, 34 insertions(+)
 create mode 100644 tests/lean/constructorTac.lean
 create mode 100644 tests/lean/constructorTac.lean.expected.out

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 685cdb7096..8ee8da61ac 100644
--- a/src/Init/Notation.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 3d7e6900d9..7368b0cddc 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Constructor.lean b/src/Lean/Meta/Tactic/Constructor.lean
index 14fbf51799..373038c167 100644
--- a/src/Lean/Meta/Tactic/Constructor.lean
+++ b/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
diff --git a/tests/lean/constructorTac.lean b/tests/lean/constructorTac.lean
new file mode 100644
index 0000000000..f3247cc3df
--- /dev/null
+++ b/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
diff --git a/tests/lean/constructorTac.lean.expected.out b/tests/lean/constructorTac.lean.expected.out
new file mode 100644
index 0000000000..5d9cc1b3c1
--- /dev/null
+++ b/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