omega canonicalizer vs. universe expressions

[nomeata]

At the time of writing, omega does not use full defEq when recognizing atoms, but since #3639 the aim is to consider atoms equal if they are definitionally equal, but differ only in implicit parameters.

Universe parameters are similarly implicit to the user, and cause great confusion in a proof like

theorem sizeOf_snd_lt_sizeOf_list
  {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {x : α × β} {xs : List (α × β)} :
  x ∈ xs → sizeOf x.snd < 1 + sizeOf xs
:= by
  intro h
  have h1 := List.sizeOf_lt_of_mem h
  have h2 : sizeOf x = 1 + sizeOf x.1 + sizeOf x.2 := rfl
  cases x; dsimp at *
  omega

where the user sees

omega did not find a contradiction:
[0, 0, 1] ∈ [0, ∞)
[0, 0, 0, 1] ∈ [0, ∞)
[1, -1, -1] ∈ [2, ∞)
[0, 1] ∈ [0, ∞)
[0, 0, 1, -1] ∈ [1, ∞)
[1] ∈ [0, ∞)

when they expect omega to solve it.

To debug the problem I had to come up with #3847 and turn on set_option pp.universes true, and now we see what goes wrong:

omega could not prove the goal:
a possible counterexample may satisfy the constraints
x₃ ∈ [0, ∞)
x₄ ∈ [0, ∞)
x₁ - x₂ - x₃ ∈ [2, ∞)
x₂ ∈ [0, ∞)
x₃ - x₄ ∈ [1, ∞)
x₁ ∈ [0, ∞)
where
x₁ := ↑(sizeOf.{(max u v) + 1} xs)
x₂ := ↑(sizeOf.{u + 1} fst✝)
x₃ := ↑(sizeOf.{v + 1} snd✝)
x₄ := ↑(sizeOf.{max (u + 1) (v + 1)} xs)

One can work around the problem by changing the lemma statement as such

theorem sizeOf_snd_lt_sizeOf_list
  {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {x : α × β} {xs : List (α × β)} :
  x ∈ xs → sizeOf x.snd < 1 + sizeOf.{(max u v)+1} xs

but arguably one shouldn't have to.

Versions

0aa6831

Impact

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