graph theory project

Stream: new members

[Lode Vermeulen]

Hi! The coming months I will be working on a project where I am looking to formalize some graph theory proofs in Lean. Currently, I am still getting to know the Lean language by looking at the existing SimpleGraph directory in Mathlib. Some of these are quite intimidating, so it would really help me if someone could answer some of my questions. Should I start a conversation for my project in #graph theory ?

[Damiano Testa]

I think that a new stream for each question in #new members is probably better.

[Lode Vermeulen]

Damiano Testa said:

I think that a new stream for each question in #new members is probably better.

In that case, I have a question about the first lemma I am working on, about the union of 2 perfect matchings being a disjoint union of cycles. I have the formalization, but I am getting stuck on trying to show that the resulting graph is 2-regular. Also, I am not sure how I would then translate this into it being a cycle.

/- Two disjoint perfect matchings -/
def IsDisjointPerfectMatchingPair (M₁ M₂ : Subgraph G) : Prop :=
M₁.IsPerfectMatching ∧ M₂.IsPerfectMatching ∧ M₁.edgeSet ∩ M₂.edgeSet = ∅

/- A graph with exclusively disjoint perfect matchings -/
def IsExclusivelyDisjointPMGraph (G : SimpleGraph V) : Prop :=
∀ (M₁ M₂ : Subgraph G), IsDisjointPerfectMatchingPair M₁ M₂

/- A graph that consists of a disjoint union of cycles -/
def IsCyclic (G : SimpleGraph V) : Prop := ∀ ⦃v : V⦄ (c : G.Walk v v), c.IsCycle

/- Two disjoint PMs form a union of cycles -/
lemma disjoint_PMs_form_union_of_cycles (M₁ M₂ : Subgraph G)
(hm : IsDisjointPerfectMatchingPair M₁ M₂) (hg : IsExclusivelyDisjointPMGraph G) :
IsCyclic (fromEdgeSet (M₁.edgeSet ∪ M₂.edgeSet)) := by
have hd : G.IsRegularOfDegree 2 := by sorry
sorry

[Yaël Dillies]

Note you could define

def IsDisjointPerfectMatchingPair (M₁ M₂ : Subgraph G) : Prop :=
  M₁.IsPerfectMatching ∧ M₂.IsPerfectMatching ∧ Disjoint M₁ M₂

[Yaël Dillies]

def IsExclusivelyDisjointPMGraph (G : SimpleGraph V) : Prop :=
  ∀ (M₁ M₂ : Subgraph G), IsDisjointPerfectMatchingPair M₁ M₂

is (almost) always false since

1. Most simple graphs have subgraphs which are not perfect matchings (eg the empty subgraph)
2. You don't forbid M₁ = M₂

[Yaël Dillies]

What you want is something like

def IsExclusivelyDisjointPMGraph (G : SimpleGraph V) : Prop :=
  {M : Subgraph G | M.IsPerfectMatching}.PairwiseDisjoint id

[Mitchell Lee]

