Cycle within circuit

Stream: graph theory

[Kiril Vinogradov]

Hi all, apologies if this question is trivial but I have not been able to locate a proof within Mathlib for the fact that every circuit must contain a cycle and was wondering if either there’s a specific reason that it hasn’t been implemented or if I’m just being silly and missing it somewhere? Thanks in advance.

[Rida Hamadani]

I believe we don't have it yet.

[John Talbot]

There is bypass in SimpleGraph.Path.lean

/-- Given a walk, produces a walk from it by bypassing subwalks between repeated vertices.
The result is a path, as shown in `SimpleGraph.Walk.bypass_isPath`.
This is packaged up in `SimpleGraph.Walk.toPath`. -/
def bypass {u v : V} : G.Walk u v → G.Walk u v

So if you start with a circuit (i.e. a non-nil closed walk with no repeated edges) then you could get a cycle as follows:

def shortcircuit {u : V} : G.Walk u u → G.Walk u u
  | nil => nil
  | cons ha p => cons ha p.bypass

[Chris Wong]

Ah, that extra match is the trick. I was confused before, because calling bypass on the entire circuit would just delete everything.

[Kiril Vinogradov]

Thank you, that's a great solution to creating a cycle from a circuit, if I wanted to go about proving that this is a cycle, similar to bypass_isPath:

theorem shortcircuit_isCycle {u : V} (p : G.Walk u u) : p.shortcircuit.IsCycle := by
  sorry

I've found beginning this with an induction causes an issue with the repeated occurrence of u within the hypothesis p due to it's repetition. Whereas cases seems to go down the wrong rabbit hole. Is there something I'm missing here?

[John Talbot]

Induction for Walks uses the fact that a walk is either empty or is an edge + a shorter walk . This isn't true of closed walks which is why induction fails.

But you can use bypass_isPath with the following result to prove your theorem:

theorem cons_isCycle_iff {u v : V} (p : G.Walk v u) (h : G.Adj u v) :
    (Walk.cons h p).IsCycle ↔ p.IsPath ∧ ¬s(u, v) ∈ p.edges

[Kiril Vinogradov]

theorem shortcircuit_isCycle {u : V} (p : G.Walk u u) (h : p.IsCircuit ) : p.shortcircuit.IsCycle := by
  simp[shortcircuit]
  match p with
  | nil =>
    have := h.ne_nil
    contradiction
  | cons ha p =>
    simp[cons_isCycle_iff, bypass_isPath]

So far this is the structure I have for the theorem so far, which leads me to the goal of proving that the unordered edge (u, v) is not in the set of edges of the bypass, which I do believe to be a true statement possible of proving, but I just wanted to ask for a take on whether it's best to prove it within this theorem or to create a separate lemma that proves this fact for a bypass path using the assumption of the G.Adj u v+ and G.Walk v+ u that we have here, or whether I'm just being silly and missing something obvious.

[John Talbot]

Either would work, for example you could prove the lemma below and then use edges_bypass_subset which says that the edges of p.bypass are also edges of p to complete the proof of your theorem

lemma shortcircuit_cons_isCycle {u v : V} (h : G.Adj u v) (p : G.Walk v u)
    (hs : s(u,v) ∉ p.bypass.edges) : (cons h p).shortcircuit.IsCycle :=

[Kiril Vinogradov]

Hi all, just wanted to verify whether this seem like a valid proof for this and if there's anything I've missed.

theorem shortcircuit_isCycle {u v : V} (p : G.Walk u u) (h : p.IsCircuit ) : p.shortcircuit.IsCycle := by
  simp[shortcircuit]
  match p with
  | nil =>
    have := h.ne_nil
    contradiction
  | cons ha p =>
    simp[cons_isCycle_iff, bypass_isPath]
    simp[isCircuit_def, isTrail_def] at h
    have : p.bypass.edges ⊆ p.edges := by simp[edges_bypass_subset]
    apply Set.not_mem_subset this h.left

[Kyle Miller]

Lean accepts it, so it's valid :-)

Are you asking whether mathlib would accept it? The only real style things are (1) v is an unused variable, it can be removed, (2) the theorem statement line is over 100 characters, (3) I think isCycle_shortcircuit might fit in with the naming convention better, and (4) make sure to use simp? to turn those into simp onlys.

I'm sure the code could be refined more now that you have something working, but here's a start, with just the changes I suggested:

import Mathlib.Combinatorics.SimpleGraph.Path

namespace SimpleGraph
variable {V : Type*} [DecidableEq V] {G : SimpleGraph V}

namespace Walk

def shortcircuit {u : V} : G.Walk u u → G.Walk u u
  | nil => nil
  | cons ha p => cons ha p.bypass

theorem isCycle_shortcircuit {u : V} (p : G.Walk u u) (h : p.IsCircuit) :
    p.shortcircuit.IsCycle := by
  simp only [shortcircuit]
  match p with
  | nil =>
    have := h.ne_nil
    contradiction
  | cons ha p =>
    simp only [cons_isCycle_iff, bypass_isPath, true_and]
    simp only [isCircuit_def, isTrail_def, edges_cons, List.nodup_cons, ne_eq, reduceCtorEq,
      not_false_eq_true, and_true] at h
    have : p.bypass.edges ⊆ p.edges := by simp [edges_bypass_subset]
    apply Set.not_mem_subset this h.left

[Kyle Miller]

Here's a possible refinement:

theorem isCycle_shortcircuit {u : V} (p : G.Walk u u) (h : p.IsCircuit) :
    p.shortcircuit.IsCycle :=
  match p with
  | nil => absurd rfl h.ne_nil
  | cons (v := v) ha p => by
    contrapose h
    suffices s(u, v) ∈ p.edges by simp [isCircuit_def, this]
    have : s(u, v) ∈ p.bypass.edges := by
      simpa [shortcircuit, cons_isCycle_iff, bypass_isPath] using h
    exact (edges_bypass_subset p) this

[Kyle Miller]

I guess we can get match to reason about h.ne_nil for us:

theorem isCycle_shortcircuit {u : V} (p : G.Walk u u) (h : p.IsCircuit) :
    p.shortcircuit.IsCycle :=
  match p, h.ne_nil with
  | cons (v := v) ha p, _ => by
    contrapose h
    suffices s(u, v) ∈ p.edges by simp [isCircuit_def, this]
    have : s(u, v) ∈ p.bypass.edges := by
      simpa [shortcircuit, cons_isCycle_iff, bypass_isPath] using h
    exact (edges_bypass_subset p) this

[Kiril Vinogradov]

Yes that's definitely cleaner, thanks! I'll have a good look over the guidelines for Mathlib contribution and polish it up any further where I can.

[Kyle Miller]

Something that's missing here are helper lemmas to characterize what shortcircuit does. You might look at all the lemmas defined after Walk.bypass for inspiration.

If we do it right, isCycle_shortcircuit might just be a line or two.

[Kiril Vinogradov]

In regards to creating helper lemmas, the main thought I had was potentially creating a definition here parallel to the existing toPath definition but with a new abbrev definition of Cycle rather than Path just to round out the whole aim of showing that each circuit contains a cycle by giving this transformation. In my time toying with this idea I made this as a rough skeleton but am paranoid of having misconstrued something:

abbrev Cycle (u : V) := { p : G.Walk u u // p.IsCycle }

def toCycle {u : V} (p : G.Walk u u) (h: p.IsCircuit) : G.Cycle u  :=
  sorry

Any other helper lemmas that would help round this as a potential PR I would love advice on!