feat: FunInd: omit unused parameters (#6330)

This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.

Part 1, before stage0 update.

Closes #6320

src/Lean/Meta/Tactic/FunInd.lean

@@ -719,13 +719,11 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
         let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
         let e' ← mkLambdaFVars #[motive] e'
 
-        -- We could pass (usedOnly := true) below, and get nicer induction principles that
-        -- do not mention odd unused parameters.
-        -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
-        -- that derives them from an function application in the goal) is harder, as
-        -- one would have to infer or keep track of which parameters to pass.
-        -- So for now lets just keep them around.
-        let e' ← mkLambdaFVars (binderInfoForMVars := .default) fixedParams e'
+        -- We used to pass (usedOnly := false) below in the hope that the types of the
+        -- induction principle match the type of the function better.
+        -- But this leads to avoidable parameters that make functional induction strictly less
+        -- useful (e.g. when the unsued parameter mentions bound variables in the users' goal)
+        let e' ← mkLambdaFVars (binderInfoForMVars := .default) (usedOnly := true) fixedParams e'
         instantiateMVars e'
     | _ =>
       if funBody.isAppOf ``WellFounded.fix then
@@ -1062,13 +1060,11 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
           let e' ← abstractIndependentMVars mvars (← motives.back!.fvarId!.getDecl).index e'
           let e' ← mkLambdaFVars motives e'
 
-          -- We could pass (usedOnly := true) below, and get nicer induction principles that
-          -- do not mention odd unused parameters.
-          -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
-          -- that derives them from an function application in the goal) is harder, as
-          -- one would have to infer or keep track of which parameters to pass.
-          -- So for now lets just keep them around.
-          let e' ← mkLambdaFVars (binderInfoForMVars := .default) xs e'
+          -- We used to pass (usedOnly := false) below in the hope that the types of the
+          -- induction principle match the type of the function better.
+          -- But this leads to avoidable parameters that make functional induction strictly less
+          -- useful (e.g. when the unsued parameter mentions bound variables in the users' goal)
+          let e' ← mkLambdaFVars (binderInfoForMVars := .default) (usedOnly := true) xs e'
           let e' ← instantiateMVars e'
           trace[Meta.FunInd] "complete body of mutual induction principle:{indentExpr e'}"
           pure e'

tests/lean/run/4320.lean

@@ -7,7 +7,7 @@ def many_map {α β : Type} (f : α → β) : Many α → Many β
   | .more x xs => Many.more (f x) (fun () => many_map f <| xs ())
 
 /--
-info: many_map.induct {α β : Type} (f : α → β) (motive : Many α → Prop) (case1 : motive Many.none)
+info: many_map.induct {α : Type} (motive : Many α → Prop) (case1 : motive Many.none)
   (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) (a✝ : Many α) : motive a✝
 -/
 #guard_msgs in

tests/lean/run/funind_proof.lean

@@ -31,7 +31,7 @@ end
 
 
 /--
-info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2 : List Term → Prop)
+info: Term.replaceConst.induct (a : String) (motive1 : Term → Prop) (motive2 : List Term → Prop)
   (case1 : ∀ (a_1 : String), (a == a_1) = true → motive1 (const a_1))
   (case2 : ∀ (a_1 : String), ¬(a == a_1) = true → motive1 (const a_1))
   (case3 : ∀ (a : String) (cs : List Term), motive2 cs → motive1 (app a cs)) (case4 : motive2 [])
@@ -64,7 +64,7 @@ theorem numConsts_replaceConst' (a b : String) (e : Term) : numConsts (replaceCo
   <;> intros <;> simp [replaceConst, numConsts, replaceConstLst, numConstsLst, *]
 
 theorem numConsts_replaceConst'' (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by
-  induction e using replaceConst.induct (a := a) (b := b)
+  induction e using replaceConst.induct (a := a)
     (motive2 := fun es =>  numConstsLst (replaceConstLst a b es) = numConstsLst es) <;>
     simp [replaceConst, numConsts, replaceConstLst, numConstsLst, *]
 

tests/lean/run/funind_tests.lean

@@ -367,8 +367,8 @@ def unary (base : Nat) : Nat → Nat
 termination_by n => n
 
 /--
-info: UnusedExtraParams.unary.induct (base : Nat) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive n.succ) (a✝ : Nat) : motive a✝
+info: UnusedExtraParams.unary.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check unary.induct
@@ -379,7 +379,7 @@ def binary (base : Nat) : Nat → Nat → Nat
 termination_by n => n
 
 /--
