The design of matroids

Stream: mathlib4

[Peter Nelson]

I've just finished with a PR (#14197) that defines the closure of a set in a matroid. At @Johan Commelin 's suggestion, I'm recording here for posterity some nontrivial design issues that came up during review. The PR itself has just been merged, so this isn't a request for help or advice as such, but the issues themselves and where we ended up are possibly interesting to some. The docstrings of Data.Matroid.Closure and Data.Matroid.Basic also record this a bit more tersely.

I'm also using this opportunity to discuss how matroids are defined in mathlib in the first place, since they use a pattern that is unlike many other things in mathlib, and this fact is quite relevant to the issues that come up with closure. So this is a bit long, and is really half for my own benefit. Anyone that reads all the way to the end has my gratitude :smile: .
(The wider context of all this is I have a repo of matroid theory consisting of around 20k LOC, which I'm trying quite hard to write in a versatile, mathlib-compatible way, and to PR as I'm doing it. It's going a bit slowly, but it's going).

The mathematics

In pen-and-paper maths, a matroid is usually defined as a pair $(E,\mathcal{I})$, where $E$ is a set, and
$\mathcal{I} \subseteq 2^E$ is a nonempty collection of 'independent' subsets of $E$ satisfying certain axioms: for example, any subset of an independent set must be independent. The prototypical model of a matroid is a 'linear matroid', where $E$ is some set of vectors in a vector space, and the independent sets of $M$ are precisely the linearly independent subsets of $E$. The closure function of a matroid is a certain function $cl : 2^E \to 2^E$ satisfying properties such as $cl(cl(X)) = cl(X)$ and $X \subseteq cl(X) \subseteq cl(Y)$ for all $X \subseteq Y$. In the case where $M$ is linear, this corresponds to a linear span, in the sense that $cl(X) = span(X) \cap E$.

Matroid Design

In formalizing matroids, one's first instinct is probably to define a matroid as a structure (or class) Matroid α consisting of a predicate Indep : Set α → Prop, with appropriate rules constraining the behaviour of Indep. This mimics the design of objects in the algebraic hierarchy. Doing this would make Matroid.closure an example of a ClosureOperator (Set α), and give access to a lot of nice API for these objects, such as Galois insertions.

Unfortunately, this design has huge drawbacks to do with the way matroids are used. Unlike algebraic objects, the ground set $E$ of a matroid is really treated like a set. A matroid on a set $E$ gives rise to many related matroids (minors) on subsets of $E$ in different and nonisomorphic ways, and it is not unusual to consider multiple matroids on the same set $E$, or to make assertions about, say, the interection of the ground sets of two different matroids. Modelling the ground set of a matroid with a type (let alone using typeclasses) is a complete non-starter for this - even very basic theorems about minors of matroids having statements that include an = sign become horrible piles of canonical isomorphisms, which are paralyzing in practice.

I know this because I tried doing things this way for a long time, before @Johan Commelin suggested the current design to me. It works as follows: For α : Type*, a Matroid α consists of a set E : Set α, and a predicate Indep : Set α → Prop, satisfying certain axioms that define a matroid, together with an extra rule h_support : ∀ I, Indep I → I ⊆ E. In other words, the ground set of a matroid is not a type, but a set within a type, and the independence predicate is defined on all sets in the type, and happens to only hold for subsets of E.

This may seem unwieldy. The real disadvantage is that it sometimes requires unmathematical bookkeeping to make sure that sets are contained in the ground set. The hypothesis X ⊆ M.E appears all over the API, where it would have been simply true by definition if the ground set were a type. The advantage is that it allows meaningful assertions that two matroids are Eq.

It's not that the disadvantage isn't bad (it is certainly quite annoying to constantly have to care about sets being 'supported'), but it's that one can't do basic matroid theory in any other way that I know. The 1000 or so lines of API in the basic file on minors in my matroid repo would be complete DTT hell if ground sets were types, and it's only the very beginning of the theory.

So as far as I know, there is no other option than to suck it up, to keep track of sets being contained in the ground set, and to devote mental energy to the junk elements outside the ground set when stating lemmas. One thing that helps is the tactic aesop_mat, which works pretty well to automatically discharge goals of the form X ⊆ M.E when this follows from things in the context.

Closure

