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).add (Int.Linear.Expr.denote ctx b)
• Int.Linear.Expr.denote ctx (a.sub b) = (Int.Linear.Expr.denote ctx a).sub (Int.Linear.Expr.denote ctx b)
• Int.Linear.Expr.denote ctx a.neg = (Int.Linear.Expr.denote ctx a).neg
• 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.mul (Int.Linear.Expr.denote ctx e)
• Int.Linear.Expr.denote ctx (e.mulR k) = (Int.Linear.Expr.denote ctx e).mul 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✝ }

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.mul (Int.Linear.Var.denote ctx v)).add (Int.Linear.Poly.denote ctx p_2)

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

• Int.Linear.Poly.denote' ctx (Int.Linear.Poly.num k) = k
• Int.Linear.Poly.denote' ctx (Int.Linear.Poly.add 1 v p_2) = Int.Linear.Poly.denote'.go ctx (Int.Linear.Var.denote ctx v) p_2
• Int.Linear.Poly.denote' ctx (Int.Linear.Poly.add k v p_2) = Int.Linear.Poly.denote'.go ctx (k.mul (Int.Linear.Var.denote ctx v)) p_2

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

Equations

• Int.Linear.Poly.denote'.go ctx r (Int.Linear.Poly.num 0) = r
• Int.Linear.Poly.denote'.go ctx r (Int.Linear.Poly.num k) = r.add k
• Int.Linear.Poly.denote'.go ctx r (Int.Linear.Poly.add 1 v p_2) = Int.Linear.Poly.denote'.go ctx (r.add (Int.Linear.Var.denote ctx v)) p_2
• Int.Linear.Poly.denote'.go ctx r (Int.Linear.Poly.add k v p_2) = Int.Linear.Poly.denote'.go ctx (r.add (k.mul (Int.Linear.Var.denote ctx v))) p_2

theorem Int.Linear.Poly.denote'_go_eq_denote (ctx : Context) (p : Poly) (r : Int) : denote'.go ctx r p = 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)

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

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

Equations

• p₁.combine p₂ = Int.Linear.Poly.combine' 100000000 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)

@[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.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 == p) = true) : denote ctx e = Poly.denote' ctx p

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

Equations

• Int.Linear.norm_eq_cert lhs rhs p = (p == (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)

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

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

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 == p.mul k && decide (k > 0))

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)

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 = (decide (k > 0) && (Int.Linear.Poly.divCoeffs k (lhs.sub rhs).norm && p == 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

theorem Int.Linear.eq_eq_false (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isUnsatEq = 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

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 && decide (k > 0) && 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 (Int.Linear.gcd✝ k' 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 == 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

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 && (k₁ == k * k₂ && p₁ == p₂.mul k))

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₂

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

Equations

• Int.Linear.dvd_elim_cert k₁ (Int.Linear.Poly.add a v p) k₂ p₂ = (k₂ == Int.Linear.gcd✝ k₁ a && p₂ == p)
• Int.Linear.dvd_elim_cert k₁ p₁ k₂ p₂ = false

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₂

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.
• Int.Linear.dvd_solve_combine_cert d₁ p₁ d₂ p₂ d p g α β = false

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

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 == 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 == p₂) = true) : Poly.denote' ctx p₁ ≤ 0 → Poly.denote' ctx p₂ ≤ 0

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

Equations

• Int.Linear.le_coeff_cert p₁ p₂ k = (decide (k > 0) && (Int.Linear.Poly.divCoeffs k p₁ && p₂ == 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

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

Equations

• Int.Linear.le_neg_cert p₁ p₂ = (p₂ == (p₁.mul (-1)).addConst 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_1).leadCoeff = a
• p.leadCoeff = 1

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

Equations

• Int.Linear.le_combine_cert p₁ p₂ p₃ = (p₃ == (p₁.mul ↑p₂.leadCoeff.natAbs).combine (p₂.mul ↑p₁.leadCoeff.natAbs))

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

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 == p₂) = true) : Poly.denote' ctx p₁ = 0 → Poly.denote' ctx p₂ = 0

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

Equations

• Int.Linear.eq_coeff_cert p p' k = (p == p'.mul k && 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

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 && decide (k > 0) && 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

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₂ == Int.Linear.abs✝ (p₁.coeff x) && p₂ == Int.Linear.Poly.insert (-p₁.coeff 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₂

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₃

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₃ == (p₁.mul (p₂.coeff x)).combine (p₂.mul (-p₁.coeff x)))

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

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₃ = (decide (p₁.coeff x ≥ 0) && p₃ == (p₂.mul (p₁.coeff x)).combine (p₁.mul (-p₂.coeff x)))

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

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₃ = (decide (p₁.coeff x ≤ 0) && p₃ == (p₁.mul (p₂.coeff x)).combine (p₂.mul (-p₁.coeff x)))

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

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

Equations

• Int.Linear.eq_of_core_cert p₁ p₂ p₃ = (p₃ == p₁.combine (p₂.mul (-1)))

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

theorem Int.Linear.diseq_norm (ctx : Context) (p₁ p₂ : Poly) (h : (p₁.norm == 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' == 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 = true → Poly.denote' ctx p ≠ 0 → False

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 != 0 && p₃ == (p₁.mul (p₂.coeff x)).combine (p₂.mul (-p₁.coeff x)))

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

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

Equations

• Int.Linear.eq_of_le_ge_cert p₁ p₂ = (p₂ == p₁.mul (-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

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₂ == p₁ || p₂ == p₁.mul (-1)) && p₃ == p₁.addConst 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

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

Equations

• Int.Linear.diseq_split_cert p₁ p₂ p₃ = (p₂ == p₁.addConst 1 && p₃ == (p₁.mul (-1)).addConst 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_unsat {p : Nat → Prop} : ¬OrOver 0 p

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

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_1).tail = p_1
• 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)

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 == b && p' == ((p₁.tail.mul b).combine (p₂.tail.mul (-p₁.leadCoeff))).addConst (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

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 == p₁.leadCoeff && p' == p₁.tail.addConst 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'

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

Equations

• Int.Linear.cooper_dvd_left_split_dvd2_cert p₁ p₃ d k d' p' = (d' == p₁.leadCoeff * d && p' == ((p₁.tail.mul p₃.leadCoeff).combine (p₃.tail.mul (-p₁.leadCoeff))).addConst (p₃.leadCoeff * ↑k))

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'

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

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 == b && p' == ((p₁.tail.mul b).combine (p₂.tail.mul (-p₁.leadCoeff))).addConst (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

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 == p₁.leadCoeff && p' == p₁.tail.addConst 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'

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)

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 == a && p' == ((p₁.tail.mul p₂.leadCoeff).combine (p₂.tail.mul (-a))).addConst (-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

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 == p₂.leadCoeff && p' == p₂.tail.addConst 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'

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

Equations

• Int.Linear.cooper_dvd_right_split_dvd2_cert p₂ p₃ d k d' p' = (d' == p₂.leadCoeff * d && p' == ((p₂.tail.mul (-p₃.leadCoeff)).combine (p₃.tail.mul p₂.leadCoeff)).addConst (-p₃.leadCoeff * ↑k))

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'

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

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 == a && p' == ((p₁.tail.mul p₂.leadCoeff).combine (p₂.tail.mul (-a))).addConst (-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

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 == p₂.leadCoeff && p' == p₂.tail.addConst 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'

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)