feat: omega: more helpful error messages

[nomeata]

while trying to help a user who was facing an unhelpful

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

I couldn’t resist and wrote a pretty-printer for these problem that
shows the linear combination as such, and includes the recognized atoms.
This is especially useful since oftem omega failures stem from failure
to recognize atoms as equal. In this case, we now get:

omega-failure.lean:19:2-19:7: error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  d - e ≥ 1
  e ≥ 0
  d ≥ 0
  a - b ≥ 1
  c ≥ 0
  b ≥ 0
  a ≥ 0
  c + d ≥ -1
where
 a := ↑(sizeOf xs)
 b := ↑(sizeOf x)
 c := ↑(sizeOf x.fst)
 d := ↑(sizeOf x.snd)
 e := ↑(sizeOf xs)

and this might help the user make progress (e.g. by using case x
first, and investingating why sizeOf xs shows up twice)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-04-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-04-08 23:01:57)
• ✅ Mathlib branch lean-pr-testing-3847 has successfully built against this PR. (2024-04-09 19:54:15) View Log
• ✅ Mathlib branch lean-pr-testing-3847 has successfully built against this PR. (2024-04-09 20:36:33) View Log
• ✅ Mathlib branch lean-pr-testing-3847 has successfully built against this PR. (2024-04-09 21:08:30) View Log
• 🟡 Mathlib branch lean-pr-testing-3847 build against this PR was cancelled. (2024-04-10 21:51:33) View Log
• ✅ Mathlib branch lean-pr-testing-3847 has successfully built against this PR. (2024-04-10 23:07:09) View Log
• ✅ Mathlib branch lean-pr-testing-3847 has successfully built against this PR. (2024-04-12 07:19:44) View Log
• ✅ Mathlib branch lean-pr-testing-3847 has successfully built against this PR. (2024-04-13 13:11:24) View Log
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 535427ada498461aa329d941c53bd2a4729513be --onto 1c20b5341956fb77fcf2c2601e64075e51d5f858. (2024-04-16 15:14:01)

[nomeata]

Draft status to indicate that I don't consider the code finished, but would like to hear if I should go ahead with this, and what changes, if any, you’d like to see for the output.

(I wonder if such non-trivial error messages should be constructed lazily, using ofPPFormat somehow, so that try omega does not get slower.)

[nomeata]

I was expecting this to be somewhat expensive in the presence of try omega, but the speedcenter thinks it’s fine:

http://speed.lean-fro.org/mathlib4/compare/a93fa055-e732-498b-8c1f-fd5ab4f48b05/to/fe837d0c-f16b-4edb-981d-f63ef9508ed5

So I guess we can merge this as it is (and maybe use lazy error message construction here once we have it.)

[david-christiansen]

This is really good stuff :-)

But are subscripted xs the easiest to read? Using different letters, perhaps resorting to subscripts when exhausting a name supply, would be easier to distinguish at a glace, I think. Eg:

omega-failure.lean:19:2-19:7: error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  d - e ≥ 1
  e ≥ 0
  d ≥ 0
  a - b ≥ 1
  c ≥ 0
  b ≥ 0
  a ≥ 0
  c + d ≥ -1
where
  a := ↑(sizeOf xs)
  b := ↑(sizeOf x)
  c := ↑(sizeOf x.fst)
  d := ↑(sizeOf x.snd)
  e := ↑(sizeOf xs)

Otherwise we may end up squinting, especially when working on laptops.

This example is not perfect - It's weird using beginning-of-alphabet for variables rather than constants, and the naming could use late-alphabet letters. But I do think separate names is good.

In either case, I would hope that the name selection avoids things already in scope, which is needed with subscripted variables anyway, as users might do that. And I noticed that there was no x_3 atom in the original message - is that because the atom was unconstrained?

[nomeata]

As much as I 🤎 unicode, I fear you are right.

[nomeata]

@david-christiansen, I implemented your idea, I think. What do you think of that?