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 difference
of the "linear combinations" represented by `l₁` and `l₂` is the linear combination represented by
`Module.qNF.sub iR l₁ l₁`. -/
def mkSubProof (iR : Q(Ring $R)) (iM : Q(AddCommGroup $M)) (iRM : Q(Module $R $M)) (l₁ l₂ : qNF R M) :
Q(NF.eval $(l₁.toNF) - NF.eval $(l₂.toNF) = NF.eval $((qNF.sub iR l₁ l₂).toNF)) :=
match l₁, l₂ with
| [], l => (q(NF.zero_sub_eq_eval $(l.toNF)) :)
| l, [] => (q(sub_zero (NF.eval $(l.toNF))) :)
| ((a₁, x₁), k₁) ::ᵣ t₁, ((a₂, x₂), k₂) ::ᵣ t₂ =>
if k₁ < k₂ then
let pf := mkSubProof iR iM iRM t₁ (((a₂, x₂), k₂) ::ᵣ t₂)
(q(NF.sub_eq_eval₁ ($a₁, $x₁) $pf) :)
else
if k₁ = k₂ then
let pf := mkSubProof iR iM iRM t₁ t₂
(q(NF.sub_eq_eval₂ $a₁ $a₂ $x₁ $pf) :)
else
let pf := mkSubProof iR iM iRM (((a₁, x₁), k₁) ::ᵣ t₁) t₂
(q(NF.sub_eq_eval₃ ($a₂, $x₂) $pf) :)
