fix: match generalization bug

doc/tactics.md

@@ -244,7 +244,7 @@ theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a
   | cons b bs ih => cases h with
     | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
     | tail a b bs h =>
-      match (generalizing := false) bs, ih h with
+      match bs, ih h with
       | _, ⟨s, ⟨t, rfl⟩⟩ =>
         exists b::s; exists t
         rw [List.cons_append]

src/Lean/Elab/Match.lean

@@ -935,10 +935,22 @@ private def generalize (discrs : Array Expr) (matchType : Expr) (altViews : Arra
       -- trace[Meta.debug] "matchType': {matchType'}"
       if (← isTypeCorrect matchType') then
         let discrs := discrs ++ ys
-        let ysIds ← ys.mapM fun y => do
-          let yDecl ← getLocalDecl y.fvarId!
-          return mkIdentFrom (← getRef) yDecl.userName
-        let altViews := altViews.map fun altView => { altView with patterns := altView.patterns ++ ysIds }
+        let altViews ← altViews.mapM fun altView => do
+          let patternVars ← getPatternsVars altView.patterns
+          -- We traverse backwards because we want to keep the most recent names.
+          -- For example, if `ys` contains `#[h, h]`, we want to make sure `mkFreshUsername is applied to the first `h`,
+          -- since it is already shadowed by the second.
+          let ysUserNames ← ys.foldrM (init := #[]) fun ys ysUserNames => do
+            let yDecl ← getLocalDecl ys.fvarId!
+            let mut yUserName := yDecl.userName
+            if ysUserNames.contains yUserName then
+              yUserName ← mkFreshUserName yUserName
+            -- Explicitly provided pattern variables shadow `y`
+            else if patternVars.any fun | PatternVar.localVar x => x == yUserName | _ => false then
+              yUserName ← mkFreshUserName yUserName
+            return ysUserNames.push yUserName
+          let ysIds ← ysUserNames.reverse.mapM fun n => return mkIdentFrom (← getRef) n
+          return { altView with patterns := altView.patterns ++ ysIds }
         return (discrs, matchType', altViews, true)
       else
         return (discrs, matchType, altViews, true)

tests/lean/run/matchGenBug.lean

@@ -0,0 +1,20 @@
+theorem foo (x : Nat) (h : x > 0) : x ≠ 0 :=
+  match x with
+  | 0   => sorry
+  | h+1 => sorry
+
+inductive Mem : α → List α → Prop where
+ | head (a : α) (as : List α)   : Mem a (a::as)
+ | tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
+infix:50 "∈" => Mem
+
+theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t := by
+  induction as with
+  | nil          => cases h
+  | cons b bs ih => cases h with
+    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
+    | tail a b bs h =>
+      match bs, ih h with
+      | _, ⟨s, t, rfl⟩ =>
+        exists b::s; exists t
+        rw [List.cons_append]