Graphic matroid

13 fully proved

Deleting a bridge adds one component

TheoremDeleting a bridge adds one component#✓fully proved

Let \(H\) be a simple graph on a finite vertex set and let \(ab\) be an edge of \(H\). If \(a\) and \(b\) are not connected in the graph obtained from \(H\) by deleting the edge \(ab\), then that graph has exactly one more connected component than \(H\).

theorem card_connectedComponent_deleteEdges_of_not_reachable [Finite V] (hab : H.Adj a b)
    (hbr : ¬ (H.deleteEdges {s(a, b)}).Reachable a b) :
    Nat.card (H.deleteEdges {s(a, b)}).ConnectedComponent =
      Nat.card H.ConnectedComponent + 1

Used by 1

Used byEdges plus components of a forest

Forests: edges plus components equal vertices

TheoremEdges plus components of a forest#✓fully proved

Let \(V\) be a finite vertex set. For every natural number \(n\) and every forest (acyclic simple graph) \(F\) on \(V\) with exactly \(n\) edges, the number of edges of \(F\) plus the number of connected components of \(F\) equals \(|V|\). So a forest on \(V\) with \(e\) edges has \(|V| - e\) connected components.

theorem ncard_edgeSet_add_card_connectedComponent [Finite V] :
    ∀ (n : ℕ) (F : SimpleGraph V), F.IsAcyclic → F.edgeSet.ncard = n →
      F.edgeSet.ncard + Nat.card F.ConnectedComponent = Nat.card V

Uses 1 · Used by 1

Proof usesDeleting a bridge adds one component

Used byAugmentation property of forests

Augmentation

TheoremAugmentation property of forests#✓fully proved

Let \(G\) be a simple graph on a finite vertex set, and let \(I\) and \(J\) be sets of edges of \(G\) that each form an acyclic graph. If \(|I| < |J|\), then there is an edge \(e \in J\) with \(e \notin I\) such that \(I \cup \{e\}\) still forms an acyclic graph.

theorem exists_insert_isAcyclic [Finite V] {G : SimpleGraph V} {I J : Set (Sym2 V)}
    (hIG : I ⊆ G.edgeSet) (hJG : J ⊆ G.edgeSet) (hI : (fromEdgeSet I).IsAcyclic)
    (hJ : (fromEdgeSet J).IsAcyclic) (hlt : I.ncard < J.ncard) :
    ∃ e ∈ J, e ∉ I ∧ (fromEdgeSet (insert e I)).IsAcyclic

Uses 1 · Used by 1

Proof usesEdges plus components of a forest

Used byGraphic matroid

The graphic matroid

DefinitionForests of a graph#✓fully proved

A set \(I\) of unordered pairs of vertices is a forest of a simple graph \(G\) when every element of \(I\) is an edge of \(G\) and the graph with edge set \(I\) has no cycles.

def IsForestSet (G : SimpleGraph V) (I : Set (Sym2 V)) : Prop :=
  I ⊆ G.edgeSet ∧ (fromEdgeSet I).IsAcyclic

Used by 4

Used byThe forest oracle decides graphic-matroid independence · Graphic matroid · Kruskal's algorithm returns a forest · Optimality of Kruskal's algorithm

DefinitionGraphic matroid#✓fully proved

For a simple graph \(G\) on a finite vertex set, the graphic matroid of \(G\) is the matroid on unordered pairs of vertices whose ground set is the edge set of \(G\) and whose independent sets are the forests of \(G\), that is, the sets of edges of \(G\) that form an acyclic graph.

That these sets form a matroid is CLRS Theorem 16.5.

noncomputable def graphicMatroid [Finite V] (G : SimpleGraph V) : Matroid (Sym2 V) :=
  (IndepMatroid.ofFinite (Set.toFinite G.edgeSet) (IsForestSet G)
    ⟨Set.empty_subset _, by simp⟩
    (fun _ _ hJ hIJ => ⟨hIJ.trans hJ.1, hJ.2.anti (SimpleGraph.fromEdgeSet_mono hIJ)⟩)
    (fun _ _ hI hJ hlt => by
      obtain ⟨e, heJ, heI, h⟩ := exists_insert_isAcyclic hI.1 hJ.1 hI.2 hJ.2 hlt
      exact ⟨e, heJ, heI, Set.insert_subset (hJ.1 heJ) hI.1, h⟩)
    (fun _ hI => hI.1)).matroid

Uses 2 · Used by 4

Statement usesForests of a graph · Augmentation property of forests

Used byThe forest oracle decides graphic-matroid independence · Kruskal's algorithm returns a maximal forest · Kruskal's algorithm returns a forest · Optimality of Kruskal's algorithm

An executable independence oracle

DefinitionGraph of a finite edge set#✓fully proved

The graph of a finite edge set, with decidable adjacency.

def chosen (T : Finset (Sym2 V)) : SimpleGraph V := fromEdgeSet ↑T

Used by 3

Used byBridge test for an edge set · Characterization of the bridge test · The forest oracle decides graphic-matroid independence

DefinitionBridge test for an edge set#✓fully proved

On a finite vertex set, for a finite set \(S\) of unordered pairs of vertices and a pair \(e = \{u, v\}\), the bridge test returns true exactly when \(u\) and \(v\) are not connected by a path in the graph whose edges are the non-loop pairs of \(S \setminus \{e\}\). When \(e \in S\) is not a loop, this says that \(e\) is a bridge of \(S\): deleting it disconnects its endpoints.

def bridgeIn (S : Finset (Sym2 V)) (e : Sym2 V) : Bool :=
  Sym2.lift ⟨fun u v => !decide ((chosen (S.erase e)).Reachable u v), fun u v => by
    simp only [SimpleGraph.reachable_comm]⟩ e

Uses 1 · Used by 3

Statement usesGraph of a finite edge set

Used byCharacterization of the bridge test · Forest oracle · The forest oracle decides graphic-matroid independence

TheoremCharacterization of the bridge test#✓fully proved

On a finite vertex set, let \(S\) be a finite set of unordered pairs of vertices and let \(u\), \(v\) be vertices. The bridge test of \(S\) on the pair \(\{u, v\}\) returns true if and only if \(u\) and \(v\) are not connected by a path in the graph whose edges are the non-loop pairs of \(S \setminus \{\{u, v\}\}\).

theorem bridgeIn_iff (S : Finset (Sym2 V)) (u v : V) :
    bridgeIn S s(u, v) = true ↔ ¬ (fromEdgeSet ↑(S.erase s(u, v))).Reachable u v

Uses 2

Statement usesBridge test for an edge set

Proof usesGraph of a finite edge set

DefinitionForest oracle#✓fully proved

For a simple graph \(G\) on a finite vertex set, the forest oracle accepts a finite set \(S\) of unordered pairs of vertices exactly when every \(e \in S\) is an edge of \(G\) and passes the bridge test in \(S\): its endpoints are not connected in the graph formed by the other pairs of \(S\). It serves as the independence oracle of the graphic matroid of \(G\), since a graph is a forest if and only if every edge is a bridge.

def forestOracle (S : Finset (Sym2 V)) : Bool :=
  decide (∀ e ∈ S, e ∈ G.edgeFinset ∧ bridgeIn S e = true)

Uses 1 · Used by 4

Statement usesBridge test for an edge set

Used byThe forest oracle decides graphic-matroid independence · Kruskal's algorithm returns a maximal forest · Kruskal's algorithm returns a forest · Optimality of Kruskal's algorithm

TheoremThe forest oracle decides graphic-matroid independence#✓fully proved

For a simple graph \(G\) on a finite vertex set and a finite set \(S\) of unordered pairs of vertices, the forest oracle of \(G\) accepts \(S\) if and only if \(S\) is independent in the graphic matroid of \(G\).

theorem forestOracle_iff (S : Finset (Sym2 V)) :
    forestOracle G S = true ↔ (graphicMatroid G).Indep ↑S

Uses 5 · Used by 3

Statement usesForest oracle · Graphic matroid

Proof usesForests of a graph · Bridge test for an edge set · Graph of a finite edge set

Used byKruskal's algorithm returns a maximal forest · Kruskal's algorithm returns a forest · Optimality of Kruskal's algorithm

Kruskal's algorithm as matroid greedy

TheoremKruskal's algorithm returns a forest#✓fully proved

Let \(G\) be a simple graph on a finite vertex type \(V\). For every list \(L\) of unordered pairs of vertices, the matroid greedy algorithm run on \(L\) with the forest oracle of \(G\) returns a forest of \(G\): a set of edges of \(G\) without cycles.

This is Kruskal's algorithm in the form of CLRS Section 16.4, the greedy algorithm on the graphic matroid.

theorem kruskal_isForest (es : List (Sym2 V)) :
    IsForestSet G ↑(matroidGreedy (forestOracle G) es).ret

Uses 6

Statement usesForests of a graph · Forest oracle · Greedy algorithm on a matroid

Proof usesThe forest oracle decides graphic-matroid independence · Graphic matroid · The matroid greedy result is independent

TheoremOptimality of Kruskal's algorithm#✓fully proved

Let \(G\) be a simple graph on a finite vertex type \(V\), let \(w\) assign a natural number to each unordered pair of vertices, and let \(L\) be a list of unordered pairs of vertices in nonincreasing order of \(w\) (each entry weighs at least as much as every later one). Let \(T\) be the set returned by the matroid greedy algorithm run on \(L\) with the forest oracle of \(G\). Then every forest \(I\) of \(G\) all of whose edges occur in \(L\) satisfies \(\sum_{x \in I} w(x) \le \sum_{x \in T} w(x)\).

This is CLRS Theorem 16.11 on the graphic matroid.

theorem kruskal_optimal (w : Sym2 V → ℕ) {es : List (Sym2 V)}
    (hsorted : es.Pairwise fun a b => w b ≤ w a) {I : Finset (Sym2 V)}
    (hI : IsForestSet G ↑I) (hIes : ∀ x ∈ I, x ∈ es) :
    ∑ x ∈ I, w x ≤ ∑ x ∈ (matroidGreedy (forestOracle G) es).ret, w x

Uses 6

Statement usesForests of a graph · Forest oracle · Greedy algorithm on a matroid

Proof usesThe forest oracle decides graphic-matroid independence · Graphic matroid · Optimality of the matroid greedy algorithm

TheoremKruskal's algorithm returns a maximal forest#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(L\) be a list of unordered pairs of vertices such that a pair is an edge of \(G\) if and only if it occurs in \(L\). Then the matroid greedy algorithm run with the forest oracle of \(G\) on \(L\) returns a base of the graphic matroid of \(G\), that is, a maximal forest of \(G\).

theorem kruskal_isBase {es : List (Sym2 V)} (hground : ∀ x, x ∈ G.edgeSet ↔ x ∈ es) :
    (graphicMatroid G).IsBase ↑(matroidGreedy (forestOracle G) es).ret

Uses 5

Statement usesForest oracle · Graphic matroid · Greedy algorithm on a matroid

Proof usesThe forest oracle decides graphic-matroid independence · The matroid greedy result is a base

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.