Helper definitions and theorems for constructing linear arithmetic proofs.

@[reducible, inline]

abbrev Int.Linear.Var : Type

@[reducible, inline]

abbrev Int.Linear.Context : Type

@[inline]

abbrev Int.Linear.Var.denote (ctx : Context) (v : Var) : Int

inductive Int.Linear.Expr : Type

• num (v : Int) : Expr
• var (i : Var) : Expr
• add (a b : Expr) : Expr
• sub (a b : Expr) : Expr
• neg (a : Expr) : Expr
• mulL (k : Int) (a : Expr) : Expr
• mulR (a : Expr) (k : Int) : Expr

def Int.Linear.instInhabitedExpr.default : Expr

@[implicit_reducible]

instance Int.Linear.instInhabitedExpr : Inhabited Expr

def Int.Linear.instBEqExpr.beq : Expr → Expr → Bool

@[implicit_reducible]

instance Int.Linear.instBEqExpr : BEq Expr

@[inline]

abbrev Int.Linear.Expr.denote (ctx : Context) : Expr → Int

inductive Int.Linear.Poly : Type

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

@[implicit_reducible]

instance Int.Linear.instBEqPoly : BEq Poly

def Int.Linear.instBEqPoly.beq : Poly → Poly → Bool

instance Int.Linear.instReflBEqPoly : ReflBEq Poly

instance Int.Linear.instLawfulBEqPoly : LawfulBEq Poly

noncomputable def Int.Linear.Poly.beq' (p₁ : Poly) : Poly → Bool

@[simp]

theorem Int.Linear.Poly.beq'_eq (p₁ p₂ : Poly) : (p₁.beq' p₂ = true) = (p₁ = p₂)

@[inline]

abbrev Int.Linear.Poly.denote (ctx : Context) (p : Poly) : Int

@[inline]

noncomputable abbrev Int.Linear.Poly.denote'.go (ctx : Context) (p : Poly) : Int → Int

@[inline]

noncomputable abbrev Int.Linear.Poly.denote' (ctx : Context) (p : Poly) : Int

Similar to Poly.denote, but produces a denotation better for simp +arith. Remark: we used to convert Poly back into Expr to achieve that.

@[simp]

theorem Int.Linear.Poly.denote'_go_eq_denote (ctx : Context) (p : Poly) (r : Int) : denote'.go ctx p r = denote ctx p + r

theorem Int.Linear.Poly.denote'_eq_denote (ctx : Context) (p : Poly) : denote' ctx p = denote ctx p

theorem Int.Linear.Poly.denote'_add (ctx : Context) (a : Int) (x : Var) (p : Poly) : denote' ctx (add a x p) = a * Var.denote ctx x + denote ctx p

def Int.Linear.Poly.addConst (p : Poly) (k : Int) : Poly

noncomputable def Int.Linear.Poly.addConst_k (p : Poly) (k : Int) : Poly

@[simp]

theorem Int.Linear.Poly.addConst_k_eq_addConst (p : Poly) (k : Int) : p.addConst_k k = p.addConst k

def Int.Linear.Poly.insert (k : Int) (v : Var) (p : Poly) : Poly

def Int.Linear.Poly.norm (p : Poly) : Poly

Normalizes the given polynomial by fusing monomial and constants.

def Int.Linear.Poly.append (p₁ p₂ : Poly) : Poly

def Int.Linear.Poly.combine' (fuel : Nat) (p₁ p₂ : Poly) : Poly

@[reducible, inline]

abbrev Int.Linear.hugeFuel : Nat

def Int.Linear.Poly.combine (p₁ p₂ : Poly) : Poly

def Int.Linear.Expr.toPoly' (e : Expr) : Poly

Converts the given expression into a polynomial.

def Int.Linear.Expr.toPoly'.go (coeff : Int) : Expr → Poly → Poly

def Int.Linear.Expr.norm (e : Expr) : Poly

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

def Int.Linear.cdiv (a b : Int) : Int

Returns the ceiling of the division a / b. That is, the result is equivalent to ⌈a / b⌉. Examples:

• cdiv 7 3 returns 3
• cdiv (-7) 3 returns -2.

def Int.Linear.cmod (a b : Int) : Int

Returns the ceiling-compatible remainder of the division a / b. This function ensures that the remainder is consistent with cdiv, meaning:

a = b * cdiv a b + cmod a b

See theorem cdiv_add_cmod. We also have

-b < cmod a b ≤ 0

theorem Int.Linear.cdiv_add_cmod (a b : Int) : b * cdiv a b + cmod a b = a

theorem Int.Linear.cmod_gt_of_pos (a : Int) {b : Int} (h : 0 < b) : cmod a b > -b

theorem Int.Linear.cmod_nonpos (a : Int) {b : Int} (h : b ≠ 0) : cmod a b ≤ 0

theorem Int.Linear.cmod_eq_zero_iff_emod_eq_zero (a b : Int) : cmod a b = 0 ↔ a % b = 0

theorem Int.Linear.cdiv_eq_div_of_divides {a b : Int} (h : a % b = 0) : a / b = cdiv a b

