From 6466bbbaf9c430f18d3f4ed598520ef15deb41ce Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Nov 2020 15:42:07 -0800
Subject: [PATCH] feat: admit alternatives that failed

---
 src/Lean/Elab/Tactic/Basic.lean     | 12 ++++++++++++
 src/Lean/Elab/Tactic/Induction.lean |  6 ++----
 2 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 45920153ca..17e28744f0 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -226,6 +226,18 @@ def focusAux {α} (tactic : TacticM α) : TacticM α := do
 def focus {α} (tactic : TacticM α) : TacticM α :=
   focusAux do let a ← tactic; done; pure a
 
+/- Close the main goal using the given tactic. If it fails, log the error and `admit` -/
+def closeUsingOrAdmit (tac : Syntax) : TacticM Unit := do
+  let (mvarId, rest) ← getMainGoal
+  try
+    evalTactic tac
+    done
+  catch ex =>
+    logException ex
+    let mvarType ← inferType (mkMVar mvarId)
+    assignExprMVar mvarId (← mkSorry mvarType (synthetic := true))
+    setGoals rest
+
 def try? {α} (tactic : TacticM α) : TacticM (Option α) := do
   try pure (some (← tactic))
   catch _ => pure none
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 263222063d..b3d6f4f4fd 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -169,8 +169,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (altsSyntax :
         for fvarId in toClear do
           altMVarId ← tryClear altMVarId fvarId
         setGoals [altMVarId]
-        evalTactic altRhs
-        done
+        closeUsingOrAdmit altRhs
   if usedWildcard then
     altsSyntax := altsSyntax.filter fun alt => getAltName alt != `_
   unless altsSyntax.isEmpty do
@@ -409,8 +408,7 @@ private def processResult (altRHSs : Array Syntax) (result : Array Meta.Inductio
         gs := gs ++ gs'
       else
         setGoals [mvarId]
-        evalTactic rhs
-        done
+        closeUsingOrAdmit rhs
     setGoals gs
 
 private def generalizeTerm (term : Expr) : TacticM Expr := do