Support for the linear arithmetic module for IntModule in grind

@[reducible, inline]

abbrev Lean.Grind.Linarith.Var : Type

Equations

• Lean.Grind.Linarith.Var = Nat

inductive Lean.Grind.Linarith.Expr : Type

• zero : Expr
• var (i : Var) : Expr
• add (a b : Expr) : Expr
• sub (a b : Expr) : Expr
• neg (a : Expr) : Expr
• natMul (k : Nat) (a : Expr) : Expr
• intMul (k : Int) (a : Expr) : Expr

@[instance_reducible]

instance Lean.Grind.Linarith.instInhabitedExpr : Inhabited Expr

Equations

• Lean.Grind.Linarith.instInhabitedExpr = { default := Lean.Grind.Linarith.instInhabitedExpr.default }

@[instance_reducible]

instance Lean.Grind.Linarith.instBEqExpr : BEq Expr

Equations

• Lean.Grind.Linarith.instBEqExpr = { beq := Lean.Grind.Linarith.instBEqExpr.beq }

def Lean.Grind.Linarith.instBEqExpr.beq : Expr → Expr → Bool

Equations

• Lean.Grind.Linarith.instBEqExpr.beq Lean.Grind.Linarith.Expr.zero Lean.Grind.Linarith.Expr.zero = true
• Lean.Grind.Linarith.instBEqExpr.beq (Lean.Grind.Linarith.Expr.var a) (Lean.Grind.Linarith.Expr.var b) = (a == b)
• Lean.Grind.Linarith.instBEqExpr.beq (a.add a_1) (b.add b_1) = (Lean.Grind.Linarith.instBEqExpr.beq a b && Lean.Grind.Linarith.instBEqExpr.beq a_1 b_1)
• Lean.Grind.Linarith.instBEqExpr.beq (a.sub a_1) (b.sub b_1) = (Lean.Grind.Linarith.instBEqExpr.beq a b && Lean.Grind.Linarith.instBEqExpr.beq a_1 b_1)
• Lean.Grind.Linarith.instBEqExpr.beq a.neg b.neg = Lean.Grind.Linarith.instBEqExpr.beq a b
• Lean.Grind.Linarith.instBEqExpr.beq (Lean.Grind.Linarith.Expr.natMul a a_1) (Lean.Grind.Linarith.Expr.natMul b b_1) = (a == b && Lean.Grind.Linarith.instBEqExpr.beq a_1 b_1)
• Lean.Grind.Linarith.instBEqExpr.beq (Lean.Grind.Linarith.Expr.intMul a a_1) (Lean.Grind.Linarith.Expr.intMul b b_1) = (a == b && Lean.Grind.Linarith.instBEqExpr.beq a_1 b_1)
• Lean.Grind.Linarith.instBEqExpr.beq x✝¹ x✝ = false

def Lean.Grind.Linarith.instReprExpr.repr : Expr → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lean.Grind.Linarith.instReprExpr : Repr Expr

Equations

• Lean.Grind.Linarith.instReprExpr = { reprPrec := Lean.Grind.Linarith.instReprExpr.repr }

@[reducible, inline]

abbrev Lean.Grind.Linarith.Context (α : Type u) : Type u

Equations

• Lean.Grind.Linarith.Context α = Lean.RArray α

@[reducible, inline]

abbrev Lean.Grind.Linarith.Var.denote {α : Type u_1} (ctx : Context α) (v : Var) : α

Equations

• Lean.Grind.Linarith.Var.denote ctx v = Lean.RArray.get ctx v

@[reducible, inline]

abbrev Lean.Grind.Linarith.Expr.denote {α : Type u_1} [IntModule α] (ctx : Context α) : Expr → α

Equations

