Linear combinations #
We use this data structure while processing hypotheses.
Internal representation of a linear combination of atoms, and a constant term.
- const : Int
Constant term.
- coeffs : Lean.Omega.Coeffs
Coefficients of the atoms.
Instances For
- Lean.Elab.Tactic.Omega.instToExprLinearCombo
- Lean.Omega.LinearCombo.instAddLinearCombo
- Lean.Omega.LinearCombo.instHMulIntLinearCombo
- Lean.Omega.LinearCombo.instInhabitedLinearCombo
- Lean.Omega.LinearCombo.instNegLinearCombo
- Lean.Omega.LinearCombo.instSubLinearCombo
- Lean.Omega.LinearCombo.instToStringLinearCombo
- Lean.Omega.instReprLinearCombo
Equations
- Lean.Omega.instReprLinearCombo = { reprPrec := Lean.Omega.reprLinearCombo✝ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Omega.LinearCombo.instInhabitedLinearCombo = { default := { const := 1, coeffs := [] } }
theorem
Lean.Omega.LinearCombo.ext
{a : Lean.Omega.LinearCombo}
{b : Lean.Omega.LinearCombo}
(w₁ : a.const = b.const)
(w₂ : a.coeffs = b.coeffs)
:
a = b
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
- Lean.Omega.LinearCombo.eval lc values = lc.const + Lean.Omega.Coeffs.dot lc.coeffs values
@[simp]
theorem
Lean.Omega.LinearCombo.eval_nil
{lc : Lean.Omega.LinearCombo}
:
Lean.Omega.LinearCombo.eval lc [] = lc.const
The i-th coordinate function.
Equations
- Lean.Omega.LinearCombo.coordinate i = { const := 0, coeffs := Lean.Omega.Coeffs.set [] i 1 }
@[simp]
theorem
Lean.Omega.LinearCombo.coordinate_eval_1
{a0 : Int}
{a1 : Int}
{t : List Int}
:
Lean.Omega.LinearCombo.eval (Lean.Omega.LinearCombo.coordinate 1) (Lean.Omega.Coeffs.ofList (a0 :: a1 :: t)) = a1
theorem
Lean.Omega.LinearCombo.coordinate_eval_2
{a0 : Int}
{a1 : Int}
{a2 : Int}
{t : List Int}
:
Lean.Omega.LinearCombo.eval (Lean.Omega.LinearCombo.coordinate 2) (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2
theorem
Lean.Omega.LinearCombo.coordinate_eval_3
{a0 : Int}
{a1 : Int}
{a2 : Int}
{a3 : Int}
{t : List Int}
:
Lean.Omega.LinearCombo.eval (Lean.Omega.LinearCombo.coordinate 3)
(Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3
theorem
Lean.Omega.LinearCombo.coordinate_eval_4
{a0 : Int}
{a1 : Int}
{a2 : Int}
{a3 : Int}
{a4 : Int}
{t : List Int}
:
Lean.Omega.LinearCombo.eval (Lean.Omega.LinearCombo.coordinate 4)
(Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4
theorem
Lean.Omega.LinearCombo.coordinate_eval_5
{a0 : Int}
{a1 : Int}
{a2 : Int}
{a3 : Int}
{a4 : Int}
{a5 : Int}
{t : List Int}
:
Lean.Omega.LinearCombo.eval (Lean.Omega.LinearCombo.coordinate 5)
(Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5
theorem
Lean.Omega.LinearCombo.coordinate_eval_7
{a0 : Int}
{a1 : Int}
{a2 : Int}
{a3 : Int}
{a4 : Int}
{a5 : Int}
{a6 : Int}
{a7 : Int}
{t : List Int}
:
Lean.Omega.LinearCombo.eval (Lean.Omega.LinearCombo.coordinate 7)
(Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) = a7
theorem
Lean.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}
:
Lean.Omega.LinearCombo.eval (Lean.Omega.LinearCombo.coordinate 8)
(Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) = a8
theorem
Lean.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}
:
Lean.Omega.LinearCombo.eval (Lean.Omega.LinearCombo.coordinate 9)
(Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) = a9
Implementation of addition on LinearCombo.
Equations
- Lean.Omega.LinearCombo.add l₁ l₂ = { const := l₁.const + l₂.const, coeffs := l₁.coeffs + l₂.coeffs }
@[simp]
theorem
Lean.Omega.LinearCombo.add_const
{l₁ : Lean.Omega.LinearCombo}
{l₂ : Lean.Omega.LinearCombo}
:
@[simp]
theorem
Lean.Omega.LinearCombo.add_coeffs
{l₁ : Lean.Omega.LinearCombo}
{l₂ : Lean.Omega.LinearCombo}
:
Implementation of subtraction on LinearCombo.
Equations
- Lean.Omega.LinearCombo.sub l₁ l₂ = { const := l₁.const - l₂.const, coeffs := l₁.coeffs - l₂.coeffs }
@[simp]
theorem
Lean.Omega.LinearCombo.sub_const
{l₁ : Lean.Omega.LinearCombo}
{l₂ : Lean.Omega.LinearCombo}
:
@[simp]
theorem
Lean.Omega.LinearCombo.sub_coeffs
{l₁ : Lean.Omega.LinearCombo}
{l₂ : Lean.Omega.LinearCombo}
:
Implementation of negation on LinearCombo.
Equations
- Lean.Omega.LinearCombo.neg lc = { const := -lc.const, coeffs := -lc.coeffs }
@[simp]
@[simp]
theorem
Lean.Omega.LinearCombo.sub_eq_add_neg
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
:
Implementation of scalar multiplication of a LinearCombo by an Int.
Equations
- Lean.Omega.LinearCombo.smul lc i = { const := i * lc.const, coeffs := Lean.Omega.Coeffs.smul lc.coeffs i }
Equations
- Lean.Omega.LinearCombo.instHMulIntLinearCombo = { hMul := fun (i : Int) (lc : Lean.Omega.LinearCombo) => Lean.Omega.LinearCombo.smul lc i }
@[simp]
@[simp]
@[simp]
theorem
Lean.Omega.LinearCombo.add_eval
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
:
Lean.Omega.LinearCombo.eval (l₁ + l₂) v = Lean.Omega.LinearCombo.eval l₁ v + Lean.Omega.LinearCombo.eval l₂ v
@[simp]
@[simp]
theorem
Lean.Omega.LinearCombo.sub_eval
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
:
Lean.Omega.LinearCombo.eval (l₁ - l₂) v = Lean.Omega.LinearCombo.eval l₁ v - Lean.Omega.LinearCombo.eval l₂ v
@[simp]
theorem
Lean.Omega.LinearCombo.smul_eval
(lc : Lean.Omega.LinearCombo)
(i : Int)
(v : Lean.Omega.Coeffs)
:
Lean.Omega.LinearCombo.eval (i * lc) v = i * Lean.Omega.LinearCombo.eval lc v
theorem
Lean.Omega.LinearCombo.smul_eval_comm
(lc : Lean.Omega.LinearCombo)
(i : Int)
(v : Lean.Omega.Coeffs)
:
Lean.Omega.LinearCombo.eval (i * lc) v = Lean.Omega.LinearCombo.eval lc v * i
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.
theorem
Lean.Omega.LinearCombo.mul_eval_of_const_left
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
(w : Lean.Omega.Coeffs.isZero l₁.coeffs)
:
theorem
Lean.Omega.LinearCombo.mul_eval_of_const_right
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
(w : Lean.Omega.Coeffs.isZero l₂.coeffs)
:
theorem
Lean.Omega.LinearCombo.mul_eval
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
(w : Lean.Omega.Coeffs.isZero l₁.coeffs ∨ Lean.Omega.Coeffs.isZero l₂.coeffs)
: