Helper definitions and theorems for constructing linear arithmetic proofs.

@[reducible, inline]

abbrev Int.Linear.Var : Type

Equations

• Int.Linear.Var = Nat

@[reducible, inline]

abbrev Int.Linear.Context : Type

Equations

• Int.Linear.Context = Lean.RArray Int

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

Equations

• Int.Linear.Var.denote ctx v = Lean.RArray.get ctx v

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

instance Int.Linear.instInhabitedExpr : Inhabited Expr

Equations

• Int.Linear.instInhabitedExpr = { default := Int.Linear.Expr.num default }

instance Int.Linear.instBEqExpr : BEq Expr

Equations

• Int.Linear.instBEqExpr = { beq := Int.Linear.beqExpr✝ }

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

Equations

• Int.Linear.Expr.denote ctx (a.add b) = Int.Linear.Expr.denote ctx a + Int.Linear.Expr.denote ctx b
• Int.Linear.Expr.denote ctx (a.sub b) = Int.Linear.Expr.denote ctx a - Int.Linear.Expr.denote ctx b
• Int.Linear.Expr.denote ctx a.neg = -Int.Linear.Expr.denote ctx a
• Int.Linear.Expr.denote ctx (Int.Linear.Expr.num k) = k
• Int.Linear.Expr.denote ctx (Int.Linear.Expr.var v) = Int.Linear.Var.denote ctx v
• Int.Linear.Expr.denote ctx (Int.Linear.Expr.mulL k e) = k * Int.Linear.Expr.denote ctx e
• Int.Linear.Expr.denote ctx (e.mulR k) = Int.Linear.Expr.denote ctx e * k

inductive Int.Linear.Poly : Type

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

instance Int.Linear.instBEqPoly : BEq Poly

Equations

• Int.Linear.instBEqPoly = { beq := Int.Linear.beqPoly✝ }

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

Equations

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

@[simp]

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

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

Equations

• Int.Linear.Poly.denote ctx (Int.Linear.Poly.num k) = k
• Int.Linear.Poly.denote ctx (Int.Linear.Poly.add k v p_2) = k * Int.Linear.Var.denote ctx v + Int.Linear.Poly.denote ctx p_2

noncomputable def 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.

Equations

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

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

Equations

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

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

Equations

• (Int.Linear.Poly.num k_1).addConst k = Int.Linear.Poly.num (k + k_1)
• (Int.Linear.Poly.add k_1 v p_2).addConst k = Int.Linear.Poly.add k_1 v (p_2.addConst k)

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

Equations

• p.addConst_k k = Int.Linear.Poly.rec (fun (k' : Int) => Int.Linear.Poly.num (k.add k')) (fun (k' : Int) (v' : Int.Linear.Var) (x ih : Int.Linear.Poly) => Int.Linear.Poly.add k' v' ih) p

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

Equations

• One or more equations did not get rendered due to their size.
• Int.Linear.Poly.insert k v (Int.Linear.Poly.num k_1) = Int.Linear.Poly.add k v (Int.Linear.Poly.num k_1)

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

Normalizes the given polynomial by fusing monomial and constants.

Equations

• (Int.Linear.Poly.num k).norm = Int.Linear.Poly.num k
• (Int.Linear.Poly.add k v p_2).norm = Int.Linear.Poly.insert k v p_2.norm

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

Equations

• (Int.Linear.Poly.num k).append p₂ = p₂.addConst k
• (Int.Linear.Poly.add k v p_1).append p₂ = Int.Linear.Poly.add k v (p_1.append p₂)

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

Equations

• One or more equations did not get rendered due to their size.
• Int.Linear.Poly.combine' 0 p₁ p₂ = p₁.append p₂
• Int.Linear.Poly.combine' fuel_2.succ (Int.Linear.Poly.num k₁) (Int.Linear.Poly.num k₂) = Int.Linear.Poly.num (k₁ + k₂)
• Int.Linear.Poly.combine' fuel_2.succ (Int.Linear.Poly.num k₁) (Int.Linear.Poly.add a x p) = Int.Linear.Poly.add a x (Int.Linear.Poly.combine' fuel_2 (Int.Linear.Poly.num k₁) p)
• Int.Linear.Poly.combine' fuel_2.succ (Int.Linear.Poly.add a x p) (Int.Linear.Poly.num k₂) = Int.Linear.Poly.add a x (Int.Linear.Poly.combine' fuel_2 p (Int.Linear.Poly.num k₂))

