From 778333c667d0ae8d29b58849214a129fa05d0878 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 20 Jan 2025 18:05:37 -0800
Subject: [PATCH] fix: match equality generation (#6719)

This PR fixes a bug in the equational theorem generator for
`match`-expressions. See new test for an example.

Signed-off-by: Leonardo de Moura <leodemoura@amazon.com>
Co-authored-by: Leonardo de Moura <leodemoura@amazon.com>
---
 src/Init/Data/Nat/Linear.lean      |  5 ++---
 src/Lean/Meta/Match/MatchEqs.lean  |  7 +++++++
 tests/lean/run/match_eqns_bug.lean | 13 +++++++++++++
 3 files changed, 22 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/match_eqns_bug.lean

diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean
index c2add718c7..69c9ad82cd 100644
--- a/src/Init/Data/Nat/Linear.lean
+++ b/src/Init/Data/Nat/Linear.lean
@@ -718,8 +718,7 @@ theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly
 
 end Linear
 
-def elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) : α := by
-  simp_arith at h₁
-  exact h₂ h₁
+def elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) : α :=
+  h₂ (Nat.add_right_cancel h₁)
 
 end Nat
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 824f993010..77897e731d 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -322,6 +322,11 @@ private def substSomeVar (mvarId : MVarId) : MetaM (Array MVarId) := mvarId.with
           | none => pure ()
   throwError "substSomeVar failed"
 
+private def unfoldElimOffset (mvarId : MVarId) : MetaM MVarId := do
+  if Option.isNone <| (← mvarId.getType).find? fun e => e.isConstOf ``Nat.elimOffset then
+    throwError "goal's target does not contain `Nat.elimOffset`"
+  mvarId.deltaTarget (· == ``Nat.elimOffset)
+
 /--
   Helper method for proving a conditional equational theorem associated with an alternative of
   the `match`-eliminator `matchDeclName`. `type` contains the type of the theorem. -/
@@ -343,6 +348,8 @@ where
       <|>
       (do mvarId.contradiction { genDiseq := true }; return #[])
       <|>
+      (do let mvarId ← unfoldElimOffset mvarId; return #[mvarId])
+      <|>
       (casesOnStuckLHS mvarId)
       <|>
       (do let mvarId' ← simpIfTarget mvarId (useDecide := true)
diff --git a/tests/lean/run/match_eqns_bug.lean b/tests/lean/run/match_eqns_bug.lean
new file mode 100644
index 0000000000..d1a3f90cc8
--- /dev/null
+++ b/tests/lean/run/match_eqns_bug.lean
@@ -0,0 +1,13 @@
+inductive Vec (α : Type u) : Nat → Type u
+  | zero : Vec α 0
+  | cons : α → Vec α n → Vec α (n+1)
+
+def g (n : Nat) (v w : Vec α n) : Nat :=
+  match v, w with
+  | .zero, _  => 1
+  | _, .cons _ (.cons _ _ ) => 2
+  | _, _ => 3
+
+example (h : g a b c = 4) : False := by
+  unfold g at h
+  split at h <;> contradiction