# `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.

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs :
Type

Type synonym for `IntList := List Int`.

Equations

- Lean.Omega.Coeffs = Lean.Omega.IntList

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.toList (xs : Coeffs) :
List Int

Identity, turning `Coeffs` into `List Int`.

Equations

- xs.toList = xs

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.ofList (xs : List Int) :
Coeffs

Identity, turning `List Int` into `Coeffs`.

Equations

- Lean.Omega.Coeffs.ofList xs = xs

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.isZero (xs : Coeffs) :
Prop

Are the coefficients all zero?

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.set (xs : Coeffs) (i : Nat) (y : Int) :
Coeffs

Shim for `IntList.set`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.get (xs : Coeffs) (i : Nat) :
Int

Shim for `IntList.get`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.gcd (xs : Coeffs) :
Nat

Shim for `IntList.gcd`.

Equations

- xs.gcd = Lean.Omega.IntList.gcd xs

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.smul (xs : Coeffs) (g : Int) :
Coeffs

Shim for `IntList.smul`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.sdiv (xs : Coeffs) (g : Int) :
Coeffs

Shim for `IntList.sdiv`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.dot (xs ys : Coeffs) :
Int

Shim for `IntList.dot`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.add (xs ys : Coeffs) :
Coeffs

Shim for `IntList.add`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.sub (xs ys : Coeffs) :
Coeffs

Shim for `IntList.sub`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.neg (xs : Coeffs) :
Coeffs

Shim for `IntList.neg`.

Equations

- xs.neg = Lean.Omega.IntList.neg xs

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.combo (a : Int) (xs : Coeffs) (b : Int) (ys : Coeffs) :
Coeffs

Shim for `IntList.combo`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.length (xs : Coeffs) :
Nat

Shim for `List.length`.

Equations

- xs.length = List.length xs

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.leading (xs : Coeffs) :
Int

Shim for `IntList.leading`.

Equations

- xs.leading = Lean.Omega.IntList.leading xs

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.map (f : Int → Int) (xs : Coeffs) :
Coeffs

Shim for `List.map`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.findIdx? (f : Int → Bool) (xs : Coeffs) :
Option Nat

Shim for `.enum.find?`.

Equations

- Lean.Omega.Coeffs.findIdx? f xs = List.findIdx? f xs

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.bmod (x : Coeffs) (m : Nat) :
Coeffs

Shim for `IntList.bmod`.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Omega.Coeffs.bmod_dot_sub_dot_bmod (m : Nat) (a b : 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

Instances For

source
theorem Lean.Omega.Coeffs.bmod_length (x : Coeffs) (m : Nat) :
(x.bmod m).length ≤ x.length
source
theorem Lean.Omega.Coeffs.dvd_bmod_dot_sub_dot_bmod (m : Nat) (xs ys : Coeffs) :
↑m ∣ bmod_dot_sub_dot_bmod m xs ys
source
theorem Lean.Omega.Coeffs.get_of_length_le {i : Nat} {xs : Coeffs} (h : xs.length ≤ i) :
xs.get i = 0
source
theorem Lean.Omega.Coeffs.dot_set_left (xs ys : Coeffs) (i : Nat) (z : Int) :
(xs.set i z).dot ys = xs.dot ys + (z - xs.get i) * ys.get i
source
theorem Lean.Omega.Coeffs.dot_sdiv_left (xs ys : Coeffs) {d : Int} (h : d ∣ ↑xs.gcd) :
(xs.sdiv d).dot ys = xs.dot ys / d
source
theorem Lean.Omega.Coeffs.dot_smul_left (xs ys : Coeffs) (i : Int) :
dot (i * xs) ys = i * xs.dot ys
source
theorem Lean.Omega.Coeffs.dot_distrib_left (xs ys zs : Coeffs) :
(xs + ys).dot zs = xs.dot zs + ys.dot zs
source
theorem Lean.Omega.Coeffs.sub_eq_add_neg (xs ys : Coeffs) :
xs - ys = xs + -ys
source
theorem Lean.Omega.Coeffs.combo_eq_smul_add_smul (a : Int) (xs : Coeffs) (b : Int) (ys : Coeffs) :
combo a xs b ys = a * xs + b * ys
source
theorem Lean.Omega.Coeffs.gcd_dvd_dot_left (xs ys : Coeffs) :
↑xs.gcd ∣ xs.dot ys
source
theorem Lean.Omega.Coeffs.map_length {f : Int → Int} {xs : Coeffs} :
(map f xs).length ≤ xs.length
source
theorem Lean.Omega.Coeffs.dot_nil_right {xs : Coeffs} :
xs.dot [] = 0
source
theorem Lean.Omega.Coeffs.get_nil {i : Nat} :
get [] i = 0
source
theorem Lean.Omega.Coeffs.dot_neg_left (xs ys : IntList) :
dot (-xs) ys = -dot xs ys