Lean4
/-- Given two terms `l₁`, `l₂` of type `qNF R M`, i.e. lists of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s
and a natural number), recursively construct a proof that in the `$R`-module `$M`, the sum of the
"linear combinations" represented by `l₁` and `l₂` is the linear combination represented by
`Module.qNF.add iR l₁ l₁`. -/
def mkAddProof {iR : Q(Semiring $R)} {iM : Q(AddCommMonoid $M)} (iRM : Q(Module $R $M)) (l₁ l₂ : qNF R M) :
Q(NF.eval $(l₁.toNF) + NF.eval $(l₂.toNF) = NF.eval $((qNF.add iR l₁ l₂).toNF)) :=
match l₁, l₂ with
| [], l => (q(zero_add (NF.eval $(l.toNF))) :)
| l, [] => (q(add_zero (NF.eval $(l.toNF))) :)
| ((a₁, x₁), k₁) ::ᵣ t₁, ((a₂, x₂), k₂) ::ᵣ t₂ =>
if k₁ < k₂ then
let pf := mkAddProof iRM t₁ (((a₂, x₂), k₂) ::ᵣ t₂)
(q(NF.add_eq_eval₁ ($a₁, $x₁) $pf) :)
else
if k₁ = k₂ then
let pf := mkAddProof iRM t₁ t₂
(q(NF.add_eq_eval₂ $a₁ $a₂ $x₁ $pf) :)
else
let pf := mkAddProof iRM (((a₁, x₁), k₁) ::ᵣ t₁) t₂
(q(NF.add_eq_eval₃ ($a₂, $x₂) $pf) :)
