Lean4
/-- Given two terms `l₁`, `l₂` of type `qNF M`, i.e. lists of `(ℤ × Q($M)) × ℕ`s (an integer, an
`Expr` and a natural number), construct another such term `l`, which will have the property that in
the field `$M`, the product of the "multiplicative linear combinations" represented by `l₁` and
`l₂` is the multiplicative linear combination represented by `l`.
The construction assumes, to be valid, that the lists `l₁` and `l₂` are in strictly decreasing order
by `ℕ`-component, and that if pairs `(a₁, x₁)` and `(a₂, x₂)` appear in `l₁`, `l₂` respectively with
the same `ℕ`-component `k`, then the expressions `x₁` and `x₂` are equal.
The construction is as follows: merge the two lists, except that if pairs `(a₁, x₁)` and `(a₂, x₂)`
appear in `l₁`, `l₂` respectively with the same `ℕ`-component `k`, then contribute a term
`(a₁ + a₂, x₁)` to the output list with `ℕ`-component `k`. -/
def mul : qNF q($M) → qNF q($M) → qNF q($M)
| [], l => l
| l, [] => l
| ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
if k₁ > k₂ then ((a₁, x₁), k₁) :: mul t₁ (((a₂, x₂), k₂) :: t₂)
else
if k₁ = k₂ then
/- If we can prove that the atom is nonzero then we could remove it from this list,
but this will be done at a later stage. -/
((a₁ + a₂, x₁), k₁) :: mul t₁ t₂
else ((a₂, x₂), k₂) :: mul (((a₁, x₁), k₁) :: t₁) t₂
