Documentation

Init.Omega.LinearCombo

Linear combinations #

We use this data structure while processing hypotheses.

structure Lean.Omega.LinearCombo :

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

const : Int
Constant term.
coeffs : Coeffs
Coefficients of the atoms.

Instances For

instance Lean.Omega.instDecidableEqLinearCombo :

DecidableEq LinearCombo

Equations

Lean.Omega.instDecidableEqLinearCombo = Lean.Omega.decEqLinearCombo✝

instance Lean.Omega.instReprLinearCombo :

Repr LinearCombo

Equations

Lean.Omega.instReprLinearCombo = { reprPrec := Lean.Omega.reprLinearCombo✝ }

instance Lean.Omega.LinearCombo.instToString :

ToString LinearCombo

Equations

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

instance Lean.Omega.LinearCombo.instInhabited :

Inhabited LinearCombo

Equations

Lean.Omega.LinearCombo.instInhabited = { default := { const := 1 } }

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

a = b

def Lean.Omega.LinearCombo.isAtom (a : LinearCombo) :

Check if a linear combination is an atom, i.e. the constant term is zero and there is exactly one nonzero coefficient, which is one.

Equations

a.isAtom = (a.const == 0 && (List.filter (fun (x : Int) => x == 1) a.coeffs).length == 1 && List.all a.coeffs fun (c : Int) => c == 0 || c == 1)

def Lean.Omega.LinearCombo.eval (lc : LinearCombo) (values : Coeffs) :

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

lc.eval values = lc.const + lc.coeffs.dot values

@[simp]

theorem Lean.Omega.LinearCombo.eval_nil {lc : LinearCombo} :

lc.eval [] = lc.const

def Lean.Omega.LinearCombo.coordinate (i : Nat) :

The i-th coordinate function.

Equations

Lean.Omega.LinearCombo.coordinate i = { coeffs := Lean.Omega.Coeffs.set [] i 1 }

@[simp]

theorem Lean.Omega.LinearCombo.coordinate_eval (i : Nat) (v : Coeffs) :

(coordinate i).eval v = v.get i

theorem Lean.Omega.LinearCombo.coordinate_eval_0 {a0 : Int} {t : List Int} :

(coordinate 0).eval (Coeffs.ofList (a0 :: t)) = a0

theorem Lean.Omega.LinearCombo.coordinate_eval_1 {a0 a1 : Int} {t : List Int} :

(coordinate 1).eval (Coeffs.ofList (a0 :: a1 :: t)) = a1

theorem Lean.Omega.LinearCombo.coordinate_eval_2 {a0 a1 a2 : Int} {t : List Int} :

(coordinate 2).eval (Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2

theorem Lean.Omega.LinearCombo.coordinate_eval_3 {a0 a1 a2 a3 : Int} {t : List Int} :

(coordinate 3).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3

theorem Lean.Omega.LinearCombo.coordinate_eval_4 {a0 a1 a2 a3 a4 : Int} {t : List Int} :

(coordinate 4).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4

theorem Lean.Omega.LinearCombo.coordinate_eval_5 {a0 a1 a2 a3 a4 a5 : Int} {t : List Int} :

(coordinate 5).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5

theorem Lean.Omega.LinearCombo.coordinate_eval_6 {a0 a1 a2 a3 a4 a5 a6 : Int} {t : List Int} :

(coordinate 6).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) = a6

theorem Lean.Omega.LinearCombo.coordinate_eval_7 {a0 a1 a2 a3 a4 a5 a6 a7 : Int} {t : List Int} :

(coordinate 7).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) = a7

theorem Lean.Omega.LinearCombo.coordinate_eval_8 {a0 a1 a2 a3 a4 a5 a6 a7 a8 : Int} {t : List Int} :

(coordinate 8).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) = a8

theorem Lean.Omega.LinearCombo.coordinate_eval_9 {a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 : Int} {t : List Int} :

(coordinate 9).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) = a9

def Lean.Omega.LinearCombo.add (l₁ l₂ : LinearCombo) :

Implementation of addition on LinearCombo.

Equations

l₁.add l₂ = { const := l₁.const + l₂.const, coeffs := l₁.coeffs + l₂.coeffs }

instance Lean.Omega.LinearCombo.instAdd :

Add LinearCombo

Equations

Lean.Omega.LinearCombo.instAdd = { add := Lean.Omega.LinearCombo.add }

@[simp]

theorem Lean.Omega.LinearCombo.add_const {l₁ l₂ : LinearCombo} :

