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 Std.Tactic.Omega.Coeffs.IntDict instead of Std.Tactic.Omega.Coeffs.IntList.

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

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs : Type

Type synonym for IntList := List Int.

Equations

• Std.Tactic.Omega.Coeffs = IntList

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.toList (xs : Std.Tactic.Omega.Coeffs) : List Int

Identity, turning Coeffs into List Int.

Equations

• Std.Tactic.Omega.Coeffs.toList xs = xs

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.ofList (xs : List Int) : Std.Tactic.Omega.Coeffs

Identity, turning List Int into Coeffs.

Equations

• Std.Tactic.Omega.Coeffs.ofList xs = xs

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.isZero (xs : Std.Tactic.Omega.Coeffs) : Prop

Are the coefficients all zero?

Equations

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

@[inline, reducible]

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

Shim for IntList.set.

Equations

• Std.Tactic.Omega.Coeffs.set xs i y = IntList.set xs i y

@[inline, reducible]

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

Shim for IntList.get.

Equations

• Std.Tactic.Omega.Coeffs.get xs i = IntList.get xs i

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.gcd (xs : Std.Tactic.Omega.Coeffs) : Nat

Shim for IntList.gcd.

Equations

• Std.Tactic.Omega.Coeffs.gcd xs = IntList.gcd xs

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.smul (xs : Std.Tactic.Omega.Coeffs) (g : Int) : Std.Tactic.Omega.Coeffs

Shim for IntList.smul.

Equations

• Std.Tactic.Omega.Coeffs.smul xs g = IntList.smul xs g

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.sdiv (xs : Std.Tactic.Omega.Coeffs) (g : Int) : Std.Tactic.Omega.Coeffs

Shim for IntList.sdiv.

Equations

• Std.Tactic.Omega.Coeffs.sdiv xs g = IntList.sdiv xs g

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.dot (xs : Std.Tactic.Omega.Coeffs) (ys : Std.Tactic.Omega.Coeffs) : Int

Shim for IntList.dot.

Equations

• Std.Tactic.Omega.Coeffs.dot xs ys = IntList.dot xs ys

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.add (xs : Std.Tactic.Omega.Coeffs) (ys : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Coeffs

Shim for IntList.add.

Equations

• Std.Tactic.Omega.Coeffs.add xs ys = IntList.add xs ys

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.sub (xs : Std.Tactic.Omega.Coeffs) (ys : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Coeffs

Shim for IntList.sub.

Equations

• Std.Tactic.Omega.Coeffs.sub xs ys = IntList.sub xs ys

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.neg (xs : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Coeffs

Shim for IntList.neg.

Equations

• Std.Tactic.Omega.Coeffs.neg xs = IntList.neg xs

@[inline, reducible]

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

Shim for IntList.combo.

Equations

• Std.Tactic.Omega.Coeffs.combo a xs b ys = IntList.combo a xs b ys

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.length (xs : Std.Tactic.Omega.Coeffs) : Nat

Shim for List.length.

Equations

• Std.Tactic.Omega.Coeffs.length xs = List.length xs

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.leading (xs : Std.Tactic.Omega.Coeffs) : Int

Shim for IntList.leading.

Equations

• Std.Tactic.Omega.Coeffs.leading xs = IntList.leading xs

@[inline, reducible]

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

Shim for List.map.

Equations

• Std.Tactic.Omega.Coeffs.map f xs = List.map f xs

@[inline, reducible]

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

Shim for .enum.find?.

Equations

• Std.Tactic.Omega.Coeffs.findIdx? f xs = List.findIdx? f xs

@[inline, reducible]

abbrev Std.Tactic.Omega.Coeffs.bmod (x : Std.Tactic.Omega.Coeffs) (m : Nat) : Std.Tactic.Omega.Coeffs

Shim for IntList.bmod.

Equations

• Std.Tactic.Omega.Coeffs.bmod x m = IntList.bmod x m

@[inline, reducible]

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

Shim for IntList.bmod_dot_sub_dot_bmod.

Equations

• Std.Tactic.Omega.Coeffs.bmod_dot_sub_dot_bmod m a b = IntList.bmod_dot_sub_dot_bmod m a b

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

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

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

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

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

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

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

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

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

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

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

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

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

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