From d2853ecbc44716217731a9e94f21421d600fb3a1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 6 Dec 2024 18:07:16 +0100 Subject: [PATCH] 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 | 24 ++++++++++-------------- tests/lean/run/4320.lean | 2 +- tests/lean/run/funind_proof.lean | 4 ++-- tests/lean/run/funind_tests.lean | 18 +++++++++--------- tests/lean/run/issue5767.lean | 11 +++++------ tests/lean/run/structuralMutual.lean | 6 +++--- 6 files changed, 30 insertions(+), 35 deletions(-) diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index 780d4438e755..2c7cda048d9a 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/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' diff --git a/tests/lean/run/4320.lean b/tests/lean/run/4320.lean index adcdfd4a3d03..5c8cadaedd25 100644 --- a/tests/lean/run/4320.lean +++ b/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 diff --git a/tests/lean/run/funind_proof.lean b/tests/lean/run/funind_proof.lean index f6b24b0c0258..09495272495f 100644 --- a/tests/lean/run/funind_proof.lean +++ b/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, *] diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean index dfd695869666..c1e2035dfc9e 100644 --- a/tests/lean/run/funind_tests.lean +++ b/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,7 +621,7 @@ 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✝ -/ @@ -629,7 +629,7 @@ info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive #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 -/ @@ -637,7 +637,7 @@ info: Tree.Tree.map_forest.induct (f : Tree → Tree) (motive1 : Tree → Prop) #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 diff --git a/tests/lean/run/issue5767.lean b/tests/lean/run/issue5767.lean index 48f6754ed35a..c7ced93d71f5 100644 --- a/tests/lean/run/issue5767.lean +++ b/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 diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index b8ad61f2509d..24eba94e9de2 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/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₁))