Coeffs as a wrapper for IntList

Currently omega uses a dense representation for coefficients. However, we can swap this out for a sparse representation.

This file sets up Coeffs as a type synonym for IntList, and abbreviations for the functions in the IntList namespace which we need to use in the omega algorithm.

There is an equivalent file setting up Coeffs as a type synonym for AssocList Nat Int, currently in a private branch. Not all the theorems about the algebraic operations on that representation have been proved yet. When they are ready, we can replace the implementation in omega simply by importing Init.Omega.IntDict instead of Init.Omega.IntList.

For small problems, the sparse representation is actually slightly slower, so it is not urgent to make this replacement.

@[reducible, inline]

abbrev Lean.Omega.Coeffs : Type

Type synonym for IntList := List Int.

Equations

• Lean.Omega.Coeffs = Lean.Omega.IntList

@[reducible, inline]

abbrev Lean.Omega.Coeffs.toList (xs : Lean.Omega.Coeffs) : List Int

Identity, turning Coeffs into List Int.

Equations

• xs.toList = xs

@[reducible, inline]

abbrev Lean.Omega.Coeffs.ofList (xs : List Int) : Lean.Omega.Coeffs

Identity, turning List Int into Coeffs.

Equations

• Lean.Omega.Coeffs.ofList xs = xs

@[reducible, inline]

abbrev Lean.Omega.Coeffs.isZero (xs : Lean.Omega.Coeffs) : Prop

Are the coefficients all zero?

Equations

• xs.isZero = ∀ (x : Int), x ∈ xs → x = 0

@[reducible, inline]

abbrev Lean.Omega.Coeffs.set (xs : Lean.Omega.Coeffs) (i : Nat) (y : Int) : Lean.Omega.Coeffs

Shim for IntList.set.

Equations

• xs.set i y = Lean.Omega.IntList.set xs i y

@[reducible, inline]

abbrev Lean.Omega.Coeffs.get (xs : Lean.Omega.Coeffs) (i : Nat) : Int

Shim for IntList.get.

Equations

• xs.get i = Lean.Omega.IntList.get xs i

@[reducible, inline]

abbrev Lean.Omega.Coeffs.gcd (xs : Lean.Omega.Coeffs) : Nat

Shim for IntList.gcd.

Equations

• xs.gcd = Lean.Omega.IntList.gcd xs

@[reducible, inline]

abbrev Lean.Omega.Coeffs.smul (xs : Lean.Omega.Coeffs) (g : Int) : Lean.Omega.Coeffs

Shim for IntList.smul.

Equations

• xs.smul g = Lean.Omega.IntList.smul xs g

@[reducible, inline]

abbrev Lean.Omega.Coeffs.sdiv (xs : Lean.Omega.Coeffs) (g : Int) : Lean.Omega.Coeffs

Shim for IntList.sdiv.

Equations

• xs.sdiv g = Lean.Omega.IntList.sdiv xs g

@[reducible, inline]

abbrev Lean.Omega.Coeffs.dot (xs : Lean.Omega.Coeffs) (ys : Lean.Omega.Coeffs) : Int

Shim for IntList.dot.

Equations

• xs.dot ys = Lean.Omega.IntList.dot xs ys

@[reducible, inline]

abbrev Lean.Omega.Coeffs.add (xs : Lean.Omega.Coeffs) (ys : Lean.Omega.Coeffs) : Lean.Omega.Coeffs

Shim for IntList.add.

Equations

• xs.add ys = Lean.Omega.IntList.add xs ys

@[reducible, inline]

abbrev Lean.Omega.Coeffs.sub (xs : Lean.Omega.Coeffs) (ys : Lean.Omega.Coeffs) : Lean.Omega.Coeffs

Shim for IntList.sub.

Equations

• xs.sub ys = Lean.Omega.IntList.sub xs ys

@[reducible, inline]

abbrev Lean.Omega.Coeffs.neg (xs : Lean.Omega.Coeffs) : Lean.Omega.Coeffs

Shim for IntList.neg.

Equations

• xs.neg = Lean.Omega.IntList.neg xs

@[reducible, inline]

abbrev Lean.Omega.Coeffs.combo (a : Int) (xs : Lean.Omega.Coeffs) (b : Int) (ys : Lean.Omega.Coeffs) : Lean.Omega.Coeffs

Shim for IntList.combo.

Equations

• Lean.Omega.Coeffs.combo a xs b ys = Lean.Omega.IntList.combo a xs b ys

@[reducible, inline]

abbrev Lean.Omega.Coeffs.length (xs : Lean.Omega.Coeffs) : Nat

Shim for List.length.

Equations

• xs.length = List.length xs

@[reducible, inline]

abbrev Lean.Omega.Coeffs.leading (xs : Lean.Omega.Coeffs) : Int

Shim for IntList.leading.

Equations

• xs.leading = Lean.Omega.IntList.leading xs

@[reducible, inline]

abbrev Lean.Omega.Coeffs.map (f : Int → Int) (xs : Lean.Omega.Coeffs) : Lean.Omega.Coeffs

Shim for List.map.

Equations

• Lean.Omega.Coeffs.map f xs = List.map f xs

@[reducible, inline]

abbrev Lean.Omega.Coeffs.findIdx? (f : Int → Bool) (xs : Lean.Omega.Coeffs) : Option Nat

Shim for .enum.find?.

Equations

• Lean.Omega.Coeffs.findIdx? f xs = Option.map (fun (x : Nat × Int) => x.fst) (List.find? (fun (x : Nat × Int) => f x.snd) (List.enum xs))

@[reducible, inline]

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

Shim for IntList.bmod.

Equations

• x.bmod m = Lean.Omega.IntList.bmod x m

@[reducible, inline]

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

Shim for IntList.bmod_dot_sub_dot_bmod.

Equations

• Lean.Omega.Coeffs.bmod_dot_sub_dot_bmod m a b = Lean.Omega.IntList.bmod_dot_sub_dot_bmod m a b

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

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

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

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

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

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

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

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

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

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

theorem Lean.Omega.Coeffs.map_length {f : Int → Int} {xs : Lean.Omega.Coeffs} : (Lean.Omega.Coeffs.map f xs).length ≤ xs.length

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

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

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