linarith and ENNReal

Stream: mathlib4

[Moritz Firsching]

While porting Topology.MetricSpace.EMetricParacompact, mathlib4#2599, there are three cases where linarith worked before and doesn't anymore. Now it says

failed to synthesize
  AddGroup ℝ≥0∞

Is this expected? Should I work around that or is there some simple way to make it work as before?

[Ruben Van de Velde]

Pretty sure that ℝ≥0∞ is not an AddGroup, but I don't know why linarith thinks it should be

[Kevin Buzzard]

In the corresponding file in Lean 3 linarith is used three times, and each time it's closing goals about nats. So this might not be a problem with linarith but a problem with elaboration, if it's now thinking it's supposed to be solving goals about ennreals (the goals are n < m, k + 1 \le m and k + 1 \le n + k + 1)

[Eric Wieser]

In Lean4 the goals are also about nats

[Eric Wieser]

If you replace the first failing line with

have : z ∉ ball x (2⁻¹ ^ k) := fun hz' => H n (by clear hz; linarith) i (hsub hz')

then it instead complains

failed to synthesize
  AddGroup (ℕ → ι → Set α)

[Eric Wieser]

This works:

have : z ∉ ball x (2⁻¹ ^ k) := fun hz' => H n (by clear hz hD; linarith) i (hsub hz')

[Eric Wieser]

But this is clearly a bug in linarith, it should just ignore inequalities in the context it doesn't understand

[Eric Wieser]

#mwe:

import Mathlib.Tactic.Linarith

example : 0 ≤ 1 := by linarith -- ok

example (s : Set ℕ) (h : s = ∅) : 0 ≤ 1 :=
by linarith
/-
failed to synthesize
  AddGroup (Set ℕ)
-/

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/pull/2605 adds a better error message

[Moritz Firsching]

Thanks for the explanation! I opened an issue for that: mathlib4#2610