• Lean.Grind.Linarith.Expr.denote ctx Lean.Grind.Linarith.Expr.zero = 0
• Lean.Grind.Linarith.Expr.denote ctx (Lean.Grind.Linarith.Expr.var v) = Lean.Grind.Linarith.Var.denote ctx v
• Lean.Grind.Linarith.Expr.denote ctx (a.add b) = Lean.Grind.Linarith.Expr.denote ctx a + Lean.Grind.Linarith.Expr.denote ctx b
• Lean.Grind.Linarith.Expr.denote ctx (a.sub b) = Lean.Grind.Linarith.Expr.denote ctx a - Lean.Grind.Linarith.Expr.denote ctx b
• Lean.Grind.Linarith.Expr.denote ctx (Lean.Grind.Linarith.Expr.natMul k a) = k • Lean.Grind.Linarith.Expr.denote ctx a
• Lean.Grind.Linarith.Expr.denote ctx (Lean.Grind.Linarith.Expr.intMul k a) = k • Lean.Grind.Linarith.Expr.denote ctx a
• Lean.Grind.Linarith.Expr.denote ctx a.neg = -Lean.Grind.Linarith.Expr.denote ctx a

inductive Lean.Grind.Linarith.Poly : Type

• nil : Poly
• add (k : Int) (v : Var) (p : Poly) : Poly

def Lean.Grind.Linarith.instBEqPoly.beq : Poly → Poly → Bool

Equations

• Lean.Grind.Linarith.instBEqPoly.beq Lean.Grind.Linarith.Poly.nil Lean.Grind.Linarith.Poly.nil = true
• Lean.Grind.Linarith.instBEqPoly.beq (Lean.Grind.Linarith.Poly.add a a_1 a_2) (Lean.Grind.Linarith.Poly.add b b_1 b_2) = (a == b && (a_1 == b_1 && Lean.Grind.Linarith.instBEqPoly.beq a_2 b_2))
• Lean.Grind.Linarith.instBEqPoly.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.Grind.Linarith.instBEqPoly : BEq Poly

Equations

• Lean.Grind.Linarith.instBEqPoly = { beq := Lean.Grind.Linarith.instBEqPoly.beq }

instance Lean.Grind.Linarith.instReflBEqPoly : ReflBEq Poly

instance Lean.Grind.Linarith.instLawfulBEqPoly : LawfulBEq Poly

def Lean.Grind.Linarith.instReprPoly.repr : Poly → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lean.Grind.Linarith.instReprPoly : Repr Poly

Equations

• Lean.Grind.Linarith.instReprPoly = { reprPrec := Lean.Grind.Linarith.instReprPoly.repr }

@[reducible, inline]

abbrev Lean.Grind.Linarith.Poly.denote {α : Type u_1} [IntModule α] (ctx : Context α) (p : Poly) : α

Equations

• Lean.Grind.Linarith.Poly.denote ctx Lean.Grind.Linarith.Poly.nil = 0
• Lean.Grind.Linarith.Poly.denote ctx (Lean.Grind.Linarith.Poly.add k v p_2) = k • Lean.Grind.Linarith.Var.denote ctx v + Lean.Grind.Linarith.Poly.denote ctx p_2

@[inline]

abbrev Lean.Grind.Linarith.Poly.denote'.go {α : Type u_1} [IntModule α] (ctx : Context α) (r : α) (p : Poly) : α

Equations

• Lean.Grind.Linarith.Poly.denote'.go ctx r Lean.Grind.Linarith.Poly.nil = r
• Lean.Grind.Linarith.Poly.denote'.go ctx r (Lean.Grind.Linarith.Poly.add 1 v p_2) = Lean.Grind.Linarith.Poly.denote'.go ctx (r + Lean.Grind.Linarith.Var.denote ctx v) p_2
• Lean.Grind.Linarith.Poly.denote'.go ctx r (Lean.Grind.Linarith.Poly.add k v p_2) = Lean.Grind.Linarith.Poly.denote'.go ctx (r + k • Lean.Grind.Linarith.Var.denote ctx v) p_2

@[inline]

