Treating SimpleGraph edges as Finset

Stream: Is there code for X?

[Christoph Spiegel]

Hi, I am having trouble proving even the most basic properties of edges in a SimpleGraph. Basically I would expect there to be some method that takes (e : Sym2) and (he : e ∈ G.edgeSet) and returns a Finset with two distinct vertices that are adjacent or at least two vertices that are members of e and that are Mem.other of each other, but I was unable to find anything and am struggling with how to handle Sym2. The only thing I managed is obtain ⟨v, w⟩ := e and have : G.Adj v w := by aesop, but v ∈ e and w ∈ eI cannot obtain.

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Data.Finset.Sym
import Aesop

variable {α : Type*} [Fintype α] [DecidableEq α]
variable {G : SimpleGraph α} [DecidableRel G.Adj]

-- Should follow by definition of Sym2
lemma t1 (e : Sym2 α) : Finset.card {v | v ∈ e} ≤ 2 := by sorry

-- Should follow by definition of Sym2 by simply picking one element out of it
lemma t2 (e : Sym2 α) : Finset.card {v | v ∈ e} ≥ 1 := by sorry

-- Should follow by irreflexivity of the edge relation in SimpleGraph
lemma t3 (e : Sym2 α) (he : e ∈ G.edgeSet) : Finset.card {v | v ∈ e} ≥ 2 := by
  obtain ⟨v, w⟩ := e
  have : G.Adj v w := by aesop
  have : v ≠ w := SimpleGraph.Adj.ne' (G.adj_symm this)
  sorry

example (e : Sym2 α) (he : e ∈ G.edgeSet) : Finset.card {v | v ∈ e} = 2 := Eq.symm (Nat.le_antisymm (t3 e he) (t1 e))

[Floris van Doorn]

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Data.Finset.Sym

variable {α : Type*} [Fintype α] [DecidableEq α]
variable {G : SimpleGraph α} [DecidableRel G.Adj]

open Finset

example (e : Sym2 α) (he : e ∈ G.edgeSet) : Finset.card {v | v ∈ e} = 2 := by
  obtain ⟨v, w⟩ := e
  have hvw : G.Adj v w := by simp_rw [← SimpleGraph.mem_edgeSet, he]
  rw [card_eq_two]
  use v, w, hvw.ne
  ext; simp

[Floris van Doorn]

I think docs#Finset.card_eq_two was your main missing ingredient.

[Christoph Spiegel]

I was actually aware of this bit didn't try to apply it this because it did not occur to me that simp could resolve this if it isn't able to resolve v ∈ e, w ∈ e, and s(v,w) = e. I think obtain works differently than I expected since it replaces e with s(v,w) in the objective, but does keep e around in the assumptions (now seemingly disjoint from anything else)?

[Floris van Doorn]

induction e with | h v w => is probably a better spelling of obtain ⟨v, w⟩ := e. The former removes e from the context and uses the nicer notation s(v, w).

[Christoph Spiegel]

Maybe more of a meta question: what is the motivation behind defining graphs through an adjacency relationship. Deriving the set notion from this still feels clumsy and once one moves to hypergraphs, multi-edges, and directed graphs the adjacency notion seems to me the less natural one. Defining it based on (multi)sets with cardinality conditions if one enforces uniformity / loop-lessnes and deriving an adjacency relationship only for the particular case of loopless simple graphs through membership of two distinct vertices in some edge is what I would have expected to be the underlying notion. But I might be missing something here.

[Christoph Spiegel]

@Floris van Doorn yeah, that makes sense. Wanting to prove v ∈ e is nonsensical since e basically doesn't exist anymore and has been replaced by s(v,w), so membership is taken care of by Sym2.mem_mk_left and Sym2.mem_mk_right as expected.

[Kevin Buzzard]

