feat: Define linear programs

[madvorak]

Linear programs over a general Module with constraints given in the form "aᵀx - b ≥ 0" and the objective function as an AffineMap to be minimized.

---

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.237386.20Linear.20Programming

Four PRs incompatible with each other:
#7386 (list of constraints)
#9693 (matrix form)
#10026 (Antoine Chambert-Loir's def; semirings, linear)
#10159 (Antoine Chambert-Loir's def; rings, affine)

[semorrison]

I don't particularly like the design, with constraints and objective bundled together. The feasibility of constraints makes no mention of the objective, and the design should allow talking about this without an objective. Please separate these.

[madvorak]

Would you be more happy with the following definitions?

def LinearProgramFeas (R : Type*) {V : Type*} (P : Type*)
    [LinearOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] :=
  List (P →ᵃ[R] R)

structure LinearProgramOpt (R : Type*) {V : Type*} (P : Type*)
    [LinearOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] where
  constraints : LinearProgramFeas R P
  objective : P →ᵃ[R] R

[semorrison]

Why not two structures, one extending the other?

Presumably for the "just the constraints" version, you then want definitions satisfiable_at and satisfiable, with lots of lemmas about how these interact with list operations (e.g. adding/erasing etc constraints).

[semorrison]

I am skeptical about making this a List rather than a Set. One is not actually going to do computation with this type: any meaningful algorithm will require a much more complicated data structure.

[eric-wieser]

I think I remember Martin expressing some objections to situations with infinitely-many constraints, as those tend not to appear in linear programming. That would rule out Set, and prohibiting duplicates or permutations isn't particularly interesting since the constraints can still be redundant.

[semorrison]

Happy to hear Martin's take on this, or for someone to click "resolve" as is.

[eric-wieser]

If finiteness is really the thing of interest though, you could argue that what we actually want is the type of convex sets built from finitely many half planes; either non-constructively via an existential, or constructively via a Finset and a proof that removing any one element increases the size of the feasible set.

[Shreyas4991]

Can you induct on Finsets?

[madvorak]

You are right. Just one comment (not contradicting to your suggestion); all point on the sphere would be vertices.

[eric-wieser]

About the second part of your comment, redundant constraints are often a thing that we have to deal with (because they come from the ambient problem in the LP). So we probably shouldn't have the proof obligation that says "removing a constraint strictly increases the feasible set"

I don't think this claim necessarily holds merit; finsets are not allowed to hold duplicates, and have a proof obligation to this end; but that doesn't stop you from writing {1, 1, 2, 2}. You only have to deal with the proof obligation if you call Finset.mk directly.

Arguably this "Finset of non-redundant affine constraints" object deserves it's own ConvexPolytope object.

[eric-wieser]

Though another reasonable approach might be to discard the proof obligation and work with the quotient of the type by equality of feasible spaces

[Shreyas4991]

A redundant LP need not have identical constraints. It just needs to be a linear combination of other constraints. I am not sure I see the value in doing, let's say Gaussian elimination on constraints, to extract independent ones makes sense every time an LP is defined. In computer science and also possibly OR, redundant constraints are a fact of life that have to be dealt with algorithmically, and so one often constructs what Mathlib devs might call API lemmas to deal with these cases.

[madvorak]

When I think about it, having infinitely many conditions is less weird than having infinitely many variables. Given that Mathlib maintainers want the variable space to be general, we should also make the condition space general. Defining conditions as a list (or a multiset, or a finite set) of any type will be bad for LP duality, unless we change the type of P along with it.

[madvorak]

Alternative: #9693

[madvorak]

Another alternative: #10026