abbrev Lean.Grind.Linarith.Poly.denote' {α : Type u_1} [IntModule α] (ctx : Context α) (p : Poly) : α

Similar to Poly.denote, but produces a denotation better for normalization.

Equations

• Lean.Grind.Linarith.Poly.denote' ctx Lean.Grind.Linarith.Poly.nil = 0
• Lean.Grind.Linarith.Poly.denote' ctx (Lean.Grind.Linarith.Poly.add 1 v p_2) = Lean.Grind.Linarith.Poly.denote'.go ctx (Lean.Grind.Linarith.Var.denote ctx v) p_2
• Lean.Grind.Linarith.Poly.denote' ctx (Lean.Grind.Linarith.Poly.add k v p_2) = Lean.Grind.Linarith.Poly.denote'.go ctx (k • Lean.Grind.Linarith.Var.denote ctx v) p_2

theorem Lean.Grind.Linarith.instAssociativeHAdd {α : Type u_1} [IntModule α] : Std.Associative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.Linarith.instCommutativeHAdd {α : Type u_1} [IntModule α] : Std.Commutative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.Linarith.Poly.denote'_eq_denote {α : Type u_1} [IntModule α] (ctx : Context α) (p : Poly) : denote' ctx p = denote ctx p

def Lean.Grind.Linarith.Poly.coeff (p : Poly) (x : Var) : Int

Equations

• (Lean.Grind.Linarith.Poly.add a y p_2).coeff x = bif x == y then a else p_2.coeff x
• Lean.Grind.Linarith.Poly.nil.coeff x = 0

def Lean.Grind.Linarith.Poly.insert (k : Int) (v : Var) (p : Poly) : Poly

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.Linarith.Poly.insert k v Lean.Grind.Linarith.Poly.nil = Lean.Grind.Linarith.Poly.add k v Lean.Grind.Linarith.Poly.nil

def Lean.Grind.Linarith.Poly.norm (p : Poly) : Poly

Normalizes the given polynomial by fusing monomial and constants.

Equations

• Lean.Grind.Linarith.Poly.nil.norm = Lean.Grind.Linarith.Poly.nil
• (Lean.Grind.Linarith.Poly.add k v p_2).norm = Lean.Grind.Linarith.Poly.insert k v p_2.norm

def Lean.Grind.Linarith.Poly.append (p₁ p₂ : Poly) : Poly

Equations

• Lean.Grind.Linarith.Poly.nil.append p₂ = p₂
• (Lean.Grind.Linarith.Poly.add k v p_1).append p₂ = Lean.Grind.Linarith.Poly.add k v (p_1.append p₂)

@[irreducible]

def Lean.Grind.Linarith.Poly.combine (p₁ p₂ : Poly) : Poly

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.Linarith.Poly.nil.combine p₂ = p₂
• p₁.combine Lean.Grind.Linarith.Poly.nil = p₁

def Lean.Grind.Linarith.Expr.toPoly' (e : Expr) : Poly

Converts the given expression into a polynomial.

Equations

• e.toPoly' = Lean.Grind.Linarith.Expr.toPoly'.go 1 e Lean.Grind.Linarith.Poly.nil

def Lean.Grind.Linarith.Expr.toPoly'.go (coeff : Int) : Expr → Poly → Poly

Equations

