module
open Std Lean.Grind
set_option sym.debug true

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedAdd α] (a b : α)
    : (2:Int) • a + b < b + a + a → False := by
  grind

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedAdd α] (a b : α)
    : (2:Int) • a + b < b + a + a → False := by
  grind

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedAdd α] (a b : α)
    : (2:Int) • a + b < b + a + a → False := by
  fail_if_success grind -linarith
  grind

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedAdd α] (a b : α)
    : (2:Int) • a + b ≥ b + a + a := by
  grind

#guard_msgs (drop error) in
example [IntModule α] [LE α] [LT α] [IsPreorder α] [OrderedAdd α] (a b : α)
    : (2:Int) • a + b ≥ b + a + a := by
  fail_if_success grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b : α)
    : 2*a + b < b + a + a → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b : α)
    : 2 + 2*a + b + 1 < b + a + a + 3 → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (a b : α)
    : 2 + 2*a + b + 1 <= b + a + a + 3 := by
  grind

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedAdd α] (a b c : α)
    : a < b → b < c → c < a → False := by
  grind

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedAdd α] (a b c : α)
    : a < b → b < c → a < c := by
  grind

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedAdd α] (a b c : α)
    : a < b → b ≤ c → a < c := by
  grind

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedAdd α] (a b c : α)
    : a ≤ b → b ≤ c → a ≤ c := by
  grind

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedAdd α] (a b c d : α)
    : a < b → b < c + d → a - d < c := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (a b c d : α)
    : a < b → b < c + d → a - d < c := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b c : α)
    : a < b → 2*b < c → c < 2*a → False := by
  grind

-- Test misconfigured instances
/--
trace: [sym.issues] type has `LE`, but is not a partial order, failed to synthesize
      IsPartialOrder α
[sym.issues] type has `LE`, but is not a linear preorder, failed to synthesize
      IsLinearPreorder α
[sym.issues] type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize
      LawfulOrderLT α
[sym.issues] type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize
      LawfulOrderLT α
[sym.issues] type has `LE`, but is not a partial order, failed to synthesize
      IsPartialOrder α
[sym.issues] type has `LE`, but is not a linear order, failed to synthesize
      IsLinearOrder α
[sym.issues] type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize
      OrderedRing α
-/
#guard_msgs (drop error, trace) in
set_option trace.sym.issues true in
example [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedAdd α] (a b c : α)
    : a < b → b + b < c → c < a → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b : α)
    : a < 2 → b < a → b > 5 → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b : α)
    : a < One.one + 4 → b < a → b ≥ 5 → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b : α)
    : a < One.one + 5 → b < a → b ≥ 5 → False := by
  fail_if_success grind
  sorry

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedAdd α] (a b c d : α)
    : a < c → b = a + d → b - d > c → False := by
  grind

example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedAdd α] (a b c d : α)
    : a + d < c → b = a + (2:Int) • d → b - d > c → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b : α)
    : a < 2 → b = a → b > 5 → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b : α)
    : a < 2 → a = b + b → b > 5 → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (a b : α)
    : a < 2 → a = b + b → b < 1 := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (a b : α)
    : a ≤ 2 → a + b = 3*b → b ≤ 1 := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (a b c d e : α) :
    2*a + b ≥ 1 → b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0
    → a ≥ 3*c → c ≥ 6*e → d - e*5 ≥ 0
    → a + b + 3*c + d + 2*e ≥ 0 := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b c d e : α) :
    2*a + b ≥ 1 → b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0
    → a ≥ 3*c → c ≥ 6*e → d - e*5 ≥ 0
    → a + b + 3*c + d + 2*e < 0 → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (a b : α)
    : a = 0 → b = 1 → a + b > 2 → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (a b c : α)
    : a = 0 → a + b > 2 → b = c → 1 = c → False := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (a b : α)
    : a = 0 → b = 1 → a + b ≤ 2 := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (a b : α)
    : a*b + b*a > 1 → a*b > 0 := by
  grind

example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (a b c : α)
    : a*b + c > 1 → c = b*a → a*b > 0 := by
  grind

-- It must not internalize subterms `b + c + d` and `b + b + d`
#guard_msgs (trace) in
set_option trace.grind.linarith.internalize true
example [CommRing α] [LE α] [LT α] [IsLinearOrder α] [OrderedRing α] (a b c d : α)
    : a < b + c + d → c = b → a < b + b + d := by
  grind

/--
trace: [grind.linarith.assert] -3 • y + 2 • x + One.one ≤ 0
[grind.linarith.assert] 2 • z + -4 • x + One.one ≤ 0
[grind.linarith.assert] -1 • z + 3 • y + One.one ≤ 0
[grind.linarith.assert] 6 • y + -4 • x + 3 • One.one ≤ 0
[grind.linarith.assert] 15 • One.one ≤ 0
[grind.linarith.assert] Zero.zero < 0
-/
#guard_msgs (trace) in
set_option trace.grind.lia.assert true in -- cutsat should **not** process the following constraints
set_option trace.grind.linarith.assert true in -- linarith should take over
set_option trace.grind.linarith.assert.store false in
example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12*y - 4* z < 0 := by
  grind -lia