def Int.Linear.Poly.getConst : Poly → Int

Returns the constant of the given linear polynomial.

def Int.Linear.Poly.div (k : Int) : Poly → Poly

p.div k divides all coefficients of the polynomial p by k, but rounds up the constant using cdiv. Notes:

• We only use this function with ks that divides all coefficients.
• We use cdiv for the constant to implement the inequality tightening rule.

def Int.Linear.Poly.divAll (k : Int) : Poly → Bool

Returns true if k divides all coefficients and the constant of the given linear polynomial.

def Int.Linear.Poly.divCoeffs (k : Int) : Poly → Bool

Returns true if k divides all coefficients of the given linear polynomial.

def Int.Linear.Poly.mul' (p : Poly) (k : Int) : Poly

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

def Int.Linear.Poly.mul (p : Poly) (k : Int) : Poly

noncomputable def Int.Linear.Poly.mul_k (p : Poly) (k : Int) : Poly

@[simp]

theorem Int.Linear.Poly.mul_k_eq_mul (k : Int) (p : Poly) : p.mul_k k = p.mul k

noncomputable def Int.Linear.Poly.combine_mul_k' (fuel : Nat) (a b : Int) : Poly → Poly → Poly

noncomputable def Int.Linear.Poly.combine_mul_k (a b : Int) (p₁ p₂ : Poly) : Poly

@[simp]

theorem Int.Linear.Poly.denote_mul (ctx : Context) (p : Poly) (k : Int) : denote ctx (p.mul k) = k * denote ctx p

theorem Int.Linear.Poly.denote_addConst (ctx : Context) (p : Poly) (k : Int) : denote ctx (p.addConst k) = denote ctx p + k

theorem Int.Linear.Poly.denote_insert (ctx : Context) (k : Int) (v : Var) (p : Poly) : denote ctx (insert k v p) = denote ctx p + k * Var.denote ctx v

theorem Int.Linear.Poly.denote_norm (ctx : Context) (p : Poly) : denote ctx p.norm = denote ctx p

theorem Int.Linear.Poly.denote_append (ctx : Context) (p₁ p₂ : Poly) : denote ctx (p₁.append p₂) = denote ctx p₁ + denote ctx p₂

theorem Int.Linear.Poly.denote_combine' (ctx : Context) (fuel : Nat) (p₁ p₂ : Poly) : denote ctx (combine' fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂

theorem Int.Linear.Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : denote ctx (p₁.combine p₂) = denote ctx p₁ + denote ctx p₂

theorem Int.Linear.Poly.denote_combine_mul_k (ctx : Context) (a b : Int) (p₁ p₂ : Poly) : denote ctx (combine_mul_k a b p₁ p₂) = a * denote ctx p₁ + b * denote ctx p₂

theorem Int.Linear.sub_fold (a b : Int) : a.sub b = a - b

theorem Int.Linear.neg_fold (a : Int) : a.neg = -a

theorem Int.Linear.Poly.denote_div_eq_of_divAll (ctx : Context) (p : Poly) (k : Int) : divAll k p = true → denote ctx (div k p) * k = denote ctx p

theorem Int.Linear.Poly.denote_div_eq_of_divCoeffs (ctx : Context) (p : Poly) (k : Int) : divCoeffs k p = true → denote ctx (div k p) * k + cmod p.getConst k = denote ctx p

theorem Int.Linear.Expr.denote_toPoly'_go {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 Int.Linear.Expr.denote_norm (ctx : Context) (e : Expr) : Poly.denote ctx e.norm = denote ctx e

