Conflicting `simp` lemmas `List.push_append_toArray` and `Array.append_singleton`

Prerequisites

• 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

#lean4 > List.push_append_toArray vs Array.push_singleton @ 💬

Simp lemmas docs#List.push_append_toArray and docs#Array.append_singleton are normalizing in opposite directions:

variable (a₁ a₂ : α) (as : Array α)

#check_tactic as.push a₁ ++ #[a₂] ~> (as.push a₁).push a₂ by simp only [Array.append_singleton]
#check_tactic as.push a₁ ++ #[a₂] ~> as ++ #[a₁, a₂] by simp only [List.push_append_toArray]

In particular this makes normalization of arrays sensitive to the context and sensitive to the number of elements of an array in the context, resulting in terms that diverge rather than converge:

variable (a₁ a₂ a₃ : α) (as : Array α)

#check_simp (as.push a₁).push a₂ ++ #[a₃] = as.push a₁ ++ #[a₂, a₃]
  ~> ((as.push a₁).push a₂).push a₃ = as ++ #[a₁, a₂, a₃]

I ran into this expecting the following to close by simp:

example (a₁ a₂ : α) (as : Array α) :
    (as.push a₁).push a₂ = as ++ #[a₁, a₂] := by simp

Should List.push_append_toArray normalize in the opposite direction (cons → push)? It would close this goal.

Versions

4.32

Impact

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

Start with the minimal reproducer and the named simp lemmas List.push_append_toArray and Array.append_singleton; compare their normalization behavior using the shown #check_tactic and #check_simp examples. Done means the conflicting directions are reconciled and the final by simp example behaves consistently without context-sensitive divergence.