feat: Defining Greedoid

[qawbecrdtey]

---

The working branch for this project is greedoid-defs. This branch does not contain all features of the working branch, and is for real contribution to Mathlib.

The current branch have two files Predefs.lean and Basic.lean.

Before greedoid is properly defined, it defines two concepts on set systems, namely exchangeProperty and accessibleProperty in Predefs.lean.

Greedoid is a structure of set systems containing empty set, which satisfies both exchangeProperty and accessibleProperty, and is defined in Basic.lean.

• Edit(4de12f4e7a4fb883e23b3447ed648d2bff6ac87d): Removed Basic.lean (will be added later), changed pull request title.
• Edit(31f82971f047caa60bc9dc48116cc07dc1d307fc): Restored Basic.lean, but removed theorems related to exchangeProperty and accessibleProperty. Removed theorems are likely to be added in the next commit.

[kim-em]

Currently it seems we can't find a technical reviewer for this one. If Mathlib is going to grow in this direction, we're going to need help from people who are already familiar with this, or adjacent, material. @apnelson1, would you be able to give this a review?

[kim-em]

@qawbecrdtey, it's helpful if you can mark the conversations with Yury above as "resolved" if you've followed the suggestions there. It makes it easier for other reviews coming in to see what has been dealt with, and what is still active.

[github-actions[bot]]

PR summary 6888731ed0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Greedoid.Accessible (new file) Mathlib.Data.Greedoid.Exchange (new file)	443
Mathlib.Data.Greedoid.Basic (new file)	445

---

Declarations diff

+ Accessible + AccessibleProperty + Bases + Basis + ExchangeProperty + Greedoid + accessible_property + bases_card_eq + bases_eq_basis_ground + bases_feasible + bases_maximal + bases_subset_ground + basis_card_eq + basis_feasible + basis_maximal + basis_subset + basis_subset_ground + construction_on_accessible + eq_of_veq + exists_feasible_superset_add_element_feasible + exists_superset_of_card_le + feasible_inj + feasible_injective + induction_on_accessible + instance : Accessible G.Feasible + nonempty_contains_empty + nonempty_contains_empty_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[qawbecrdtey]

There are a few things to review:

1. Finset (Finset α) or Finset α -> Prop or Set α -> Prop: Currently it uses Finset (Finset α), as many lemmas on finite family of finite sets in the Combinatorics directory used it. Still I agree there are some conveniences which follow when the family of sets is implemented as Set α -> Prop just like Matroid, only if we discard computability. Finset α -> Prop is an option between those two.
2. Use of lemma instead of theorem: I could see a new keyword lemma in many other files. I wonder if this can be also applied to this file and afterwards.

[kim-em]

I've never heard of a greedoid, so this is out of ignorance, but I don't see any reason to mention Finset in this file. Switching to Set a -> Prop seems a good idea.

[apnelson1]

I've never heard of a greedoid, so this is out of ignorance, but I don't see any reason to mention Finset in this file. Switching to Set a -> Prop seems a good idea.

I can see the reason for feasible sets being Finsets; you are in a setting where everything is finite by nature, and you get some computability consequences (being able to use cons for example) but I can't understand why feasible should itself be a Finset.

Presumably since with your setup there can only be finitely many feasible sets, you will never be considering a greedoid on an infinite type? If not, then why not just use Fintype a where it may be needed, and have Feasible : Finset a -> Prop in the definition. 'feasible' is an adjective rather than a noun, after all.

[qawbecrdtey]

Let me state again that I couldn't find any appearance of greedoids elaborating infinite sets. So for now it should be okay to state it as a family of finite sets. Even if we consider infinite greedoid of any type, the generalization of greedoids will probably not be what we were expecting, thus rewriting the library is a must in any case of generalization.

