From 0072d13bd40aef791090d1e3e964413f1176162e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 6 Mar 2024 16:56:17 +0100 Subject: [PATCH] =?UTF-8?q?feat:=20MatcherApp.transform:=20Try=20to=20pres?= =?UTF-8?q?erve=20alt=E2=80=99s=20variable=20name=20(#3620)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit this makes the ugly `fst`/`snd` variable names in the functional induction principles go away. Ironically I thought in order to fix these name, I should touch the mutual/n-ary argument packing code used for well-founded recursion, and embarked on a big refactor/rewrite of that code, only to find that at least this particular instance of the issue was somewhere else. Hence breaking this into its own PR; the refactoring will follow (and will also improve some other variable names.) --- src/Lean/Meta/Match/MatcherApp/Transform.lean | 20 +++++++++++-- tests/lean/run/funind_mutual_dep.lean | 18 ++++++------ tests/lean/run/funind_tests.lean | 29 +++++++++---------- 3 files changed, 39 insertions(+), 28 deletions(-) diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean index 27790d1f3d93..28183b813892 100644 --- a/src/Lean/Meta/Match/MatcherApp/Transform.lean +++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean @@ -176,6 +176,17 @@ def arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr) := do type := β return ts +/-- +Sets the user name of the FVars in the local context according to the given array of names. + +If they differ in size the shorter size wins. +-/ +def withUserNames {α} (fvars : Array Expr) (names : Array Name) (k : MetaM α ) : MetaM α := do + let lctx := (Array.zip fvars names).foldl (init := ← (getLCtx)) fun lctx (fvar, name) => + lctx.setUserName fvar.fvarId! name + withTheReader Meta.Context (fun ctx => { ctx with lctx }) k + + /-- Performs a possibly type-changing transformation to a `MatcherApp`. @@ -320,9 +331,12 @@ def transform (matcherApp : MatcherApp) altType in altTypes do let alt' ← forallBoundedTelescope altType numParams fun xs altType => do forallBoundedTelescope altType extraEqualities fun ys4 altType => do - let alt ← instantiateLambda alt xs - let alt' ← onAlt altType alt - mkLambdaFVars (xs ++ ys4) alt' + -- we should try to preserve the variable names in the alternative + let names ← lambdaTelescope alt fun xs _ => xs.mapM (·.fvarId!.getUserName) + withUserNames xs names do + let alt ← instantiateLambda alt xs + let alt' ← onAlt altType alt + mkLambdaFVars (xs ++ ys4) alt' alts' := alts'.push alt' remaining' := remaining' ++ (← onRemaining matcherApp.remaining) diff --git a/tests/lean/run/funind_mutual_dep.lean b/tests/lean/run/funind_mutual_dep.lean index e503e181c292..e3a4d6c96c83 100644 --- a/tests/lean/run/funind_mutual_dep.lean +++ b/tests/lean/run/funind_mutual_dep.lean @@ -53,18 +53,18 @@ info: Finite.functions.induct (motive1 : Finite → Prop) (motive2 : (x : Type) (case3 : ∀ (t1 t2 : Finite), motive1 t1 → motive1 t2 → motive1 (Finite.pair t1 t2)) (case4 : ∀ (t1 t2 : Finite), motive1 t2 → motive2 (Finite.asType t2) t1 (Finite.enumerate t2) → motive1 (Finite.arr t1 t2)) - (case5 : ∀ (fst : Type) (snd : List fst), motive2 fst Finite.unit snd) - (case6 : ∀ (fst : Type) (snd : List fst), motive2 fst Finite.bool snd) + (case5 : ∀ (α : Type) (results : List α), motive2 α Finite.unit results) + (case6 : ∀ (α : Type) (results : List α), motive2 α Finite.bool results) (case7 : - ∀ (fst : Type) (snd : List fst) (t1 t2 : Finite), - motive2 fst t2 snd → - motive2 (Finite.asType t2 → fst) t1 (Finite.functions t2 snd) → motive2 fst (Finite.pair t1 t2) snd) + ∀ (α : Type) (results : List α) (t1 t2 : Finite), + motive2 α t2 results → + motive2 (Finite.asType t2 → α) t1 (Finite.functions t2 results) → motive2 α (Finite.pair t1 t2) results) (case8 : - ∀ (fst : Type) (snd : List fst) (t1 t2 : Finite), + ∀ (α : Type) (results : List α) (t1 t2 : Finite), motive1 t1 → - (∀ (rest : List (Finite.asType (Finite.arr t1 t2) → fst)), - motive2 (Finite.asType (Finite.arr t1 t2) → fst) t2 rest) → - motive2 fst (Finite.arr t1 t2) snd) + (∀ (rest : List (Finite.asType (Finite.arr t1 t2) → α)), + motive2 (Finite.asType (Finite.arr t1 t2) → α) t2 rest) → + motive2 α (Finite.arr t1 t2) results) (x : Type) (x : Finite) (x : List x) : motive2 x x x -/ #guard_msgs in diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean index 9c9fc4361145..175cf0069d45 100644 --- a/tests/lean/run/funind_tests.lean +++ b/tests/lean/run/funind_tests.lean @@ -242,9 +242,9 @@ termination_by i derive_functional_induction with_arg_refining_match1 /-- -info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (fst : Nat), motive fst 0) +info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0) (case2 : ∀ (n : Nat), motive 0 (Nat.succ n)) - (case3 : ∀ (fst n : Nat), ¬fst = 0 → motive (fst - 1) n → motive fst (Nat.succ n)) (x x : Nat) : motive x x + (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i (Nat.succ n)) (x x : Nat) : motive x x -/ #guard_msgs in #check with_arg_refining_match1.induct @@ -257,9 +257,9 @@ termination_by i derive_functional_induction with_arg_refining_match2 /-- -info: with_arg_refining_match2.induct (motive : Nat → Nat → Prop) (case1 : ∀ (snd : Nat), motive 0 snd) - (case2 : ∀ (fst : Nat), ¬fst = 0 → motive fst 0) - (case3 : ∀ (fst : Nat), ¬fst = 0 → ∀ (n : Nat), motive (fst - 1) n → motive fst (Nat.succ n)) (x x : Nat) : motive x x +info: with_arg_refining_match2.induct (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), motive 0 n) + (case2 : ∀ (i : Nat), ¬i = 0 → motive i 0) + (case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i (Nat.succ n)) (x x : Nat) : motive x x -/ #guard_msgs in #check with_arg_refining_match2.induct @@ -292,10 +292,8 @@ termination_by n => n derive_functional_induction with_mixed_match_tailrec /-- -info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) - (case1 : ∀ (fst snd x : Nat), motive 0 x fst snd) - (case2 : ∀ (fst snd a x : Nat), motive a x (fst % 2) (snd % 2) → motive (Nat.succ a) x fst snd) (x x x x : Nat) : - motive x x x x +info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (c d x : Nat), motive 0 x c d) + (case2 : ∀ (c d a x : Nat), motive a x (c % 2) (d % 2) → motive (Nat.succ a) x c d) (x x x x : Nat) : motive x x x x -/ #guard_msgs in #check with_mixed_match_tailrec.induct @@ -313,9 +311,8 @@ derive_functional_induction with_mixed_match_tailrec2 /-- info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop) - (case1 : ∀ (fst fst_1 fst_2 snd : Nat), motive 0 fst fst_1 fst_2 snd) - (case2 : ∀ (fst snd n x : Nat), motive (Nat.succ n) 0 x fst snd) - (case3 : ∀ (fst snd n a x : Nat), motive n a x (fst % 2) (snd % 2) → motive (Nat.succ n) (Nat.succ a) x fst snd) + (case1 : ∀ (a b c d : Nat), motive 0 a b c d) (case2 : ∀ (c d n x : Nat), motive (Nat.succ n) 0 x c d) + (case3 : ∀ (c d n a x : Nat), motive n a x (c % 2) (d % 2) → motive (Nat.succ n) (Nat.succ a) x c d) (x x x x x : Nat) : motive x x x x x -/ #guard_msgs in @@ -655,7 +652,7 @@ derive_functional_induction Tree.map /-- info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop) (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts)) - (case2 : ∀ (val : List Tree), (∀ (t : Tree), t ∈ val → motive1 t) → motive2 val) (x : Tree) : motive1 x + (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (x : Tree) : motive1 x -/ #guard_msgs in #check Tree.map.induct @@ -663,7 +660,7 @@ info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive /-- info: Tree.Tree.map_forest.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop) (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts)) - (case2 : ∀ (val : List Tree), (∀ (t : Tree), t ∈ val → motive1 t) → motive2 val) (x : List Tree) : motive2 x + (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (x : List Tree) : motive2 x -/ #guard_msgs in #check Tree.map_forest.induct @@ -696,8 +693,8 @@ termination_by n derive_functional_induction foo /-- -info: DefaultArgument.foo.induct (fixed : Bool) (motive : Nat → Nat → Prop) (case1 : ∀ (snd : Nat), motive 0 snd) - (case2 : ∀ (snd n : Nat), motive n snd → motive (Nat.succ n) snd) (x x : Nat) : motive x x +info: DefaultArgument.foo.induct (fixed : Bool) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) + (case2 : ∀ (m n : Nat), motive n m → motive (Nat.succ n) m) (x x : Nat) : motive x x -/ #guard_msgs in #check foo.induct