@[reducible, inline]

abbrev Int.Linear.hugeFuel : Nat

Equations

• Int.Linear.hugeFuel = 100000000

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

Equations

• p₁.combine p₂ = Int.Linear.Poly.combine' Int.Linear.hugeFuel p₁ p₂

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

Converts the given expression into a polynomial.

Equations

• e.toPoly' = Int.Linear.Expr.toPoly'.go 1 e (Int.Linear.Poly.num 0)

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

Equations

• Int.Linear.Expr.toPoly'.go coeff (Int.Linear.Expr.num k) = bif k == 0 then id else fun (x : Int.Linear.Poly) => x.addConst (coeff.mul k)
• Int.Linear.Expr.toPoly'.go coeff (Int.Linear.Expr.var v) = fun (x : Int.Linear.Poly) => Int.Linear.Poly.add coeff v x
• Int.Linear.Expr.toPoly'.go coeff (a.add b) = Int.Linear.Expr.toPoly'.go coeff a ∘ Int.Linear.Expr.toPoly'.go coeff b
• Int.Linear.Expr.toPoly'.go coeff (a.sub b) = Int.Linear.Expr.toPoly'.go coeff a ∘ Int.Linear.Expr.toPoly'.go (-coeff) b
• Int.Linear.Expr.toPoly'.go coeff (Int.Linear.Expr.mulL k a) = bif k == 0 then id else Int.Linear.Expr.toPoly'.go (coeff.mul k) a
• Int.Linear.Expr.toPoly'.go coeff (a.mulR k) = bif k == 0 then id else Int.Linear.Expr.toPoly'.go (coeff.mul k) a
• Int.Linear.Expr.toPoly'.go coeff a.neg = Int.Linear.Expr.toPoly'.go (-coeff) a

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

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

Equations

• e.norm = e.toPoly'.norm

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.

Equations

• Int.Linear.cdiv a b = -(-a / b)

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

Equations

• Int.Linear.cmod a b = -(-a % b)

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.

Equations

• (Int.Linear.Poly.num k).getConst = k
• (Int.Linear.Poly.add k v p_1).getConst = p_1.getConst

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.

Equations

• Int.Linear.Poly.div k (Int.Linear.Poly.num k_1) = Int.Linear.Poly.num (Int.Linear.cdiv k_1 k)
• Int.Linear.Poly.div k (Int.Linear.Poly.add k_1 v p_1) = Int.Linear.Poly.add (k_1 / k) v (Int.Linear.Poly.div k p_1)

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

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

Equations

• Int.Linear.Poly.divAll k (Int.Linear.Poly.num k_1) = (k_1 % k == 0)
• Int.Linear.Poly.divAll k (Int.Linear.Poly.add k_1 v p_1) = (k_1 % k == 0 && Int.Linear.Poly.divAll k p_1)

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

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

Equations

• Int.Linear.Poly.divCoeffs k (Int.Linear.Poly.num k_1) = true
• Int.Linear.Poly.divCoeffs k (Int.Linear.Poly.add k_1 v p_1) = (k_1 % k == 0 && Int.Linear.Poly.divCoeffs k p_1)

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

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

Equations

• (Int.Linear.Poly.num k_1).mul' k = Int.Linear.Poly.num (k * k_1)
• (Int.Linear.Poly.add k_1 v p_2).mul' k = Int.Linear.Poly.add (k * k_1) v (p_2.mul' k)

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

Equations

• p.mul k = if (k == 0) = true then Int.Linear.Poly.num 0 else p.mul' k

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

Equations

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

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

Equations

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

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

Equations

• Int.Linear.Poly.combine_mul_k a b = Int.Linear.Poly.combine_mul_k' Int.Linear.hugeFuel a b

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

instance Int.Linear.instLawfulBEqPoly : LawfulBEq Poly

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

Equations

• Int.Linear.norm_eq_cert lhs rhs p = p.beq' (lhs.sub rhs).norm

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

Equations

• Int.Linear.norm_eq_var_cert lhs rhs x y = (lhs.sub rhs).norm.beq' (Int.Linear.Poly.add 1 x (Int.Linear.Poly.add (-1) y (Int.Linear.Poly.num 0)))

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

