fix: fun_induction to generalize like induction does (#7127)

This PR follows up on #7103 which changes the generaliziation behavior
of `induction`, to keep `fun_induction` in sync. Also fixes a `Syntax`
indexing off-by-one error.

src/Lean/Elab/Tactic/Induction.lean

@@ -447,10 +447,16 @@ end ElimApp
   generalizingVars := optional (" generalizing " >> many1 ident)
   «induction»  := leading_parser nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> optional inductionAlts
   ```
-  `stx` is syntax for `induction`. -/
+  `stx` is syntax for `induction` or `fun_induction`. -/
 private def getUserGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
   withRef stx do
-    let generalizingStx := stx[3]
+    let generalizingStx :=
+    if stx.getKind == ``Lean.Parser.Tactic.induction then
+      stx[3]
+    else if stx.getKind == ``Lean.Parser.Tactic.funInduction then
+      stx[2]
+    else
+      panic! "getUserGeneralizingFVarIds: Unexpected syntax kind {stx.getKind}"
     if generalizingStx.isNone then
       pure #[]
     else
@@ -677,19 +683,6 @@ private def shouldGeneralizeTarget (e : Expr) : MetaM Bool := do
   else
     return true
 
-/--
-Simple target generalization scheme.
-Ensures that each target is a cdecl fvar, using `Lean.MVarId.generalize` as necessary.
-
-See also `Lean.Elab.Tactic.elabElimTargets`, which is what `induction` and `cases` use instead.
--/
-private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
-  if (← withMainContext <| exprs.anyM (shouldGeneralizeTarget ·)) then
-    liftMetaTacticAux fun mvarId => do
-      let (fvarIds, mvarId) ← mvarId.generalize (exprs.map fun expr => { expr })
-      return (fvarIds.map mkFVar, [mvarId])
-  else
-    return exprs
 
 /-- View of `Lean.Parser.Tactic.elimTarget`. -/
 structure ElimTargetView where
@@ -755,6 +748,28 @@ def elabElimTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ide
         assert! hIdents.size + j == fvarIdsNew.size
         return ((result, hIdents.zip fvarIdsNew[j:]), [mvarId])
 
+/--
+Generalize targets in `fun_induction` and `fun_cases`. Should behave like `elabCasesTargets` with
+no targets annotated with `h : _`.
+-/
+private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
+  withMainContext do
+    let exprToGeneralize ← exprs.filterM (shouldGeneralizeTarget ·)
+    if exprToGeneralize.isEmpty then
+      return exprs
+    liftMetaTacticAux fun mvarId => do
+      let (fvarIdsNew, mvarId) ← mvarId.generalize (exprToGeneralize.map ({ expr := · }))
+      assert! fvarIdsNew.size == exprToGeneralize.size
+      let mut result := #[]
+      let mut j := 0
+      for expr in exprs do
+        if (← shouldGeneralizeTarget expr) then
+          result := result.push (mkFVar fvarIdsNew[j]!)
+          j := j+1
+        else
+          result := result.push expr
+      return (result, [mvarId])
+
 def checkInductionTargets (targets : Array Expr) : MetaM Unit := do
   let mut foundFVars : FVarIdSet := {}
   for target in targets do

tests/lean/run/funinduction_generalize.lean

@@ -0,0 +1,208 @@
+/-!
+Checks the generalization behavior of `fun_induction`.
+
+In particular that it behaves the same as `induction … using ….induct`.
+-/
+
+variable (xs ys : List Nat)
+variable (P : ∀ {α}, List α → Prop)
+
+/--
+error: unsolved goals
+case case1
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+x✝ : Nat
+xs✝ : List Nat
+y✝ : Nat
+ys✝ : List Nat
+ih1✝ : P (xs✝.zip ys✝)
+⊢ P ((x✝ :: xs✝).zip (y✝ :: ys✝))
+
+case case2
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+t✝ x✝¹ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+⊢ P (t✝.zip x✝¹)
+-/
+#guard_msgs in
+example : P (List.zip xs ys) := by
+  fun_induction List.zipWith _ xs ys
+
+
+/--
+error: unsolved goals
+case case1
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+x✝ : Nat
+xs✝ : List Nat
+y✝ : Nat
+ys✝ : List Nat
+ih1✝ : xs✝.isEmpty = true → P (xs✝.zip ys✝)
+h : (x✝ :: xs✝).isEmpty = true
+⊢ P ((x✝ :: xs✝).zip (y✝ :: ys✝))
+
+case case2
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+t✝ x✝¹ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+h : t✝.isEmpty = true
+⊢ P (t✝.zip x✝¹)
+-/
+#guard_msgs in
+example (h : xs.isEmpty) : P (List.zip xs ys) := by
+  fun_induction List.zipWith _ xs ys
+
+
+/--
+error: unsolved goals
+case case1
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+x✝ : Nat
+xs✝ : List Nat
+y✝ : Nat
+ys✝ : List Nat
+ih1✝ : xs✝.isEmpty = true → P (xs✝.zip ys)
+h : (x✝ :: xs✝).isEmpty = true
+⊢ P ((x✝ :: xs✝).zip ys)
+
+case case2
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+t✝ x✝¹ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+h : t✝.isEmpty = true
+⊢ P (t✝.zip ys)
+-/
+#guard_msgs in
+example (h : xs.isEmpty) : P (List.zip xs ys) := by
+  fun_induction List.zipWith _ xs (ys.take 2)
+
+/--
+error: unsolved goals
+case case1
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+x✝ : Nat
+xs✝ : List Nat
+y✝ : Nat
+ys✝ : List Nat
+ih1✝ : xs✝.isEmpty = true → P (xs✝.zip ys)
+h : (x✝ :: xs✝).isEmpty = true
+⊢ P ((x✝ :: xs✝).zip ys)
+
+case case2
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+t✝ x✝¹ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+h : t✝.isEmpty = true
+⊢ P (t✝.zip ys)
+-/
+#guard_msgs in
+example (h : xs.isEmpty) : P (List.zip xs ys) := by
+  induction xs, ys.take 2 using List.zipWith.induct
+
+/--
+error: unsolved goals
+case case1
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+h : xs.isEmpty = true
+x✝ : Nat
+xs✝ : List Nat
+y✝ : Nat
+ys✝ : List Nat
+ih1✝ : P (xs.zip ys✝)
+⊢ P (xs.zip (y✝ :: ys✝))
+
+case case2
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+h : xs.isEmpty = true
+t✝ x✝¹ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+⊢ P (xs.zip x✝¹)
+-/
+#guard_msgs in
+example (h : xs.isEmpty) : P (List.zip xs ys) := by
+  fun_induction List.zipWith _ (xs.take 2) ys
+
+/--
+error: unsolved goals
+case case1
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+h : xs.isEmpty = true
+x✝ : Nat
+xs✝ : List Nat
+y✝ : Nat
+ys✝ : List Nat
+ih1✝ : P (xs.zip ys✝)
+⊢ P (xs.zip (y✝ :: ys✝))
+
+case case2
+xs ys : List Nat
+P : {α : Type} → List α → Prop
+h : xs.isEmpty = true
+t✝ x✝¹ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+⊢ P (xs.zip x✝¹)
+-/
+#guard_msgs in
+example (h : xs.isEmpty) : P (List.zip xs ys) := by
+  induction xs.take 2, ys using List.zipWith.induct
+
+/--
+error: unsolved goals
+case case1
+P : {α : Type} → List α → Prop
+x✝ : Nat
+xs✝ : List Nat
+y✝ : Nat
+ys✝ : List Nat
+ih1✝ : ∀ (xs : List Nat), xs.isEmpty = true → P (xs.zip ys✝)
+xs : List Nat
+h : xs.isEmpty = true
+⊢ P (xs.zip (y✝ :: ys✝))
+
+case case2
+P : {α : Type} → List α → Prop
+t✝ x✝¹ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+xs : List Nat
+h : xs.isEmpty = true
+⊢ P (xs.zip x✝¹)
+-/
+#guard_msgs in
+example (h : xs.isEmpty) : P (List.zip xs ys) := by
+  fun_induction List.zipWith _ (xs.take 2) ys generalizing xs
+
+/--
+error: unsolved goals
+case case1
+P : {α : Type} → List α → Prop
+x✝ : Nat
+xs✝ : List Nat
+y✝ : Nat
+ys✝ : List Nat
+ih1✝ : ∀ (xs : List Nat), xs.isEmpty = true → P (xs.zip ys✝)
+xs : List Nat
+h : xs.isEmpty = true
+⊢ P (xs.zip (y✝ :: ys✝))
+
+case case2
+P : {α : Type} → List α → Prop
+t✝ x✝¹ : List Nat
+x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
+xs : List Nat
+h : xs.isEmpty = true
+⊢ P (xs.zip x✝¹)
+-/
+#guard_msgs in
+example (h : xs.isEmpty) : P (List.zip xs ys) := by
+  induction xs.take 2, ys using List.zipWith.induct generalizing xs