The reason I used Finset (Finset α) is simply because I referenced some files in Combinatorics/SetFamily (1, 2) while writing the first draft. This way we can easily know the feasible set of greedoid is also finite. However, the major problem with this approach which I noticed while implementing the draft is that it consumes too much memory. For matroids there is a method of converting a family of bases to a family of independent sets, but the similar thing doesn't work for greedoids. So we should store all the feasible sets, including the basis, if we're not dealing with ranks or closures. This should grow exponentially in most cases, so I also think that Finset (Finset α) is not a great idea in this sense. Although it is already implemented, and it was easy to take care of the structure using Finset of Finsets up to now, I think this should be replaced as it is not really 'computable'.

Set α -> Prop should work great as in matroids. As mentioned above we can restrict α as a Fintype, or we may simply restrict the feasibility to be True only if the set is finite. Of course there may be several other options, but all these can be simply managed using Finset α -> Prop (and probably assuming DecidableEq α?). Also,

'feasible' is an adjective rather than a noun, after all.

So maybe I should work on implementing again with family of feasible sets being Finset α -> Prop, with possible improvements. I'll bring the update at around mid-August. Thanks!

[apnelson1]

Let me state again that I couldn't find any appearance of greedoids elaborating infinite sets. So for now it should be okay to state it as a family of finite sets. Even if we consider infinite greedoid of any type, the generalization of greedoids will probably not be what we were expecting, thus rewriting the library is a must in any case of generalization.

The reason I used Finset (Finset α) is simply because I referenced some files in Combinatorics/SetFamily (1, 2) while writing the first draft. This way we can easily know the feasible set of greedoid is also finite. However, the major problem with this approach which I noticed while implementing the draft is that it consumes too much memory. For matroids there is a method of converting a family of bases to a family of independent sets, but the similar thing doesn't work for greedoids. So we should store all the feasible sets, including the basis, if we're not dealing with ranks or closures. This should grow exponentially in most cases, so I also think that Finset (Finset α) is not a great idea in this sense. Although it is already implemented, and it was easy to take care of the structure using Finset of Finsets up to now, I think this should be replaced as it is not really 'computable'.

Set α -> Prop should work great as in matroids. As mentioned above we can restrict α as a Fintype, or we may simply restrict the feasibility to be True only if the set is finite. Of course there may be several other options, but all these can be simply managed using Finset α -> Prop (and probably assuming DecidableEq α?). Also,

'feasible' is an adjective rather than a noun, after all.

So maybe I should work on implementing again with family of feasible sets being Finset α -> Prop, with possible improvements. I'll bring the update at around mid-August. Thanks!

Let me state again that I couldn't find any appearance of greedoids elaborating infinite sets. So for now it should be okay to state it as a family of finite sets. Even if we consider infinite greedoid of any type, the generalization of greedoids will probably not be what we were expecting, thus rewriting the library is a must in any case of generalization.

The reason I used Finset (Finset α) is simply because I referenced some files in Combinatorics/SetFamily (1, 2) while writing the first draft. This way we can easily know the feasible set of greedoid is also finite. However, the major problem with this approach which I noticed while implementing the draft is that it consumes too much memory. For matroids there is a method of converting a family of bases to a family of independent sets, but the similar thing doesn't work for greedoids. So we should store all the feasible sets, including the basis, if we're not dealing with ranks or closures. This should grow exponentially in most cases, so I also think that Finset (Finset α) is not a great idea in this sense. Although it is already implemented, and it was easy to take care of the structure using Finset of Finsets up to now, I think this should be replaced as it is not really 'computable'.

Set α -> Prop should work great as in matroids. As mentioned above we can restrict α as a Fintype, or we may simply restrict the feasibility to be True only if the set is finite. Of course there may be several other options, but all these can be simply managed using Finset α -> Prop (and probably assuming DecidableEq α?). Also,

'feasible' is an adjective rather than a noun, after all.

So maybe I should work on implementing again with family of feasible sets being Finset α -> Prop, with possible improvements. I'll bring the update at around mid-August. Thanks!