There are lots of ways to write a foundation for graph theory, and it might well be one of those situations where you can't please all of the people all of the time. It seems to me that the word "graph" is used in many different ways in the literature, and this only compounds the problem -- people come along who are used to their kind of graphs, and find that mathlib's is different, and this is already a source of frustration.

[Floris van Doorn]

For a long time we didn't have any graph theory library, because we weren't sure in what generality we should set it up (multigraphs, (un)directed graphs, ...). At some point @Kyle Miller and others decided to just go ahead defining simple graphs and we got a graph library based on that.
Note that a multigraph is just an element of V → V → Type*, which you can find under docs#Quiver

[Christoph Spiegel]

I understand that. The adjacency notion feels more like the CS / DO / OR point of view and closer to how graphs were "originally" defined. Papers from the early 20th century will always talk about points with a relationship, rather than a set of edges that is a subset of the powerset. The set notion (which perhaps generalizes more easily to hypergraphs) seems to be more popular with the Extremal Combinatorics crowd and started somewhat later.

[Christoph Spiegel]

How difficult is it to maintain competing notions with a translation / bijection layer? One could define them both ways and then have a statement that converts from one into the other, which would allow one to pull results established for either notion to the other one. I am not sure how neatly this can be done in LEAN though and if this still aligns with the mathlib principles (probably not).

[Christoph Spiegel]

The formalization of the Sensitivity conjecture also went its own way and just picked one view of the hypercube that worked best for the linear algebra proof, i.e., vertices as 0-1-vectors as opposed to the poset lattice. Graphs seem to be particularly messy like that and people just freely switch between several different but isomorphic definitions in their papers based on what happens to be cleaner... seems to be a challenge to find a common ground for that in some general library like mathlib.

[Vincent Beffara]

One could define a GraphLike typeclass covering several implementations, with a chosen short-list of features constituting the API (and then prove things on the abstract version whenever it is possible). But it is not clear how possible it is to abstract away the basic definitions.

[Christoph Spiegel]

Back to the original question, using the suggestion of @Floris van Doorn one can at least make the proof somewhat less obscure and more compact as follows:

  rw [Finset.card_eq_two]
  induction e with | _ v w =>
    use v, w, (by aesop)
    ext; simp

This still seems too much work for "an edge contains two distinct vertices" but given the current notion of SimpleGraph this is perhaps the cleanest way to establish that.

[Kevin Buzzard]

Counting is hard in a formal system. I thought that group theory would be easy and then I looked at what we were teaching the undergraduates and it was all about finite groups, which made things much more fiddly.

[Kyle Miller]

@Christoph Spiegel Think about SimpleGraph as being the abstract interface for simple graphs, it's not the definition of a graph. Any particular concrete example can be worked with by creating a function from the data of the graph to the SimpleGraph and then proving things about it there.

For example, https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Konigsberg.lean creates some inductive types with the graph data, it's linked up to SimpleGraph with the graph definition, and then there are lemmas doing some computations.

[Kyle Miller]

Here's another version of Floris's proof:

example (e : Sym2 α) (he : e ∈ G.edgeSet) : Finset.card {v | v ∈ e} = 2 := by
  rw [card_eq_two]
  induction e with | _ x y =>
  use x, y, he.ne
  ext; simp

The definition of G.edgeSet is set up so that s(x, y) ∈ G.edgeSet is definitionally equal to G.Adj x y.

[Kyle Miller]

Can you say a bit about what you are working on @Christoph Spiegel, where you need to know the cardinality of edges as sets?

[Kyle Miller]

You might also like to know about docs#SimpleGraph.fromEdgeSet, which is a different constructor for SimpleGraph that gives the set-of-edges point of view.

One of the reasons SimpleGraph is an adjacency relation rather than a set-of-edges is that it's much easier writing proofs about an adjacency relation. Working with Sym2 is a bit of a pain in comparison, though it's doable.

[Christoph Spiegel]

