(kernel) constant has already been declared during simp

[TwoFX]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

inductive Impl where
  | inner (l r : Impl)
  | leaf

namespace Impl

inductive Balanced : Impl → Prop where
  | leaf : Balanced leaf

@[inline]
def balanceLErase (r : Impl) (hrb : Balanced r) : Impl :=
  match r with
  | leaf => .leaf
  | l@(inner _ _) =>
    match l with
    | leaf => .leaf
    | r@(inner ll lr) =>
        if true then
          match ll, lr with
          | inner _ _, inner _ _ => .leaf
          | _, _ => .leaf
        else .leaf

/-- error: (kernel) constant has already been declared 'Impl.balanceLErase.match_1.eq_1' -/
#guard_msgs in
theorem size_balanceLErase {r : Impl} {hrb} : (balanceLErase r hrb) = .leaf := by
  simp only [balanceLErase.eq_def]

Expected behavior: No error

Actual behavior: See above

Versions

4.15.0-nightly-2024-11-13 on live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

One of the matches cannot be split:

set_option trace.split.failure true
/--
error: tactic 'split' failed, consider using `set_option trace.split.failure true`
case h_2.h_2
r✝¹ : Impl
hrb✝² : r✝¹.Balanced
l✝¹ r✝ l✝ : Impl
h✝¹ : l✝ = l✝¹.inner r✝
hrb✝¹ : (namedPattern l✝ (l✝¹.inner r✝) h✝¹).Balanced
ll✝ lr✝ : Impl
h✝ : ll✝.inner lr✝ = l✝¹.inner r✝
hrb✝ : (l✝¹.inner r✝).Balanced
heq✝¹ : l✝¹.inner r✝ = ll✝.inner lr✝
heq✝ : HEq ⋯ h✝
⊢ (match ll✝, lr✝, ⋯, h✝, hrb✝ with
    | l.inner r, l_1.inner r_1, h, h_1, hrb => leaf
    | x, x_1, h, h_1, hrb => leaf) =
    leaf
---
info: [split.failure] `split` tactic failed at
      match ll✝, lr✝, ⋯, h✝, hrb✝ with
      | l.inner r, l_1.inner r_1, h, h_1, hrb => Impl.leaf
      | x, x_1, h, h_1, hrb => Impl.leaf
    tactic 'contradiction' failed, metavariable has already been assigned
    l✝¹ r✝¹ l✝ r✝ : Impl
    hrb✝ : ((l✝¹.inner r✝¹).inner (l✝.inner r✝)).Balanced
    motive :
      (ll lr : Impl) →
        (h : (l✝¹.inner r✝¹).inner (l✝.inner r✝) = ll.inner lr) →
          (h_3 :
              namedPattern ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) (ll.inner lr) h =
                (l✝¹.inner r✝¹).inner (l✝.inner r✝)) →
            (namedPattern (namedPattern ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) (ll.inner lr) h)
                  ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) h_3).Balanced →
              Sort u_1
    h✝ :
      namedPattern ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) ⋯ =
        (l✝¹.inner r✝¹).inner (l✝.inner r✝)
    hrb :
      (namedPattern (namedPattern ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) ⋯)
          ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) h✝).Balanced
    h_1 :
      (l r l_1 r_1 : Impl) →
        (h : (l✝¹.inner r✝¹).inner (l✝.inner r✝) = (l.inner r).inner (l_1.inner r_1)) →
          (h_3 :
              namedPattern ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) ((l.inner r).inner (l_1.inner r_1)) h =
                (l✝¹.inner r✝¹).inner (l✝.inner r✝)) →
            (hrb :
                (namedPattern (namedPattern ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) ((l.inner r).inner (l_1.inner r_1)) h)
                    ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) h_3).Balanced) →
              motive (l.inner r) (l_1.inner r_1) h h_3 hrb
    h_2 :
      (x x_1 : Impl) →
        (h : (l✝¹.inner r✝¹).inner (l✝.inner r✝) = x.inner x_1) →
          (h_3 :
              namedPattern ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) (x.inner x_1) h =
                (l✝¹.inner r✝¹).inner (l✝.inner r✝)) →
            (hrb :
                (namedPattern (namedPattern ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) (x.inner x_1) h)
                    ((l✝¹.inner r✝¹).inner (l✝.inner r✝)) h_3).Balanced) →
              motive x x_1 h h_3 hrb
    l_eq✝² : l✝¹ = l✝¹
    r_eq✝³ : r✝¹ = r✝¹
    l_eq✝¹ : l✝ = l✝
    r_eq✝² : r✝ = r✝
    r_eq✝¹ : l✝.inner r✝ = l✝.inner r✝
    l_eq✝ : l✝¹ = l✝¹
    r_eq✝ : r✝¹ = r✝¹
    ⊢ False
-/
#guard_msgs in
theorem size_balanceLErase {r : Impl} {hrb} : (balanceLErase r hrb) = .leaf := by
  rw [balanceLErase.eq_def]
  split
  · rfl
  · split
    · rfl
    · dsimp
      split      

My assumption for this bug is that when simp tries to rewrite with the equations, and thus creates the splitter and equations, then this process fails when adding .eq_1, but the environment isn’t rolled back, so simp tries again, but now .eq_1 already exists.

Didn’t dig deeper, but if that’s true, then

• we should move the splitter generation into the same machinery as other realizable constants, just for uniformity (I believe @Kha has that on a branch already?)
• implemented RFC: Realizalbe constants error handling #5944 so that we do not try to generate the splitter over and over
• make sure that if it fails, we roll back the environment changes.

[Kha]

we should move the splitter generation into the same machinery as other realizable constants, just for uniformity (I believe @Kha has that on a branch already?)

Yep, I can land that independently once the general Environment.realizeConst machinery has landed