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.
Identity, turning Coeffs into List Int.
Equations
- Lean.Omega.Coeffs.toList xs = xs
Identity, turning List Int into Coeffs.
Equations
- Lean.Omega.Coeffs.ofList xs = xs
Are the coefficients all zero?
Equations
- Lean.Omega.Coeffs.isZero xs = ∀ (x : Int), x ∈ xs → x = 0
Shim for IntList.set.
Equations
- Lean.Omega.Coeffs.set xs i y = Lean.Omega.IntList.set xs i y
Shim for IntList.get.
Equations
- Lean.Omega.Coeffs.get xs i = Lean.Omega.IntList.get xs i
Shim for IntList.smul.
Equations
- Lean.Omega.Coeffs.smul xs g = Lean.Omega.IntList.smul xs g
Shim for IntList.sdiv.
Equations
- Lean.Omega.Coeffs.sdiv xs g = Lean.Omega.IntList.sdiv xs g
Shim for IntList.dot.
Equations
- Lean.Omega.Coeffs.dot xs ys = Lean.Omega.IntList.dot xs ys
Shim for IntList.add.
Equations
- Lean.Omega.Coeffs.add xs ys = Lean.Omega.IntList.add xs ys
Shim for IntList.sub.
Equations
- Lean.Omega.Coeffs.sub xs ys = Lean.Omega.IntList.sub xs ys
Shim for IntList.combo.
Equations
- Lean.Omega.Coeffs.combo a xs b ys = Lean.Omega.IntList.combo a xs b ys
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))
Shim for IntList.bmod_dot_sub_dot_bmod.