There are many other natural predicates on sets in a matroid; a set $X \subseteq E$ may be a 'circuit', 'base', 'basis', 'flat', 'cocircuit', ... of $M$, and mostly they follow a similar design to Indep. For instance, we have a predicate Base : Set α → Prop which is defined in such a way that Base B → B ⊆ M.E is a theorem; bases of a matroid only exist as subsets of its ground set. Formalizing closure is different, though. Since $cl : 2^E \to 2^E$, we need to formalize it s Matroid.closure : Set α → Set α, so we are forced to say where the junk goes. That is, if X is not a subset of M.E, then how should M.closure X be defined?

There are quite a few potential choices. For instance, we could declare that M.closure X = ∅ whenever X isn't a subset of M.E. This choice would be bad, though, since it necessitates adding a lot of support assumption to theorems about closure; we would need to know that Y ⊆ M.E for X ⊆ Y to imply M.closure X ⊆ M.closure Y, so M.closure would fail to be monotone.

After discarding the chaff like the above, there are two reasonable choices that remain. Suppose that M.closure X has been defined as the mathematics dictates for every subset X of M.E. When X is not a subset of M.E, we can either

(1) : Define M.closure X so that M.closure X = M.closure (X ∩ M.E), or
(2) : Define M.closure X = M.closure (X ∩ M.E) ∪ X.

And this choice is why I'm making this post. Originally my repo used (1), and the PR initially did. But Johan suggested (2) for the PR, giving some quite good arguments for it, and I spend several days work experimenting with (2) in my repo.
I eventually settled on (1), but not without reservations.

It's a hard choice! Both (1) and (2) are good and bad for different reasons, and it felt very annoying to be forced to settle on one or the other. I'll summarize the points here.

(1) is nice for two reasons. First, it guarantees that M.closure X ⊆ M.E for all X, even when X contains junk outside the ground set. This is great for aesop_mat; in general knowing that things are contained in the ground set is very useful, since it's needed so often as an assumption. The second reason is that when proving something about M.closure X with no assumptions on X, one can quickly rw the term to M.closure (X ∩ M.E), and obtain a statement that is only about subsets of ground set (i.e. sets which are mathematically meaningful in the context of this matroid). This reduces cognitive load; thinking about junk elements is unmathematical and annoying.

(2) is nice for reasons that probably appear more attractive. The statement that M.closure X ⊆ M.E is no longer unconditionally true (it needs X ⊆ M.E), but the statement that X ⊆ M.closure X is unconditionally true.
This turns out to imply that Matroid.closure is actually an example of docs#ClosureOperator. This opens up access to a lot of nice API, giving a GaloisInsertion, for example. A side benefit is that a function satisfying (2) is actually the closure function of a different matroid with ground set univ, which can simplify proofs in a few places.

So I made a branch of my repo, and refactored the whole thing so that closure was defined as ClosureOperator, satisfying (2). This affected countless lemmas across dozens of files, and it was a few days work adding/removing 'non-junk' assumptions before I had (2) working almost everywhere.

It was a close thing, but the slightly less mathematically principled and more hacky solution won out: I decided that (1) was better. The nice API was tempting, reduced duplication a little and was in some places useful, but having access to M.closure X ⊆ M.E and being able to easily rw away junk elements was too much to give up. A common idiom with (2) was having a term M.closure X with no assumptions on X, then rewriting it to M.closure (X ∩ M.E) ∪ (X \ M.E) to separate the non-junk and junk parts of the term. But this expression still contains the unmathematical junk X \ M.E; any time and keystrokes spent dealing with those elements is a waste and arguably a failure of the design. And of course the term M.closure (X ∩ M.E) ∪ (X \ M.E) itself is horrible, especially if X itself is a complicated expression. Losing the API was difficult, but in fact it was still available in a different guise. With (1), we do still get a ClosureOperator on the subtype {X // X ⊆ M.E}, through which the API lemmas can be (a little clunkily) transferred from the subtype to the type.

[Peter Nelson]

Conclusion

I don't know what the lesson is here, but it is clear that the 'embedded ground set' design was consequential. It forced me to decide between (1) and (2), and it would have been really nice to have the advantages of both. If the ground set were a type, we could have had both (1) and (2), but we would then be unable to assert that two different-looking matroids are Eq, which is central enough to the combinatorial theory that it is a deal-breaker.

This isn't the only time that embedded ground sets have caused me pain. Whenever functions in and out of matroids crop up, they make things a little more difficult. The material in docs#Data.Matroid.Map is forced to consider many different flavours of maps between matroids involving subtypes of subsets, and this is because ground sets are not types. When formalizing the heavily studied subject of linear representations of a matroid, you need to consider functions f : M.E → W for a vector space W; this would be much easier if the domain were a plain type rather than a coerced set.

But none of this pain is as bad as the alternative: being unable to consider different matroids on related ground sets as terms in a common type.

So going forward, I'm putting up with the pain, using subtypes once functions get involved, and using automation tactics like aesop_mat with autoparams to minimize manually keeping track of X ⊆ M.E proofs. (by the way, I hacked aesop_mat together a year ago and it's doing something quite simple not particularly quickly; anyone that knows how to speed up specialized aesop-like tactics that would be willing to have a look with me would have my gratitude!) Maybe there is a good design I'm unaware of that would make my life much easier, and maybe HOTT has something to offer. But in the meantime I think this is what matroid theory looks like in lean.

