match_pattern and induction/cases

Stream: lean4

[Ghilain Bergeron]

I have this MWE (lean v4.11.0-rc1) because my original problem is quite large, but the core of the problem is here

inductive X : Type
  | mkX : List Unit → X

@[match_pattern]
abbrev X.nil : X := ⟨[]⟩

@[match_pattern]
abbrev X.cons : Unit → X → X | x, ⟨xs⟩ => ⟨x :: xs⟩

inductive P : X → X → Prop
  | step {x'} : P x' x' → P (X.cons () x') (X.cons () x')
  | nil : P X.nil X.nil

theorem bug? {x' a} (h : P (X.cons () x') a) : ∃ x'', a = X.cons () x'' := by
  cases h
  -- error

I get the error that

dependent elimination failed, failed to solve equation
  x'.1 = x'✝.1

Obviously this comes from my X.cons, which somehow the dependent pattern matcher fails to match against (although it is a @[match_pattern])
Is this to be expected? If yes, how can I work around this issue without having to call P.casesOn by hand with the correct motive?

---

For reference, this proof works but is not very elegant and seems like a hack to me (which, also, does not scale well with the number of cases of the inductively defined type/prop):

  refine P.casesOn (motive := λ a_1 a_2 t => X.cons () x' = a_1 → a = a_2 → HEq h t → ∃ x'', a = X.cons () x'') h ?_ ?_ (Eq.refl (X.cons () x')) (Eq.refl a) (HEq.refl h)
  · intros _ _ _ a_eq _
    exact ⟨_, a_eq⟩
  · intros _ _ _
    exfalso
    injections

[Filippo A. E. Nuccio]

If you separate it to another lemma, you can make this work:

inductive X : Type
  | mkX : List Unit → X

abbrev X.nil : X := ⟨[]⟩

abbrev X.cons : Unit → X → X | x, ⟨xs⟩ => ⟨x :: xs⟩

inductive P : X → X → Prop
  | step (x' : X) : P x' x' → P (X.cons () x') (X.cons () x')
  | nil : P X.nil X.nil

theorem no_bug {x' y a : X} (h : P y a) (hy : y = X.cons () x' ): ∃ x'', a = X.cons () x'' := by
  rcases h with ⟨x, h'⟩ | _
  · exact ⟨x, rfl⟩
  · refine ⟨x', hy⟩

theorem bug? {x' a} (h : P (X.cons () x') a) : ∃ x'', a = X.cons () x'' := by
  let y := X.cons () x'
  have hy : y = X.cons () x' := rfl
  rw [← hy] at h
  exact no_bug h hy

[Filippo A. E. Nuccio]

Observe that if you import mathlib, the sequence let+have can be replaced by set y ... with rfl.

[Ghilain Bergeron]

Oh I see, indeed generalizing the problematic bit to a variable seems to make it work!

[Filippo A. E. Nuccio]

Also, no need for the @match tag.