• Lean.Grind.Linarith.Expr.toPoly'.go coeff Lean.Grind.Linarith.Expr.zero = id
• Lean.Grind.Linarith.Expr.toPoly'.go coeff (Lean.Grind.Linarith.Expr.var v) = fun (x : Lean.Grind.Linarith.Poly) => Lean.Grind.Linarith.Poly.add coeff v x
• Lean.Grind.Linarith.Expr.toPoly'.go coeff (a.add b) = Lean.Grind.Linarith.Expr.toPoly'.go coeff a ∘ Lean.Grind.Linarith.Expr.toPoly'.go coeff b
• Lean.Grind.Linarith.Expr.toPoly'.go coeff (a.sub b) = Lean.Grind.Linarith.Expr.toPoly'.go coeff a ∘ Lean.Grind.Linarith.Expr.toPoly'.go (-coeff) b
• Lean.Grind.Linarith.Expr.toPoly'.go coeff (Lean.Grind.Linarith.Expr.natMul k a) = bif k == 0 then id else Lean.Grind.Linarith.Expr.toPoly'.go (coeff.mul ↑k) a
• Lean.Grind.Linarith.Expr.toPoly'.go coeff (Lean.Grind.Linarith.Expr.intMul k a) = bif k == 0 then id else Lean.Grind.Linarith.Expr.toPoly'.go (coeff.mul k) a
• Lean.Grind.Linarith.Expr.toPoly'.go coeff a.neg = Lean.Grind.Linarith.Expr.toPoly'.go (-coeff) a

def Lean.Grind.Linarith.Expr.norm (e : Expr) : Poly

Converts the given expression into a polynomial, and then normalizes it.

Equations

• e.norm = e.toPoly'.norm

def Lean.Grind.Linarith.Poly.mul' (p : Poly) (k : Int) : Poly

p.mul k multiplies all coefficients and constant of the polynomial p by k.

Equations

• Lean.Grind.Linarith.Poly.nil.mul' k = Lean.Grind.Linarith.Poly.nil
• (Lean.Grind.Linarith.Poly.add k_1 v p_2).mul' k = Lean.Grind.Linarith.Poly.add (k * k_1) v (p_2.mul' k)

def Lean.Grind.Linarith.Poly.mul (p : Poly) (k : Int) : Poly

Equations

• p.mul k = if (k == 0) = true then Lean.Grind.Linarith.Poly.nil else p.mul' k

@[simp]

theorem Lean.Grind.Linarith.Poly.denote_mul {α : Type u_1} [IntModule α] (ctx : Context α) (p : Poly) (k : Int) : denote ctx (p.mul k) = k • denote ctx p

theorem Lean.Grind.Linarith.Poly.denote_insert {α : Type u_1} [IntModule α] (ctx : Context α) (k : Int) (v : Var) (p : Poly) : denote ctx (insert k v p) = denote ctx p + k • Var.denote ctx v

theorem Lean.Grind.Linarith.Poly.denote_norm {α : Type u_1} [IntModule α] (ctx : Context α) (p : Poly) : denote ctx p.norm = denote ctx p

theorem Lean.Grind.Linarith.Poly.denote_append {α : Type u_1} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly) : denote ctx (p₁.append p₂) = denote ctx p₁ + denote ctx p₂

theorem Lean.Grind.Linarith.Poly.denote_combine {α : Type u_1} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly) : denote ctx (p₁.combine p₂) = denote ctx p₁ + denote ctx p₂

theorem Lean.Grind.Linarith.Expr.denote_norm {α : Type u_1} [IntModule α] (ctx : Context α) (e : Expr) : Poly.denote ctx e.norm = denote ctx e

def Lean.Grind.Linarith.Poly.leadCoeff (p : Poly) : Int

Equations

• (Lean.Grind.Linarith.Poly.add a v p_2).leadCoeff = a
• p.leadCoeff = 1

Helper theorems for conflict resolution during model construction.

def Lean.Grind.Linarith.le_le_combine_cert (p₁ p₂ p₃ : Poly) : Bool

Equations

• Lean.Grind.Linarith.le_le_combine_cert p₁ p₂ p₃ = (p₃ == (p₁.mul ↑p₂.leadCoeff.natAbs).combine (p₂.mul ↑p₁.leadCoeff.natAbs))

theorem Lean.Grind.Linarith.le_le_combine {α : Type u_1} [IntModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) : le_le_combine_cert p₁ p₂ p₃ = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₃ ≤ 0

def Lean.Grind.Linarith.le_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool

Equations

