From aba0a479ec221ad2e31de09c6e71ce82a705ec38 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Aug 2021 20:57:37 -0700
Subject: [PATCH] fix: `intro` at `split` tactic

---
 src/Lean/Meta/Tactic/Split.lean | 12 ++++++++----
 tests/lean/run/split1.lean      | 16 ++++++++++++++++
 2 files changed, 24 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/split1.lean

diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 3212dc2ec0..7cfb476c0d 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -24,6 +24,7 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
   let (reverted, mvarId) ← revert mvarId discrFVarIds
   trace[Meta.debug] "split [2]:\n{MessageData.ofGoal mvarId}"
   let (discrFVarIds, mvarId) ← introNP mvarId discrFVarIds.size
+  let numExtra := reverted.size - discrFVarIds.size
   trace[Meta.debug] "split [3]:\n{MessageData.ofGoal mvarId}"
   let discrs := discrFVarIds.map mkFVar
   let matchEqns ← Match.getEquationsFor app.matcherName
@@ -41,11 +42,14 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
     trace[Meta.debug] "splitter: {splitter}"
     check splitter -- TODO
     let mvarIds ← apply mvarId splitter
-    mvarIds.mapM fun mvarId => do
+    let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do
       trace[Meta.debug] "split [5]:\n{MessageData.ofGoal mvarId}"
-      -- TODO: fix intros, use equation lemmas to reduce `match`-expressions
-      let (_, mvarId) ← intros mvarId
-      return mvarId
+      let numParams := matchEqns.splitterAltNumParams[i]
+      -- TODO: use equation lemmas to reduce `match`-expressions
+      let (_, mvarId) ← introN mvarId numParams
+      let (_, mvarId) ← introNP mvarId numExtra
+      return (i+1, mvarId::mvarIds)
+    return mvarIds.reverse
 
 /-- Return an `if-then-else` or `match-expr` to split. -/
 partial def findSplit? (env : Environment) (e : Expr) : Option Expr :=
diff --git a/tests/lean/run/split1.lean b/tests/lean/run/split1.lean
new file mode 100644
index 0000000000..8dfde9a0ce
--- /dev/null
+++ b/tests/lean/run/split1.lean
@@ -0,0 +1,16 @@
+def f (xs : List Nat) : Nat :=
+  match xs with
+  | [] => 1
+  | [a, b] => (a + b).succ
+  | _ => 2
+
+theorem ex (xs : List Nat) (hr : xs.reverse = xs) (ys : Nat) : ys > 0 → f xs > 0 := by
+  simp [f]
+  split
+  next => intro hys; simp
+  next => intro hys; simp; apply Nat.zero_lt_succ
+  next zs n₁ n₂ =>
+    intro hys
+    rw [f.match_1.eq_3]
+    anyGoals assumption
+    decide