It feels to me like you are mixing ideas about computation and ideas about reasoning in a way that is causing confusion. What exactly are you hoping to achieve with greedoids in lean, computation-wise?

[apnelson1]

Let me state again that I couldn't find any appearance of greedoids elaborating infinite sets. So for now it should be okay to state it as a family of finite sets. Even if we consider infinite greedoid of any type, the generalization of greedoids will probably not be what we were expecting, thus rewriting the library is a must in any case of generalization. The reason I used Finset (Finset α) is simply because I referenced some files in Combinatorics/SetFamily (1, 2) while writing the first draft. This way we can easily know the feasible set of greedoid is also finite. However, the major problem with this approach which I noticed while implementing the draft is that it consumes too much memory. For matroids there is a method of converting a family of bases to a family of independent sets, but the similar thing doesn't work for greedoids. So we should store all the feasible sets, including the basis, if we're not dealing with ranks or closures. This should grow exponentially in most cases, so I also think that Finset (Finset α) is not a great idea in this sense. Although it is already implemented, and it was easy to take care of the structure using Finset of Finsets up to now, I think this should be replaced as it is not really 'computable'. Set α -> Prop should work great as in matroids. As mentioned above we can restrict α as a Fintype, or we may simply restrict the feasibility to be True only if the set is finite. Of course there may be several other options, but all these can be simply managed using Finset α -> Prop (and probably assuming DecidableEq α?). Also,

'feasible' is an adjective rather than a noun, after all.

So maybe I should work on implementing again with family of feasible sets being Finset α -> Prop, with possible improvements. I'll bring the update at around mid-August. Thanks!

Let me state again that I couldn't find any appearance of greedoids elaborating infinite sets. So for now it should be okay to state it as a family of finite sets. Even if we consider infinite greedoid of any type, the generalization of greedoids will probably not be what we were expecting, thus rewriting the library is a must in any case of generalization. The reason I used Finset (Finset α) is simply because I referenced some files in Combinatorics/SetFamily (1, 2) while writing the first draft. This way we can easily know the feasible set of greedoid is also finite. However, the major problem with this approach which I noticed while implementing the draft is that it consumes too much memory. For matroids there is a method of converting a family of bases to a family of independent sets, but the similar thing doesn't work for greedoids. So we should store all the feasible sets, including the basis, if we're not dealing with ranks or closures. This should grow exponentially in most cases, so I also think that Finset (Finset α) is not a great idea in this sense. Although it is already implemented, and it was easy to take care of the structure using Finset of Finsets up to now, I think this should be replaced as it is not really 'computable'. Set α -> Prop should work great as in matroids. As mentioned above we can restrict α as a Fintype, or we may simply restrict the feasibility to be True only if the set is finite. Of course there may be several other options, but all these can be simply managed using Finset α -> Prop (and probably assuming DecidableEq α?). Also,

'feasible' is an adjective rather than a noun, after all.

So maybe I should work on implementing again with family of feasible sets being Finset α -> Prop, with possible improvements. I'll bring the update at around mid-August. Thanks!

It feels to me like you are mixing ideas about computation and ideas about reasoning in a way that is causing confusion. What exactly are you hoping to achieve with greedoids in lean, computation-wise?

By the way, am I right in deducing that you are at Kaist? I will be giving a talk about matroid formalization on August 13 - see https://dimag.ibs.re.kr/event/2024-08-13/ . I'd be happy to discuss this in person.

[qawbecrdtey]

By the way, am I right in deducing that you are at Kaist? I will be giving a talk about matroid formalization on August 13 - see https://dimag.ibs.re.kr/event/2024-08-13/ . I'd be happy to discuss this in person.

What a coincidence! I'll be looking forward to meeting you then!

[kbuzzard]

Sadly we can find nobody to review or maintain this theory so I think it's best if we close this PR.