Documentation

Init.Grind.Ordered.Linarith

Support for the linear arithmetic module for IntModule in grind

@[reducible, inline]
Equations
@[reducible, inline]
Equations
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'_go_eq_denote {α : Type u_1} [IntModule α] (ctx : Context α) (p : Poly) (r : α) :
denote'.go ctx r p = denote ctx p + r
theorem Lean.Grind.Linarith.Poly.denote'_eq_denote {α : Type u_1} [IntModule α] (ctx : Context α) (p : Poly) :
denote' ctx p = denote ctx p

Normalizes the given polynomial by fusing monomial and constants.

Equations
def Lean.Grind.Linarith.Poly.combine' (fuel : Nat) (p₁ p₂ : Poly) :
Equations
Equations

Converts the given expression into a polynomial.

Equations

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

Equations

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

Equations
@[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 α) (fuel : Nat) (p₁ p₂ : Poly) :
denote ctx (combine' fuel p₁ 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_toPoly'_go {α : Type u_1} [IntModule α] {k : Int} {p : Poly} (ctx : Context α) (e : Expr) :
Poly.denote ctx (toPoly'.go k e p) = k * denote ctx e + Poly.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

Helper theorems for conflict resolution during model construction.

Equations
theorem Lean.Grind.Linarith.le_le_combine {α : Type u_1} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) :
le_le_combine_cert p₁ p₂ p₃ = truePoly.denote' ctx p₁ 0Poly.denote' ctx p₂ 0Poly.denote' ctx p₃ 0
Equations
theorem Lean.Grind.Linarith.le_lt_combine {α : Type u_1} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) :
le_lt_combine_cert p₁ p₂ p₃ = truePoly.denote' ctx p₁ 0Poly.denote' ctx p₂ < 0Poly.denote' ctx p₃ < 0
Equations
  • One or more equations did not get rendered due to their size.
theorem Lean.Grind.Linarith.lt_lt_combine {α : Type u_1} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly) :
lt_lt_combine_cert p₁ p₂ p₃ = truePoly.denote' ctx p₁ < 0Poly.denote' ctx p₂ < 0Poly.denote' ctx p₃ < 0
theorem Lean.Grind.Linarith.diseq_split {α : Type u_1} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) :
diseq_split_cert p₁ p₂ = truePoly.denote' ctx p₁ 0Poly.denote' ctx p₁ < 0 Poly.denote' ctx p₂ < 0
theorem Lean.Grind.Linarith.diseq_split_resolve {α : Type u_1} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) :
diseq_split_cert p₁ p₂ = truePoly.denote' ctx p₁ 0¬Poly.denote' ctx p₁ < 0Poly.denote' ctx p₂ < 0

Helper theorems for internalizing facts into the linear arithmetic procedure

Equations
theorem Lean.Grind.Linarith.eq_norm {α : Type u_1} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) :
norm_cert lhs rhs p = trueExpr.denote ctx lhs = Expr.denote ctx rhsPoly.denote' ctx p = 0
theorem Lean.Grind.Linarith.le_of_eq {α : Type u_1} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) :
norm_cert lhs rhs p = trueExpr.denote ctx lhs = Expr.denote ctx rhsPoly.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 = trueExpr.denote ctx lhs Expr.denote ctx rhsPoly.denote' ctx p 0
theorem Lean.Grind.Linarith.le_norm {α : Type u_1} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) :
norm_cert lhs rhs p = trueExpr.denote ctx lhs Expr.denote ctx rhsPoly.denote' ctx p 0
theorem Lean.Grind.Linarith.lt_norm {α : Type u_1} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) :
norm_cert lhs rhs p = trueExpr.denote ctx lhs < Expr.denote ctx rhsPoly.denote' ctx p < 0
theorem Lean.Grind.Linarith.not_le_norm {α : Type u_1} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) :
norm_cert rhs lhs p = true¬Expr.denote ctx lhs Expr.denote ctx rhsPoly.denote' ctx p < 0
theorem Lean.Grind.Linarith.not_lt_norm {α : Type u_1} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) :
norm_cert rhs lhs p = true¬Expr.denote ctx lhs < Expr.denote ctx rhsPoly.denote' ctx p 0
theorem Lean.Grind.Linarith.not_le_norm' {α : Type u_1} [IntModule α] [Preorder α] [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 α] [Preorder α] [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

