Zulip Chat Archive
Stream: new members
Topic: Implementing Greedoids
Jihoon Hyun (Jun 12 2023 at 00:45):
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/greedoidmathlib4/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 (Jun 12 2023 at 13:18):
Cool, thanks for sharing. @Peter Nelson has also worked on matroids for a while in mathlib 3 (https://github.com/apnelson1/leanmatroids), 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 (Jun 12 2023 at 23:56):
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/287929mathlib4/topic/mathport.20on.20external.20projects
Jihoon Hyun (Jun 13 2023 at 04:34):
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 (Jun 13 2023 at 05:31):
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 (Jun 13 2023 at 06:10):
Thanks for the feedback, I'll spend more time on those!
Jihoon Hyun (Jun 13 2023 at 06:16):
(removed, duplicate of above)
Jihoon Hyun (Jun 27 2023 at 07:46):
[[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 (Jul 02 2023 at 06:07):
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 (Jul 10 2023 at 17:27):
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.

Language
is defined asSet (List \alpha)
inMathlib/Computability/Language.lean
. This sure is a nice definition for language, but I only needFinset (List \alpha)
with additional instances to work further. Should I narrow the definition of predefinedLanguage
with a finite restriction, or would it be okay to define a newLanguage
withFinset
and instances? 
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 (Jul 10 2023 at 17:34):
It may be easiest to use Set plus a Set.Finite assumption where needed
Jihoon Hyun (Jul 10 2023 at 17:35):
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 (Jul 23 2023 at 10:29):
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 (Jul 23 2023 at 13:04):
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 'qmatroids', 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 (Jul 23 2023 at 14:54):
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 'qmatroids', 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!
Last updated: Dec 20 2023 at 11:08 UTC