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.

@[inline, reducible]

abbrev Lean.Omega.Coeffs : Type

Type synonym for IntList := List Int.

Equations

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

@[inline, reducible]

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

Identity, turning Coeffs into List Int.

Equations

• Lean.Omega.Coeffs.toList xs = xs

@[inline, reducible]

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

Identity, turning List Int into Coeffs.

Equations

• Lean.Omega.Coeffs.ofList xs = xs

@[inline, reducible]

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

Are the coefficients all zero?

Equations

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

@[inline, reducible]

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

Shim for IntList.set.

Equations

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

@[inline, reducible]

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

Shim for IntList.get.

Equations

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

@[inline, reducible]

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

Shim for IntList.gcd.

Equations

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

@[inline, reducible]

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

Shim for IntList.smul.

Equations

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

@[inline, reducible]

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

Shim for IntList.sdiv.

Equations

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

@[inline, reducible]

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

Shim for IntList.dot.

Equations

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

@[inline, reducible]

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

Shim for IntList.add.

Equations

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

@[inline, reducible]

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

Shim for IntList.sub.

Equations

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

@[inline, reducible]

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

Shim for IntList.neg.

Equations

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

@[inline, reducible]

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

@[inline, reducible]

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

Shim for List.length.

Equations

• Lean.Omega.Coeffs.length xs = List.length xs

@[inline, reducible]

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

Shim for IntList.leading.

Equations

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

@[inline, reducible]

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

@[inline, reducible]

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))

@[inline, reducible]

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

Shim for IntList.bmod.

Equations

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

@[inline, reducible]

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) : Lean.Omega.Coeffs.length (Lean.Omega.Coeffs.bmod x m) ≤ Lean.Omega.Coeffs.length x

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 : Lean.Omega.Coeffs.length xs ≤ i) : Lean.Omega.Coeffs.get xs i = 0

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

theorem Lean.Omega.Coeffs.dot_sdiv_left (xs : Lean.Omega.Coeffs) (ys : Lean.Omega.Coeffs) {d : Int} (h : d ∣ ↑(Lean.Omega.Coeffs.gcd xs)) : Lean.Omega.Coeffs.dot (Lean.Omega.Coeffs.sdiv xs d) ys = Lean.Omega.Coeffs.dot xs 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 * Lean.Omega.Coeffs.dot xs ys

theorem Lean.Omega.Coeffs.dot_distrib_left (xs : Lean.Omega.Coeffs) (ys : Lean.Omega.Coeffs) (zs : Lean.Omega.Coeffs) : Lean.Omega.Coeffs.dot (xs + ys) zs = Lean.Omega.Coeffs.dot xs zs + Lean.Omega.Coeffs.dot ys 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) : ↑(Lean.Omega.Coeffs.gcd xs) ∣ Lean.Omega.Coeffs.dot xs ys

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

theorem Lean.Omega.Coeffs.dot_nil_right {xs : Lean.Omega.Coeffs} : Lean.Omega.Coeffs.dot xs [] = 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