Graph theory def: Maximal/maximum cliques & independent sets

[SnirBroshi]

We have SimpleGraph.IsClique and SimpleGraph.IsIndepSet for cliques & independent sets in simple graphs.

We also have SimpleGraph.IsMaximumClique and SimpleGraph.IsMaximumIndepSet for the maximum versions.

The file Mathlib.Combinatorics.SimpleGraph.Clique also proves things about the maximal versions, using Maximal G.IsClique s and Maximal G.IsIndepSet s inline while naming theorems with "isMaximalClique" and "isMaximalIndepSet".

I suggest we're missing the following defs:

open Cardinal

def IsMaximalClique (G : SimpleGraph V) (s : Set V) :=
  Maximal G.IsClique s

def IsMaximumClique (G : SimpleGraph V) (s : Set V) :=
  MaximalFor G.IsClique (#·) s

def IsMaximalIndepSet (G : SimpleGraph V) (s : Set V) :=
  Maximal G.IsIndepSet s

def IsMaximumIndepSet (G : SimpleGraph V) (s : Set V) :=
  MaximalFor G.IsIndepSet (#·) s

where the maximum versions are intended to replace the existing structures with the same name.

I think not having the maximal versions is hurting Loogle-ability, and that we should use Maximal/MaximalFor where possible to gain access to useful API.

[b-mehta]

I agree we should use the Maximal/MaximalFor API. I'm not yet convinced that we should make these defs though, my instinct is instead to remove the defs and to talk about, eg, Maximal G.IsIndepSet s directly, I think this is essentially as readable as G.IsMaximalIndepSet s. But a sufficiently good argument could convince me!

[SnirBroshi]

I'm not sure my arguments are great but here are a few:

• For the maximums we should standardize the cardinality that they use (whether it's Finset.card/Cardinal.mk/Nat.card/ENat.card/...). If we inline the definition then theorems might differ based on what's open before them.

• The maximums are pretty long and hard to type compared to their definition; 10 more key presses

• These are well known definitions in math and mathematicians will be looking for them, possibly by typing G.clique and looking at the autocomplete list. The same is true for maximal/maximum matchings and minimal/minimum vertex covers. This argument applies to many defs. I think named defs are the least surprising option for users trying to use Mathlib's graph theory.

• There are theorems already named with isMaximalClique and isMaximalIndepSet but they use Maximal. This violates the naming convention, we should either make such a def or rename them. (they used to exist)

• If we're inlining MaximalFors I think this should extend to inlining G.IsTuranMaximal r to be MaximalFor (·.CliqueFree (r + 1)) (·.edgeSet.ncard) G, which seems similarly counterproductive

• To Loogle for theorems about them, compare SimpleGraph.IsMaximalClique vs Maximal (SimpleGraph.IsClique _), or even SimpleGraph.IsMaximumIndepSet vs MaximalFor (SimpleGraph.IsIndepSet _) fun _ ↦ Cardinal.mk _. I guess the last one can be shorter if we never use MaximalFor with independent sets and something that isn't their size, so we can avoid the function argument.

To summarize, I really think definitions are worth it in general, and especially for things which are well known and defined in undergraduate maths.
Thanks!

[b-mehta]

I don't agree with most of these arguments, except the first one, but that one is convincing enough! So yeah let's make these defs.