Problem proving statements about graphs

Stream: new members

[Leo Shine]

Hi, I'm trying to prove a theorem saying that if a graph is acyclic then it is not 2-edge connected, (at least if there are at least 2 vertices...)

I would have thought this would be quite easy, all you have to do in informal maths, is suppose it was edge connected and acyclic take a path from one node to another, delete the first edge from that path from the graph, the 2-edge-connectedness implies there's still a path from one node to the other, so we get a second path, these paths can't be the same because they don't share a first edge, also its a mathlib theorem that paths between two nodes in an acyclic graphs are unique, so therefore we have a contradiction.

I'm sure I'm just interacting with lean in a horrible way, but the thing that I seem to be really strugglign to prove is that the two paths are not equal, this seems like it ought to be the simple part of the proof. In general how do people go about trying to deal with challenges like this, where a seemingly trivial step is difficult? And does anyone have any advice on ensuring you don't get really messy formalizations like the one below seems to be.

import Mathlib.Combinatorics.SimpleGraph.Acyclic
namespace SimpleGraph
variable {V V' : Type*} (G : SimpleGraph V) (G' : SimpleGraph V')
open Walk
def IsEdgeReachable (k : ℕ) (u v : V) : Prop :=
  ∀ ⦃s : Set (Sym2 V)⦄, s.encard < k → (G.deleteEdges s).Reachable u v

def IsEdgeConnected (k : ℕ) : Prop := ∀ u v, G.IsEdgeReachable k u v


theorem IsAcyclic.not_twoConnected (h : G.IsAcyclic) (u : V) (v : V) (hunev : u ≠ v)
    : ¬ G.IsEdgeConnected 2 := by
  by_contra hconn
  specialize hconn u v
  by_cases h2 : G.Reachable u v
  · obtain ⟨ p1: G.Walk u v, hp1⟩  := (Reachable.exists_isPath h2)
    match hp1eq : p1 with
    | nil => contradiction
    | cons' _ w vvv huw p =>
      let s1 := ({s(u,w)} : Set (Sym2 V))
      have hv : v = vvv:= by assumption
      subst hv
      have hsletwo : s1.encard < 2 := by
        unfold s1
        simp
      have hdeladj: ¬(G.deleteEdges s1).Adj u w :=by
            unfold s1
            unfold deleteEdges
            unfold Adj
            simp
            intro h3 h4
            rw [h4] at h3
            apply G.loopless w h3
      specialize hconn hsletwo
      obtain ⟨ p2: (G.deleteEdges s1).Walk u v, hp2⟩  := (Reachable.exists_isPath hconn)
      -- use isAcyclic_iff_path_unique paths then show path having removed an edge in the first path
      -- from the graph is not equal
      match hp2eq : p2 with
      | nil => contradiction
      | cons' _ w' vv huw' prst =>
        have wne : w' ≠ w:= by
          by_contra hweq
          rw[← hweq] at hdeladj
          contradiction
        let p3 := p2.mapLe (deleteEdges_le s1)
        have hv : v = vv:= by assumption
        subst hv
        have hp2eq:  p2 = cons huw' prst := by
          cases hp2eq
          simp
        have hp1eq:  p1 = cons huw p := by
          cases hp1eq
          simp
        have hp1: p1.IsPath := by
          unfold cons' at hp1
          rw[hp1eq]
          assumption
        have hp3 : p3.IsPath := by
          refine (mapLe_isPath (deleteEdges_le s1)).mpr ?_
          unfold cons' at hp2
          rw[hp2eq]
          assumption
        rw[isAcyclic_iff_path_unique] at h
        specialize h ⟨p3, hp3⟩ ⟨p1, hp1⟩
        -- Now prove not the same
        have h: p3 = p1 := by simpa using h
        rw[← h] at hp1eq
        unfold p3 at hp1eq
        rw[hp2eq] at hp1eq
        unfold mapLe at hp1eq
        unfold Walk.map at hp1eq
        sorry
  · have hempt: (∅ : Set (Sym2 V)).encard < 2 := by
      simp
    specialize hconn  hempt
    rw[deleteEdges_empty] at hconn
    contradiction

[Vlad Tsyrklevich]

import Mathlib.Combinatorics.SimpleGraph.Acyclic
namespace SimpleGraph
variable {V V' : Type*} (G : SimpleGraph V) (G' : SimpleGraph V')
open Walk
def IsEdgeReachable (k : ℕ) (u v : V) : Prop :=
  ∀ ⦃s : Set (Sym2 V)⦄, s.encard < k → (G.deleteEdges s).Reachable u v

def IsEdgeConnected (k : ℕ) : Prop := ∀ u v, G.IsEdgeReachable k u v

theorem IsAcyclic.not_twoConnected (h : G.IsAcyclic) (u : V) (v : V) (hunev : u ≠ v)
    : ¬ G.IsEdgeConnected 2 := by
  simp [IsEdgeConnected, IsEdgeReachable]
  by_cases h' : ∃ w : V, G.Adj u w
  · obtain ⟨w, hadj⟩ := h'
    have := SimpleGraph.isAcyclic_iff_forall_adj_isBridge.mp h hadj
    have : ¬(G.deleteEdges {s(u, w)}).Reachable u w := this.2
    exact ⟨u, w, {s(u, w)}, by simp, this⟩
  · refine ⟨u, v, ∅, by simp, ?_⟩
    simp at ⊢ h'
    by_contra hh
    obtain ⟨w⟩ := hh
    exact h' w.snd (w.adj_snd (not_nil_of_ne hunev))

[Vlad Tsyrklevich]

The IsBridge API already provides what you wanted, so it was easier to just use it rather than trying to re-derive its basic properties on the spot. I was reminded that isBridge existed by loogling for lemmas about acyclicity

[Vlad Tsyrklevich]

also JFYI the canonical spelling of (u : V) (v : V) (hunev : u ≠ v) is Nontrivial V

[Vlad Tsyrklevich]

Leo Shine said:

In general how do people go about trying to deal with challenges like this, where a seemingly trivial step is difficult?

The approach you take on pen-and-paper is not always what makes the most sense in formalization. Searching the library for what's available to you should inform how you approach the proof.

When something is painful it often means you want some more basic piece of API. That might mean proving more basic facts about IsEdgeReachable/Connected, or in this case you want some basic API about deleting edges disconnecting a graph. In this case it happened to already exist, but often times it helps to step back and ask yourself "What is the general statement that would solve the problem I am having right now?" and often times it can be easier and cleaner to prove the more general statement rather than your specific instance.

[Kevin Buzzard]

i.e. "seek the right abstraction".

[Leo Shine]

Thanks ill look at this this evening

[Leo Shine]

Okay had a look at this, and this is really helpful thank you for the help