Documentation

Init.Omega.IntList

@[reducible, inline]

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 NatInt.

Equations
Instances For

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

Equations
@[simp]
theorem Lean.Omega.IntList.get_nil {i : Nat} :
get [] i = 0
@[simp]
theorem Lean.Omega.IntList.get_cons_zero {x : Int} {xs : List Int} :
get (x :: xs) 0 = x
@[simp]
theorem Lean.Omega.IntList.get_cons_succ {x : Int} {xs : List Int} {i : Nat} :
get (x :: xs) (i + 1) = get xs i
theorem Lean.Omega.IntList.get_map {f : IntInt} {i : Nat} {xs : IntList} (h : f 0 = 0) :
get (List.map f xs) i = f (xs.get i)
theorem Lean.Omega.IntList.get_of_length_le {i : Nat} {xs : IntList} (h : List.length xs i) :
xs.get i = 0
def Lean.Omega.IntList.set (xs : IntList) (i : Nat) (y : Int) :

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

Equations
@[simp]
theorem Lean.Omega.IntList.set_nil_zero {y : Int} :
set [] 0 y = [y]
@[simp]
theorem Lean.Omega.IntList.set_nil_succ {i : Nat} {y : Int} :
set [] (i + 1) y = 0 :: set [] i y
@[simp]
theorem Lean.Omega.IntList.set_cons_zero {x : Int} {xs : List Int} {y : Int} :
set (x :: xs) 0 y = y :: xs
@[simp]
theorem Lean.Omega.IntList.set_cons_succ {x : Int} {xs : List Int} {i : Nat} {y : Int} :
set (x :: xs) (i + 1) y = x :: set xs i y

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

Equations

Implementation of + on IntList.

Equations
theorem Lean.Omega.IntList.add_def (xs ys : 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 ys : IntList) (i : Nat) :
(xs + ys).get i = xs.get i + ys.get i
@[simp]
theorem Lean.Omega.IntList.add_nil (xs : IntList) :
xs + [] = xs
@[simp]
theorem Lean.Omega.IntList.nil_add (xs : IntList) :
[] + xs = xs
@[simp]
theorem Lean.Omega.IntList.cons_add_cons (x : Int) (xs : IntList) (y : Int) (ys : IntList) :
x :: xs + y :: ys = (x + y) :: (xs + ys)

Implementation of * on IntList.

