[Merged by Bors] - feat(combinatorics/simple_graph/basic): add definition of complement of simple graph

[agusakov]

Add definition of the complement of a simple graph. Part of branch strongly_regular_graph, with the goal of proving facts about strongly regular graphs.

---

[eric-wieser]

Can you add a simp lemma that shows complement (complement g) = g?

[agusakov]

Done!

[kmill]

Other than adding the additional @[simp] attributes, 👍

[eric-wieser]

Instead of G.compl, does it make sense to use has_compl here and use the notation?

[kmill]

@eric-wieser Graphs do form a boolean_algebra under operations on the edge set (which would be implemented through boolean operations on the values of adj), so it wouldn't hurt to add a has_compl instance.

The two textbooks I have in front of me use overlines for complementation, but Gᶜ isn't uncommon.

[eric-wieser]

I'm starting to wonder if simple_graph should have been defined as set (edge V), so that the boolean algebra structure is automatic. Here, edge is just a subtype of sym2 that forbids reflexive objects.

[kmill]

@eric-wieser You can think of the current definition as being that but expanded out to not mention quotients or sets of subtypes. The following are equivalent:

• set (edge V)
• set {e : sym2 V // ¬e.is_diag}
• {s : set (sym2 V) // ∀ e ∈ s, ¬e.is_diag}
• {s : set (V × V) // ∀ e ∈ s, e.1 ≠ e.2 ∧ e.swap ∈ s}
• {s : V × V → Prop // ∀ e, s e → e.1 ≠ e.2 ∧ s e.swap}
• {s : V → V → Prop // irreflexive s ∧ symmetric s}

It tends to be easier to deal with this last form in proofs because it's all basic logic. Feel free to experiment, though, to see if it ends up being easier overall:

structure simple_graph' (V : Type u) :=
(edges : set {e : finset V // e.card = 2})

[eric-wieser]

It tends to be easier to deal with this last form in proofs because it's all basic logic.

Right, but it also means you don't have the entire set API automatically available to apply to graphs. Your first two definitions get that for free.

Of course, you can always pick one definition and then write an API to make it have the desirable properties of another definition - my claim is simply that the current choice requires more of this glue than other choices. But I don't have experience proving things about graphs so could be mistaken.

[b-mehta]

structure simple_graph' (V : Type u) :=
(edges : set {e : finset V // e.card = 2})

I've found that this particular version can be really awkward to work with, especially compared to the sym2 version which looks similar a priori

[eric-wieser]

I guess an equiv between graphs and set {e : sym2 V // ¬e.is_diag} would be enough to transfer the entire boolean algebra structure

[agusakov]

Should I add the equivalence and boolean_algebra instance to this PR?

[bryangingechen]

Should I add the equivalence and boolean_algebra instance to this PR?

If they're simple and straightforward (e.g. the fields are mostly 1-line proofs after golfing), yes. Otherwise you can add them to a PR that's dependent on this one.

[agusakov]

Should I add the equivalence and boolean_algebra instance to this PR?

If they're simple and straightforward (e.g. the fields are mostly 1-line proofs after golfing), yes. Otherwise you can add them to a PR that's dependent on this one.

I think I'm going to need to make it a separate PR - iirc the boolean algebra instance relies on definitions of subgraphs and such

[agusakov]

Also, for some reason compl_adj doesn't work (anymore?). Not sure how to fix that

[kmill]

I'd say hold off implementing the boolean algebra structure until you actually need it -- I'm not really sure where the full structure would even be used.

[bryangingechen]

Thanks!
bors r+

[eric-wieser]

iirc the boolean algebra instance relies on definitions of subgraphs and such

I'd look at this the other way - the boolean algebra gives you definitions of (edge-)subgraphs for free.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests