@[inline, reducible]

abbrev 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

• IntList = List Int

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem IntList.lt_length_of_get_nonzero {i : Nat} {xs : IntList} (h : IntList.get xs i ≠ 0) : i < List.length xs

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem IntList.set_get_eq {xs : IntList} {i : Nat} {y : Int} {j : Nat} : IntList.get (IntList.set xs i y) j = if i = j then y else IntList.get xs j

@[simp]

theorem IntList.set_get_self {xs : IntList} {i : Nat} {y : Int} : IntList.get (IntList.set xs i y) i = y

@[simp]

theorem IntList.set_get_of_ne {i : Nat} {j : Nat} {xs : IntList} {y : Int} (h : i ≠ j) : IntList.get (IntList.set xs i y) j = IntList.get xs j

def IntList.leading (xs : IntList) : Int

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

Equations

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

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

Implementation of + on IntList.

Equations

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

instance IntList.instAddIntList : Add IntList

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Implementation of * on IntList.

Equations

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

instance IntList.instMulIntList : Mul IntList

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def IntList.neg (xs : IntList) : IntList

Implementation of negation on IntList.

Equations

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

instance IntList.instNegIntList : Neg IntList

Equations

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

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

@[simp]

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

@[simp]

theorem IntList.neg_nil : -[] = []

@[simp]

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

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

Implementation of subtraction on IntList.

Equations

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

instance IntList.instSubIntList : Sub IntList

Equations

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

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

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

Implementation of scalar multiplication by an integer on IntList.

Equations

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

instance IntList.instHMulIntIntList : HMul Int IntList IntList

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A linear combination of two IntLists.

Equations

• 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 IntList.combo_def {a : Int} {b : Int} (xs : IntList) (ys : IntList) : 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

@[simp]

theorem IntList.combo_get {a : Int} {b : Int} (xs : IntList) (ys : IntList) (i : Nat) : IntList.get (IntList.combo a xs b ys) i = a * IntList.get xs i + b * IntList.get ys i

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

theorem IntList.mul_comm (xs : IntList) (ys : IntList) : xs * ys = ys * xs

@[simp]

theorem IntList.neg_neg {xs : IntList} : - -xs = xs

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

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

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

@[simp]

theorem IntList.sub_get (xs : IntList) (ys : IntList) (i : Nat) : IntList.get (xs - ys) i = IntList.get xs i - IntList.get ys i

@[simp]

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

def IntList.sum (xs : IntList) : Int

The sum of the entries of an IntList.

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

The dot product of two IntLists.

Equations

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

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

@[simp]

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

@[simp]

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

theorem IntList.dot_comm (xs : IntList) (ys : IntList) : IntList.dot xs ys = IntList.dot ys xs

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem IntList.dot_sub_left (xs : IntList) (ys : IntList) (zs : IntList) : IntList.dot (xs - ys) zs = IntList.dot xs zs - IntList.dot ys zs

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

theorem IntList.dvd_dot_of_dvd_left {xs : IntList} {m : Int} {ys : IntList} (w : ∀ (x : Int), x ∈ xs → m ∣ x) : m ∣ IntList.dot xs ys

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

Division of an IntList by a integer.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem IntList.sdiv_get {xs : IntList} {g : Int} {i : Nat} : IntList.get (IntList.sdiv xs g) i = IntList.get xs i / g

theorem IntList.mem_sdiv {x : Int} {g : Int} {xs : IntList} (h : x ∈ xs) : x / g ∈ IntList.sdiv xs g

def IntList.gcd (xs : IntList) : Nat

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem IntList.dot_eq_zero_of_gcd_left_eq_zero {xs : IntList} {ys : IntList} (h : IntList.gcd xs = 0) : IntList.dot xs ys = 0

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

@[simp]

theorem IntList.dot_sdiv_gcd_left (xs : IntList) (ys : IntList) : IntList.dot (IntList.sdiv xs ↑(IntList.gcd xs)) ys = IntList.dot xs ys / ↑(IntList.gcd xs)

def IntList.leadingSign (xs : IntList) : Int

The leading sign in an IntList.

Equations

• IntList.leadingSign [] = 0
• IntList.leadingSign (Int.ofNat 0 :: xs_2) = IntList.leadingSign xs_2
• IntList.leadingSign (x :: tail) = Int.sign x

@[simp]

theorem IntList.leadingSign_nil : IntList.leadingSign [] = 0

@[simp]

theorem IntList.leadingSign_cons_zero {xs : List Int} : IntList.leadingSign (0 :: xs) = IntList.leadingSign xs

theorem IntList.leadingSign_cons {x : Int} {xs : List Int} : IntList.leadingSign (x :: xs) = if x = 0 then IntList.leadingSign xs else Int.sign x

theorem IntList.leadingSign_neg {xs : IntList} : IntList.leadingSign (-xs) = -IntList.leadingSign xs

def IntList.trim? (xs : IntList) : Option IntList

Trim trailing zeroes from a List Int, returning none if none were removed.

Equations

• IntList.trim? xs = match List.reverse xs with | [] => none | Int.ofNat 0 :: xs => some (List.reverse (List.dropWhile (fun (x : Int) => x == 0) xs)) | head :: tail => none

theorem IntList.trim?_isSome {xs : IntList} : (Option.isSome (IntList.trim? xs) = true) = (List.getLast? xs = some 0)

def IntList.trim (xs : IntList) : IntList

Trailing trailing zeroes from a List Int.

Equations

• IntList.trim xs = Option.getD (IntList.trim? xs) xs

theorem IntList.trim?_eq_some {t : IntList} {xs : IntList} (w : IntList.trim? xs = some t) : IntList.trim xs = t

theorem IntList.trim_spec {xs : IntList} : IntList.trim xs = List.reverse (List.dropWhile (fun (x : Int) => x == 0) (List.reverse xs))

@[simp]

theorem IntList.trim_nil : IntList.trim [] = []

@[simp]

theorem IntList.trim_append_zero {xs : IntList} : IntList.trim (xs ++ [0]) = IntList.trim xs

@[simp]

theorem IntList.trim_neg {xs : IntList} : IntList.trim (-xs) = -IntList.trim xs

@[inline, reducible]

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

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

Equations

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

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

@[inline, reducible]

abbrev IntList.bmod_dot_sub_dot_bmod (m : Nat) (a : IntList) (b : 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

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

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