Minimal or maximal structures

Stream: graph theory

[Shreyas Srinivas]

In graph theory (at least for finite graphs), we often work with proofs which start by saying "Consider a maximal/maximum structure with such and such property (for example maximal/maximum length simple path)". Usually for finite graphs, such structures exist because there are only a finite number of them in an n vertex graph. How do you do express this in lean? My best guess is that one needs to have a theorem saying, for example "there exists a maximal length path in any finite graph" or "there exists a cut which has minimum cut-size" . Is there a better, more general way to do it?

[Yaël Dillies]

One of the basic lessons of order theory is that maximum/minimum principles are the same as induction. So the most general way to do this is well-foundedness, but of course that's not a very concrete answer. The cases you're mentioning all can be expressed using a function to $ℕ$ so I assume you would be happy using docs#nat.find, docs#nat.find_greatest?

[Shreyas Srinivas]

Yaël Dillies said:

One of the basic lessons of order theory is that maximum/minimum principles are the same as induction. So the most general way to do this is well-foundedness, but of course that's not a very concrete answer. The cases you're mentioning all can be expressed using a function to $$ℕ so I assume you would be happy using docs#nat.find, docs#nat.find_greatest?

Is there a version for partial orders?

[Shreyas Srinivas]

For example, when I want to make an argument which requires choosing a maximal matching or maximal path.

[Shreyas Srinivas]

My best guess is there might be some theorem in mathlib that makes it possible to choose the maximal or minimal subset according to the subset ordering on finsets

[Yaël Dillies]

Well, you have Zorn's lemma for finding maximal elements in partial orders, but you will to be more precise for me to come up with concrete answers.

[Shreyas Srinivas]

theorem maximal_set_exists {α : Type} (S : Finset α) (p : Finset α → Prop) :
   ( ∃ (U : Finset α), U ⊆ S ∧ p U) →
      ∃ (T : Finset α), (T ⊆ S) ∧ p T ∧ (∀ V : Finset α, V ⊆ S ∧ T ⊂ V  → ¬p V) := by
      sorry

[Shreyas Srinivas]

Isn't Zorn's lemma overkill for finite structures?