Equations
theorem Lean.Omega.IntList.mul_def (xs ys : IntList) :
xs * ys = List.zipWith (fun (x1 x2 : Int) => x1 * x2) xs ys
@[simp]
theorem Lean.Omega.IntList.mul_get (xs ys : 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

Implementation of negation on IntList.

Equations
theorem Lean.Omega.IntList.neg_def (xs : IntList) :
-xs = List.map (fun (x : Int) => -x) xs
@[simp]
theorem Lean.Omega.IntList.neg_get (xs : IntList) (i : Nat) :
(-xs).get i = -xs.get i
@[simp]
@[simp]
theorem Lean.Omega.IntList.neg_cons {x : Int} {xs : List Int} :
-(x :: xs) = -x :: -xs

Implementation of subtraction on IntList.

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

Implementation of scalar multiplication by an integer on IntList.

Equations
theorem Lean.Omega.IntList.smul_def (xs : IntList) (i : Int) :
i * xs = List.map (fun (x : Int) => i * x) xs
@[simp]
theorem Lean.Omega.IntList.smul_get (xs : 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 : IntList) (b : Int) (ys : IntList) :

A linear combination of two IntLists.

Equations
theorem Lean.Omega.IntList.combo_eq_smul_add_smul (a : Int) (xs : IntList) (b : Int) (ys : IntList) :
combo a xs b ys = a * xs + b * ys
theorem Lean.Omega.IntList.mul_distrib_left (xs ys zs : IntList) :
(xs + ys) * zs = xs * zs + ys * zs
theorem Lean.Omega.IntList.mul_neg_left (xs ys : IntList) :
-xs * ys = -(xs * ys)
theorem Lean.Omega.IntList.sub_eq_add_neg (xs ys : IntList) :
xs - ys = xs + -ys
@[simp]
theorem Lean.Omega.IntList.mul_smul_left {i : Int} {xs ys : IntList} :
i * xs * ys = i * (xs * ys)

The sum of the entries of an IntList.

Equations
@[simp]
@[simp]
theorem Lean.Omega.IntList.sum_cons {x : Int} {xs : List Int} :
sum (x :: xs) = x + sum xs
theorem Lean.Omega.IntList.sum_add (xs ys : IntList) :
(xs + ys).sum = xs.sum + ys.sum
@[simp]
theorem Lean.Omega.IntList.sum_neg (xs : IntList) :
(-xs).sum = -xs.sum
@[simp]
theorem Lean.Omega.IntList.sum_smul (i : Int) (xs : IntList) :
(i * xs).sum = i * xs.sum

The dot product of two IntLists.

Equations
  • xs.dot ys = (xs * ys).sum
@[simp]
theorem Lean.Omega.IntList.dot_nil_right {xs : IntList} :
xs.dot [] = 0
@[simp]
theorem Lean.Omega.IntList.dot_cons₂ {x : Int} {xs : List Int} {y : Int} {ys : List Int} :
dot (x :: xs) (y :: ys) = x * y + dot xs ys
@[simp]
theorem Lean.Omega.IntList.dot_set_left (xs ys : 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 ys zs : IntList) :
(xs + ys).dot zs = xs.dot zs + ys.dot zs
@[simp]
theorem Lean.Omega.IntList.dot_neg_left (xs ys : IntList) :
(-xs).dot ys = -xs.dot ys
@[simp]
theorem Lean.Omega.IntList.dot_smul_left (xs ys : IntList) (i : Int) :
(i * xs).dot ys = i * xs.dot ys
theorem Lean.Omega.IntList.dot_of_left_zero {xs ys : IntList} (w : ∀ (x : Int), x xsx = 0) :
xs.dot ys = 0

Division of an IntList by a integer.

Equations
@[simp]
theorem Lean.Omega.IntList.sdiv_nil {g : Int} :
sdiv [] g = []
@[simp]
theorem Lean.Omega.IntList.sdiv_cons {x : Int} {xs : List Int} {g : Int} :
sdiv (x :: xs) g = x / g :: sdiv xs g

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

Equations
@[simp]
@[simp]
theorem Lean.Omega.IntList.gcd_cons {x : Int} {xs : List Int} :
gcd (x :: xs) = x.natAbs.gcd (gcd xs)
theorem Lean.Omega.IntList.gcd_cons_div_left {x : Int} {xs : List Int} :
(gcd (x :: xs)) x
theorem Lean.Omega.IntList.gcd_cons_div_right' {x : Int} {xs : List Int} :
(gcd (x :: xs)) (gcd xs)
theorem Lean.Omega.IntList.gcd_dvd (xs : IntList) {a : Int} (m : a xs) :
xs.gcd a
theorem Lean.Omega.IntList.dvd_gcd (xs : IntList) (c : Nat) (w : ∀ {a : Int}, a xsc a) :
c xs.gcd
theorem Lean.Omega.IntList.gcd_eq_iff {xs : IntList} {g : Nat} :
xs.gcd = g (∀ {a : Int}, a xsg a) ∀ (c : Nat), (∀ {a : Int}, a xsc a)c g
@[simp]
theorem Lean.Omega.IntList.gcd_eq_zero {xs : IntList} :
xs.gcd = 0 ∀ (x : Int), x xsx = 0
@[simp]
theorem Lean.Omega.IntList.dot_mod_gcd_left (xs ys : IntList) :
xs.dot ys % xs.gcd = 0
theorem Lean.Omega.IntList.gcd_dvd_dot_left (xs ys : IntList) :
xs.gcd xs.dot ys
theorem Lean.Omega.IntList.dot_eq_zero_of_left_eq_zero {xs ys : IntList} (h : ∀ (x : Int), x xsx = 0) :
xs.dot ys = 0
@[simp]
theorem Lean.Omega.IntList.nil_dot (xs : IntList) :
dot [] xs = 0
theorem Lean.Omega.IntList.dot_sdiv_left (xs ys : IntList) {d : Int} (h : d xs.gcd) :
(xs.sdiv d).dot ys = xs.dot ys / d
@[reducible, inline]

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

Equations
@[reducible, inline]

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