Lean4
/-- `mkLTZeroProof coeffs pfs` takes a list of proofs of the form `tᵢ Rᵢ 0`,
paired with coefficients `cᵢ`.
It produces a proof that `∑cᵢ * tᵢ R 0`, where `R` is as strong as possible.
-/
def mkLTZeroProof : List (Expr × ℕ) → MetaM Expr
| [] => throwError"no linear hypotheses found"
| [(h, c)] => do
let (_, t) ← mkSingleCompZeroOf c h
return t
| ((h, c) :: t) => do
let (iq, h') ← mkSingleCompZeroOf c h
let (_, t) ← t.foldlM (fun pr ce ↦ step pr.1 pr.2 ce.1 ce.2) (iq, h')
return t
where/-- `step c pf npf coeff` assumes that `pf` is a proof of `t1 R1 0` and `npf` is a proof
of `t2 R2 0`. It uses `mkSingleCompZeroOf` to prove `t1 + coeff*t2 R 0`, and returns `R`
along with this proof.
-/
step (c : Ineq) (pf npf : Expr) (coeff : ℕ) : MetaM (Ineq × Expr) := do
let (iq, h') ← mkSingleCompZeroOf coeff npf
let (nm, niq) := addIneq c iq
return (niq, ← mkAppM nm #[pf, h'])