Equations

• Int.Linear.norm_eq_var_const_cert lhs rhs x k = (lhs.sub rhs).norm.beq' (Int.Linear.Poly.add 1 x (Int.Linear.Poly.num (-k)))

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

Equations

• Int.Linear.norm_eq_coeff_cert lhs rhs p k = ((lhs.sub rhs).norm.beq' (p.mul_k k)).and' (Int.blt' 0 k)

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

Equations

• Int.Linear.norm_le_coeff_tight_cert lhs rhs p k = (Int.blt' 0 k).and' ((Int.Linear.Poly.divCoeffs k (lhs.sub rhs).norm).and' (p.beq' (Int.Linear.Poly.div k (lhs.sub rhs).norm)))

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

Equations

• (Int.Linear.Poly.num k).isUnsatEq = (k != 0)
• p.isUnsatEq = false

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

Equations

• (Int.Linear.Poly.num k).isValidEq = (k == 0)
• p.isValidEq = false

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

Equations

• p.isUnsatEq_k = Int.Linear.Poly.rec (fun (k : Int) => (k.beq' 0).not') (fun (x : Int) (x : Int.Linear.Var) (x : Int.Linear.Poly) (x : Bool) => false) p

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

Equations

• (Int.Linear.Poly.num k).isUnsatLe = decide (k > 0)
• p.isUnsatLe = false

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

Equations

• (Int.Linear.Poly.num k).isValidLe = decide (k ≤ 0)
• p.isValidLe = false

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

Equations

• Int.Linear.unsatEqDivCoeffCert lhs rhs k = (Int.Linear.Poly.divCoeffs k (lhs.sub rhs).norm).and' ((Int.blt' 0 k).and' (decide (Int.Linear.cmod (lhs.sub rhs).norm.getConst k < 0)))

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

Equations

• (Int.Linear.Poly.num k).gcdCoeffs x✝ = x✝
• (Int.Linear.Poly.add k' v p).gcdCoeffs x✝ = p.gcdCoeffs ↑(k'.gcd x✝)

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

Equations

• Int.Linear.Poly.isUnsatDvd k p = (p.getConst % p.gcdCoeffs k != 0)

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

Equations

• Int.Linear.dvd_coeff_cert k₁ p₁ k₂ p₂ k = (k != 0).and' ((k₁.beq' (k.mul k₂)).and' (p₁.beq' (p₂.mul_k k)))

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

Equations

• Int.Linear.norm_dvd_gcd_cert k₁ e₁ k₂ p₂ k = Int.Linear.dvd_coeff_cert k₁ e₁.norm k₂ p₂ k

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

Equations

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Int.Linear.dvd_solve_elim_cert d₁ p₁ d₂ p₂ d p = false

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

Equations

• Int.Linear.le_coeff_cert p₁ p₂ k = (Int.blt' 0 k).and' ((Int.Linear.Poly.divCoeffs k p₁).and' (p₂.beq' (Int.Linear.Poly.div k p₁)))

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

Equations

• Int.Linear.le_neg_cert p₁ p₂ = p₂.beq' ((p₁.mul_k (-1)).addConst_k 1)

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

Equations

• (Int.Linear.Poly.add a v p_2).leadCoeff = a
• p.leadCoeff = 1

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

Equations

• Int.Linear.le_combine_cert p₁ p₂ p₃ = p₃.beq' (Int.Linear.Poly.combine_mul_k (↑p₂.leadCoeff.natAbs) (↑p₁.leadCoeff.natAbs) p₁ p₂)

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

Equations

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

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

Equations

• Int.Linear.eq_coeff_cert p p' k = (p.beq' (p'.mul_k k)).and' (decide (k > 0))

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

Equations

• Int.Linear.eq_unsat_coeff_cert p k = (Int.Linear.Poly.divCoeffs k p).and' ((Int.blt' 0 k).and' (decide (Int.Linear.cmod p.getConst k < 0)))

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

Equations

• (Int.Linear.Poly.add a y p_2).coeff x = bif x == y then a else p_2.coeff x
• (Int.Linear.Poly.num k).coeff x = 0

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

Equations

