feat: improve discriminant refinement procedure

src/Lean/Elab/Match.lean

@@ -905,7 +905,8 @@ where
     match (← altViews'.mapM (fun altView => elabMatchAltView discrs' altView matchType' (toClear ++ toClear')) |>.run) with
     | Except.ok alts => return (discrs', matchType', alts, first?.isSome || refined)
     | Except.error { patternIdx := patternIdx, pathToIndex := pathToIndex, ex := ex } =>
-      let some index ← getIndexToInclude? discrs[patternIdx].expr pathToIndex
+      let discr := discrs[patternIdx]
+      let some index ← getIndexToInclude? discr.expr pathToIndex
         | throwEx (← updateFirst first? ex)
       trace[Elab.match] "index to include: {index}"
       if (← discrs.anyM fun discr => isDefEq discr.expr index) then
@@ -931,7 +932,14 @@ where
         else
           return mkHole ref
       let altViews  := altViews.map fun altView => { altView with patterns := wildcards ++ altView.patterns }
-      let discrs    := (indices.map fun i => { expr := i : Discr }) ++ discrs
+      let indDiscrs ← indices.mapM fun i => do
+        match discr.h? with
+        | none => return { expr := i : Discr }
+        | some h =>
+          -- If the discriminant that introduced this index is annotated with `h : discr`, then we should annotate the new discriminant too.
+          let h := mkIdentFrom h (← mkFreshUserName `h)
+          return { expr := i, h? := h : Discr }
+      let discrs    := indDiscrs ++ discrs
       let indexFVarIds := indices.filterMap fun | .fvar fvarId .. => some fvarId | _  => none
       loop discrs (toClear ++ indexFVarIds) matchType altViews first
 

tests/lean/run/splitList.lean

@@ -23,15 +23,14 @@ def len : List α → Nat
   | l@h₁:(a :: b :: as) =>
     -- Remark: we didn't use `_` because we currently don't have a way for getting a hypothesis stating that the previous two case were not taken here.
     -- h₁ : l = a :: b :: as
-    match h₂ : l, h₃ : splitList l with
-    | _, ListSplit.split fst snd =>
+    match h₂ : splitList l with
+    | ListSplit.split fst snd =>
       -- Remark: `match` refined `h₁`s type to `h₁ : fst ++ snd = a :: b :: as`
-      -- h₂ : l = fst ++ snd
-      -- h₃ : splitList l = ListSplit.split fst snd
+      -- h₂ : HEq (splitList l) (ListSplit.split fst snd)
       have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
       -- The following two proofs ase used to justify the recursive applications `len fst` and `len snd`
-      have dec₁ : fst.length < as.length + 2 := by subst h₂; simp_arith [eq_of_heq h₃] at this |- ; simp [this]
-      have dec₂ : snd.length < as.length + 2 := by subst h₂; simp_arith [eq_of_heq h₃] at this |- ; simp [this]
+      have dec₁ : fst.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
+      have dec₂ : snd.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
       len fst + len snd
 termination_by _ xs => xs.length