Linear combinations

We use this data structure while processing hypotheses.

structure Std.Tactic.Omega.LinearCombo : Type

Internal representation of a linear combination of atoms, and a constant term.

• const : Int

  Constant term.

• coeffs : Std.Tactic.Omega.Coeffs

  Coefficients of the atoms.

instance Std.Tactic.Omega.instDecidableEqLinearCombo : DecidableEq Std.Tactic.Omega.LinearCombo

Equations

• Std.Tactic.Omega.instDecidableEqLinearCombo = Std.Tactic.Omega.decEqLinearCombo✝

instance Std.Tactic.Omega.instReprLinearCombo : Repr Std.Tactic.Omega.LinearCombo

Equations

• Std.Tactic.Omega.instReprLinearCombo = { reprPrec := Std.Tactic.Omega.reprLinearCombo✝ }

instance Std.Tactic.Omega.LinearCombo.instToStringLinearCombo : ToString Std.Tactic.Omega.LinearCombo

Equations

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

instance Std.Tactic.Omega.LinearCombo.instToExprLinearCombo : Lean.ToExpr Std.Tactic.Omega.LinearCombo

Equations

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

instance Std.Tactic.Omega.LinearCombo.instInhabitedLinearCombo : Inhabited Std.Tactic.Omega.LinearCombo

Equations

• Std.Tactic.Omega.LinearCombo.instInhabitedLinearCombo = { default := { const := 1, coeffs := [] } }

theorem Std.Tactic.Omega.LinearCombo.ext {a : Std.Tactic.Omega.LinearCombo} {b : Std.Tactic.Omega.LinearCombo} (w₁ : a.const = b.const) (w₂ : a.coeffs = b.coeffs) : a = b

def Std.Tactic.Omega.LinearCombo.eval (lc : Std.Tactic.Omega.LinearCombo) (values : Std.Tactic.Omega.Coeffs) : Int

Evaluate a linear combination ⟨r, [c_1, …, c_k]⟩ at values [v_1, …, v_k] to obtain r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0)))).

Equations

• Std.Tactic.Omega.LinearCombo.eval lc values = lc.const + Std.Tactic.Omega.Coeffs.dot lc.coeffs values

@[simp]

theorem Std.Tactic.Omega.LinearCombo.eval_nil {lc : Std.Tactic.Omega.LinearCombo} : Std.Tactic.Omega.LinearCombo.eval lc [] = lc.const

def Std.Tactic.Omega.LinearCombo.coordinate (i : Nat) : Std.Tactic.Omega.LinearCombo

The i-th coordinate function.

Equations

• Std.Tactic.Omega.LinearCombo.coordinate i = { const := 0, coeffs := Std.Tactic.Omega.Coeffs.set [] i 1 }