theorem Int.Linear.Expr.eq_of_norm_eq (ctx : Context) (e : Expr) (p : Poly) (h : e.norm.beq' p = true) : denote ctx e = Poly.denote' ctx p

noncomputable def Int.Linear.norm_eq_cert (lhs rhs : Expr) (p : Poly) : Bool

theorem Int.Linear.norm_eq (ctx : Context) (lhs rhs : Expr) (p : Poly) (h : norm_eq_cert lhs rhs p = true) : (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Poly.denote' ctx p = 0)

theorem Int.Linear.norm_le (ctx : Context) (lhs rhs : Expr) (p : Poly) (h : norm_eq_cert lhs rhs p = true) : (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Poly.denote' ctx p ≤ 0)

noncomputable def Int.Linear.norm_eq_var_cert (lhs rhs : Expr) (x y : Var) : Bool

theorem Int.Linear.norm_eq_var (ctx : Context) (lhs rhs : Expr) (x y : Var) (h : norm_eq_var_cert lhs rhs x y = true) : (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Var.denote ctx x = Var.denote ctx y)

noncomputable def Int.Linear.norm_eq_var_const_cert (lhs rhs : Expr) (x : Var) (k : Int) : Bool

theorem Int.Linear.norm_eq_var_const (ctx : Context) (lhs rhs : Expr) (x : Var) (k : Int) (h : norm_eq_var_const_cert lhs rhs x k = true) : (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Var.denote ctx x = k)

theorem Int.Linear.norm_eq_coeff' (ctx : Context) (p p' : Poly) (k : Int) : p = p'.mul k → k > 0 → (Poly.denote ctx p = 0 ↔ Poly.denote ctx p' = 0)

noncomputable def Int.Linear.norm_eq_coeff_cert (lhs rhs : Expr) (p : Poly) (k : Int) : Bool

theorem Int.Linear.norm_eq_coeff (ctx : Context) (lhs rhs : Expr) (p : Poly) (k : Int) : norm_eq_coeff_cert lhs rhs p k = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Poly.denote' ctx p = 0)

theorem Int.Linear.norm_le_coeff (ctx : Context) (lhs rhs : Expr) (p : Poly) (k : Int) : norm_eq_coeff_cert lhs rhs p k = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Poly.denote' ctx p ≤ 0)

noncomputable def Int.Linear.norm_le_coeff_tight_cert (lhs rhs : Expr) (p : Poly) (k : Int) : Bool

theorem Int.Linear.norm_le_coeff_tight (ctx : Context) (lhs rhs : Expr) (p : Poly) (k : Int) : norm_le_coeff_tight_cert lhs rhs p k = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Poly.denote' ctx p ≤ 0)

def Int.Linear.Poly.isUnsatEq (p : Poly) : Bool

def Int.Linear.Poly.isValidEq (p : Poly) : Bool

noncomputable def Int.Linear.Poly.isUnsatEq_k (p : Poly) : Bool

theorem Int.Linear.eq_eq_false (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isUnsatEq_k = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = False

theorem Int.Linear.eq_eq_true (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isValidEq = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = True

def Int.Linear.Poly.isUnsatLe (p : Poly) : Bool

def Int.Linear.Poly.isValidLe (p : Poly) : Bool

theorem Int.Linear.le_eq_false (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isUnsatLe = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = False

theorem Int.Linear.le_eq_true (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isValidLe = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = True

noncomputable def Int.Linear.unsatEqDivCoeffCert (lhs rhs : Expr) (k : Int) : Bool

theorem Int.Linear.eq_eq_false_of_divCoeff (ctx : Context) (lhs rhs : Expr) (k : Int) : unsatEqDivCoeffCert lhs rhs k = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = False

def Int.Linear.Poly.gcdCoeffs : Poly → Int → Int

theorem Int.Linear.Poly.gcd_dvd_const {ctx : Context} {p : Poly} {k : Int} (h : k ∣ denote ctx p) : p.gcdCoeffs k ∣ p.getConst

def Int.Linear.Poly.isUnsatDvd (k : Int) (p : Poly) : Bool

theorem Int.Linear.dvd_unsat (ctx : Context) (k : Int) (p : Poly) : Poly.isUnsatDvd k p = true → k ∣ Poly.denote' ctx p → False

theorem Int.Linear.norm_dvd (ctx : Context) (k : Int) (e : Expr) (p : Poly) : e.norm.beq' p = true → (k ∣ Expr.denote ctx e) = (k ∣ Poly.denote' ctx p)

theorem Int.Linear.dvd_eq_false (ctx : Context) (k : Int) (e : Expr) (h : Poly.isUnsatDvd k e.norm = true) : (k ∣ Expr.denote ctx e) = False

noncomputable def Int.Linear.dvd_coeff_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly) (k : Int) : Bool

noncomputable def Int.Linear.norm_dvd_gcd_cert (k₁ : Int) (e₁ : Expr) (k₂ : Int) (p₂ : Poly) (k : Int) : Bool

theorem Int.Linear.norm_dvd_gcd (ctx : Context) (k₁ : Int) (e₁ : Expr) (k₂ : Int) (p₂ : Poly) (g : Int) : norm_dvd_gcd_cert k₁ e₁ k₂ p₂ g = true → (k₁ ∣ Expr.denote ctx e₁) = (k₂ ∣ Poly.denote' ctx p₂)

theorem Int.Linear.dvd_coeff (ctx : Context) (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly) (g : Int) : dvd_coeff_cert k₁ p₁ k₂ p₂ g = true → k₁ ∣ Poly.denote' ctx p₁ → k₂ ∣ Poly.denote' ctx p₂

noncomputable def Int.Linear.dvd_elim_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly) : Bool

theorem Int.Linear.dvd_elim (ctx : Context) (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly) : dvd_elim_cert k₁ p₁ k₂ p₂ = true → k₁ ∣ Poly.denote' ctx p₁ → k₂ ∣ Poly.denote' ctx p₂

noncomputable def Int.Linear.dvd_solve_combine_cert (d₁ : Int) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d : Int) (p : Poly) (g α β : Int) : Bool

theorem Int.Linear.dvd_solve_combine (ctx : Context) (d₁ : Int) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d : Int) (p : Poly) (g α β : Int) : dvd_solve_combine_cert d₁ p₁ d₂ p₂ d p g α β = true → d₁ ∣ Poly.denote' ctx p₁ → d₂ ∣ Poly.denote' ctx p₂ → d ∣ Poly.denote' ctx p

noncomputable def Int.Linear.dvd_solve_elim_cert (d₁ : Int) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d : Int) (p : Poly) : Bool

