fix: fixes #310

@Kha I implemented the following approach:

- Error if user tries to revert `auxDecl`.
- Clear any `auxDecl` that depends on variables being reverted by the user.

src/Lean/Meta/Tactic/Induction.lean

@@ -124,6 +124,7 @@ private def throwUnexpectedMajorType {α} (mvarId : MVarId) (majorType : Expr) :
 
 def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) :=
   withMVarContext mvarId do
+    trace[Meta.Tactic.induction]! "initial\n{MessageData.ofGoal mvarId}"
     checkNotAssigned mvarId `induction
     let majorLocalDecl ← getLocalDecl majorFVarId
     let recursorInfo ← mkRecursorInfo recursorName

src/Lean/Meta/Tactic/Revert.lean

@@ -3,25 +3,43 @@ Copyright (c) 2020 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.Util
+import Lean.Meta.Tactic.Clear
 
 namespace Lean.Meta
 
-def revert (mvarId : MVarId) (fvars : Array FVarId) (preserveOrder : Bool := false) : MetaM (Array FVarId × MVarId) := do
-  if fvars.isEmpty then
-    pure (fvars, mvarId)
+def revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := false) : MetaM (Array FVarId × MVarId) := do
+  if fvarIds.isEmpty then
+    pure (#[], mvarId)
   else withMVarContext mvarId do
-    let tag ← getMVarTag mvarId
     checkNotAssigned mvarId `revert
-    -- Set metavariable kind to natural to make sure `elimMVarDeps` will assign it.
-    setMVarKind mvarId MetavarKind.natural
-    let (e, toRevert) ←
-      try
-        liftMkBindingM <| MetavarContext.revert (fvars.map mkFVar) mvarId preserveOrder
-      finally
-        setMVarKind mvarId MetavarKind.syntheticOpaque
-    let mvar := e.getAppFn
-    setMVarTag mvar.mvarId! tag
-    return (toRevert.map Expr.fvarId!, mvar.mvarId!)
+    for fvarId in fvarIds do
+      if (← getLocalDecl fvarId) |>.isAuxDecl then
+        throwError "failed to revert {mkFVar fvarId}, it is an auxiliary declaration created to represent recursive definitions"
+    let fvars := fvarIds.map mkFVar
+    match MetavarContext.MkBinding.collectDeps (← getMCtx) (← getLCtx) fvars preserveOrder with
+    | Except.error _     => throwError "failed to revert variables {fvars}"
+    | Except.ok toRevert =>
+      /- We should clear any `auxDecl` in `toRevert` -/
+      let mut mvarId      := mvarId
+      let mut toRevertNew := #[]
+      for x in toRevert do
+        if (← getLocalDecl x.fvarId!) |>.isAuxDecl then
+          mvarId ← clear mvarId x.fvarId!
+        else
+          toRevertNew := toRevertNew.push x
+      let tag ← getMVarTag mvarId
+      -- TODO: the following code can be optimized because `MetavarContext.revert` will compute `collectDeps` again.
+      -- We should factor out the relevat part
+
+      -- Set metavariable kind to natural to make sure `revert` will assign it.
+      setMVarKind mvarId MetavarKind.natural
+      let (e, toRevert) ←
+        try
+          liftMkBindingM <| MetavarContext.revert toRevertNew mvarId preserveOrder
+        finally
+          setMVarKind mvarId MetavarKind.syntheticOpaque
+      let mvar := e.getAppFn
+      setMVarTag mvar.mvarId! tag
+      return (toRevert.map Expr.fvarId!, mvar.mvarId!)
 
 end Lean.Meta

src/Lean/MetavarContext.lean

@@ -788,7 +788,7 @@ def collectDeps (mctx : MetavarContext) (lctx : LocalContext) (toRevert : Array
 
 /-- Create a new `LocalContext` by removing the free variables in `toRevert` from `lctx`.
     We use this function when we create auxiliary metavariables at `elimMVarDepsAux`. -/
-private def reduceLocalContext (lctx : LocalContext) (toRevert : Array Expr) : LocalContext :=
+def reduceLocalContext (lctx : LocalContext) (toRevert : Array Expr) : LocalContext :=
   toRevert.foldr (init := lctx) fun x lctx =>
     lctx.erase x.fvarId!
 

tests/lean/run/310.lean

@@ -0,0 +1,9 @@
+variable (xs : List Nat)
+
+theorem foo1 : xs = xs := by
+  induction xs <;> rfl
+
+theorem foo2 : xs = xs := by
+  cases xs with
+  | nil        => rfl
+  | cons x xs  => rfl