chore: upstream left/right tactics (#3307)

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Init/Tactics.lean

@@ -207,6 +207,28 @@ the first matching constructor, or else fails.
 -/
 syntax (name := constructor) "constructor" : tactic
 
+/--
+Applies the second constructor when
+the goal is an inductive type with exactly two constructors, or fails otherwise.
+```
+example : True ∨ False := by
+  left
+  trivial
+```
+-/
+syntax (name := left) "left" : tactic
+
+/--
+Applies the second constructor when
+the goal is an inductive type with exactly two constructors, or fails otherwise.
+```
+example {p q : Prop} (h : q) : p ∨ q := by
+  right
+  exact h
+```
+-/
+syntax (name := right) "right" : tactic
+
 /--
 * `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`,
   or else fails.

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Refl
@@ -468,4 +469,10 @@ where
   | none    => throwIllFormedSyntax
   | some ms => IO.sleep ms.toUInt32
 
+@[builtin_tactic left] def evalLeft : Tactic := fun _stx => do
+  liftMetaTactic (fun g => g.nthConstructor `left 0 (some 2))
+
+@[builtin_tactic right] def evalRight : Tactic := fun _stx => do
+  liftMetaTactic (fun g => g.nthConstructor `right 1 (some 2))
+
 end Lean.Elab.Tactic

src/Lean/Meta/Tactic/Apply.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Siddhartha Gadgil
 -/
 import Lean.Util.FindMVar
 import Lean.Meta.SynthInstance
@@ -230,4 +230,25 @@ def _root_.Lean.MVarId.exfalso (mvarId : MVarId) : MetaM MVarId :=
     mvarId.assign (mkApp2 (mkConst ``False.elim [u]) target mvarIdNew)
     return mvarIdNew.mvarId!
 
+/--
+Apply the `n`-th constructor of the target type,
+checking that it is an inductive type,
+and that there are the expected number of constructors.
+-/
+def _root_.Lean.MVarId.nthConstructor
+    (name : Name) (idx : Nat) (expected? : Option Nat := none) (goal : MVarId) :
+    MetaM (List MVarId) := do
+  goal.withContext do
+    goal.checkNotAssigned name
+    matchConstInduct (← goal.getType').getAppFn
+      (fun _ => throwTacticEx name goal "target is not an inductive datatype")
+      fun ival us => do
+        if let some e := expected? then unless ival.ctors.length == e do
+          throwTacticEx name goal
+            s!"{name} tactic works for inductive types with exactly {e} constructors"
+        if h : idx < ival.ctors.length then
+          goal.apply <| mkConst ival.ctors[idx] us
+        else
+          throwTacticEx name goal s!"index {idx} out of bounds, only {ival.ctors.length} constructors"
+
 end Lean.Meta