• p.coeff_k x = Int.Linear.Poly.rec (fun (x : Int) => 0) (fun (a : Int) (y : Int.Linear.Var) (x_1 : Int.Linear.Poly) (ih : Int) => Bool.rec ih a (Nat.beq x y)) p

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

Equations

• Int.Linear.abs x = Int.ofNat x.natAbs

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

Equations

• Int.Linear.dvd_of_eq_cert x p₁ d₂ p₂ = (d₂.beq' (Int.Linear.abs (p₁.coeff_k x))).and' (p₂.beq' (Int.Linear.Poly.insert (-p₁.coeff_k x) x p₁))

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

Equations

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

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

Equations

• Int.Linear.eq_eq_subst_cert x p₁ p₂ p₃ = p₃.beq' (Int.Linear.Poly.combine_mul_k (p₂.coeff_k x) (-p₁.coeff_k x) p₁ p₂)

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

Equations

• Int.Linear.eq_eq_subst'_cert a b p₁ p₂ p₃ = p₃.beq' (Int.Linear.Poly.combine_mul_k b (-a) p₁ p₂)

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

Equations

• Int.Linear.eq_le_subst_nonneg_cert x p₁ p₂ p₃ = (Int.ble' 0 (p₁.coeff x)).and' (p₃.beq' (Int.Linear.Poly.combine_mul_k (p₁.coeff x) (-p₂.coeff x) p₂ p₁))

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

Equations

• Int.Linear.eq_le_subst_nonpos_cert x p₁ p₂ p₃ = ((p₁.coeff x).ble' 0).and' (p₃.beq' (Int.Linear.Poly.combine_mul_k (p₂.coeff x) (-p₁.coeff x) p₁ p₂))

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

Equations

• Int.Linear.eq_of_core_cert p₁ p₂ p₃ = p₃.beq' (Int.Linear.Poly.combine_mul_k 1 (-1) p₁ p₂)

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

Equations

• (Int.Linear.Poly.num 0).isUnsatDiseq = true
• p.isUnsatDiseq = false

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

Equations

• p.isUnsatDiseq_k = Int.Linear.Poly.rec (fun (k : Int) => k.beq' 0) (fun (x : Int) (x : Int.Linear.Var) (x : Int.Linear.Poly) (x : Bool) => false) p

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

Equations

• Int.Linear.diseq_eq_subst_cert x p₁ p₂ p₃ = (!(p₁.coeff x).beq' 0).and' (p₃.beq' (Int.Linear.Poly.combine_mul_k (p₂.coeff x) (-p₁.coeff x) p₁ p₂))

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

Equations

• Int.Linear.eq_of_le_ge_cert p₁ p₂ = p₂.beq' (p₁.mul_k (-1))

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

Equations

• Int.Linear.le_of_le_diseq_cert p₁ p₂ p₃ = (p₂.beq' p₁ || p₂.beq' (p₁.mul_k (-1))).and' (p₃.beq' (p₁.addConst_k 1))

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

Equations

• Int.Linear.diseq_split_cert p₁ p₂ p₃ = (p₂.beq' (p₁.addConst_k 1)).and' (p₃.beq' ((p₁.mul_k (-1)).addConst_k 1))

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

Equations

• Int.Linear.OrOver 0 p = False
• Int.Linear.OrOver fuel_1.succ p = (p fuel_1 ∨ Int.Linear.OrOver fuel_1 p)

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

Equations

• Int.Linear.OrOver_cases_type 0 p = p 0
• Int.Linear.OrOver_cases_type fuel_1.succ p = (¬p (fuel_1 + 1) → Int.Linear.OrOver_cases_type fuel_1 p)

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

Equations

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

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

Equations

• (Int.Linear.Poly.add a v p_2).tail = p_2
• p.tail = p

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

Equations

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

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

Equations

• Int.Linear.cooper_dvd_left_split_ineq_cert p₁ p₂ k b p' = (p₂.leadCoeff.beq' b).and' (p'.beq' ((Int.Linear.Poly.combine_mul_k b (-p₁.leadCoeff) p₁.tail p₂.tail).addConst_k (b * k)))

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

Equations

• Int.Linear.cooper_dvd_left_split_dvd1_cert p₁ p' a k = (a.beq' p₁.leadCoeff).and' (p'.beq' (p₁.tail.addConst_k k))

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Int.Linear.cooper_left_split_ineq_cert p₁ p₂ k b p' = (p₂.leadCoeff.beq' b).and' (p'.beq' ((Int.Linear.Poly.combine_mul_k b (-p₁.leadCoeff) p₁.tail p₂.tail).addConst_k (b * k)))

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

Equations

• Int.Linear.cooper_left_split_dvd_cert p₁ p' a k = (a.beq' p₁.leadCoeff).and' (p'.beq' (p₁.tail.addConst_k k))

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

Equations

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

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

Equations

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

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

Equations

• Int.Linear.cooper_dvd_right_split_ineq_cert p₁ p₂ k a p' = (p₁.leadCoeff.beq' a).and' (p'.beq' ((Int.Linear.Poly.combine_mul_k p₂.leadCoeff (-a) p₁.tail p₂.tail).addConst_k (-a * k)))

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

Equations

• Int.Linear.cooper_dvd_right_split_dvd1_cert p₂ p' b k = (b.beq' p₂.leadCoeff).and' (p'.beq' (p₂.tail.addConst_k k))

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Int.Linear.cooper_right_split_ineq_cert p₁ p₂ k a p' = (p₁.leadCoeff.beq' a).and' (p'.beq' ((Int.Linear.Poly.combine_mul_k p₂.leadCoeff (-a) p₁.tail p₂.tail).addConst_k (-a * k)))

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

Equations

• Int.Linear.cooper_right_split_dvd_cert p₂ p' b k = (b.beq' p₂.leadCoeff).and' (p'.beq' (p₂.tail.addConst_k k))

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

Equations

• p.casesOnAdd k = Int.Linear.Poly.casesOn p (fun (x : Int) => false) k

@[reducible, inline]

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

Equations

• p.casesOnNum k = Int.Linear.Poly.casesOn p k fun (x : Int) (x : Int.Linear.Var) (x : Int.Linear.Poly) => false

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

Equations

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

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

Equations

• Int.Linear.emod_le_cert y n = (y != 0 && n == 1 - ↑y.natAbs)

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

Equations

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

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

Equations

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

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

Equations

• Int.Linear.not_le_norm_expr_cert lhs rhs p = p.beq' (((lhs.sub rhs).norm.mul_k (-1)).addConst_k 1)

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

Equations

• Int.Linear.eq_def_cert x xPoly p = p.beq' (Int.Linear.Poly.add (-1) x xPoly)

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

Equations

• Int.Linear.eq_def'_cert x e p = p.beq' (Int.Linear.Poly.add (-1) x e.norm)

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

Equations

• Int.Linear.eq_def'_norm_cert x e ePoly ePoly' p = (ePoly.beq' e.norm).and' (p.beq' (Int.Linear.Poly.add (-1) x ePoly'))

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

Equations

• Int.Linear.le_of_le_cert (Int.Linear.Poly.add k v p) (Int.Linear.Poly.num k_1) = false
• Int.Linear.le_of_le_cert (Int.Linear.Poly.num k) (Int.Linear.Poly.add k_1 v p) = false
• Int.Linear.le_of_le_cert (Int.Linear.Poly.num c₁) (Int.Linear.Poly.num c₂) = decide (c₁ ≥ c₂)
• Int.Linear.le_of_le_cert (Int.Linear.Poly.add a₁ x₁ p₁_2) (Int.Linear.Poly.add a₂ x₂ p₂_2) = (a₁ == a₂ && x₁ == x₂ && Int.Linear.le_of_le_cert p₁_2 p₂_2)

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

Equations

• Int.Linear.not_le_of_le_cert (Int.Linear.Poly.add k v p) (Int.Linear.Poly.num k_1) = false
• Int.Linear.not_le_of_le_cert (Int.Linear.Poly.num k) (Int.Linear.Poly.add k_1 v p) = false
• Int.Linear.not_le_of_le_cert (Int.Linear.Poly.num c₁) (Int.Linear.Poly.num c₂) = decide (c₁ ≥ 1 - c₂)
• Int.Linear.not_le_of_le_cert (Int.Linear.Poly.add a₁ x₁ p₁_2) (Int.Linear.Poly.add a₂ x₂ p₂_2) = (a₁ == -a₂ && x₁ == x₂ && Int.Linear.not_le_of_le_cert p₁_2 p₂_2)

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.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)