Support for the linear arithmetic module for IntModule in grind

@[reducible, inline]

abbrev Lean.Grind.Linarith.Var : Type

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

@[instance_reducible]

instance Lean.Grind.Linarith.instBEqExpr : BEq Expr

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

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

@[instance_reducible]

instance Lean.Grind.Linarith.instReprExpr : Repr Expr

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

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

@[instance_reducible]

instance Lean.Grind.Linarith.instBEqPoly : BEq Poly

instance Lean.Grind.Linarith.instReflBEqPoly : ReflBEq Poly

instance Lean.Grind.Linarith.instLawfulBEqPoly : LawfulBEq Poly

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

@[instance_reducible]

instance Lean.Grind.Linarith.instReprPoly : Repr Poly

@[reducible, inline]

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

@[inline]

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

@[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.

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

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

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

Normalizes the given polynomial by fusing monomial and constants.

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

@[irreducible]

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

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

Converts the given expression into a polynomial.

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

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

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

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.

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

@[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

Helper theorems for conflict resolution during model construction.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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