@[simp]

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval (i : Nat) (v : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate i) v = Std.Tactic.Omega.Coeffs.get v i

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_0 {a0 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 0) (Std.Tactic.Omega.Coeffs.ofList (a0 :: t)) = a0

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_1 {a0 : Int} {a1 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 1) (Std.Tactic.Omega.Coeffs.ofList (a0 :: a1 :: t)) = a1

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_2 {a0 : Int} {a1 : Int} {a2 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 2) (Std.Tactic.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_3 {a0 : Int} {a1 : Int} {a2 : Int} {a3 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 3) (Std.Tactic.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_4 {a0 : Int} {a1 : Int} {a2 : Int} {a3 : Int} {a4 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 4) (Std.Tactic.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_5 {a0 : Int} {a1 : Int} {a2 : Int} {a3 : Int} {a4 : Int} {a5 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 5) (Std.Tactic.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_6 {a0 : Int} {a1 : Int} {a2 : Int} {a3 : Int} {a4 : Int} {a5 : Int} {a6 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 6) (Std.Tactic.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) = a6

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_7 {a0 : Int} {a1 : Int} {a2 : Int} {a3 : Int} {a4 : Int} {a5 : Int} {a6 : Int} {a7 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 7) (Std.Tactic.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) = a7

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_8 {a0 : Int} {a1 : Int} {a2 : Int} {a3 : Int} {a4 : Int} {a5 : Int} {a6 : Int} {a7 : Int} {a8 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 8) (Std.Tactic.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) = a8

theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_9 {a0 : Int} {a1 : Int} {a2 : Int} {a3 : Int} {a4 : Int} {a5 : Int} {a6 : Int} {a7 : Int} {a8 : Int} {a9 : Int} {t : List Int} : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.coordinate 9) (Std.Tactic.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) = a9

def Std.Tactic.Omega.LinearCombo.add (l₁ : Std.Tactic.Omega.LinearCombo) (l₂ : Std.Tactic.Omega.LinearCombo) : Std.Tactic.Omega.LinearCombo

Implementation of addition on LinearCombo.

Equations

• Std.Tactic.Omega.LinearCombo.add l₁ l₂ = { const := l₁.const + l₂.const, coeffs := l₁.coeffs + l₂.coeffs }

instance Std.Tactic.Omega.LinearCombo.instAddLinearCombo : Add Std.Tactic.Omega.LinearCombo

Equations

• Std.Tactic.Omega.LinearCombo.instAddLinearCombo = { add := Std.Tactic.Omega.LinearCombo.add }

@[simp]

theorem Std.Tactic.Omega.LinearCombo.add_const {l₁ : Std.Tactic.Omega.LinearCombo} {l₂ : Std.Tactic.Omega.LinearCombo} : (l₁ + l₂).const = l₁.const + l₂.const

@[simp]

theorem Std.Tactic.Omega.LinearCombo.add_coeffs {l₁ : Std.Tactic.Omega.LinearCombo} {l₂ : Std.Tactic.Omega.LinearCombo} : (l₁ + l₂).coeffs = l₁.coeffs + l₂.coeffs

def Std.Tactic.Omega.LinearCombo.sub (l₁ : Std.Tactic.Omega.LinearCombo) (l₂ : Std.Tactic.Omega.LinearCombo) : Std.Tactic.Omega.LinearCombo

Implementation of subtraction on LinearCombo.

Equations

• Std.Tactic.Omega.LinearCombo.sub l₁ l₂ = { const := l₁.const - l₂.const, coeffs := l₁.coeffs - l₂.coeffs }

instance Std.Tactic.Omega.LinearCombo.instSubLinearCombo : Sub Std.Tactic.Omega.LinearCombo

Equations

• Std.Tactic.Omega.LinearCombo.instSubLinearCombo = { sub := Std.Tactic.Omega.LinearCombo.sub }

@[simp]

theorem Std.Tactic.Omega.LinearCombo.sub_const {l₁ : Std.Tactic.Omega.LinearCombo} {l₂ : Std.Tactic.Omega.LinearCombo} : (l₁ - l₂).const = l₁.const - l₂.const

@[simp]

theorem Std.Tactic.Omega.LinearCombo.sub_coeffs {l₁ : Std.Tactic.Omega.LinearCombo} {l₂ : Std.Tactic.Omega.LinearCombo} : (l₁ - l₂).coeffs = l₁.coeffs - l₂.coeffs

def Std.Tactic.Omega.LinearCombo.neg (lc : Std.Tactic.Omega.LinearCombo) : Std.Tactic.Omega.LinearCombo

Implementation of negation on LinearCombo.

Equations

• Std.Tactic.Omega.LinearCombo.neg lc = { const := -lc.const, coeffs := -lc.coeffs }

instance Std.Tactic.Omega.LinearCombo.instNegLinearCombo : Neg Std.Tactic.Omega.LinearCombo

Equations

• Std.Tactic.Omega.LinearCombo.instNegLinearCombo = { neg := Std.Tactic.Omega.LinearCombo.neg }

@[simp]

theorem Std.Tactic.Omega.LinearCombo.neg_const {l : Std.Tactic.Omega.LinearCombo} : (-l).const = -l.const

@[simp]

theorem Std.Tactic.Omega.LinearCombo.neg_coeffs {l : Std.Tactic.Omega.LinearCombo} : (-l).coeffs = -l.coeffs

theorem Std.Tactic.Omega.LinearCombo.sub_eq_add_neg (l₁ : Std.Tactic.Omega.LinearCombo) (l₂ : Std.Tactic.Omega.LinearCombo) : l₁ - l₂ = l₁ + -l₂

def Std.Tactic.Omega.LinearCombo.smul (lc : Std.Tactic.Omega.LinearCombo) (i : Int) : Std.Tactic.Omega.LinearCombo

Implementation of scalar multiplication of a LinearCombo by an Int.

Equations

• Std.Tactic.Omega.LinearCombo.smul lc i = { const := i * lc.const, coeffs := Std.Tactic.Omega.Coeffs.smul lc.coeffs i }

instance Std.Tactic.Omega.LinearCombo.instHMulIntLinearCombo : HMul Int Std.Tactic.Omega.LinearCombo Std.Tactic.Omega.LinearCombo

Equations

• Std.Tactic.Omega.LinearCombo.instHMulIntLinearCombo = { hMul := fun (i : Int) (lc : Std.Tactic.Omega.LinearCombo) => Std.Tactic.Omega.LinearCombo.smul lc i }

@[simp]

theorem Std.Tactic.Omega.LinearCombo.smul_const {lc : Std.Tactic.Omega.LinearCombo} {i : Int} : (i * lc).const = i * lc.const

@[simp]

theorem Std.Tactic.Omega.LinearCombo.smul_coeffs {lc : Std.Tactic.Omega.LinearCombo} {i : Int} : (i * lc).coeffs = i * lc.coeffs

@[simp]

theorem Std.Tactic.Omega.LinearCombo.add_eval (l₁ : Std.Tactic.Omega.LinearCombo) (l₂ : Std.Tactic.Omega.LinearCombo) (v : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.LinearCombo.eval (l₁ + l₂) v = Std.Tactic.Omega.LinearCombo.eval l₁ v + Std.Tactic.Omega.LinearCombo.eval l₂ v

@[simp]

theorem Std.Tactic.Omega.LinearCombo.neg_eval (lc : Std.Tactic.Omega.LinearCombo) (v : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.LinearCombo.eval (-lc) v = -Std.Tactic.Omega.LinearCombo.eval lc v

@[simp]

theorem Std.Tactic.Omega.LinearCombo.sub_eval (l₁ : Std.Tactic.Omega.LinearCombo) (l₂ : Std.Tactic.Omega.LinearCombo) (v : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.LinearCombo.eval (l₁ - l₂) v = Std.Tactic.Omega.LinearCombo.eval l₁ v - Std.Tactic.Omega.LinearCombo.eval l₂ v

@[simp]

theorem Std.Tactic.Omega.LinearCombo.smul_eval (lc : Std.Tactic.Omega.LinearCombo) (i : Int) (v : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.LinearCombo.eval (i * lc) v = i * Std.Tactic.Omega.LinearCombo.eval lc v

theorem Std.Tactic.Omega.LinearCombo.smul_eval_comm (lc : Std.Tactic.Omega.LinearCombo) (i : Int) (v : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.LinearCombo.eval (i * lc) v = Std.Tactic.Omega.LinearCombo.eval lc v * i

def Std.Tactic.Omega.LinearCombo.mul (l₁ : Std.Tactic.Omega.LinearCombo) (l₂ : Std.Tactic.Omega.LinearCombo) : Std.Tactic.Omega.LinearCombo

Multiplication of two linear combinations. This is useful only if at least one of the linear combinations is constant, and otherwise should be considered as a junk value.

Equations

• Std.Tactic.Omega.LinearCombo.mul l₁ l₂ = l₂.const * l₁ + l₁.const * l₂ - { const := l₁.const * l₂.const, coeffs := [] }

theorem Std.Tactic.Omega.LinearCombo.mul_eval_of_const_left (l₁ : Std.Tactic.Omega.LinearCombo) (l₂ : Std.Tactic.Omega.LinearCombo) (v : Std.Tactic.Omega.Coeffs) (w : Std.Tactic.Omega.Coeffs.isZero l₁.coeffs) : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.mul l₁ l₂) v = Std.Tactic.Omega.LinearCombo.eval l₁ v * Std.Tactic.Omega.LinearCombo.eval l₂ v

theorem Std.Tactic.Omega.LinearCombo.mul_eval_of_const_right (l₁ : Std.Tactic.Omega.LinearCombo) (l₂ : Std.Tactic.Omega.LinearCombo) (v : Std.Tactic.Omega.Coeffs) (w : Std.Tactic.Omega.Coeffs.isZero l₂.coeffs) : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.mul l₁ l₂) v = Std.Tactic.Omega.LinearCombo.eval l₁ v * Std.Tactic.Omega.LinearCombo.eval l₂ v

theorem Std.Tactic.Omega.LinearCombo.mul_eval (l₁ : Std.Tactic.Omega.LinearCombo) (l₂ : Std.Tactic.Omega.LinearCombo) (v : Std.Tactic.Omega.Coeffs) (w : Std.Tactic.Omega.Coeffs.isZero l₁.coeffs ∨ Std.Tactic.Omega.Coeffs.isZero l₂.coeffs) : Std.Tactic.Omega.LinearCombo.eval (Std.Tactic.Omega.LinearCombo.mul l₁ l₂) v = Std.Tactic.Omega.LinearCombo.eval l₁ v * Std.Tactic.Omega.LinearCombo.eval l₂ v