(l₁ + l₂).const = l₁.const + l₂.const

@[simp]

theorem Lean.Omega.LinearCombo.add_coeffs {l₁ l₂ : LinearCombo} :

(l₁ + l₂).coeffs = l₁.coeffs + l₂.coeffs

def Lean.Omega.LinearCombo.sub (l₁ l₂ : LinearCombo) :

Implementation of subtraction on LinearCombo.

Equations

l₁.sub l₂ = { const := l₁.const - l₂.const, coeffs := l₁.coeffs - l₂.coeffs }

instance Lean.Omega.LinearCombo.instSub :

Sub LinearCombo

Equations

Lean.Omega.LinearCombo.instSub = { sub := Lean.Omega.LinearCombo.sub }

@[simp]

theorem Lean.Omega.LinearCombo.sub_const {l₁ l₂ : LinearCombo} :

(l₁ - l₂).const = l₁.const - l₂.const

@[simp]

theorem Lean.Omega.LinearCombo.sub_coeffs {l₁ l₂ : LinearCombo} :

(l₁ - l₂).coeffs = l₁.coeffs - l₂.coeffs

def Lean.Omega.LinearCombo.neg (lc : LinearCombo) :

Implementation of negation on LinearCombo.

Equations

lc.neg = { const := -lc.const, coeffs := -lc.coeffs }

instance Lean.Omega.LinearCombo.instNeg :

Neg LinearCombo

Equations

Lean.Omega.LinearCombo.instNeg = { neg := Lean.Omega.LinearCombo.neg }

@[simp]

theorem Lean.Omega.LinearCombo.neg_const {l : LinearCombo} :

(-l).const = -l.const

@[simp]

theorem Lean.Omega.LinearCombo.neg_coeffs {l : LinearCombo} :

(-l).coeffs = -l.coeffs

theorem Lean.Omega.LinearCombo.sub_eq_add_neg (l₁ l₂ : LinearCombo) :

l₁ - l₂ = l₁ + -l₂

def Lean.Omega.LinearCombo.smul (lc : LinearCombo) (i : Int) :

Implementation of scalar multiplication of a LinearCombo by an Int.

Equations

lc.smul i = { const := i * lc.const, coeffs := lc.coeffs.smul i }

instance Lean.Omega.LinearCombo.instHMulInt :

HMul Int LinearCombo LinearCombo

Equations

Lean.Omega.LinearCombo.instHMulInt = { hMul := fun (i : Int) (lc : Lean.Omega.LinearCombo) => lc.smul i }

@[simp]

theorem Lean.Omega.LinearCombo.smul_const {lc : LinearCombo} {i : Int} :

(i * lc).const = i * lc.const

@[simp]

theorem Lean.Omega.LinearCombo.smul_coeffs {lc : LinearCombo} {i : Int} :

(i * lc).coeffs = i * lc.coeffs

@[simp]

theorem Lean.Omega.LinearCombo.add_eval (l₁ l₂ : LinearCombo) (v : Coeffs) :

(l₁ + l₂).eval v = l₁.eval v + l₂.eval v

@[simp]

theorem Lean.Omega.LinearCombo.neg_eval (lc : LinearCombo) (v : Coeffs) :

(-lc).eval v = -lc.eval v

@[simp]

theorem Lean.Omega.LinearCombo.sub_eval (l₁ l₂ : LinearCombo) (v : Coeffs) :

(l₁ - l₂).eval v = l₁.eval v - l₂.eval v

@[simp]

theorem Lean.Omega.LinearCombo.smul_eval (lc : LinearCombo) (i : Int) (v : Coeffs) :

(i * lc).eval v = i * lc.eval v

theorem Lean.Omega.LinearCombo.smul_eval_comm (lc : LinearCombo) (i : Int) (v : Coeffs) :

(i * lc).eval v = lc.eval v * i

def Lean.Omega.LinearCombo.mul (l₁ l₂ : 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

l₁.mul l₂ = l₂.const * l₁ + l₁.const * l₂ - { const := l₁.const * l₂.const }

theorem Lean.Omega.LinearCombo.mul_eval_of_const_left (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero) :

(l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

theorem Lean.Omega.LinearCombo.mul_eval_of_const_right (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₂.coeffs.isZero) :

(l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

theorem Lean.Omega.LinearCombo.mul_eval (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero ∨ l₂.coeffs.isZero) :

(l₁.mul l₂).eval v = l₁.eval v * l₂.eval v