[Johan Commelin]

@Peter Nelson Thank you so much for writing up this detailed "post-mortem". I think it will be a valuable piece of writing to point to now and then.

[Patrick Massot]

It would probably be easier to find as a blog post.

[Peter Nelson]

Is there an appropriate venue? I'm happy to turn this into a guest post somewhere, but have no blog setup myself.

[Ruben Van de Velde]

The lean prover community blog?

[Peter Nelson]

Anyone relevant should feel free to DM me

[Kim Morrison]

Apologising ahead of time that I haven't read everything, but could you not have a field E : Set \a and then Indep : Set E -> Prop? (i.e. bundling independence and support together, using the coercion from sets back to types).

Naively it seems like this might avoid having to worry about support side conditions when working with a fixed E, but still allow having many matroids on the same \a.

[Kim Morrison]

@Peter Nelson instructions for submitting a blog post are at https://leanprover-community.github.io/blog/about/. I'd encourage you to send this write up there!

[Peter Nelson]

Kim Morrison said:

Apologising ahead of time that I haven't read everything, but could you not have a field E : Set \a and then Indep : Set E -> Prop? (i.e. bundling independence and support together, using the coercion from sets back to types).

Naively it seems like this might avoid having to worry about support side conditions when working with a fixed E, but still allow having many matroids on the same \a.

Yes, that was an option I looked into. The problem is that it will cause heq hell when you have pairs of matroids with equal but not defeq ground sets, which is a common occurence. For instance this lemma would be quite hard to state.

[Kyle Miller]

There can always be a Matroid.Indep' : Set E -> Prop defined in terms of Indep and h_support in case it's useful. There's no need to bake DTT hell into the definition itself. I think 'making the ext theorem nice' is a good design principle.

[Peter Nelson]

Kim Morrison said:

Peter Nelson instructions for submitting a blog post are at https://leanprover-community.github.io/blog/about/. I'd encourage you to send this write up there!

I'll do this early next week!

[Peter Nelson]

Kyle Miller said:

There can always be a Matroid.Indep' : Set E -> Prop defined in terms of Indep and h_support in case it's useful. There's no need to bake DTT hell into the definition itself.

yes, and it barely needs a definition, because of the coercion from Set X to Set a in docs#Data.Set.Notation. For X : Set E, we haveM.Indep' X := M.Indep ↑X

[Eric Wieser]

Kyle Miller said:

I think 'making the ext theorem nice' is a good design principle.

Given you can write the ext theorem by hand, I don't think this design principle really influences how you build the type itself. Certainly, the ext theorem for Equiv is different to the one that would be autogenerated, and this is a good thing.

[Eric Wieser]

Peter Nelson said:

The problem is that it will cause heq hell when you have pairs of matroids with equal but not defeq ground sets

The confusion for me has always been a lack of knowledge about what makes ground sets of matroids fundamentally different from carrier sets of submodules (which is on me for not having the matroid background). It would be great if you could make this comparison explicit in the potential blog post!

[Peter Nelson]

The relevant ext theorem for matroids is the following; note the I ⊆ M₁.E in the statement. I should really rename it Matroid.ext_indep or something.

Matroid.eq_of_indep_iff_indep_forall.{u_1} {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ I ⊆ M₁.E, M₁.Indep I ↔ M₂.Indep I) : M₁ = M₂

[Peter Nelson]

Eric Wieser said:

Peter Nelson said:

The problem is that it will cause heq hell when you have pairs of matroids with equal but not defeq ground sets

The confusion for me has always been a lack of knowledge about what makes ground sets of matroids fundamentally different from carrier sets of submodules (which is on me for not having the matroid background). It would be great if you could make this comparison explicit in the potential blog post!

