From 80d2455b6401acf6b0d107388b814c175e64c0d3 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sun, 24 Mar 2024 11:15:50 +0100
Subject: [PATCH] fix: prune universe params in functional induction (#3754)

fixes #3752
---
 src/Lean/Meta/Tactic/FunInd.lean        |  6 ++-
 tests/lean/run/funind_fewer_levels.lean | 57 +++++++++++++++++++++++++
 2 files changed, 62 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/funind_fewer_levels.lean

diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 3b81a82e88..31c6a871c9 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -603,8 +603,12 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
       logError m!"failed to derive induction priciple:{indentExpr e'}"
       check e'
 
+    let params := (collectLevelParams {} eTyp).params
+    -- Prune unused level parameters, preserving the original order
+    let us := info.levelParams.filter (params.contains ·)
+
     addDecl <| Declaration.thmDecl
-      { name := inductName, levelParams := info.levelParams, type := eTyp, value := e' }
+      { name := inductName, levelParams := us, type := eTyp, value := e' }
     return inductName
 
 /--
diff --git a/tests/lean/run/funind_fewer_levels.lean b/tests/lean/run/funind_fewer_levels.lean
new file mode 100644
index 0000000000..d1dbcd762c
--- /dev/null
+++ b/tests/lean/run/funind_fewer_levels.lean
@@ -0,0 +1,57 @@
+
+/-!
+This test checks if the functional induction principle has fewer universe parameters
+if the original function has a parameter that disappears.
+-/
+
+namespace WellFounded
+def foo.{u,v} {α : Type v} : List α  → PUnit.{u}
+| [] => .unit
+| _ :: xs => foo xs
+termination_by xs => xs
+
+derive_functional_induction foo
+/--
+info: WellFounded.foo.induct.{v} {α : Type v} (motive : List α → Prop) (case1 : motive [])
+  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) (x : List α) : motive x
+-/
+#guard_msgs in
+#check foo.induct
+
+example : foo xs = .unit := by
+  induction xs using foo.induct with
+  | case1 => unfold foo; rfl
+  | case2 _ xs ih => unfold foo; exact ih
+
+end WellFounded
+
+
+namespace Mutual
+mutual
+def foo.{u} : Nat → PUnit.{u}
+| 0 => .unit
+| n+1 => bar n
+termination_by n => n
+def bar.{u} : Nat → PUnit.{u}
+| 0 => .unit
+| n+1 => foo n
+termination_by n => n
+end
+
+derive_functional_induction foo
+/--
+info: Mutual.foo.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0)
+  (case3 : ∀ (n : Nat), motive2 n → motive1 n.succ) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) :
+  ∀ (a : Nat), motive1 a
+-/
+#guard_msgs in
+#check foo.induct
+
+example : foo n = .unit := by
+  induction n using foo.induct (motive2 := fun n => bar n = .unit) with
+  | case1 => unfold foo; rfl
+  | case2 => unfold bar; rfl
+  | case3 n ih => unfold foo; exact ih
+  | case4 n ih => unfold bar; exact ih
+
+end Mutual