@[inline, reducible]

abbrev Lean.Omega.IntList : Type

A type synonym for List Int, used by omega for dense representation of coefficients.

We define algebraic operations, interpreting List Int as a finitely supported function Nat → Int.

Equations

• Lean.Omega.IntList = List Int

def Lean.Omega.IntList.get (xs : Lean.Omega.IntList) (i : Nat) : Int

Get the i-th element (interpreted as 0 if the list is not long enough).

Equations

• Lean.Omega.IntList.get xs i = Option.getD (List.get? xs i) 0

@[simp]

theorem Lean.Omega.IntList.get_nil {i : Nat} : Lean.Omega.IntList.get [] i = 0

@[simp]

theorem Lean.Omega.IntList.get_cons_zero {x : Int} {xs : List Int} : Lean.Omega.IntList.get (x :: xs) 0 = x

@[simp]

theorem Lean.Omega.IntList.get_cons_succ {x : Int} {xs : List Int} {i : Nat} : Lean.Omega.IntList.get (x :: xs) (i + 1) = Lean.Omega.IntList.get xs i

theorem Lean.Omega.IntList.get_map {f : Int → Int} {i : Nat} {xs : Lean.Omega.IntList} (h : f 0 = 0) : Lean.Omega.IntList.get (List.map f xs) i = f (Lean.Omega.IntList.get xs i)

theorem Lean.Omega.IntList.get_of_length_le {i : Nat} {xs : Lean.Omega.IntList} (h : List.length xs ≤ i) : Lean.Omega.IntList.get xs i = 0

def Lean.Omega.IntList.set (xs : Lean.Omega.IntList) (i : Nat) (y : Int) : Lean.Omega.IntList

Like List.set, but right-pad with zeroes as necessary first.

Equations

• Lean.Omega.IntList.set [] 0 y = [y]
• Lean.Omega.IntList.set [] (Nat.succ i_2) y = 0 :: Lean.Omega.IntList.set [] i_2 y
• Lean.Omega.IntList.set (head :: xs_2) 0 y = y :: xs_2
• Lean.Omega.IntList.set (x :: xs_2) (Nat.succ i_2) y = x :: Lean.Omega.IntList.set xs_2 i_2 y

@[simp]

theorem Lean.Omega.IntList.set_nil_zero {y : Int} : Lean.Omega.IntList.set [] 0 y = [y]

@[simp]

theorem Lean.Omega.IntList.set_nil_succ {i : Nat} {y : Int} : Lean.Omega.IntList.set [] (i + 1) y = 0 :: Lean.Omega.IntList.set [] i y

@[simp]

theorem Lean.Omega.IntList.set_cons_zero {x : Int} {xs : List Int} {y : Int} : Lean.Omega.IntList.set (x :: xs) 0 y = y :: xs

@[simp]

theorem Lean.Omega.IntList.set_cons_succ {x : Int} {xs : List Int} {i : Nat} {y : Int} : Lean.Omega.IntList.set (x :: xs) (i + 1) y = x :: Lean.Omega.IntList.set xs i y

def Lean.Omega.IntList.leading (xs : Lean.Omega.IntList) : Int

Returns the leading coefficient, i.e. the first non-zero entry.

Equations

• Lean.Omega.IntList.leading xs = Option.getD (List.find? (fun (x : Int) => !x == 0) xs) 0