• Lean.Grind.Linarith.le_lt_combine_cert p₁ p₂ p₃ = (decide (↑p₁.leadCoeff.natAbs > 0) && p₃ == (p₁.mul ↑p₂.leadCoeff.natAbs).combine (p₂.mul ↑p₁.leadCoeff.natAbs))

theorem Lean.Grind.Linarith.le_lt_combine {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) : le_lt_combine_cert p₁ p₂ p₃ = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ < 0 → Poly.denote' ctx p₃ < 0

def Lean.Grind.Linarith.lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool

Equations

• One or more equations did not get rendered due to their size.

theorem Lean.Grind.Linarith.lt_lt_combine {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) : lt_lt_combine_cert p₁ p₂ p₃ = true → Poly.denote' ctx p₁ < 0 → Poly.denote' ctx p₂ < 0 → Poly.denote' ctx p₃ < 0

def Lean.Grind.Linarith.diseq_split_cert (p₁ p₂ : Poly) : Bool

Equations

• Lean.Grind.Linarith.diseq_split_cert p₁ p₂ = (p₂ == p₁.mul (-1))

theorem Lean.Grind.Linarith.diseq_split {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) : diseq_split_cert p₁ p₂ = true → Poly.denote' ctx p₁ ≠ 0 → Poly.denote' ctx p₁ < 0 ∨ Poly.denote' ctx p₂ < 0

theorem Lean.Grind.Linarith.diseq_split_resolve {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) : diseq_split_cert p₁ p₂ = true → Poly.denote' ctx p₁ ≠ 0 → ¬Poly.denote' ctx p₁ < 0 → Poly.denote' ctx p₂ < 0

Helper theorems for internalizing facts into the linear arithmetic procedure

def Lean.Grind.Linarith.norm_cert (lhs rhs : Expr) (p : Poly) : Bool

Equations

• Lean.Grind.Linarith.norm_cert lhs rhs p = (p == (lhs.sub rhs).norm)

theorem Lean.Grind.Linarith.eq_norm {α : Type u_1} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Poly.denote' ctx p = 0

