The Königsberg bridges problem

We show that a graph that represents the islands and mainlands of Königsberg and seven bridges between them has no Eulerian trail.

inductive Konigsberg.Verts : Type

The vertices for the Königsberg graph; four vertices for the bodies of land and seven vertices for the bridges.

• V1: Konigsberg.Verts
• V2: Konigsberg.Verts
• V3: Konigsberg.Verts
• V4: Konigsberg.Verts
• B1: Konigsberg.Verts
• B2: Konigsberg.Verts
• B3: Konigsberg.Verts
• B4: Konigsberg.Verts
• B5: Konigsberg.Verts
• B6: Konigsberg.Verts
• B7: Konigsberg.Verts

instance Konigsberg.instDecidableEqVerts : DecidableEq Konigsberg.Verts

Equations

• Konigsberg.instDecidableEqVerts x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Konigsberg.instFintypeVerts : Fintype Konigsberg.Verts

Equations

• Konigsberg.instFintypeVerts = { elems := { val := ↑Konigsberg.Verts.enumList, nodup := Konigsberg.Verts.enumList_nodup }, complete := Konigsberg.instFintypeVerts.proof_1 }

def Konigsberg.edges : List (Konigsberg.Verts × Konigsberg.Verts)

Each of the connections between the islands/mainlands and the bridges. These are ordered pairs, but the data becomes symmetric in Konigsberg.adj.

Equations

• One or more equations did not get rendered due to their size.

def Konigsberg.adj (v : Konigsberg.Verts) (w : Konigsberg.Verts) : Bool

The adjacency relation for the Königsberg graph.

Equations

• Konigsberg.adj v w = (decide ((v, w) ∈ Konigsberg.edges) || decide ((w, v) ∈ Konigsberg.edges))

@[simp]

theorem Konigsberg.graph_adj (v : Konigsberg.Verts) (w : Konigsberg.Verts) : Konigsberg.graph.Adj v w = (Konigsberg.adj v w = true)

def Konigsberg.graph : SimpleGraph Konigsberg.Verts

The Königsberg graph structure. While the Königsberg bridge problem is usually described using a multigraph, the we use a "mediant" construction to transform it into a simple graph -- every edge in the multigraph is subdivided into a path of two edges. This construction preserves whether a graph is Eulerian.

(TODO: once mathlib has multigraphs, either prove the mediant construction preserves the Eulerian property or switch this file to use multigraphs.

Equations

• Konigsberg.graph = { Adj := fun (v w : Konigsberg.Verts) => Konigsberg.adj v w = true, symm := Konigsberg.graph.proof_1, loopless := Konigsberg.graph.proof_2 }

instance Konigsberg.instDecidableRelVertsAdjGraph : DecidableRel Konigsberg.graph.Adj

Equations

• Konigsberg.instDecidableRelVertsAdjGraph a b = inferInstanceAs (Decidable (Konigsberg.adj a b = true))

def Konigsberg.degree : Konigsberg.Verts → ℕ

To speed up the proof, this is a cache of all the degrees of each vertex, proved in Konigsberg.degree_eq_degree.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Konigsberg.degree_eq_degree (v : Konigsberg.Verts) : Konigsberg.graph.degree v = Konigsberg.degree v

theorem Konigsberg.not_even_degree_iff (w : Konigsberg.Verts) : ¬Even (Konigsberg.degree w) ↔ w = Konigsberg.Verts.V1 ∨ w = Konigsberg.Verts.V2 ∨ w = Konigsberg.Verts.V3 ∨ w = Konigsberg.Verts.V4

theorem Konigsberg.setOf_odd_degree_eq : {v : Konigsberg.Verts | Odd (Konigsberg.graph.degree v)} = {Konigsberg.Verts.V1, Konigsberg.Verts.V2, Konigsberg.Verts.V3, Konigsberg.Verts.V4}

theorem Konigsberg.not_isEulerian {u : Konigsberg.Verts} {v : Konigsberg.Verts} (p : Konigsberg.graph.Walk u v) (h : p.IsEulerian) : False

The Königsberg graph is not Eulerian.