feat: MatcherApp.transform: Try to preserve alt’s variable name (#3620)

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

@@ -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)

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

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,15 +652,15 @@ 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
 
 /--
 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