Maybe the shortest answer there is that, given a fixed module, a submodule is determined by its carrier set.

[Kyle Miller]

Given you can write the ext theorem by hand

Certainly. However, I still mean what I'm saying: it's a good design principle to design your types to have a straightforward ext lemma without needing to wrangle dependent types. I find that this is a quick test to see if you're going to down a road of trouble. It's nothing to do with autogeneration. (For that reason, Equiv.ext is not an example of this — it's funext composed with what would be the generated ext lemma, but in a defeq form.)

[Bryan Gin-ge Chen]

Apologies for asking this without having given this much thought, but will we run into similar issues with formalizing graphs?

[Eric Wieser]

Kyle Miller said:

Equiv.ext [is] funext composed with what would be the generated ext lemma, but in a defeq form.)

Equiv.ext doesn't mention Equiv.invFun, while the generated ext lemma would

[Eric Wieser]

Bryan's comment is a good one; comparing to the SimpleGraph/Subgraph approach sounds much more relevant than my bad suggestion of comparing to Submodule.

[Peter Nelson]

If you start thinking about minors of graphs rather than subgraphs, all the same problems will arise, and they will likely be worse because both vertices and edges will have to be separate types.

[Peter Nelson]

Again, a minor of a graph is not determined by its edge set.

[Kyle Miller]