theorem Int.Linear.dvd_solve_elim (ctx : Context) (d₁ : Int) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d : Int) (p : Poly) : dvd_solve_elim_cert d₁ p₁ d₂ p₂ d p = true → d₁ ∣ Poly.denote' ctx p₁ → d₂ ∣ Poly.denote' ctx p₂ → d ∣ Poly.denote' ctx p

theorem Int.Linear.dvd_norm (ctx : Context) (d : Int) (p₁ p₂ : Poly) : p₁.norm.beq' p₂ = true → d ∣ Poly.denote' ctx p₁ → d ∣ Poly.denote' ctx p₂

theorem Int.Linear.le_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm.beq' p₂ = true) : Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0

noncomputable def Int.Linear.le_coeff_cert (p₁ p₂ : Poly) (k : Int) : Bool

theorem Int.Linear.le_coeff (ctx : Context) (p₁ p₂ : Poly) (k : Int) : le_coeff_cert p₁ p₂ k = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0

noncomputable def Int.Linear.le_neg_cert (p₁ p₂ : Poly) : Bool

theorem Int.Linear.le_neg (ctx : Context) (p₁ p₂ : Poly) : le_neg_cert p₁ p₂ = true → ¬Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0

def Int.Linear.Poly.leadCoeff (p : Poly) : Int

