From c1f45ecd48a53de9da57d23213ead2c2aa9b2ef4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Apr 2021 19:10:24 -0700
Subject: [PATCH] fix: fixes #394

The bug was due to the auto-generalization feature.
---
 src/Lean/Elab/Tactic/Induction.lean | 5 ++++-
 tests/lean/run/394.lean             | 9 +++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/394.lean

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index b819e39eae..ae128f47ba 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -277,13 +277,16 @@ where
   Collect forward dependencies that are not in the forbidden set, and depend on some variable in `targets`.
 
   Remark: this method assumes `targets` are free variables.
+
+  Remark: we *not* collect instance implicit arguments nor auxiliary declarations for compiling
+  recursive declarations.
 -/
 private def collectForwardDeps (targets : Array Expr) (forbidden : NameSet) : MetaM NameSet := do
   let mut s : NameSet := targets.foldl (init := {}) fun s target => s.insert target.fvarId!
   let mut r : NameSet := {}
   for localDecl in (← getLCtx) do
     unless forbidden.contains localDecl.fvarId do
-      unless localDecl.isAuxDecl do
+      unless localDecl.isAuxDecl || localDecl.binderInfo.isInstImplicit do
       if (← getMCtx).findLocalDeclDependsOn localDecl fun fvarId => s.contains fvarId then
         r := r.insert localDecl.fvarId
         s := s.insert localDecl.fvarId
diff --git a/tests/lean/run/394.lean b/tests/lean/run/394.lean
new file mode 100644
index 0000000000..1d0e284aca
--- /dev/null
+++ b/tests/lean/run/394.lean
@@ -0,0 +1,9 @@
+def casesTFOn {motive : Prop → Sort _} (P) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
+  λ ht hf => match inst with
+  | isTrue H => eqTrue H ▸ ht
+  | isFalse H => eqFalse H ▸ hf
+
+example (P) [Decidable P] : ¬¬P → P := by
+  induction P using casesTFOn
+  admit
+  admit