feat: omega: more helpful error messages

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -526,6 +526,59 @@ 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 mask ← mentioned p.constraints
+      return m!"a possible counterexample may satisfy the constraints\n" ++
+        m!"{prettyConstraints p.constraints}\nwhere\n" ++
+        (← prettyAtoms mask)
+  else
+    -- formatErrorMessage should not be used in this case
+    return "it is trivially solvable"
+where
+  var (n : Nat) : String :=
+    "x" ++ ((toString (n+1)).map fun c => .ofNat (c.toNat - '0'.toNat + '₀'.toNat))
+
+  prettyConstraints (constraints : HashMap Coeffs Fact) : String :=
+    constraints.toList
+      |>.map (fun ⟨coeffs, ⟨_, cst, _⟩⟩ => "  " ++ prettyConstraint (prettyCoeffs 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 (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 var i else s!"{c.natAbs}*{var 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 (mask : Array Bool) : OmegaM MessageData := do
+    return (← atoms).toList.enum
+      |>.filter (fun (i, _) => mask.getD i false)
+      |>.map (fun (i, a) => m!"  {var i} := {a}")
+      |> m!"\n".joinSep
+
 
 mutual
 
@@ -535,7 +588,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

tests/lean/omega-failure.lean

@@ -0,0 +1,26 @@
+/-!
+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
+
+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 := 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
+
+example (a b c d e f g h i j k l m n o p : Nat) :
+  a + b + c + d + e + f + g + h + i + j + k + l + m + n + o + p < 100 := by omega

tests/lean/omega-failure.lean.expected.out

@@ -0,0 +1,83 @@
+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
+  x₁ ≥ 0
+where
+  x₁ := ↑x
+omega-failure.lean:9:42-9:47: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  x₁ - x₂ ≥ 0
+  x₁ ≥ 0
+where
+  x₁ := ↑x
+  x₂ := y
+omega-failure.lean:11:51-11:56: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  x₂ ≤ 0
+  6 ≤ x₁ ≤ 9
+where
+  x₁ := x
+  x₂ := y
+omega-failure.lean:19:2-19:7: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  x₅ - x₆ ≥ 1
+  x₆ ≥ 0
+  x₅ ≥ 0
+  x₁ - x₂ ≥ 1
+  x₄ ≥ 0
+  x₂ ≥ 0
+  x₁ ≥ 0
+  x₄ + x₅ ≥ -1
+where
+  x₁ := ↑(sizeOf xs)
+  x₂ := ↑(sizeOf x)
+  x₄ := ↑(sizeOf x.fst)
+  x₅ := ↑(sizeOf x.snd)
+  x₆ := ↑(sizeOf xs)
+omega-failure.lean:23:67-23:72: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  x₃ ≥ 0
+  x₁ - x₂ - x₃ ≥ 0
+  x₂ ≥ 0
+  x₁ ≥ 0
+where
+  x₁ := ↑reallyreallyreallyreally
+  x₂ := ↑longlonglonglong
+  x₃ := ↑namenamename
+omega-failure.lean:26:76-26:81: error: omega could not prove the goal:
+a possible counterexample may satisfy the constraints
+  x₈ ≥ 0
+  x₁₁ ≥ 0
+  x₆ ≥ 0
+  x₁₃ ≥ 0
+  x₁₂ ≥ 0
+  x₁₅ ≥ 0
+  x₁₀ ≥ 0
+  x₁ ≥ 0
+  x₁₆ ≥ 0
+  x₃ ≥ 0
+  x₁₄ ≥ 0
+  x₅ ≥ 0
+  x₄ ≥ 0
+  x₁ + x₂ + x₃ + x₄ + x₅ + x₆ + x₇ + x₈ + x₉ + x₁₀ + x₁₁ + x₁₂ + x₁₃ + x₁₄ + x₁₅ + x₁₆ ≥ 100
+  x₇ ≥ 0
+  x₂ ≥ 0
+  x₉ ≥ 0
+where
+  x₁ := ↑a
+  x₂ := ↑b
+  x₃ := ↑c
+  x₄ := ↑d
+  x₅ := ↑e
+  x₆ := ↑f
+  x₇ := ↑g
+  x₈ := ↑h
+  x₉ := ↑i
+  x₁₀ := ↑j
+  x₁₁ := ↑k
+  x₁₂ := ↑l
+  x₁₃ := ↑m
+  x₁₄ := ↑n
+  x₁₅ := ↑o
+  x₁₆ := ↑p