theorem Lean.Grind.Linarith.eq_of_le_ge {α : Type u_1} [IntModule α] [PartialOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) :
eq_of_le_ge_cert p₁ p₂ = truePoly.denote' ctx p₁ 0Poly.denote' ctx p₂ 0Poly.denote' ctx p₁ = 0

Helper theorems for closing the goal

theorem Lean.Grind.Linarith.lt_unsat {α : Type u_1} [IntModule α] [Preorder α] (ctx : Context α) :
theorem Lean.Grind.Linarith.zero_lt_one {α : Type u_1} [Ring α] [Preorder α] [OrderedRing α] (ctx : Context α) (p : Poly) :
theorem Lean.Grind.Linarith.zero_ne_one_of_char0 {α : Type u_1} [Ring α] [IsCharP α 0] (ctx : Context α) (p : Poly) :
theorem Lean.Grind.Linarith.zero_ne_one_of_charC {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p : Poly) :

Coefficient normalization

Equations
theorem Lean.Grind.Linarith.eq_neg {α : Type u_1} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly) :
eq_neg_cert p₁ p₂ = truePoly.denote' ctx p₁ = 0Poly.denote' ctx p₂ = 0
Equations
theorem Lean.Grind.Linarith.eq_coeff {α : Type u_1} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) :
eq_coeff_cert p₁ p₂ k = truePoly.denote' ctx p₁ = 0Poly.denote' ctx p₂ = 0
def Lean.Grind.Linarith.coeff_cert (p₁ p₂ : Poly) (k : Nat) :
Equations
theorem Lean.Grind.Linarith.le_coeff {α : Type u_1} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) :
coeff_cert p₁ p₂ k = truePoly.denote' ctx p₁ 0Poly.denote' ctx p₂ 0
theorem Lean.Grind.Linarith.lt_coeff {α : Type u_1} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat) :
coeff_cert p₁ p₂ k = truePoly.denote' ctx p₁ < 0Poly.denote' ctx p₂ < 0
theorem Lean.Grind.Linarith.diseq_neg {α : Type u_1} [IntModule α] (ctx : Context α) (p p' : Poly) :
(p' == p.mul (-1)) = truePoly.denote' ctx p 0Poly.denote' ctx p' 0

Substitution

def Lean.Grind.Linarith.eq_diseq_subst_cert (k₁ k₂ : Int) (p₁ p₂ p₃ : Poly) :
Equations
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₃ = truePoly.denote' ctx p₁ = 0Poly.denote' ctx p₂ 0Poly.denote' ctx p₃ 0
Equations
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₃ = truePoly.denote' ctx p₁ = 0Poly.denote' ctx p₂ 0Poly.denote' ctx p₃ 0
def Lean.Grind.Linarith.eq_le_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :
Equations
theorem Lean.Grind.Linarith.eq_le_subst {α : Type u_1} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly) :
eq_le_subst_cert x p₁ p₂ p₃ = truePoly.denote' ctx p₁ = 0Poly.denote' ctx p₂ 0Poly.denote' ctx p₃ 0
def Lean.Grind.Linarith.eq_lt_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :
Equations
theorem Lean.Grind.Linarith.eq_lt_subst {α : Type u_1} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly) :
eq_lt_subst_cert x p₁ p₂ p₃ = truePoly.denote' ctx p₁ = 0Poly.denote' ctx p₂ < 0Poly.denote' ctx p₃ < 0
def Lean.Grind.Linarith.eq_eq_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :
Equations
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₃ = truePoly.denote' ctx p₁ = 0Poly.denote' ctx p₂ = 0Poly.denote' ctx p₃ = 0