-info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
+info: UnusedExtraParams.binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (n m : Nat), motive n m → motive n.succ m) (a✝ a✝¹ : Nat) : motive a✝ a✝¹
 -/
 #guard_msgs in
@@ -621,23 +621,23 @@ def Tree.map_forest (f : Tree → Tree) (ts : List Tree) : List Tree :=
 end
 
 /--
-info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
+info: Tree.Tree.map.induct (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
   (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts))
   (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (a✝ : Tree) : motive1 a✝
 -/
 #guard_msgs in
 #check Tree.map.induct
 
 /--
-info: Tree.Tree.map_forest.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
+info: Tree.Tree.map_forest.induct (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
   (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts))
   (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (ts : List Tree) : motive2 ts
 -/
 #guard_msgs in
 #check Tree.map_forest.induct
 
 /--
-info: Tree.Tree.map.mutual_induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
+info: Tree.Tree.map.mutual_induct (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
   (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts))
   (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) :
   (∀ (a : Tree), motive1 a) ∧ ∀ (ts : List Tree), motive2 ts
@@ -658,8 +658,8 @@ def unary (fixed : Bool := false) (n : Nat := 0)  : Nat :=
 termination_by n
 
 /--
-info: DefaultArgument.unary.induct (fixed : Bool) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive n.succ) (n : Nat) : motive n
+info: DefaultArgument.unary.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check unary.induct
@@ -671,7 +671,7 @@ def foo (fixed : Bool := false) (n : Nat) (m : Nat := 0) : Nat :=
 termination_by n
 
 /--
-info: DefaultArgument.foo.induct (fixed : Bool) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
+info: DefaultArgument.foo.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (m n : Nat), motive n m → motive n.succ m) (n m : Nat) : motive n m
 -/
 #guard_msgs in

tests/lean/run/issue5767.lean

@@ -53,12 +53,11 @@ def go2 (ss : Int) (st0 : St) : Bool :=
       decreasing_by sorry
 
 /--
-info: go2.induct : Int →
-  ∀ (motive : St → Prop),
-    (∀ (x : St),
-        let st1 := { m := x.m, map := x.map.insert };
-        motive st1 → motive x) →
-      ∀ (st0 : St), motive st0
+info: go2.induct : ∀ (motive : St → Prop),
+  (∀ (x : St),
+      let st1 := { m := x.m, map := x.map.insert };
+      motive st1 → motive x) →
+    ∀ (st0 : St), motive st0
 -/
 #guard_msgs in
 #check @go2.induct

tests/lean/run/structuralMutual.lean

@@ -682,7 +682,7 @@ info: EvenOdd.isEven.induct (motive_1 motive_2 : Nat → Prop) (case1 : motive_1
 #check EvenOdd.isEven.induct
 
 /--
-info: WithTuple.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithTuple.Tree α → Prop)
+info: WithTuple.Tree.map.induct {α : Type} (motive_1 : WithTuple.Tree α → Prop)
   (motive_2 : WithTuple.Tree α × WithTuple.Tree α → Prop)
   (case1 :
     ∀ (x : α) (arrs : WithTuple.Tree α × WithTuple.Tree α), motive_2 arrs → motive_1 (WithTuple.Tree.node x arrs))
@@ -693,8 +693,8 @@ info: WithTuple.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithT
 #check WithTuple.Tree.map.induct
 
 /--
-info: WithArray.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithArray.Tree α → Prop)
-  (motive_2 : Array (WithArray.Tree α) → Prop) (motive_3 : List (WithArray.Tree α) → Prop)
+info: WithArray.Tree.map.induct {α : Type} (motive_1 : WithArray.Tree α → Prop) (motive_2 : Array (WithArray.Tree α) → Prop)
+  (motive_3 : List (WithArray.Tree α) → Prop)
   (case1 : ∀ (x : α) (arr₁ : Array (WithArray.Tree α)), motive_2 arr₁ → motive_1 (WithArray.Tree.node x arr₁))
   (case2 : ∀ (arr₁ : List (WithArray.Tree α)), motive_3 arr₁ → motive_2 { toList := arr₁ }) (case3 : motive_3 [])
   (case4 : ∀ (h₁ : WithArray.Tree α) (t₁ : List (WithArray.Tree α)), motive_1 h₁ → motive_3 t₁ → motive_3 (h₁ :: t₁))