From 3e75d8f74297bc258352f8d89f71496aacefe7ae Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 7 Oct 2024 21:47:43 +0200
Subject: [PATCH] fix: FunInd: avoid over-eta-expanding in preprocessing step
 (#5619)

fixes #5602
---
 src/Lean/Meta/Tactic/FunInd.lean | 18 +++++++++++++++---
 tests/lean/run/issue5602.lean    | 22 ++++++++++++++++++++++
 2 files changed, 37 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/issue5602.lean

diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index b2d077115e..a1f82e6059 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -662,8 +662,16 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
   let varNames ← forallTelescope info.type fun xs _ => xs.mapM (·.fvarId!.getUserName)
 
   -- Uses of WellFounded.fix can be partially applied. Here we eta-expand the body
-  -- to avoid dealing with this
-  let e ← lambdaTelescope info.value fun params body => do mkLambdaFVars params (← etaExpand body)
+  -- to make sure that `target` indeed the last parameter
+  let e := info.value
+  let e ← lambdaTelescope e fun params body => do
+    if body.isAppOfArity ``WellFounded.fix 5 then
+      forallBoundedTelescope (← inferType body) (some 1) fun xs _ => do
+        unless xs.size = 1 do
+          throwError "functional induction: Failed to eta-expand{indentExpr e}"
+        mkLambdaFVars (params ++ xs) (mkAppN body xs)
+    else
+      pure e
   let e' ← lambdaTelescope e fun params funBody => MatcherApp.withUserNames params varNames do
     match_expr funBody with
     | fix@WellFounded.fix α _motive rel wf body target =>
@@ -710,7 +718,11 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
         -- So for now lets just keep them around.
         let e' ← mkLambdaFVars (binderInfoForMVars := .default) fixedParams e'
         instantiateMVars e'
-    | _ => throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
+    | _ =>
+      if funBody.isAppOf ``WellFounded.fix then
+        throwError "Function {name} defined via WellFounded.fix with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
+      else
+        throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
 
   unless (← isTypeCorrect e') do
     logError m!"failed to derive a type-correct induction principle:{indentExpr e'}"
diff --git a/tests/lean/run/issue5602.lean b/tests/lean/run/issue5602.lean
new file mode 100644
index 0000000000..06a3e75392
--- /dev/null
+++ b/tests/lean/run/issue5602.lean
@@ -0,0 +1,22 @@
+abbrev Word := List Nat
+abbrev Alphabet := Nat
+
+inductive Regex where
+  | none: Regex
+
+axiom inter: Regex → (Word → Prop)
+axiom concatenate (a b: Word → Prop) : (Word → Prop)
+axiom eps: Word → Prop
+
+def conc (a: Array Regex) (i: Nat): Word → Prop :=
+  if h: i < a.size then
+    concatenate (inter a[i]) (conc a (i + 1))
+  else
+    eps
+
+/--
+info: conc.induct (a : Array Regex) (motive : Nat → Prop) (case1 : ∀ (x : Nat), x < a.size → motive (x + 1) → motive x)
+  (case2 : ∀ (x : Nat), ¬x < a.size → motive x) (i : Nat) : motive i
+-/
+#guard_msgs in
+#check conc.induct