theorem Lean.Grind.Linarith.le_of_eq {α : Type u_1} [IntModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Poly.denote' ctx p ≤ 0

theorem Lean.Grind.Linarith.diseq_norm {α : Type u_1} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Poly.denote' ctx p ≠ 0

theorem Lean.Grind.Linarith.le_norm {α : Type u_1} [IntModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p = true → Expr.denote ctx lhs ≤ Expr.denote ctx rhs → Poly.denote' ctx p ≤ 0

theorem Lean.Grind.Linarith.lt_norm {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p = true → Expr.denote ctx lhs < Expr.denote ctx rhs → Poly.denote' ctx p < 0

theorem Lean.Grind.Linarith.not_le_norm {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert rhs lhs p = true → ¬Expr.denote ctx lhs ≤ Expr.denote ctx rhs → Poly.denote' ctx p < 0

theorem Lean.Grind.Linarith.not_lt_norm {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert rhs lhs p = true → ¬Expr.denote ctx lhs < Expr.denote ctx rhs → Poly.denote' ctx p ≤ 0

theorem Lean.Grind.Linarith.not_le_norm' {α : Type u_1} [IntModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p = true → ¬Expr.denote ctx lhs ≤ Expr.denote ctx rhs → ¬Poly.denote' ctx p ≤ 0

theorem Lean.Grind.Linarith.not_lt_norm' {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : norm_cert lhs rhs p = true → ¬Expr.denote ctx lhs < Expr.denote ctx rhs → ¬Poly.denote' ctx p < 0

Equality detection

def Lean.Grind.Linarith.eq_of_le_ge_cert (p₁ p₂ : Poly) : Bool

Equations

• Lean.Grind.Linarith.eq_of_le_ge_cert p₁ p₂ = (p₂ == p₁.mul (-1))

theorem Lean.Grind.Linarith.eq_of_le_ge {α : Type u_1} [IntModule α] [LE α] [Std.IsPartialOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) : eq_of_le_ge_cert p₁ p₂ = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₁ = 0

Helper theorems for closing the goal

theorem Lean.Grind.Linarith.diseq_unsat {α : Type u_1} [IntModule α] (ctx : Context α) : Poly.denote ctx Poly.nil ≠ 0 → False

theorem Lean.Grind.Linarith.lt_unsat {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] (ctx : Context α) : Poly.denote ctx Poly.nil < 0 → False

def Lean.Grind.Linarith.zero_lt_one_cert (p : Poly) : Bool

Equations

• Lean.Grind.Linarith.zero_lt_one_cert p = (p == Lean.Grind.Linarith.Poly.add (-1) 0 Lean.Grind.Linarith.Poly.nil)

theorem Lean.Grind.Linarith.zero_lt_one {α : Type u_1} [Ring α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (p : Poly) : zero_lt_one_cert p = true → Var.denote ctx 0 = One.one → Poly.denote' ctx p < 0

def Lean.Grind.Linarith.zero_ne_one_cert (p : Poly) : Bool

Equations

• Lean.Grind.Linarith.zero_ne_one_cert p = (p == Lean.Grind.Linarith.Poly.add 1 0 Lean.Grind.Linarith.Poly.nil)

theorem Lean.Grind.Linarith.zero_ne_one_of_ord_ring {α : Type u_1} [Ring α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (p : Poly) : zero_ne_one_cert p = true → Var.denote ctx 0 = One.one → Poly.denote' ctx p ≠ 0

theorem Lean.Grind.Linarith.zero_ne_one_of_field {α : Type u_1} [Field α] (ctx : Context α) (p : Poly) : zero_ne_one_cert p = true → Var.denote ctx 0 = One.one → Poly.denote' ctx p ≠ 0

theorem Lean.Grind.Linarith.zero_ne_one_of_char0 {α : Type u_1} [Ring α] [IsCharP α 0] (ctx : Context α) (p : Poly) : zero_ne_one_cert p = true → Var.denote ctx 0 = One.one → Poly.denote' ctx p ≠ 0

def Lean.Grind.Linarith.zero_ne_one_of_charC_cert (c : Nat) (p : Poly) : Bool

Equations

• Lean.Grind.Linarith.zero_ne_one_of_charC_cert c p = (decide (↑c > 1) && p == Lean.Grind.Linarith.Poly.add 1 0 Lean.Grind.Linarith.Poly.nil)

theorem Lean.Grind.Linarith.zero_ne_one_of_charC {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p : Poly) : zero_ne_one_of_charC_cert c p = true → Var.denote ctx 0 = One.one → Poly.denote' ctx p ≠ 0

Coefficient normalization

def Lean.Grind.Linarith.eq_neg_cert (p₁ p₂ : Poly) : Bool

Equations

• Lean.Grind.Linarith.eq_neg_cert p₁ p₂ = (p₂ == p₁.mul (-1))

theorem Lean.Grind.Linarith.eq_neg {α : Type u_1} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly) : eq_neg_cert p₁ p₂ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ = 0

def Lean.Grind.Linarith.eq_coeff_cert (p₁ p₂ : Poly) (k : Nat) : Bool

Equations

• Lean.Grind.Linarith.eq_coeff_cert p₁ p₂ k = (k != 0 && p₁ == p₂.mul ↑k)

theorem Lean.Grind.Linarith.eq_coeff {α : Type u_1} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) : eq_coeff_cert p₁ p₂ k = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ = 0

def Lean.Grind.Linarith.coeff_cert (p₁ p₂ : Poly) (k : Nat) : Bool

Equations

• Lean.Grind.Linarith.coeff_cert p₁ p₂ k = (decide (k > 0) && p₁ == p₂.mul ↑k)

theorem Lean.Grind.Linarith.le_coeff {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) : coeff_cert p₁ p₂ k = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0

theorem Lean.Grind.Linarith.lt_coeff {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) : coeff_cert p₁ p₂ k = true → Poly.denote' ctx p₁ < 0 → Poly.denote' ctx p₂ < 0

theorem Lean.Grind.Linarith.diseq_neg {α : Type u_1} [IntModule α] (ctx : Context α) (p p' : Poly) : (p' == p.mul (-1)) = true → Poly.denote' ctx p ≠ 0 → Poly.denote' ctx p' ≠ 0

Substitution

def Lean.Grind.Linarith.eq_diseq_subst_cert (k₁ k₂ : Int) (p₁ p₂ p₃ : Poly) : Bool

Equations

• Lean.Grind.Linarith.eq_diseq_subst_cert k₁ k₂ p₁ p₂ p₃ = (decide (k₁.natAbs ≠ 0) && p₃ == (p₁.mul k₂).combine (p₂.mul k₁))

theorem Lean.Grind.Linarith.eq_diseq_subst {α : Type u_1} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (k₁ k₂ : Int) (p₁ p₂ p₃ : Poly) : eq_diseq_subst_cert k₁ k₂ p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ ≠ 0 → Poly.denote' ctx p₃ ≠ 0

def Lean.Grind.Linarith.eq_diseq_subst1_cert (k : Int) (p₁ p₂ p₃ : Poly) : Bool

Equations

• Lean.Grind.Linarith.eq_diseq_subst1_cert k p₁ p₂ p₃ = (p₃ == (p₁.mul k).combine p₂)

theorem Lean.Grind.Linarith.eq_diseq_subst1 {α : Type u_1} [IntModule α] (ctx : Context α) (k : Int) (p₁ p₂ p₃ : Poly) : eq_diseq_subst1_cert k p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ ≠ 0 → Poly.denote' ctx p₃ ≠ 0

def Lean.Grind.Linarith.eq_le_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) : Bool

Equations

• Lean.Grind.Linarith.eq_le_subst_cert x p₁ p₂ p₃ = (decide (p₁.coeff x ≥ 0) && p₃ == (p₂.mul (p₁.coeff x)).combine (p₁.mul (-p₂.coeff x)))

theorem Lean.Grind.Linarith.eq_le_subst {α : Type u_1} [IntModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly) : eq_le_subst_cert x p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₃ ≤ 0

def Lean.Grind.Linarith.eq_lt_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) : Bool

Equations

• Lean.Grind.Linarith.eq_lt_subst_cert x p₁ p₂ p₃ = (decide (p₁.coeff x > 0) && p₃ == (p₂.mul (p₁.coeff x)).combine (p₁.mul (-p₂.coeff x)))

theorem Lean.Grind.Linarith.eq_lt_subst {α : Type u_1} [IntModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly) : eq_lt_subst_cert x p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ < 0 → Poly.denote' ctx p₃ < 0

def Lean.Grind.Linarith.eq_eq_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) : Bool

Equations

• Lean.Grind.Linarith.eq_eq_subst_cert x p₁ p₂ p₃ = (p₃ == (p₂.mul (p₁.coeff x)).combine (p₁.mul (-p₂.coeff x)))

theorem Lean.Grind.Linarith.eq_eq_subst {α : Type u_1} [IntModule α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly) : eq_eq_subst_cert x p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ = 0 → Poly.denote' ctx p₃ = 0

def Lean.Grind.Linarith.imp_eq_cert (p : Poly) (x y : Var) : Bool

Equations

• Lean.Grind.Linarith.imp_eq_cert p x y = (p == Lean.Grind.Linarith.Poly.add 1 x (Lean.Grind.Linarith.Poly.add (-1) y Lean.Grind.Linarith.Poly.nil))

theorem Lean.Grind.Linarith.imp_eq {α : Type u_1} [IntModule α] (ctx : Context α) (p : Poly) (x y : Var) : imp_eq_cert p x y = true → Poly.denote' ctx p = 0 → Var.denote ctx x = Var.denote ctx y