Linarith in the presence of WithBot?

Stream: lean4

[Siddharth Bhat]

I have a goal of the form

qt: ℕ
hqgt1: Fact (q > 1)
n: ℕ
M: Type u_1
inst✝¹: Semiring M
inst✝: DecidableEq M
x: M
xs: List M
IH: degree { toFinsupp := List.toFinsupp xs } ≤ ↑(List.length xs)
a: ℕ
ha: a ∈ Finset.filter (fun i => ¬List.getD (x :: xs) i 0 = 0) (insert (List.length xs) (Finset.range (List.length xs)))
ha₁: a ∈ insert (List.length xs) (Finset.range (List.length xs))
ha₂: ¬List.getD (x :: xs) a 0 = 0
ha₅: a ∈ Finset.range (List.length xs)
ha₆: a < List.length xs
⊢ a ≤ List.length xs + 1

and this should follow from linarith (via ha₆), but I get the error:

application type mismatch
  neg_nonpos_of_nonneg (Linarith.nat_cast_nonneg (WithBot ℕ) (List.length xs))
argument
  Linarith.nat_cast_nonneg (WithBot ℕ) (List.length xs)
has type
  @OfNat.ofNat (WithBot ℕ) 0 (@Zero.toOfNat0 (WithBot ℕ) MonoidWithZero.toZero) ≤ ↑(List.length xs) : Prop
but is expected to have type
  @OfNat.ofNat (WithBot ℕ) 0 (@Zero.toOfNat0 (WithBot ℕ) NegZeroClass.toZero) ≤ ?a : Prop

Is this expected behaviour?

[Alex J. Best]

No, if you could minify it that would be helpful to debug further

[Eric Wieser]

I think the error message is saying that linarith can't handle this because WithBot Nat is a semiring and not a ring

[Alex J. Best]

linarith should be able to handle proving the goal from h6 in this example, and indeed it can in a simplified example c.f.

import Mathlib.Tactic

example {l : List T} (h : a < l.length) : a <= l.length + 1 := by
  linarith

so it must be some other part of the context confusing things, which shouldn't happen. But I can't reproduce the failure easily without a #mwe

[Mario Carneiro]

I think this recently came up and I made a PR to fix it, unsure if it landed

[Mario Carneiro]

#7916 did land