From 784972462a0eb2ea55ffc6eadacdc27173f9dd72 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 16 Apr 2024 17:11:51 +0200
Subject: [PATCH] feat: omega: more helpful error messages (#3847)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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)
---
 src/Init/Data/Repr.lean                    | 26 +++++++
 src/Lean/Elab/Tactic/Omega/Frontend.lean   | 78 ++++++++++++++++++++-
 tests/lean/omega-failure.lean              | 32 +++++++++
 tests/lean/omega-failure.lean.expected.out | 79 ++++++++++++++++++++++
 4 files changed, 214 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/omega-failure.lean
 create mode 100644 tests/lean/omega-failure.lean.expected.out

diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index c7043589f1..42ec4ccecc 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -175,6 +175,32 @@ def toSuperDigits (n : Nat) : List Char :=
 def toSuperscriptString (n : Nat) : String :=
   (toSuperDigits n).asString
 
+def subDigitChar (n : Nat) : Char :=
+  if n = 0 then '₀' else
+  if n = 1 then '₁' else
+  if n = 2 then '₂' else
+  if n = 3 then '₃' else
+  if n = 4 then '₄' else
+  if n = 5 then '₅' else
+  if n = 6 then '₆' else
+  if n = 7 then '₇' else
+  if n = 8 then '₈' else
+  if n = 9 then '₉' else
+  '*'
+
+partial def toSubDigitsAux : Nat → List Char → List Char
+  | n, ds =>
+    let d  := subDigitChar <| n % 10;
+    let n' := n / 10;
+    if n' = 0 then d::ds
+    else toSubDigitsAux n' (d::ds)
+
+def toSubDigits (n : Nat) : List Char :=
+  toSubDigitsAux n []
+
+def toSubscriptString (n : Nat) : String :=
+  (toSubDigits n).asString
+
 end Nat
 
 instance : Repr Nat where
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index 9662fbe3f7..a382690a9c 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -526,6 +526,82 @@ def cases₂ (mvarId : MVarId) (p : Expr) (hName : Name := `h) :
     | throwError "'cases' tactic failed, unexpected new hypothesis"
   return ((s₁.mvarId, f₁), (s₂.mvarId, f₂))
 
+/--
+Helpful error message when omega cannot find a solution
+-/
+def formatErrorMessage (p : Problem) : OmegaM MessageData := do
+  if p.possible then
+    if p.isEmpty then
+      return m!"it is false"
+    else
+      let as ← atoms
+      let mask ← mentioned p.constraints
+      let names ← varNames mask
+      return m!"a possible counterexample may satisfy the constraints\n" ++
+        m!"{prettyConstraints names p.constraints}\nwhere\n{prettyAtoms names as mask}"
+  else
+    -- formatErrorMessage should not be used in this case
+    return "it is trivially solvable"
+where
+  varNameOf (i : Nat) : String :=
+    let c : Char := .ofNat ('a'.toNat + (i % 26))
+    let suffix := if i < 26 then "" else s!"_{i / 26}"
+    s!"{c}{suffix}"
+
+  inScope (s : String) : MetaM Bool := do
+    let n := .mkSimple s
+    if (← resolveGlobalName n).isEmpty then
+      if ((← getLCtx).findFromUserName? n).isNone then
+        return false
+    return true
+
+  -- Assign ascending names a, b, c, …, z, a1 … to all atoms mentioned according to the mask
+  -- but avoid names in the local or global scope
+  varNames (mask : Array Bool) : MetaM (Array String) := do
+    let mut names := #[]
+    let mut next := 0
+    for h : i in [:mask.size] do
+      if mask[i] then
+        while ← inScope (varNameOf next) do next := next + 1
+        names := names.push (varNameOf next)
+        next := next + 1
+      else
+        names := names.push "(masked)"
+    return names
+
+  prettyConstraints (names : Array String) (constraints : HashMap Coeffs Fact) : String :=
+    constraints.toList
+      |>.map (fun ⟨coeffs, ⟨_, cst, _⟩⟩ => "  " ++ prettyConstraint (prettyCoeffs names coeffs) cst)
+      |> "\n".intercalate
+
+  prettyConstraint (e : String) : Constraint → String
+    | ⟨none, none⟩ => s!"{e} is unconstrained" -- should not happen in error messages
+    | ⟨none, some y⟩ => s!"{e} ≤ {y}"
+    | ⟨some x, none⟩ => s!"{e} ≥ {x}"
+    | ⟨some x, some y⟩ =>
+      if y < x then "∅" else -- should not happen in error messages
+      s!"{x} ≤ {e} ≤ {y}"
+
+  prettyCoeffs (names : Array String) (coeffs : Coeffs) : String :=
+    coeffs.toList.enum
+      |>.filter (fun (_,c) => c ≠ 0)
+      |>.enum
+      |>.map (fun (j, (i,c)) =>
+        (if j > 0 then if c > 0 then " + " else " - " else if c > 0 then "" else "- ") ++
+        (if Int.natAbs c = 1 then names[i]! else s!"{c.natAbs}*{names[i]!}"))
+      |> String.join
+
+  mentioned (constraints : HashMap Coeffs Fact) : OmegaM (Array Bool) := do
+    let initMask := Array.mkArray (← getThe State).atoms.size false
+    return constraints.fold (init := initMask) fun mask coeffs _ =>
+      coeffs.enum.foldl (init := mask) fun mask (i, c) =>
+        if c = 0 then mask else mask.set! i true
+
+  prettyAtoms (names : Array String) (atoms : Array Expr) (mask : Array Bool) : MessageData :=
+    (Array.zip names atoms).toList.enum
+      |>.filter (fun (i, _) => mask.getD i false)
+      |>.map (fun (_, (n, a)) => m!" {n} := {a}")
+      |> m!"\n".joinSep
 
 mutual
 
@@ -535,7 +611,7 @@ call `omegaImpl` in both branches.
 -/
 partial def splitDisjunction (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withContext do
   match m.disjunctions with
-    | [] => throwError "omega did not find a contradiction:\n{m.problem}"
+    | [] => throwError "omega could not prove the goal:\n{← formatErrorMessage m.problem}"
     | h :: t =>
       trace[omega] "Case splitting on {← inferType h}"
       let ctx ← getMCtx
diff --git a/tests/lean/omega-failure.lean b/tests/lean/omega-failure.lean
new file mode 100644
index 0000000000..e0e33d759b
--- /dev/null
+++ b/tests/lean/omega-failure.lean
@@ -0,0 +1,32 @@
+/-!
+Testing omega's failure message
+-/
+
+example : 0 < 0 := by omega
+
+example (x : Nat) : x < 0 := by omega
+
+example (x : Nat) (y : Int) : x < y := by omega
+
+example (x y : Int) : 5 < x ∧ x < 10 → y > 0 := by omega
+
+-- this used to fail with y = x, but then omega got better, so now there are unrelated x and y
+-- to make omega fail
+theorem sizeOf_snd_lt_sizeOf_list {α : Type u} {β : Type v} [SizeOf α] [SizeOf β]
+  {x y : α × β} {xs : List (α × β)} :
+  y ∈ xs → sizeOf x.snd < 1 + sizeOf xs
+:= by
+  intro h
+  have := List.sizeOf_lt_of_mem h
+  have : sizeOf x = 1 + sizeOf x.1 + sizeOf x.2 := rfl
+  omega
+
+
+example (reallyreallyreallyreally longlonglonglong namenamename : Nat) :
+  reallyreallyreallyreally < longlonglonglong + namenamename := by omega
+
+
+def a := 1
+
+example (b c d e f g h i j k l m n o p : Nat) :
+  b + c + d + e + f + g + h + i + j + k + l + m + n + o + p < 100 := by omega
diff --git a/tests/lean/omega-failure.lean.expected.out b/tests/lean/omega-failure.lean.expected.out
new file mode 100644
index 0000000000..e200591cd0
--- /dev/null
+++ b/tests/lean/omega-failure.lean.expected.out
@@ -0,0 +1,79 @@
+omega-failure.lean:5:22-5:27: error: omega could not prove the goal:
+it is false
+omega-failure.lean:7:32-7:37: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  a ≥ 0
+where
+ a := ↑x
+omega-failure.lean:9:42-9:47: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  a - b ≥ 0
+  a ≥ 0
+where
+ a := ↑x
+ b := y
+omega-failure.lean:11:51-11:56: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  b ≤ 0
+  6 ≤ a ≤ 9
+where
+ a := x
+ b := y
+omega-failure.lean:22:2-22:7: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  d ≥ 0
+  a - b ≥ 1
+  c ≥ 0
+  a - d ≤ -1
+  b ≥ 0
+  a ≥ 0
+  c + d ≥ -1
+where
+ a := ↑(sizeOf xs)
+ b := ↑(sizeOf y)
+ c := ↑(sizeOf x.fst)
+ d := ↑(sizeOf x.snd)
+omega-failure.lean:26:67-26:72: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  c ≥ 0
+  a - b - c ≥ 0
+  b ≥ 0
+  a ≥ 0
+where
+ a := ↑reallyreallyreallyreally
+ b := ↑longlonglonglong
+ c := ↑namenamename
+omega-failure.lean:32:72-32:77: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  x ≥ 0
+  a_1 ≥ 0
+  v ≥ 0
+  c_1 ≥ 0
+  b_1 ≥ 0
+  e_1 ≥ 0
+  z ≥ 0
+  q ≥ 0
+  s ≥ 0
+  d_1 ≥ 0
+  u ≥ 0
+  t ≥ 0
+  w ≥ 0
+  q + r + s + t + u + v + w + x + y + z + a_1 + b_1 + c_1 + d_1 + e_1 ≥ 100
+  r ≥ 0
+  y ≥ 0
+where
+ q := ↑b
+ r := ↑c
+ s := ↑d
+ t := ↑e
+ u := ↑f
+ v := ↑g
+ w := ↑h
+ x := ↑i
+ y := ↑j
+ z := ↑k
+ a_1 := ↑l
+ b_1 := ↑m
+ c_1 := ↑n
+ d_1 := ↑o
+ e_1 := ↑p