From 27b70021389a4226dde2225ce7e01b227cfdb31a Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 18 Jan 2024 10:44:17 +0100
Subject: [PATCH] fix: `checkTargets` check for duplicate target (#3171)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The `checkTargets` function introduced in 4a0f8bf2 as
```
  checkTargets (targets : Array Expr) : MetaM Unit := do
    let mut foundFVars : FVarIdSet := {}
    for target in targets do
      unless target.isFVar do
        throwError "index in target's type is not a variable (consider using the `cases` tactic instead){indentExpr target}"
      if foundFVars.contains target.fvarId! then
        throwError "target (or one of its indices) occurs more than once{indentExpr target}"
```
looks like it tries to check for duplicate indices, but it doesn’t
actually, as `foundFVars` is never written to.

This adds
```
      foundFVars := foundFVars.insert target.fvarId!
```
and a test case.

Maybe a linter that warns about `let mut` that are never writen to would
be useful?
---
 src/Lean/Elab/Tactic/Induction.lean       |  1 +
 tests/lean/inductionGen.lean              | 10 ++++++++++
 tests/lean/inductionGen.lean.expected.out |  2 ++
 3 files changed, 13 insertions(+)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 85e0489a7b..ab070547ba 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -571,6 +571,7 @@ where
         throwError "index in target's type is not a variable (consider using the `cases` tactic instead){indentExpr target}"
       if foundFVars.contains target.fvarId! then
         throwError "target (or one of its indices) occurs more than once{indentExpr target}"
+      foundFVars := foundFVars.insert target.fvarId!
 
 def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ident × FVarId)) :=
   withMainContext do
diff --git a/tests/lean/inductionGen.lean b/tests/lean/inductionGen.lean
index c20f580c66..c95297fa38 100644
--- a/tests/lean/inductionGen.lean
+++ b/tests/lean/inductionGen.lean
@@ -66,3 +66,13 @@ theorem ex3 (a b : Expr α) (h : a = b) : eval (constProp a) = eval b := by
   induction a
   trace_state -- b's type must have been refined, `h` too
   repeat admit
+
+inductive Foo : Nat → Nat → Type where
+  | mk : Foo 1 2
+
+theorem ex4 (n m : Nat) (heq : n = m) (h : Foo n m) : False := by
+  induction h using Foo.rec
+  case mk => contradiction
+
+theorem ex5 (n : Nat) (h : Foo n n) : False := by
+  induction h using Foo.rec -- error, target repeated
diff --git a/tests/lean/inductionGen.lean.expected.out b/tests/lean/inductionGen.lean.expected.out
index 565fc6d855..eb5894e71b 100644
--- a/tests/lean/inductionGen.lean.expected.out
+++ b/tests/lean/inductionGen.lean.expected.out
@@ -41,3 +41,5 @@ a_ih✝ : ∀ (b : Expr ExprType.nat), a✝ = b → eval (constProp a✝) = eval
 b : Expr ExprType.nat
 h : Expr.add a✝¹ a✝ = b
 ⊢ eval (constProp (Expr.add a✝¹ a✝)) = eval b
+inductionGen.lean:78:2-78:27: error: target (or one of its indices) occurs more than once
+  n