(I missed the missing invFun field, but Equiv.ext is still not an example of dependent type madness @Eric Wieser. The Equiv type clearly passes the design principle I'm talking about, even if in practice there's a better one, though one that's an optimized version of the autogenerated one.)

[Kyle Miller]

@Bryan Gin-ge Chen In an earlier version of SimpleGraph.Subgraph, I was experimenting with using subtypes for the Adj relation, but it became clear that writing out a "first-order" version worked out much better: https://github.com/leanprover-community/mathlib4/blob/82e01e3c5f7f05515affcee83152fb573c4097b3/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean#L59-L64

[Eric Wieser]

Regarding minors on graphs, this thread and this thread are relevant. I assume one obvious difference here is that minors are essential to matroids, but you can do a lot of graph theory without them?

[Peter Nelson]

Sure, but there is a lot of graph theory that involves them, both classically and at the cutting edge.

Arguably the deepest single theorem in graph theory is about the minor order: https://en.m.wikipedia.org/wiki/Graph_structure_theorem

[Kyle Miller]

It turns out a minor is the same thing as an interval of subgraphs, so minors aren't so bad, though there's pain in treating a minor like a graph itself, since the vertex set is a quotient.

[Peter Nelson]

‘The vertex set is a quotient’ is a matter for debate.

[Kyle Miller]

What do you mean?

[Eric Wieser]

Kyle Miller said:

It turns out a minor is the same thing as an interval of subgraphs, so minors aren't so bad, though there's pain in treating a minor like a graph itself, since the vertex set is a quotient.

Indeed, I just found your thread here.

[Kyle Miller]

If you mean "circumvent using Quot by using choice", then you're still working with a quotient (it has the correct universal property)

[Peter Nelson]

It’s certainly not a useful perspective if you’re contracting a single edge e, and applying the inductive hypothesis. It’s much more convenient to think of getting another graph which shares most of its vertices with the original one.

[Peter Nelson]

You have to pick a name for the identified vertex, sure. But i think such a ‘labelled contraction’ is more the way a lot of people think about minors.

[Peter Nelson]

Formalizing a proof of Kuratowski’s theorem where a minor is an interval of subgraphs doesn’t sound fun.

[Kyle Miller]

The point here is to make it so that minors have a good extensionality theorem, so that deletion-contraction relations can be written with equality.

It might be that there need to be auxiliary definitions to "represent" this point of view, maybe similar to how matroids have multiple definitions.

[Peter Nelson]

I think I'm not so excited at the idea of Minor G for G : Graph V E. It feels very constraining; what if H is a minor of G and I want to consider some other graph that has H as a minor?

I would rather that a minor be a Graph itself. I think this can be done using a design similar to what I am doing for matroids (with the same tradeoffs).

Given a choice between a minor/subgraph having a 'canonical' vertex type, i.e. a coerced Set or a quotient, and a notion of minor/subgraph where the vertices/edges of the subobject can be Eq to vertices/edges of the host, I'd go for the latter every time.

[Peter Nelson]

At the moment, I'm working with grad students who know combinatorics but are new to formalization. If I have a Walk in H : Subgraph (G : SimpleGraph V) and they want to consider the 'corresponding' walk in G itself, I have to explain to them about maps between graphs, the canonical map from a subgraph to a graph, transferring the walk along said map, issues to do with defeq of coerced vertices, etc etc. All this is cognitive load, and it's simply not there in informal mathematics (i.e. set theory).

In the way most graph theorists think about graphs and subgraphs, there is no 'corresponding' walk. If $W$ is a walk of a subgraph $H$ of $G$, then $W$ is a walk of $G$, because its vertices and edges are vertices and edges of $G$. There are no maps.

And this isn't just a matter of getting used to a new and better perspective. Even once you learn it, it's annoying, departs from the mathematical idiom, and comes up everywhere. If subgraphs/minors aren't Graphs with the same vertex and edge type, this is unavoidable. But I don't think it needs to be that way.

[Eric Wieser]

Peter Nelson said:

the canonical map from [X] to [Y], transferring [P] along said map, [...]. All this is cognitive load, and it's simply not there in informal mathematics (i.e. set theory).

I think this is a fairly ubiquitous design decision in mathlib; we have this for (X, Y, P) = (ℕ, ℤ, ≤ ), subsets vs sets vs types, submonoids vs monoids, etc. I think the general design you are hoping for is much more closely followed by systems like Isabelle which are using something much closer to set theory.

[Peter Nelson]

In those examples, there is a good reason for doing things that way. What's the good reason here?

[Sébastien Gouëzel]

In the maths I'm doing, graphs come up pretty frequently, but it's always as a fixed graph. In this case, it's definitely simpler if the graph is a type, not a set in a type.

[Peter Nelson]

This is the case in matroid theory for many things too - when minors aren't involved, I generally want them to be a type. But it becomes so much more difficult to work with minors if they are a type, that it isn't an option.

And there is room for API for the special case where M.E = univ (or G.V = univ for a graph). It amounts to duplication, but I'd rather have that than be unable to work with minors.

For subgraphs and simple graphs, I think that the discussion is more nuanced, because subgraphs are essentially set-like. But there are pros and cons there as well.

[Peter Nelson]

It's also worth noting that there are tons of interelated partial orders on graphs, including subgraphs, minors, topological minors, induced subgraphs, homomorphic images, minors, induced minors, vertex minors and pivot minors. Do they all get their own Subgraph-like type?

[Peter Nelson]

Kim Morrison said:

Peter Nelson instructions for submitting a blog post are at https://leanprover-community.github.io/blog/about/. I'd encourage you to send this write up there!

I just tried to PR but it looks like I need permission to create a branch.

[Yaël Dillies]

You can always PR from a :fork_and_knife:

[Patrick Massot]

Yes, the whole story of not PRing from a fork is only for Mathlib.

[Martin Dvořák]

Thank you so much @Peter Nelson for the detailed post!

Following on the design decisions, when we now work with matroids (which heavily use sets as opposed to types), there is a rising need for a good interface between "type theory" and "set theory" (by which I don't mean axiomatic set theory but rather working with sets expressed in Lean).

One of the things touching the interface are binary matroids. Since the Seymour project (@Ivan S. et al) is all about binary matroids, I hacked together an ad-hoc API for translation between set unions and sum types, starting here:
https://github.com/Ivan-Sergeyev/seymour/blob/45a9ff84d86c95af8b3d09fbddd7e2b9754f3275/Seymour/Basic.lean#L18

Do you think it would make sense to develop this API more systematically and integrate it into Mathlib? Should I start submitting PRs to Mathlib for the API as an independent contribution, or only when another contribution needs a part of it?

[Eric Wieser]

I think that function is docs#Set.inclusion ?

[Eric Wieser]

And the next one is docs#Equiv.Set.union

[Martin Dvořák]

Thanks for pointing them out! I didn't know we had them.

Should the mathlib's version of Matrix.toMatrixUnionUnion be built from docs#Matrix.reindex and docs#Equiv.Set.union then?

[Eric Wieser]

I don't it should exist at all, we can't afford to have a def for every possible reindex

[Eric Wieser]

We probably could have abbrev reindex\_2 for reindexing square matrices

[Mahdi Khaleghi]

Could you provide guidance on how I can check the current state of matroid theory implementation in lean? I need to work on implementing some matroid models and would like to understand the recent progress. Additionally, I would greatly appreciate information about areas of matroid theory that still need to be implemented or explored further.