noncomputable def Int.Linear.le_combine_cert (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.le_combine (ctx : Context) (p₁ p₂ p₃ : Poly) : le_combine_cert p₁ p₂ p₃ = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₃ ≤ 0

noncomputable def Int.Linear.le_combine_coeff_cert (p₁ p₂ p₃ : Poly) (k : Int) : Bool

theorem Int.Linear.le_combine_coeff (ctx : Context) (p₁ p₂ p₃ : Poly) (k : Int) : le_combine_coeff_cert p₁ p₂ p₃ k = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₃ ≤ 0

theorem Int.Linear.le_unsat (ctx : Context) (p : Poly) : p.isUnsatLe = true → Poly.denote' ctx p ≤ 0 → False

theorem Int.Linear.eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm.beq' p₂ = true) : Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ = 0

noncomputable def Int.Linear.eq_coeff_cert (p p' : Poly) (k : Int) : Bool

theorem Int.Linear.eq_coeff (ctx : Context) (p p' : Poly) (k : Int) : eq_coeff_cert p p' k = true → Poly.denote' ctx p = 0 → Poly.denote' ctx p' = 0

theorem Int.Linear.eq_unsat (ctx : Context) (p : Poly) : p.isUnsatEq = true → Poly.denote' ctx p = 0 → False

noncomputable def Int.Linear.eq_unsat_coeff_cert (p : Poly) (k : Int) : Bool

theorem Int.Linear.eq_unsat_coeff (ctx : Context) (p : Poly) (k : Int) : eq_unsat_coeff_cert p k = true → Poly.denote' ctx p = 0 → False

def Int.Linear.Poly.coeff (p : Poly) (x : Var) : Int

noncomputable def Int.Linear.Poly.coeff_k (p : Poly) (x : Var) : Int

@[simp]

theorem Int.Linear.Poly.coeff_k_eq_coeff (p : Poly) (x : Var) : p.coeff_k x = p.coeff x

def Int.Linear.abs (x : Int) : Int

noncomputable def Int.Linear.dvd_of_eq_cert (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) : Bool

theorem Int.Linear.dvd_of_eq (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) : dvd_of_eq_cert x p₁ d₂ p₂ = true → Poly.denote' ctx p₁ = 0 → d₂ ∣ Poly.denote' ctx p₂

noncomputable def Int.Linear.eq_dvd_subst_cert (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d₃ : Int) (p₃ : Poly) : Bool

theorem Int.Linear.eq_dvd_subst (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d₃ : Int) (p₃ : Poly) : eq_dvd_subst_cert x p₁ d₂ p₂ d₃ p₃ = true → Poly.denote' ctx p₁ = 0 → d₂ ∣ Poly.denote' ctx p₂ → d₃ ∣ Poly.denote' ctx p₃

noncomputable def Int.Linear.eq_eq_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.eq_eq_subst (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

noncomputable def Int.Linear.eq_eq_subst'_cert (a b : Int) (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.eq_eq_subst' (ctx : Context) (a b : Int) (p₁ p₂ p₃ : Poly) : eq_eq_subst'_cert a b p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ = 0 → Poly.denote' ctx p₃ = 0

noncomputable def Int.Linear.eq_le_subst_nonneg_cert (x : Var) (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.eq_le_subst_nonneg (ctx : Context) (x : Var) (p₁ p₂ p₃ : Poly) : eq_le_subst_nonneg_cert x p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₃ ≤ 0

noncomputable def Int.Linear.eq_le_subst_nonpos_cert (x : Var) (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.eq_le_subst_nonpos (ctx : Context) (x : Var) (p₁ p₂ p₃ : Poly) : eq_le_subst_nonpos_cert x p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₃ ≤ 0

noncomputable def Int.Linear.eq_of_core_cert (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.eq_of_core (ctx : Context) (p₁ p₂ p₃ : Poly) : eq_of_core_cert p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = Poly.denote' ctx p₂ → Poly.denote' ctx p₃ = 0

def Int.Linear.Poly.isUnsatDiseq (p : Poly) : Bool

noncomputable def Int.Linear.Poly.isUnsatDiseq_k (p : Poly) : Bool

theorem Int.Linear.diseq_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm.beq' p₂ = true) : Poly.denote' ctx p₁ ≠ 0 → Poly.denote' ctx p₂ ≠ 0

theorem Int.Linear.diseq_coeff (ctx : Context) (p p' : Poly) (k : Int) : eq_coeff_cert p p' k = true → Poly.denote' ctx p ≠ 0 → Poly.denote' ctx p' ≠ 0

theorem Int.Linear.diseq_neg (ctx : Context) (p p' : Poly) : p'.beq' (p.mul (-1)) = true → Poly.denote' ctx p ≠ 0 → Poly.denote' ctx p' ≠ 0

theorem Int.Linear.diseq_unsat (ctx : Context) (p : Poly) : p.isUnsatDiseq_k = true → Poly.denote' ctx p ≠ 0 → False

noncomputable def Int.Linear.diseq_eq_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.eq_diseq_subst (ctx : Context) (x : Var) (p₁ p₂ p₃ : Poly) : diseq_eq_subst_cert x p₁ p₂ p₃ = true → Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ ≠ 0 → Poly.denote' ctx p₃ ≠ 0

theorem Int.Linear.diseq_of_core (ctx : Context) (p₁ p₂ p₃ : Poly) : eq_of_core_cert p₁ p₂ p₃ = true → Poly.denote' ctx p₁ ≠ Poly.denote' ctx p₂ → Poly.denote' ctx p₃ ≠ 0

noncomputable def Int.Linear.eq_of_le_ge_cert (p₁ p₂ : Poly) : Bool

theorem Int.Linear.eq_of_le_ge (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

noncomputable def Int.Linear.le_of_le_diseq_cert (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.le_of_le_diseq (ctx : Context) (p₁ p₂ p₃ : Poly) : le_of_le_diseq_cert p₁ p₂ p₃ = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≠ 0 → Poly.denote' ctx p₃ ≤ 0

noncomputable def Int.Linear.diseq_split_cert (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.diseq_split (ctx : Context) (p₁ p₂ p₃ : Poly) : diseq_split_cert p₁ p₂ p₃ = true → Poly.denote' ctx p₁ ≠ 0 → Poly.denote' ctx p₂ ≤ 0 ∨ Poly.denote' ctx p₃ ≤ 0

theorem Int.Linear.diseq_split_resolve (ctx : Context) (p₁ p₂ p₃ : Poly) : diseq_split_cert p₁ p₂ p₃ = true → Poly.denote' ctx p₁ ≠ 0 → ¬Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₃ ≤ 0

def Int.Linear.OrOver (n : Nat) (p : Nat → Prop) : Prop

theorem Int.Linear.orOver_one {p : Nat → Prop} : OrOver 1 p → p 0

theorem Int.Linear.orOver_resolve {n : Nat} {p : Nat → Prop} : OrOver (n + 1) p → ¬p n → OrOver n p

def Int.Linear.OrOver_cases_type (n : Nat) (p : Nat → Prop) : Prop

theorem Int.Linear.orOver_cases {n : Nat} {p : Nat → Prop} : OrOver (n + 1) p → OrOver_cases_type n p

noncomputable def Int.Linear.cooper_dvd_left_cert (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat) : Bool

def Int.Linear.Poly.tail (p : Poly) : Poly

def Int.Linear.cooper_dvd_left_split (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) : Prop

theorem Int.Linear.cooper_dvd_left (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat) : cooper_dvd_left_cert p₁ p₂ p₃ d n = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0 → d ∣ Poly.denote' ctx p₃ → OrOver n (cooper_dvd_left_split ctx p₁ p₂ p₃ d)

noncomputable def Int.Linear.cooper_dvd_left_split_ineq_cert (p₁ p₂ : Poly) (k b : Int) (p' : Poly) : Bool

theorem Int.Linear.cooper_dvd_left_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (b : Int) (p' : Poly) : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_ineq_cert p₁ p₂ (↑k) b p' = true → Poly.denote' ctx p' ≤ 0

noncomputable def Int.Linear.cooper_dvd_left_split_dvd1_cert (p₁ p' : Poly) (a k : Int) : Bool

theorem Int.Linear.cooper_dvd_left_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (a : Int) (p' : Poly) : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_dvd1_cert p₁ p' a ↑k = true → a ∣ Poly.denote' ctx p'

noncomputable def Int.Linear.cooper_dvd_left_split_dvd2_cert (p₁ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly) : Bool

theorem Int.Linear.cooper_dvd_left_split_dvd2 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly) : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_dvd2_cert p₁ p₃ d k d' p' = true → d' ∣ Poly.denote' ctx p'

noncomputable def Int.Linear.cooper_left_cert (p₁ p₂ : Poly) (n : Nat) : Bool

def Int.Linear.cooper_left_split (ctx : Context) (p₁ p₂ : Poly) (k : Nat) : Prop

theorem Int.Linear.cooper_left (ctx : Context) (p₁ p₂ : Poly) (n : Nat) : cooper_left_cert p₁ p₂ n = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0 → OrOver n (cooper_left_split ctx p₁ p₂)

noncomputable def Int.Linear.cooper_left_split_ineq_cert (p₁ p₂ : Poly) (k b : Int) (p' : Poly) : Bool

theorem Int.Linear.cooper_left_split_ineq (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b : Int) (p' : Poly) : cooper_left_split ctx p₁ p₂ k → cooper_left_split_ineq_cert p₁ p₂ (↑k) b p' = true → Poly.denote' ctx p' ≤ 0

noncomputable def Int.Linear.cooper_left_split_dvd_cert (p₁ p' : Poly) (a k : Int) : Bool

theorem Int.Linear.cooper_left_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (a : Int) (p' : Poly) : cooper_left_split ctx p₁ p₂ k → cooper_left_split_dvd_cert p₁ p' a ↑k = true → a ∣ Poly.denote' ctx p'

noncomputable def Int.Linear.cooper_dvd_right_cert (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat) : Bool

def Int.Linear.cooper_dvd_right_split (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) : Prop

theorem Int.Linear.cooper_dvd_right (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat) : cooper_dvd_right_cert p₁ p₂ p₃ d n = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0 → d ∣ Poly.denote' ctx p₃ → OrOver n (cooper_dvd_right_split ctx p₁ p₂ p₃ d)

noncomputable def Int.Linear.cooper_dvd_right_split_ineq_cert (p₁ p₂ : Poly) (k a : Int) (p' : Poly) : Bool

theorem Int.Linear.cooper_dvd_right_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (a : Int) (p' : Poly) : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_ineq_cert p₁ p₂ (↑k) a p' = true → Poly.denote' ctx p' ≤ 0

noncomputable def Int.Linear.cooper_dvd_right_split_dvd1_cert (p₂ p' : Poly) (b k : Int) : Bool

theorem Int.Linear.cooper_dvd_right_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (b : Int) (p' : Poly) : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd1_cert p₂ p' b ↑k = true → b ∣ Poly.denote' ctx p'

noncomputable def Int.Linear.cooper_dvd_right_split_dvd2_cert (p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly) : Bool

theorem Int.Linear.cooper_dvd_right_split_dvd2 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly) : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd2_cert p₂ p₃ d k d' p' = true → d' ∣ Poly.denote' ctx p'

noncomputable def Int.Linear.cooper_right_cert (p₁ p₂ : Poly) (n : Nat) : Bool

def Int.Linear.cooper_right_split (ctx : Context) (p₁ p₂ : Poly) (k : Nat) : Prop

theorem Int.Linear.cooper_right (ctx : Context) (p₁ p₂ : Poly) (n : Nat) : cooper_right_cert p₁ p₂ n = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0 → OrOver n (cooper_right_split ctx p₁ p₂)

noncomputable def Int.Linear.cooper_right_split_ineq_cert (p₁ p₂ : Poly) (k a : Int) (p' : Poly) : Bool

theorem Int.Linear.cooper_right_split_ineq (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (a : Int) (p' : Poly) : cooper_right_split ctx p₁ p₂ k → cooper_right_split_ineq_cert p₁ p₂ (↑k) a p' = true → Poly.denote' ctx p' ≤ 0

noncomputable def Int.Linear.cooper_right_split_dvd_cert (p₂ p' : Poly) (b k : Int) : Bool

theorem Int.Linear.cooper_right_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b : Int) (p' : Poly) : cooper_right_split ctx p₁ p₂ k → cooper_right_split_dvd_cert p₂ p' b ↑k = true → b ∣ Poly.denote' ctx p'

@[reducible, inline]

abbrev Int.Linear.Poly.casesOnAdd (p : Poly) (k : Int → Var → Poly → Bool) : Bool

@[reducible, inline]

abbrev Int.Linear.Poly.casesOnNum (p : Poly) (k : Int → Bool) : Bool

noncomputable def Int.Linear.cooper_unsat_cert (p₁ p₂ p₃ : Poly) (d α β : Int) : Bool

theorem Int.Linear.cooper_unsat (ctx : Context) (p₁ p₂ p₃ : Poly) (d α β : Int) : cooper_unsat_cert p₁ p₂ p₃ d α β = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0 → d ∣ Poly.denote' ctx p₃ → False

theorem Int.Linear.ediv_emod (x y : Int) : -1 * x + y * (x / y) + x % y = 0

theorem Int.Linear.emod_nonneg (x y : Int) : (y != 0) = true → -1 * (x % y) ≤ 0

def Int.Linear.emod_le_cert (y n : Int) : Bool

theorem Int.Linear.emod_le (x y n : Int) : emod_le_cert y n = true → x % y + n ≤ 0

noncomputable def Int.Linear.dvd_le_tight_cert (d : Int) (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.dvd_le_tight (ctx : Context) (d : Int) (p₁ p₂ p₃ : Poly) : dvd_le_tight_cert d p₁ p₂ p₃ = true → d ∣ Poly.denote' ctx p₁ → Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₃ ≤ 0

noncomputable def Int.Linear.dvd_neg_le_tight_cert (d : Int) (p₁ p₂ p₃ : Poly) : Bool

theorem Int.Linear.Poly.mul_minus_one_getConst_eq (p : Poly) : (p.mul (-1)).getConst = -p.getConst

theorem Int.Linear.dvd_neg_le_tight (ctx : Context) (d : Int) (p₁ p₂ p₃ : Poly) : dvd_neg_le_tight_cert d p₁ p₂ p₃ = true → d ∣ Poly.denote' ctx p₁ → Poly.denote' ctx p₂ ≤ 0 → Poly.denote' ctx p₃ ≤ 0

theorem Int.Linear.le_norm_expr (ctx : Context) (lhs rhs : Expr) (p : Poly) : norm_eq_cert lhs rhs p = true → Expr.denote ctx lhs ≤ Expr.denote ctx rhs → Poly.denote' ctx p ≤ 0

noncomputable def Int.Linear.not_le_norm_expr_cert (lhs rhs : Expr) (p : Poly) : Bool

theorem Int.Linear.not_le_norm_expr (ctx : Context) (lhs rhs : Expr) (p : Poly) : not_le_norm_expr_cert lhs rhs p = true → ¬Expr.denote ctx lhs ≤ Expr.denote ctx rhs → Poly.denote' ctx p ≤ 0

theorem Int.Linear.dvd_norm_expr (ctx : Context) (d : Int) (e : Expr) (p : Poly) : (p == e.norm) = true → d ∣ Expr.denote ctx e → d ∣ Poly.denote' ctx p

theorem Int.Linear.eq_norm_expr (ctx : Context) (lhs rhs : Expr) (p : Poly) : norm_eq_cert lhs rhs p = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Poly.denote' ctx p = 0

theorem Int.Linear.not_eq_norm_expr (ctx : Context) (lhs rhs : Expr) (p : Poly) : norm_eq_cert lhs rhs p = true → ¬Expr.denote ctx lhs = Expr.denote ctx rhs → ¬Poly.denote' ctx p = 0

theorem Int.Linear.of_not_dvd (a b : Int) : (a != 0) = true → ¬a ∣ b → b % a > 0

noncomputable def Int.Linear.eq_def_cert (x : Var) (xPoly p : Poly) : Bool

theorem Int.Linear.eq_def (ctx : Context) (x : Var) (xPoly p : Poly) : eq_def_cert x xPoly p = true → Var.denote ctx x = Poly.denote' ctx xPoly → Poly.denote' ctx p = 0

theorem Int.Linear.eq_def_norm (ctx : Context) (x : Var) (xPoly xPoly' p : Poly) : eq_def_cert x xPoly' p = true → Var.denote ctx x = Poly.denote' ctx xPoly → Poly.denote' ctx xPoly = Poly.denote' ctx xPoly' → Poly.denote' ctx p = 0

noncomputable def Int.Linear.eq_def'_cert (x : Var) (e : Expr) (p : Poly) : Bool

theorem Int.Linear.eq_def' (ctx : Context) (x : Var) (e : Expr) (p : Poly) : eq_def'_cert x e p = true → Var.denote ctx x = Expr.denote ctx e → Poly.denote' ctx p = 0

noncomputable def Int.Linear.eq_def'_norm_cert (x : Var) (e : Expr) (ePoly ePoly' p : Poly) : Bool

theorem Int.Linear.eq_def'_norm (ctx : Context) (x : Var) (e : Expr) (ePoly ePoly' p : Poly) : eq_def'_norm_cert x e ePoly ePoly' p = true → Var.denote ctx x = Expr.denote ctx e → Poly.denote' ctx ePoly = Poly.denote' ctx ePoly' → Poly.denote' ctx p = 0

theorem Int.Linear.eq_norm_poly (ctx : Context) (p p' : Poly) : Poly.denote' ctx p = Poly.denote' ctx p' → Poly.denote' ctx p = 0 → Poly.denote' ctx p' = 0

theorem Int.Linear.le_norm_poly (ctx : Context) (p p' : Poly) : Poly.denote' ctx p = Poly.denote' ctx p' → Poly.denote' ctx p ≤ 0 → Poly.denote' ctx p' ≤ 0

theorem Int.Linear.diseq_norm_poly (ctx : Context) (p p' : Poly) : Poly.denote' ctx p = Poly.denote' ctx p' → Poly.denote' ctx p ≠ 0 → Poly.denote' ctx p' ≠ 0

theorem Int.Linear.dvd_norm_poly (ctx : Context) (d : Int) (p p' : Poly) : Poly.denote' ctx p = Poly.denote' ctx p' → d ∣ Poly.denote' ctx p → d ∣ Poly.denote' ctx p'

Constraint propagation helper theorems.

def Int.Linear.le_of_le_cert (p₁ p₂ : Poly) : Bool

theorem Int.Linear.le_of_le' (ctx : Context) (p₁ p₂ : Poly) : le_of_le_cert p₁ p₂ = true → ∀ (k : Int), Poly.denote' ctx p₁ ≤ k → Poly.denote' ctx p₂ ≤ k

theorem Int.Linear.le_of_le (ctx : Context) (p₁ p₂ : Poly) : le_of_le_cert p₁ p₂ = true → Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0

def Int.Linear.not_le_of_le_cert (p₁ p₂ : Poly) : Bool

theorem Int.Linear.not_le_of_le' (ctx : Context) (p₁ p₂ : Poly) : not_le_of_le_cert p₁ p₂ = true → ∀ (k : Int), Poly.denote' ctx p₁ ≤ k → ¬Poly.denote' ctx p₂ ≤ -k

theorem Int.Linear.not_le_of_le (ctx : Context) (p₁ p₂ : Poly) : not_le_of_le_cert p₁ p₂ = true → Poly.denote' ctx p₁ ≤ 0 → ¬Poly.denote' ctx p₂ ≤ 0

theorem Int.Linear.natCast_sub (x y : Nat) : ↑(x - y) = if ↑y + -1 * ↑x ≤ 0 then ↑x + -1 * ↑y else 0

Helper theorem for linearizing nonlinear terms

noncomputable def Int.Linear.var_eq_cert (x : Var) (k : Int) (p : Poly) : Bool

theorem Int.Linear.var_eq (ctx : Context) (x : Var) (k : Int) (p : Poly) : var_eq_cert x k p = true → Poly.denote' ctx p = 0 → Var.denote ctx x = k

noncomputable def Int.Linear.of_var_eq_mul_cert (x : Var) (k : Int) (y : Var) (p : Poly) : Bool

theorem Int.Linear.of_var_eq_mul (ctx : Context) (x : Var) (k : Int) (y : Var) (p : Poly) : of_var_eq_mul_cert x k y p = true → Var.denote ctx x = k * Var.denote ctx y → Poly.denote' ctx p = 0

noncomputable def Int.Linear.of_var_eq_var_cert (x y : Var) (p : Poly) : Bool

theorem Int.Linear.of_var_eq_var (ctx : Context) (x y : Var) (p : Poly) : of_var_eq_var_cert x y p = true → Var.denote ctx x = Var.denote ctx y → Poly.denote' ctx p = 0

noncomputable def Int.Linear.of_var_eq_cert (x : Var) (k : Int) (p : Poly) : Bool

theorem Int.Linear.of_var_eq (ctx : Context) (x : Var) (k : Int) (p : Poly) : of_var_eq_cert x k p = true → Var.denote ctx x = k → Poly.denote' ctx p = 0

theorem Int.Linear.eq_one_mul (a : Int) : a = 1 * a

theorem Int.Linear.mul_eq_kk (a b k₁ k₂ k : Int) (h₁ : a = k₁) (h₂ : b = k₂) (h₃ : (k₁ * k₂ == k) = true) : a * b = k

theorem Int.Linear.mul_eq_kkx (a b k₁ k₂ c k : Int) (h₁ : a = k₁) (h₂ : b = k₂ * c) (h₃ : (k₁ * k₂ == k) = true) : a * b = k * c

theorem Int.Linear.mul_eq_kxk (a b k₁ c k₂ k : Int) (h₁ : a = k₁ * c) (h₂ : b = k₂) (h₃ : (k₁ * k₂ == k) = true) : a * b = k * c

theorem Int.Linear.mul_eq_zero_left (a b : Int) (h : a = 0) : a * b = 0

theorem Int.Linear.mul_eq_zero_right (a b : Int) (h : b = 0) : a * b = 0

theorem Int.Linear.div_eq (a b k : Int) (h : b = k) : a / b = a / k

theorem Int.Linear.mod_eq (a b k : Int) (h : b = k) : a % b = a % k

theorem Int.Linear.div_eq' (a b b' k : Int) (h₁ : b = b') (h₂ : (k == a / b') = true) : a / b = k

theorem Int.Linear.mod_eq' (a b b' k : Int) (h₁ : b = b') (h₂ : (k == a % b') = true) : a % b = k

theorem Int.Linear.pow_eq (a : Int) (b : Nat) (a' b' k : Int) (h₁ : a = a') (h₂ : ↑b = b') (h₃ : (k == a' ^ b'.toNat) = true) : a ^ b = k

theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a)

theorem Int.not_ge_eq (a b : Int) : (¬a ≥ b) = (a + 1 ≤ b)

theorem Int.not_lt_eq (a b : Int) : (¬a < b) = (b ≤ a)

theorem Int.not_gt_eq (a b : Int) : (¬a > b) = (a ≤ b)