If you want to write the condition that the graph G is the union of the two disjoint perfect matchings M₁ M₂ : Subgraph G, that would be M₁.IsPerfectMatching ∧ M₂.IsPerfectMatching ∧ IsCompl M₁ M₂. (See docs#IsCompl.) It might not be worth introducing a new definition for that.

[Mitchell Lee]

(Of course, you should use three separate hypotheses of types M₁.IsPerfectMatching, M₂.IsPerfectMatching, and IsCompl M₁ M₂ rather than one hypothesis of type M₁.IsPerfectMatching ∧ M₂.IsPerfectMatching ∧ IsCompl M₁ M₂.)

[Mitchell Lee]

I think your definition of IsCyclic is wrong. It states that every walk from a vertex to itself is a cycle. This isn't possible if the graph has any edges, because you can walk back and forth along that edge several times.

[Mitchell Lee]

Yaël Dillies said:

Note you could define

def IsDisjointPerfectMatchingPair (M₁ M₂ : Subgraph G) : Prop :=
  M₁.IsPerfectMatching ∧ M₂.IsPerfectMatching ∧ Disjoint M₁ M₂

Unfortunately, for M₁ M₂ : Subgraph G, I think that Disjoint M₁ M₂ means that M₁ and M₂ don't share any vertices, not that they don't share any edges. So this isn't what you want.

(In a perfect world, you could get around this problem by taking M₁ and M₂ to be of type SimpleGraph V instead. Then Disjoint M₁ M₂ would mean that M₁ and M₂ don't share any edges. But then you wouldn't have IsMatching or IsPerfectMatching. I think it would be nice to be able to use IsMatching on SimpleGraph V in addition to Subgraph G. See #11911.)

For now, you can use M₁.edgeSet ∩ M₂.edgeSet = ∅ or Disjoint M₁.edgeSet M₂.edgeSet.

[Lode Vermeulen]

Yaël Dillies said:

def IsExclusivelyDisjointPMGraph (G : SimpleGraph V) : Prop :=
  ∀ (M₁ M₂ : Subgraph G), IsDisjointPerfectMatchingPair M₁ M₂

is (almost) always false since

1. Most simple graphs have subgraphs which are not perfect matchings (eg the empty subgraph)
2. You don't forbid M₁ = M₂

I see, thanks for the correction

[Lode Vermeulen]

Mitchell Lee said:

I think your definition of IsCyclic is wrong. It states that every walk from a vertex to itself is a cycle. This isn't possible if the graph has any edges, because you can walk back and forth along that edge several times.

Right, that makes sense. I have adjusted it to impose that the walk should be a trail first:

/- A graph that consists of a disjoint union of cycles -/
def IsCyclic (G : SimpleGraph V) : Prop :=
∀ ⦃v : V⦄ (w : G.Walk v v), w.IsTrail → w.IsCycle

[Lode Vermeulen]

How I see it then, is that I have to show the following statements:

1. That a trail exists
2. The trail is nonempty
3. The trail starts and ends at the same vertex.
4. The only repeating vertex is the first one.
   Because point 2, 3 and 4 are the only differences between a trail and a cycle.

Does anyone know of any examples I can use in order to show these points?

[Yaël Dillies]

Lode Vermeulen said:

I have adjusted it to impose that the walk should be a trail first:

/- A graph that consists of a disjoint union of cycles -/
def IsCyclic (G : SimpleGraph V) : Prop :=
∀ ⦃v : V⦄ (w : G.Walk v v), w.IsTrail → w.IsCycle

You also need to assume w ≠ nil. nil is a trail but not a cycle.

[Lode Vermeulen]

Yaël Dillies said:

≠ nil

That makes sense. I guess that also removes one thing that needs to be shown from the lemma. Is there any way you could show me how to start proving this? I have tried looking at a bunch of similar Lean code, but I can't find a way to attack this.

[Rida Hamadani]

Can you please provide an #mwe? I couldn't figure out what imports, opens, variables, etc. you're using.

[Yaël Dillies]

Sorry, I don't have much time right now, but I will remark three more things

• fromEdgeSet (M₁.edgeSet ∪ M₂.edgeSet) is just M₁ ⊔ M₂
• IsCyclic is still wrongly stated because it currently allows vertices that don't lie on any cycle. I believe what you want is

def IsCyclic (G : SimpleGraph V) : Prop := ∀ ⦃v : V⦄, (∃ w : G.Walk v v, w ≠ nil) ∧ ∀ (w : G.Walk v v), w.IsTrail → w.IsCycle

• Your theorem is wrong because you haven't assumed V is finite. Without that assumption, you can at least prove that M₁ ⊔ M₂ is a disjoint union of cycles/two-sided infinite paths.

[Lode Vermeulen]

Rida Hamadani said:

Can you please provide an #mwe? I couldn't figure out what imports, opens, variables, etc. you're using.

Yes, my apologies, here is an instance of the lean web editor with all my code so far.

[Rida Hamadani]

The first thing that would come to mind is a plan like this:

lemma disjoint_PMs_form_union_of_cycles (M₁ M₂ : Subgraph G)
    (hm : IsDisjointPerfectMatchingPair M₁ M₂) : IsCyclic (fromEdgeSet (M₁.edgeSet ∪ M₂.edgeSet)) :=
  fun v => by
  refine ⟨?_, ?_⟩
  · obtain ⟨hm, -⟩ := hm
    rw [isPerfectMatching_iff] at hm
    obtain ⟨w, hw, -⟩ := hm v
    sorry
  · sorry

Now you have to find a way to use docs#SimpleGraph.Adj.toWalk with hw to construct the walk, and docs#SimpleGraph.Adj.ne to get v ≠ w, and finishing the first goal with docs#SimpleGraph.Walk.not_nil_of_ne.

P.S. I'm using @Yaël Dillies's definition of IsCyclic, but I couldn't replace fromEdgeSet (M₁.edgeSet ∪ M₂.edgeSet) with M₁ ⊔ M₂.

[Rida Hamadani]

I couldn't really figure out how to apply SimpleGraph theorems to Subgraph, I suppose there should be an easy way to do that?
Also by the way, in your link, you can remove import Mathlib.Combinatorics.SimpleGraph.Subgraph, since it is already included in SimpleGraph.Matching.

[Yaël Dillies]

Rida Hamadani said:

I couldn't replace fromEdgeSet (M₁.edgeSet ∪ M₂.edgeSet) with M₁ ⊔ M₂.

Hint: You want to use docs#SimpleGraph.fromEdgeSet_sup, docs#SimpleGraph.fromEdgeSet_edgeSet and some glue between SimpleGraph.edgeSet and SimpleGraph.Subgraph.edgeSet

[Mitchell Lee]

Hi, I think that [LocallyFinite G] isn't enough; the vertex set V actually needs to be finite.

[Mitchell Lee]

Another note: the definition of IsCyclic G you have is now equivalent to the statement that G is a disjoint union of cycles. However, you said that your goal is to prove that G is a disjoint union of cycles, not just to prove that G has a property that's equivalent to being a disjoint union of cycles. (After all, if you just wanted to do the latter, you could stop at proving that G is regular of degree 2.)

Here's one way of expressing it.

/- The graph `G` is a disjoint union of cycles -/
def IsDisjointUnionOfCycles (G : SimpleGraph V) : Prop :=
  ∃ P : Set (Subgraph G), -- There exists a set `P` of subgraphs of `G`, such that:
    P.Pairwise Disjoint -- The subgraphs are pairwise disjoint,
    ∧ sSup P = ⊤ -- The union of all of the subgraphs is the whole graph, and
    ∧ ∀ H ∈ P, ∃ (v : V) (c : G.Walk v v), c.IsCycle ∧ H = c.toSubgraph /- every subgraph `H ∈ P`
      consists of the vertices and edges of some cycle of `G`. -/

Another way to express this, which is less direct but probably easier for proofs, is to state that the induced subgraph on each connected component of G consists of the vertices and edges of a cycle of G.

/- The graph `G` is a disjoint union of cycles -/
def IsDisjointUnionOfCycles' (G : SimpleGraph V) : Prop :=
  ∀ H : G.ConnectedComponent, ∃ (v : V) (c : G.Walk v v), c.IsCycle ∧ Subgraph.induce ⊤ H = c.toSubgraph

[Lode Vermeulen]

Rida Hamadani said:

The first thing that would come to mind is a plan like this:...

Thanks a lot for this start! This helps a lot with my understanding of Lean as well :grinning_face_with_smiling_eyes: . After playing around with the code, I do have a some questions which I hope you could speak to and which would help me with understanding basic proofs in Lean:

1. The proof starts with a lambda function. Is this just to address that the following should hold for every v?
2. The documentation of refine states that it behaves like exact. In my experience, the exact tactic solves a goal if the types match. From what I can tell in this example, refine splits the goal into two subgoals. Furthermore, the ⟨⟩ brackets stand for pattern matching right? Which in this case is done without assigning a name, hence the anonymous 'dot notation'?
3. The obtain tactic seems to be used as a destructuring function in this example. Especially the second time it is used is confusing to me. Here, we somehow get hw: M₁.Adj v w from hm, which states that that shouldn't exist.
4. To address the first sorry, I tried, as you suggested, applying Adj.toWalk hw. From looking at the code for Adj.toWalk, this should work, as it is expecting an argument of type G.Adj u v, but it throws the error argument hw has type M₁.Adj v w : Prop but is expected to have type ?m.671.Adj ?m.672 ?m.673 : Prop. The only difference seems like M₁ is a SubGraph, but I am not sure whether this is the problem.
5. To try to address the second sorry, I tried fun w =>, but Lean says it is expecting a tactic. Do I not have to loop over all walks, like we also do with v?

[Lode Vermeulen]

Yaël Dillies said:

Rida Hamadani said:

I couldn't replace fromEdgeSet (M₁.edgeSet ∪ M₂.edgeSet) with M₁ ⊔ M₂.

Hint: You want to use docs#SimpleGraph.fromEdgeSet_sup, docs#SimpleGraph.fromEdgeSet_edgeSet and some glue between SimpleGraph.edgeSet and SimpleGraph.Subgraph.edgeSet

Is there a benefit of using ⊔ over ∪? It seems quite a hassle at this point, and, in my opinion, is little less readable.

[Lode Vermeulen]

Mitchell Lee said:

/- The graph `G` is a disjoint union of cycles -/
def IsDisjointUnionOfCycles (G : SimpleGraph V) : Prop :=
  ∃ P : Set (Subgraph G), -- There exists a set `P` of subgraphs of `G`, such that:
    P.Pairwise Disjoint -- The subgraphs are pairwise disjoint,
    ∧ sSup P = ⊤ -- The union of all of the subgraphs is the whole graph, and
    ∧ ∀ H ∈ P, ∃ (v : V) (c : G.Walk v v), c.IsCycle ∧ H = c.toSubgraph /- every subgraph `H ∈ P`
      consists of the vertices and edges of some cycle of `G`. -/

Thank you, this looks like a really robust way to define it! It might be beneficial to use this in the long run as well, as I intent to show the matchings form a Hamiltonian cycle when the graph is IsExclusivelyDisjointPMGraph (which I hope could then be as simple as proving Card P = 1).

[Mitchell Lee]

What do you mean by IsExclusivelyDisjointPMGraph?

[Lode Vermeulen]

Mitchell Lee said:

What do you mean by IsExclusivelyDisjointPMGraph?

It is defined at the top of this thread (note Yaël's correction as well).

[Mitchell Lee]

Can you describe it without using code? Currently the definition is expressing a property that's equivalent to the graph having at most one perfect matching. But I am not sure whether this is what you want because I can't figure out what "A graph with exclusively disjoint perfect matchings" means.

[Lode Vermeulen]

Maybe the code is not right, but it is supposed to represent the property that a graph has only disjoint perfect matchings. So a graph with 2 disjoint PMs and no other (non-disjoint) PMs would satisfy this property.

[Mitchell Lee]

I see. That shouldn't be necessary as a hypothesis of your theorem disjoint_PMs_form_union_of_cycles.

[Mitchell Lee]

Also, please see this MathOverflow page: https://mathoverflow.net/questions/267002/graphs-with-only-disjoint-perfect-matchings

[Lode Vermeulen]

Haha, this is actually the post which my project is based upon. See the following document where I worked out the math more formally.Bogdanov_s_lemma.pdf

[Lode Vermeulen]

Lode Vermeulen said:

Rida Hamadani said:

The first thing that would come to mind is a plan like this:...

Thanks a lot for this start! This helps a lot with my understanding of Lean as well :grinning_face_with_smiling_eyes: . After playing around with the code, I do have a some questions which I hope you could speak to and which would help me with understanding basic proofs in Lean:

1. The proof starts with a lambda function. Is this just to address that the following should hold for every v?
2. The documentation of refine states that it behaves like exact. In my experience, the exact tactic solves a goal if the types match. From what I can tell in this example, refine splits the goal into two subgoals. Furthermore, the ⟨⟩ brackets stand for pattern matching right? Which in this case is done without assigning a name, hence the anonymous 'dot notation'?
3. The obtain tactic seems to be used as a destructuring function in this example. Especially the second time it is used is confusing to me. Here, we somehow get hw: M₁.Adj v w from hm, which states that that shouldn't exist.
4. To address the first sorry, I tried, as you suggested, applying Adj.toWalk hw. From looking at the code for Adj.toWalk, this should work, as it is expecting an argument of type G.Adj u v, but it throws the error argument hw has type M₁.Adj v w : Prop but is expected to have type ?m.671.Adj ?m.672 ?m.673 : Prop. The only difference seems like M₁ is a SubGraph, but I am not sure whether this is the problem.
5. To try to address the second sorry, I tried fun w =>, but Lean says it is expecting a tactic. Do I not have to loop over all walks, like we also do with v?

Bumping this because it might have gotten buried.

[Rida Hamadani]

Lode Vermeulen said:

Bumping this because it might have gotten buried.

I've been away from my computer, I'll try to reply tonight, sorry for the late response.

[Lode Vermeulen]

Rida Hamadani said:

I've been away from my computer, I'll try to reply tonight, sorry for the late response.

That is completely fine, no rush, I was just worried that it had gotten buried.

[Mark Fischer]

I'm just starting out too! I'm sure you'll get more detailed answers still.

Re: question 1. I think you have it right.
Consider that:

λv ↦ by
  refine ...

Is very similar to

by
  intro v
  refine ...

Function abstraction is the term-level way to introduce an assumption or hypothesis, so you can use a tactic like intro, or just use function abstraction directly.

---

If the term introduced is part of a dependent type, then you sometimes say that what follows holds ∀ v

import Mathlib

example: (n : ℕ) → n < 1 → n = 0 := by
  intro n h
  linarith

example: (n : ℕ) → n < 1 → n = 0 :=
  λ n h ↦ by linarith

example: ∀n : ℕ, n < 1 → n = 0 := by
  intro n h
  linarith

example: ∀n : ℕ, n < 1 → n = 0 :=
  λ n h ↦ by linarith

though in cases like this, it's probably more common to see n and h as parameters already:

example (n : ℕ) (h : n < 1) : n = 0 := by linarith

[Rida Hamadani]

Lode Vermeulen said:

I do have a some questions:

1. Yes.
2. Yes, but I'm not sure about assigning names, never saw it in action. A quick test shows that you can assign a name and use dots anyways.
3. Yes. I think you confused "shouldn't exist" with "there exists a unique", because in programming languages ! stands for negation, but in math ∃!stands for existence with uniqueness.
4. You can use have hvw : G.Adj v w := hw.adj_sub to get G.Adj v w, however I've noticed now that my plan was wrong, because the walk that you need to show is not nil must be of the type w : Walk (fromEdgeSet (edgeSet M₁ ∪ edgeSet M₂)) v v. I didn't notice this at first.
5. Lean has a "term mode", and a "tactic mode". fun w => is a term, while intro w is a tactic.

Note that there was a job posting here years ago for formalizing what you are working on, check this, so I wonder if anybody ended up taking the offer and formalizing this.

[Mario Krenn]

Rida Hamadani said:

Note that there was a job posting here years ago for formalizing what you are working on, check this, so I wonder if anybody ended up taking the offer and formalizing this.

Indeed @Yaël Dillies with help of @Bhavik Mehta worked on this when i posted it. Time ran out at the time (mainly due to time-constraints of the fundings from my side), and it was not finished. But i shared all of the codes from that time with Lode.

[Yaël Dillies]

The biggest issue was that mathlib didn't have a proper notion of multigraphs at the time, so I worked a lot on figuring this out but nothing ended up in mathlib

[Rida Hamadani]

I think having multigraphs in mathlib would be neat, what are the challenges of porting them?

[Rida Hamadani]

I think having multigraphs in mathlib would be neat, what are the challenges of porting them?
(This message got double sent for some weird reason, sorry!)

[Lode Vermeulen]

Rida Hamadani said:

1. Yes....

Thanks a lot for these insights, they are really useful!

[Lode Vermeulen]

As the previous approach did not really work out, I have been looking into proving the lemma using the following definition:

Mitchell Lee said:

/- The graph `G` is a disjoint union of cycles -/
def IsDisjointUnionOfCycles (G : SimpleGraph V) : Prop :=
  ∃ P : Set (Subgraph G), -- There exists a set `P` of subgraphs of `G`, such that:
    P.Pairwise Disjoint -- The subgraphs are pairwise disjoint,
    ∧ sSup P = ⊤ -- The union of all of the subgraphs is the whole graph, and
    ∧ ∀ H ∈ P, ∃ (v : V) (c : G.Walk v v), c.IsCycle ∧ H = c.toSubgraph /- every subgraph `H ∈ P`
      consists of the vertices and edges of some cycle of `G`. -/

The first step of proving that a graph complies to this definition seems to me to be the most important. Constructing a set of subgraphs by alternating the edges added to a subgraph between the two PMs would naturally mean the subgraphs are disjoint and cycles.

See this document as well for more info about constructing these subgraphs (Lemma 3.2):
Bogdanov_s_lemma.pdf

Doing this in Python code would look something like this:

#Assumption: G is made with 2 disjoint PMs -> G is 2-regular
sub_graphs = []
for edge in G.edgeSet:
   edge_added = False
   for sub_graph in sub_graphs:
      if hasVertexInCommon(sub_graph, edge):
         sub_graph.append(edge)
         edge_added = True
         break
      if edge_added:
         continue
   subGraphs.append([edge])

My question: is it possible to define something similar in Lean? And could this actually lead to a simpler proof in Lean?

[Lode Vermeulen]

Yaël Dillies said:

What you want is something like

def IsExclusivelyDisjointPMGraph (G : SimpleGraph V) : Prop :=
  {M : Subgraph G | M.IsPerfectMatching}.PairwiseDisjoint id

I am finally getting around to using this definition, but I am struggling to see why this definition does not also say that the vertex sets of the Subgraphs are disjoint. How does Lean know that we are talking about the disjointness of the edgesets, rather than the vertex sets?

[Yaël Dillies]

As Mitchell mentioned above, this definition is indeed wrong because it should only require that the edge sets are disjoint. The correct definition is

def IsExclusivelyDisjointPMGraph (G : SimpleGraph V) : Prop :=
  {M : Subgraph G | M.IsPerfectMatching}.PairwiseDisjoint Subgraph.edgeSet