@[reducible, inline]

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

• xs.get i = (List.get? xs i).getD 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 (xs.get i)

theorem Lean.Omega.IntList.get_of_length_le {i : Nat} {xs : Lean.Omega.IntList} (h : List.length xs ≤ i) : xs.get 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 [] i_2.succ 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) i_2.succ 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

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

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

Implementation of + on IntList.

Equations

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

instance Lean.Omega.IntList.instAdd : Add Lean.Omega.IntList

Equations

• Lean.Omega.IntList.instAdd = { 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) => x.getD 0 + y.getD 0) xs ys

@[simp]

theorem Lean.Omega.IntList.add_get (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Nat) : (xs + ys).get i = xs.get i + ys.get 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

• xs.mul ys = List.zipWith (fun (x1 x2 : Int) => x1 * x2) xs ys

instance Lean.Omega.IntList.instMul : Mul Lean.Omega.IntList

Equations

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

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

@[simp]

theorem Lean.Omega.IntList.mul_get (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Nat) : (xs * ys).get i = xs.get i * ys.get 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

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

instance Lean.Omega.IntList.instNeg : Neg Lean.Omega.IntList

Equations

• Lean.Omega.IntList.instNeg = { 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) : (-xs).get i = -xs.get 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

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

instance Lean.Omega.IntList.instSub : Sub Lean.Omega.IntList

Equations

• Lean.Omega.IntList.instSub = { 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) => x.getD 0 - y.getD 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

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

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

Equations

• Lean.Omega.IntList.instHMulInt = { hMul := fun (i : Int) (xs : Lean.Omega.IntList) => xs.smul 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) : (a * xs).get i = a * xs.get 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 * x.getD 0 + b * y.getD 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

• xs.sum = List.foldr (fun (x1 x2 : Int) => x1 + x2) 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) : (xs + ys).sum = xs.sum + ys.sum

@[simp]

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

@[simp]

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

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

The dot product of two IntLists.

Equations

• xs.dot ys = (xs * ys).sum

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} : xs.dot [] = 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) : (xs.set i z).dot ys = xs.dot ys + (z - xs.get i) * ys.get i

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

@[simp]

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

@[simp]

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

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

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

Division of an IntList by a integer.

Equations

• xs.sdiv 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

• xs.gcd = List.foldr (fun (x : Int) (g : Nat) => x.natAbs.gcd 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) = x.natAbs.gcd (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) : ↑xs.gcd ∣ a

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

theorem Lean.Omega.IntList.gcd_eq_iff (xs : Lean.Omega.IntList) (g : Nat) : xs.gcd = 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) : xs.gcd = 0 ↔ ∀ (x : Int), x ∈ xs → x = 0

@[simp]

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

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

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) : xs.dot ys = 0

@[simp]

theorem Lean.Omega.IntList.nil_dot (xs : Lean.Omega.IntList) : Lean.Omega.IntList.dot [] xs = 0

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

@[reducible, inline]

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

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

Equations

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

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

@[reducible, inline]

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 = (a.dot b).bmod m - (a.bmod m).dot 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