Implementing Greedoids

Stream: new members

[Jihoon Hyun]

Hello, I was working on greedoids for a relatively short period, based on the book referenced below.
Here is the repository I'm working on: https://github.com/qawbecrdtey/greedoid-mathlib4/tree/greedoid
I thought it'd be nice to get helps and feedbacks to successfully contribute it to mathlib.

KORTE, Bernhard; LOVÁSZ, László; SCHRADER, Rainer. Greedoids. Springer Science & Business Media, 2012.

[Alex J. Best]

Cool, thanks for sharing. @Peter Nelson has also worked on matroids for a while in mathlib 3 (https://github.com/apnelson1/lean-matroids), but maybe soon in mathlib 4 also. I don't know how much overlap between your projects there is but it would be great to get this sort of thing into mathlib

[Julian Berman]

I think @Scott Morrison also has ported it (via mathport at least) which I caught via GitHub stalking :) -- looks like there's some further detail here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mathport.20on.20external.20projects

[Jihoon Hyun]

By the way, the new file is in directory Combinatorics/Greedoid, for those who want to check it out. It has thousand lines and many sorries..

[Scott Morrison]

Saying it that way is not going to convince anyone to look at it. People want to see a short file, with no sorries, along with a promise that an interesting theorem has been proved (possibly many files and thousands of lines downstream). If you can arrange that you will be drowning in (bors merge) and :peace_sign: (bor delegate). :-)

[Jihoon Hyun]

Thanks for the feedback, I'll spend more time on those!

[Jihoon Hyun]

(removed, duplicate of above)

[Jihoon Hyun]

[[resolved]]
I got stuck while working on the project, so I ask here about it. (If this is not a nice place to ask, please notice me so that I can ask there.)
context
So I'm wiring a proof for hereditary_language_lemma, and I have a single sorry on proof of that.
The next step is to set a maximal list w' in Lang which is a postfix of w. If the maximal list w' is w itself, then we're done, and if not, then that will lead to a counterexample by the property h, showing that w' is actually not maximal.
I'm not sure how to go to the next step from here. I wish I could get some help.

[Jihoon Hyun]

Currently the definition of greedoid is available with only one theorem weakerExchangeAxiom_exchangeAxiom containing sorry. (Actually two (1) (2), which are helper functions for the theorem)
The next step is to define rank and closure functions and prove its related theorems properly, as shown after the definition of Greedoid

[Jihoon Hyun]

I am moving theorems from fork to branch under Mathlib/Combinatorics/SetFamily.
I'm splitting the sinlge file to multiple files, and I'd like to ask a few questions on design of structures and file paths.

1. Language is defined as Set (List \alpha) in Mathlib/Computability/Language.lean. This sure is a nice definition for language, but I only need Finset (List \alpha) with additional instances to work further. Should I narrow the definition of predefined Language with a finite restriction, or would it be okay to define a new Language with Finset and instances?

2. I am currently making files under Mathlib/Combinatorics/SetFamily/(Accessible, Bases, ExchangeAxiom, to be added...).lean. Please tell and give advice if this is not a nice choice.

[Ruben Van de Velde]

It may be easiest to use Set plus a Set.Finite assumption where needed

[Jihoon Hyun]

What does it mean for a 'Set plus a Set'? I just realized that 'Set.Finite'
Thanks for the advice! The project might get a bit complicated than expected though..

[Jihoon Hyun]

The greedoid is now defined (again, with no sorries up to definition of the structure).
This version has separated files and more comments.
Next step is to define rank and closure of greedoids.
I know that @Peter Nelson is almost done with formalizing matroids, according to this thread.
Since these two structures are highly related and the matroid is almost ready for takeoff while mine is not, it would be nice to take his opinion for me to continue afterwards. So please leave your comments if you don't mind.
P.S. The main structure is defined here.

[Peter Nelson]

Nice job!

My main question about the code is why so much needs to happen before the definition. (Disclaimer: I don't know very much about greedoids).
From what I can see, a greedoid is can be defined in at least two different ways that turn out to be equivalent : via a set system, and via a language. You could just pick one of these ways (say, a set system), and then implement all the language stuff afterwards, proving that a Greedoid (as defined via a set system) gives rise to a language, with these properties....

And then you can have a constructor for a greedoid in terms of a language obeying the language axioms, whose mathematical content would be tantamount to your FromLanguageToSystem-type lemmas. This approach means that the definition of a greedoid itself contains less data, and also has the advantage that it only gives O(n) interface lemmas where n is the number of different ways to get a greedoid, rather than O(n^2).

In my matroid code, I do something similar. I make an arbitrary choice in defining a matroid in terms of bases (which I can do right at the beginning of the code), but then develop the API for independent sets and give constructors via the independence axioms later.

With regards to how your greedoids code and matroids fit together: it is true that finite matroids are a special case of greedoids, but the way I've written things my matroids can be infinite, so neither object strictly generalizes the other. I don't know how quickly the theory of greedoids diverges from matroid theory, but I get the sense that the API overlap is likely not too large for practical purposes.

I've thought a little in the past about what the right common generalization of such objects would be; they are both set systems, but in fact matroids are a special case of 'q-matroids', which are systems of points in more general lattices. I think for the moment it would make sense to have them as separate objects in mathlib; maybe a future refactor can unify them.

[Jihoon Hyun]

First of all, thanks for your response!

Peter Nelson 말함:

My main question about the code is why so much needs to happen before the definition. (Disclaimer: I don't know very much about greedoids).
From what I can see, a greedoid is can be defined in at least two different ways that turn out to be equivalent : via a set system, and via a language. You could just pick one of these ways (say, a set system), and then implement all the language stuff afterwards, proving that a Greedoid (as defined via a set system) gives rise to a language, with these properties....

You're right. When I started the project after reading the lean book, I thought the most easiest way to relate languages and systems was to directly relate them in a structure. And it turns out that it's not, I'll change the definition to use 'finite' set systems, and then extend it for other structures. There are only few (if any) resources on infinite greedoids, so it should be okay to formalize it only in the finite case for now.

I've thought a little in the past about what the right common generalization of such objects would be; they are both set systems, but in fact matroids are a special case of 'q-matroids', which are systems of points in more general lattices. I think for the moment it would make sense to have them as separate objects in mathlib; maybe a future refactor can unify them.

If that's the case, I'll focus on implementing greedoids solely. There definitely is a section which merges both concepts, but let's think about those difficult stuffs later..

Thanks again for your feedback!