@Kyle Miller So very concretely I wanted to type up the Cauchy-Schwarz proof of Mantel's Theorem, for which I first wanted (mostly as an exercise to get familiar with mathlib's notion of SimpleGraph) to prove the Handshake Lemma. I know it is already implemented, but I wanted to see a version that more closely mimics what you would see in the first week of any graph theory course instead of something that abstracts a lot of things away; I had never heard about darts in the context of graph theory prior to seeing it in mathlib.

[Christoph Spiegel]

This is currently the cleanest I could come up with and it requires the proof that an edge contains two vertices:

import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Combinatorics.Enumerative.DoubleCounting

variable {α : Type*} [Fintype α] [DecidableEq α]
variable {G : SimpleGraph α} [DecidableRel G.Adj]

prefix:100 "#" => Finset.card
local notation "E" => G.edgeFinset
local notation "d(" v ")" => G.degree v
local notation "I(" v ")" => G.incidenceFinset v

lemma edge_card_eq_two (e : Sym2 α) (he : e ∈ E): #{v | v ∈ e} = 2 := by
  rw [Finset.card_eq_two]
  induction e with | _ v w => use v, w, (by aesop); ext; simp

-- Proof through direct calculation
lemma handshaking : ∑ v, d(v) = 2 * #E := by
  calc  ∑ v, d(v)
    _ = ∑ v, #I(v)                := by simp [G.card_incidenceFinset_eq_degree]
    _ = ∑ v, #{e ∈ E | v ∈ e}     := by simp [G.incidenceFinset_eq_filter]
    _ = ∑ e ∈ E, #{v | v ∈ e}     := Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow _
    _ = ∑ e ∈ E, 2                := Finset.sum_congr rfl (λ e he ↦ edge_card_eq_two e he)
    _ = 2 * ∑ e ∈ E, 1            := (Finset.mul_sum E (λ _ ↦ 1) 2).symm
    _ = 2 * #E                    := by rw [Finset.card_eq_sum_ones E]

[Kyle Miller]

I'm not sure what you mean by "instead of something that abstracts something away" (the mathlib version tries to make the proof be very combinatorial: both sides of the equality count darts in a different way, where a dart is just an ordered pair of adjacent vertices instead of a non-ordered pair), but your proof is nice.

Lots of times with formalization you have to rethink how to prove something cleanly, so I was worried you were trying to force some edges-as-sets argument, but sums-and-indicator-functions-style arguments are a good justification for it.

[Kyle Miller]

These edge-cardinality theorems are clearly missing from mathlib. They're not there just because they haven't been needed yet.

[Christoph Spiegel]

That's good to know, then I'll PR at least edge_card_eq_two when I have a moment!

[Kyle Miller]

I started collecting some theory here: https://github.com/leanprover-community/mathlib4/pull/17587

I'd like edge_card_eq_two to be an immediate consequence of things from Sym2

[Christoph Spiegel]

Re abstracting away: mathlib in my (admittedly very limited) experience tends to abstract, dissect, and generalize as much as possible; this is absolutely the right thing to do, but can also make connecting ones math knowledge to what's in the library difficult. I am (perhaps misguidedly) therefore currently trying to write up some simple proofs as closely as possible to what one would find on paper in some lecture notes without introducing additional more abstract notions but still basing it on mathlib. This is partially for my own amusement and partially with the hopes that it might eventually make a good resource to make lean and mathlib more approachable for others. Think of it sort of half-way between The Natural Number Game and full on mathlib-level coding.

[Kyle Miller]

I think what you are doing is valuable, since that's how we find missing material. The main way new stuff gets added to the library is when someone tries to do something and runs into the inevitable gaps.

[Kyle Miller]

(Feel free to push edge_card_eq_two to that branch @Christoph Spiegel, we can refactor later)

[Christoph Spiegel]

Done, also defined Sym2.card as Sym2.toFinset.card. Hope that makes sense!

[Christoph Spiegel]

Or is there a more natural way to have any Finset definition apply to Sym2 by simply first applying toFinset?