simp Discrtree question

Stream: lean4

[Floris van Doorn]

When doing simp investigations, I found something surprising.
In the following code snippet simp doesn't simplify anything (as expected), but there are two unification failures, that I thought would be lemmas excluded because of the discrimination tree.

import Std.Data.Nat.Lemmas

set_option trace.Meta.Tactic.simp true
attribute [simp] Nat.succ_ne_self -- this is a simp-lemma in Mathlib
example (a : Nat) : 0 = a := by
  simp

This gives three unification failures:

[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
      ?a = ?a
    with
      0 = a

[Meta.Tactic.simp.unify] Nat.succ.injEq:1000, failed to unify
      Nat.succ ?n = Nat.succ ?n
    with
      0 = a

[Meta.Tactic.simp.unify] Nat.succ_ne_self:1000, failed to unify
      Nat.succ ?n = ?n
    with
      0 = a

The first one makes sense to me, but why are the other two not caught by Discrimination tree considerations. 0 = _ shouldn't match the discrimination tree entries for these two lemmas, or should they?
For convenience, here is the statement for these lemmas:

#check Nat.succ.injEq -- Nat.succ.injEq (n m : Nat) : (Nat.succ n = Nat.succ m) = (n = m)
#check Nat.succ_ne_self -- Nat.succ_ne_self (n : Nat) : Nat.succ n ≠ n

[Mario Carneiro]

I think Nat.succ is considered as matching numerals, although maybe it shouldn't be considered for that particular numeral

[Floris van Doorn]

Oh, that makes sense. Probably there is some rule that Nat.succ and OfNat.ofNat fall into the same category, because the patterns overlap.