Importing Mathlib breaks simp_arith

Stream: mathlib4

[Francisco Giordano]

This example works:

example (l₀ : List α) (l : List α) (i : Nat) (h : l₀.length = l.length + i) : i < l₀.length := by
  cases l with
  | nil => sorry
  | cons => rw [h]; simp_arith

However, if I add an import of Mathlib.Data.List.Basic, the simp_arith tactic above stops working. The goal is converted to ⊢ Zero.zero ≤ List.length tail✝ and it remains unsolved. Oddly, using simp instead of simp_arith makes it work with the import, but it doesn't work without the import.

Is this normal or expected?

[Francisco Giordano]

(Please move to #mathlib4 if more appropriate... I meant to post there)

[Scott Morrison]

This is unfortunate, but not totally surprising. It appears that Mathlib has added simp lemmas that prevent simp_arith from working. As Mathlib essentially never uses simp_arith, this perhaps just hasn't been noticed.

[Francisco Giordano]

I've found that adding the following simp lemma, simp_arithworks as expected:

@[simp]
lemma zero_is_zero : Zero.zero = 0 := by rfl

Does this look like something that should be in Mathlib?

[Scott Morrison]

Looks plausible!

[Eric Wieser]

That statement looks like nonsense to me, it would elaborate as a tautology in most of mathlib

[Kevin Buzzard]

Your claim would contradict the claim that it fixes the problem above, right?

[Yaël Dillies]

We did have docs3#nat.nat_zero_eq_zero

[Ruben Van de Velde]

We still have that, right? But there the issue is with an inductive constructor that happens to be named zero

[Ruben Van de Velde]

Is zero_is_zero about Zero vs OfNat?

[Eric Wieser]

Kevin Buzzard said:

Your claim would contradict the claim that it fixes the problem above, right?

I guess my claim was that the message above is missing the context needed to be actionable, and the lemma elaborates in different ways depending on which file it goes in. I now realize that's also wrong.

[Joachim Breitner]

As Mathlib essentially never uses simp_arith, this perhaps just hasn't been noticed.

simp_arith is used as part of the default decreasing_tactic, so I hope this isn't broken :-)

[Alex J. Best]

It certainly is broken with mathlib see #7631

[Alex J. Best]

And https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Function.20on.20Tree.20type

[Eric Wieser]

Why is Zero.zero ever appearing in a goal in the first place?

[Eric Wieser]

Loogle suggests docs#AddLocalization.zero_def (which should be fixed) and docs#Mathlib.Meta.NormNum.isNat_zero (which might be an optimization?) are the only things that mention it

[Alex J. Best]

I guess simp arith tries to unfold as much as it can and gets stuck

[Francisco Giordano]

Here's a simpler example:

import Mathlib.Data.List.Basic -- causes simp_arith to fail to solve goal below
example : i < List.length (x :: xs) + i := by
  simp_arith

With tracing I found that the import causes simp to invoke docs#lt_add_iff_pos_left , which is defined for [AddZeroClass α]. This seems to be what causes Zero.zero to appear. At that point it is like #7631 and simp can't prove Zero.zero ≤ n

[Eric Wieser]

Oh, is the problem docs#AddZeroClass.add_zero ?