def Lean.Omega.IntList.add (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : Lean.Omega.IntList

Implementation of + on IntList.

Equations

• Lean.Omega.IntList.add xs ys = List.zipWithAll (fun (x y : Option Int) => Option.getD x 0 + Option.getD y 0) xs ys

instance Lean.Omega.IntList.instAddIntList : Add Lean.Omega.IntList

Equations

• Lean.Omega.IntList.instAddIntList = { add := Lean.Omega.IntList.add }

theorem Lean.Omega.IntList.add_def (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : xs + ys = List.zipWithAll (fun (x y : Option Int) => Option.getD x 0 + Option.getD y 0) xs ys

@[simp]

theorem Lean.Omega.IntList.add_get (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Nat) : Lean.Omega.IntList.get (xs + ys) i = Lean.Omega.IntList.get xs i + Lean.Omega.IntList.get ys i

@[simp]

theorem Lean.Omega.IntList.add_nil (xs : Lean.Omega.IntList) : xs + [] = xs

@[simp]

theorem Lean.Omega.IntList.nil_add (xs : Lean.Omega.IntList) : [] + xs = xs

@[simp]

theorem Lean.Omega.IntList.cons_add_cons (x : Int) (xs : Lean.Omega.IntList) (y : Int) (ys : Lean.Omega.IntList) : x :: xs + y :: ys = (x + y) :: (xs + ys)

def Lean.Omega.IntList.mul (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : Lean.Omega.IntList

Implementation of * on IntList.

Equations

• Lean.Omega.IntList.mul xs ys = List.zipWith (fun (x x_1 : Int) => x * x_1) xs ys

instance Lean.Omega.IntList.instMulIntList : Mul Lean.Omega.IntList

Equations

• Lean.Omega.IntList.instMulIntList = { mul := Lean.Omega.IntList.mul }

theorem Lean.Omega.IntList.mul_def (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : xs * ys = List.zipWith (fun (x x_1 : Int) => x * x_1) xs ys

@[simp]

theorem Lean.Omega.IntList.mul_get (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Nat) : Lean.Omega.IntList.get (xs * ys) i = Lean.Omega.IntList.get xs i * Lean.Omega.IntList.get ys i

@[simp]

theorem Lean.Omega.IntList.mul_nil_left {ys : List Int} : [] * ys = []

@[simp]

theorem Lean.Omega.IntList.mul_nil_right {xs : List Int} : xs * [] = []

@[simp]

theorem Lean.Omega.IntList.mul_cons₂ {x : Int} {xs : List Int} {y : Int} {ys : List Int} : (x :: xs) * (y :: ys) = x * y :: xs * ys

def Lean.Omega.IntList.neg (xs : Lean.Omega.IntList) : Lean.Omega.IntList

Implementation of negation on IntList.

Equations

• Lean.Omega.IntList.neg xs = List.map (fun (x : Int) => -x) xs

instance Lean.Omega.IntList.instNegIntList : Neg Lean.Omega.IntList

Equations

• Lean.Omega.IntList.instNegIntList = { neg := Lean.Omega.IntList.neg }

theorem Lean.Omega.IntList.neg_def (xs : Lean.Omega.IntList) : -xs = List.map (fun (x : Int) => -x) xs

@[simp]

theorem Lean.Omega.IntList.neg_get (xs : Lean.Omega.IntList) (i : Nat) : Lean.Omega.IntList.get (-xs) i = -Lean.Omega.IntList.get xs i

@[simp]

theorem Lean.Omega.IntList.neg_nil : -[] = []

@[simp]

theorem Lean.Omega.IntList.neg_cons {x : Int} {xs : List Int} : -(x :: xs) = -x :: -xs

def Lean.Omega.IntList.sub (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : Lean.Omega.IntList

Implementation of subtraction on IntList.

Equations

• Lean.Omega.IntList.sub xs ys = List.zipWithAll (fun (x y : Option Int) => Option.getD x 0 - Option.getD y 0) xs ys

instance Lean.Omega.IntList.instSubIntList : Sub Lean.Omega.IntList

Equations

• Lean.Omega.IntList.instSubIntList = { sub := Lean.Omega.IntList.sub }

theorem Lean.Omega.IntList.sub_def (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : xs - ys = List.zipWithAll (fun (x y : Option Int) => Option.getD x 0 - Option.getD y 0) xs ys

def Lean.Omega.IntList.smul (xs : Lean.Omega.IntList) (i : Int) : Lean.Omega.IntList

Implementation of scalar multiplication by an integer on IntList.

Equations

• Lean.Omega.IntList.smul xs i = List.map (fun (x : Int) => i * x) xs

instance Lean.Omega.IntList.instHMulIntIntList : HMul Int Lean.Omega.IntList Lean.Omega.IntList

Equations

• Lean.Omega.IntList.instHMulIntIntList = { hMul := fun (i : Int) (xs : Lean.Omega.IntList) => Lean.Omega.IntList.smul xs i }

theorem Lean.Omega.IntList.smul_def (xs : Lean.Omega.IntList) (i : Int) : i * xs = List.map (fun (x : Int) => i * x) xs

@[simp]

theorem Lean.Omega.IntList.smul_get (xs : Lean.Omega.IntList) (a : Int) (i : Nat) : Lean.Omega.IntList.get (a * xs) i = a * Lean.Omega.IntList.get xs i

@[simp]

theorem Lean.Omega.IntList.smul_nil {i : Int} : i * [] = []

@[simp]

theorem Lean.Omega.IntList.smul_cons {x : Int} {xs : List Int} {i : Int} : i * (x :: xs) = i * x :: i * xs

def Lean.Omega.IntList.combo (a : Int) (xs : Lean.Omega.IntList) (b : Int) (ys : Lean.Omega.IntList) : Lean.Omega.IntList

A linear combination of two IntLists.

Equations

• Lean.Omega.IntList.combo a xs b ys = List.zipWithAll (fun (x y : Option Int) => a * Option.getD x 0 + b * Option.getD y 0) xs ys

theorem Lean.Omega.IntList.combo_eq_smul_add_smul (a : Int) (xs : Lean.Omega.IntList) (b : Int) (ys : Lean.Omega.IntList) : Lean.Omega.IntList.combo a xs b ys = a * xs + b * ys

theorem Lean.Omega.IntList.mul_distrib_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (zs : Lean.Omega.IntList) : (xs + ys) * zs = xs * zs + ys * zs

theorem Lean.Omega.IntList.mul_neg_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : -xs * ys = -(xs * ys)

theorem Lean.Omega.IntList.sub_eq_add_neg (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : xs - ys = xs + -ys

@[simp]

theorem Lean.Omega.IntList.mul_smul_left {i : Int} {xs : Lean.Omega.IntList} {ys : Lean.Omega.IntList} : i * xs * ys = i * (xs * ys)

def Lean.Omega.IntList.sum (xs : Lean.Omega.IntList) : Int

The sum of the entries of an IntList.

Equations

• Lean.Omega.IntList.sum xs = List.foldr (fun (x x_1 : Int) => x + x_1) 0 xs

@[simp]

theorem Lean.Omega.IntList.sum_nil : Lean.Omega.IntList.sum [] = 0

@[simp]

theorem Lean.Omega.IntList.sum_cons {x : Int} {xs : List Int} : Lean.Omega.IntList.sum (x :: xs) = x + Lean.Omega.IntList.sum xs

theorem Lean.Omega.IntList.sum_add (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : Lean.Omega.IntList.sum (xs + ys) = Lean.Omega.IntList.sum xs + Lean.Omega.IntList.sum ys

@[simp]

theorem Lean.Omega.IntList.sum_neg (xs : Lean.Omega.IntList) : Lean.Omega.IntList.sum (-xs) = -Lean.Omega.IntList.sum xs

@[simp]

theorem Lean.Omega.IntList.sum_smul (i : Int) (xs : Lean.Omega.IntList) : Lean.Omega.IntList.sum (i * xs) = i * Lean.Omega.IntList.sum xs

def Lean.Omega.IntList.dot (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : Int

The dot product of two IntLists.

Equations

• Lean.Omega.IntList.dot xs ys = Lean.Omega.IntList.sum (xs * ys)

theorem Lean.Omega.IntList.dot_nil_left {ys : Lean.Omega.IntList} : Lean.Omega.IntList.dot [] ys = 0

@[simp]

theorem Lean.Omega.IntList.dot_nil_right {xs : Lean.Omega.IntList} : Lean.Omega.IntList.dot xs [] = 0

@[simp]

theorem Lean.Omega.IntList.dot_cons₂ {x : Int} {xs : List Int} {y : Int} {ys : List Int} : Lean.Omega.IntList.dot (x :: xs) (y :: ys) = x * y + Lean.Omega.IntList.dot xs ys

@[simp]

theorem Lean.Omega.IntList.dot_set_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Nat) (z : Int) : Lean.Omega.IntList.dot (Lean.Omega.IntList.set xs i z) ys = Lean.Omega.IntList.dot xs ys + (z - Lean.Omega.IntList.get xs i) * Lean.Omega.IntList.get ys i

theorem Lean.Omega.IntList.dot_distrib_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (zs : Lean.Omega.IntList) : Lean.Omega.IntList.dot (xs + ys) zs = Lean.Omega.IntList.dot xs zs + Lean.Omega.IntList.dot ys zs

@[simp]

theorem Lean.Omega.IntList.dot_neg_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : Lean.Omega.IntList.dot (-xs) ys = -Lean.Omega.IntList.dot xs ys

@[simp]

theorem Lean.Omega.IntList.dot_smul_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Int) : Lean.Omega.IntList.dot (i * xs) ys = i * Lean.Omega.IntList.dot xs ys

theorem Lean.Omega.IntList.dot_of_left_zero {xs : Lean.Omega.IntList} {ys : Lean.Omega.IntList} (w : ∀ (x : Int), x ∈ xs → x = 0) : Lean.Omega.IntList.dot xs ys = 0

def Lean.Omega.IntList.sdiv (xs : Lean.Omega.IntList) (g : Int) : Lean.Omega.IntList

Division of an IntList by a integer.

Equations

• Lean.Omega.IntList.sdiv xs g = List.map (fun (x : Int) => x / g) xs

@[simp]

theorem Lean.Omega.IntList.sdiv_nil {g : Int} : Lean.Omega.IntList.sdiv [] g = []

@[simp]

theorem Lean.Omega.IntList.sdiv_cons {x : Int} {xs : List Int} {g : Int} : Lean.Omega.IntList.sdiv (x :: xs) g = x / g :: Lean.Omega.IntList.sdiv xs g

def Lean.Omega.IntList.gcd (xs : Lean.Omega.IntList) : Nat

The gcd of the absolute values of the entries of an IntList.

Equations

• Lean.Omega.IntList.gcd xs = List.foldr (fun (x : Int) (g : Nat) => Nat.gcd (Int.natAbs x) g) 0 xs

@[simp]

theorem Lean.Omega.IntList.gcd_nil : Lean.Omega.IntList.gcd [] = 0

@[simp]

theorem Lean.Omega.IntList.gcd_cons {x : Int} {xs : List Int} : Lean.Omega.IntList.gcd (x :: xs) = Nat.gcd (Int.natAbs x) (Lean.Omega.IntList.gcd xs)

theorem Lean.Omega.IntList.gcd_cons_div_left {x : Int} {xs : List Int} : ↑(Lean.Omega.IntList.gcd (x :: xs)) ∣ x

theorem Lean.Omega.IntList.gcd_cons_div_right {x : Int} {xs : List Int} : Lean.Omega.IntList.gcd (x :: xs) ∣ Lean.Omega.IntList.gcd xs

theorem Lean.Omega.IntList.gcd_cons_div_right' {x : Int} {xs : List Int} : ↑(Lean.Omega.IntList.gcd (x :: xs)) ∣ ↑(Lean.Omega.IntList.gcd xs)

theorem Lean.Omega.IntList.gcd_dvd (xs : Lean.Omega.IntList) {a : Int} (m : a ∈ xs) : ↑(Lean.Omega.IntList.gcd xs) ∣ a

theorem Lean.Omega.IntList.dvd_gcd (xs : Lean.Omega.IntList) (c : Nat) (w : ∀ {a : Int}, a ∈ xs → ↑c ∣ a) : c ∣ Lean.Omega.IntList.gcd xs

theorem Lean.Omega.IntList.gcd_eq_iff (xs : Lean.Omega.IntList) (g : Nat) : Lean.Omega.IntList.gcd xs = g ↔ (∀ {a : Int}, a ∈ xs → ↑g ∣ a) ∧ ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g

@[simp]

theorem Lean.Omega.IntList.gcd_eq_zero (xs : Lean.Omega.IntList) : Lean.Omega.IntList.gcd xs = 0 ↔ ∀ (x : Int), x ∈ xs → x = 0

@[simp]

theorem Lean.Omega.IntList.dot_mod_gcd_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : Lean.Omega.IntList.dot xs ys % ↑(Lean.Omega.IntList.gcd xs) = 0

theorem Lean.Omega.IntList.gcd_dvd_dot_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : ↑(Lean.Omega.IntList.gcd xs) ∣ Lean.Omega.IntList.dot xs ys

@[simp]

theorem Lean.Omega.IntList.dot_eq_zero_of_left_eq_zero {xs : Lean.Omega.IntList} {ys : Lean.Omega.IntList} (h : ∀ (x : Int), x ∈ xs → x = 0) : Lean.Omega.IntList.dot xs ys = 0

theorem Lean.Omega.IntList.dot_sdiv_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) {d : Int} (h : d ∣ ↑(Lean.Omega.IntList.gcd xs)) : Lean.Omega.IntList.dot (Lean.Omega.IntList.sdiv xs d) ys = Lean.Omega.IntList.dot xs ys / d

@[inline, reducible]

abbrev Lean.Omega.IntList.bmod (x : Lean.Omega.IntList) (m : Nat) : Lean.Omega.IntList

Apply "balanced mod" to each entry in an IntList.

Equations

• Lean.Omega.IntList.bmod x m = List.map (fun (x : Int) => Int.bmod x m) x

theorem Lean.Omega.IntList.bmod_length (x : Lean.Omega.IntList) (m : Nat) : List.length (Lean.Omega.IntList.bmod x m) ≤ List.length x

@[inline, reducible]

abbrev Lean.Omega.IntList.bmod_dot_sub_dot_bmod (m : Nat) (a : Lean.Omega.IntList) (b : Lean.Omega.IntList) : Int

The difference between the balanced mod of a dot product, and the dot product with balanced mod applied to each entry of the left factor.

Equations

• Lean.Omega.IntList.bmod_dot_sub_dot_bmod m a b = Int.bmod (Lean.Omega.IntList.dot a b) m - Lean.Omega.IntList.dot (Lean.Omega.IntList.bmod a m) b

theorem Lean.Omega.IntList.dvd_bmod_dot_sub_dot_bmod (m : Nat) (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) : ↑m ∣ Lean.Omega.IntList.bmod_dot_sub_dot_bmod m xs ys