Documentation

Archive.Wiedijk100Theorems.Konigsberg

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 :

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

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

Instances For

instance Konigsberg.instDecidableEqVerts :

DecidableEq Verts

Equations

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

instance Konigsberg.instFintypeVerts :

Equations

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

def Konigsberg.edges :

List (Verts × 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.

Instances For

def Konigsberg.adj (v w : Verts) :

The adjacency relation for the Königsberg graph.

Equations

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

Instances For

def Konigsberg.graph :

SimpleGraph Verts

The Königsberg graph structure. While the Königsberg bridge problem is usually described using a multigraph, 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_5, loopless := Konigsberg.graph._proof_6 }

Instances For

@[simp]

theorem Konigsberg.graph_adj (v w : Verts) :

graph.Adj v w = (adj v w = true)

instance Konigsberg.instDecidableRelVertsAdjGraph :

DecidableRel graph.Adj

Equations

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

def Konigsberg.degree :

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

Equations

Instances For

@[simp]

theorem Konigsberg.degree_eq_degree (v : Verts) :

graph.degree v = degree v

theorem Konigsberg.not_even_degree_iff (w : Verts) :

¬Even (degree w) ↔ w = Verts.V1 ∨ w = Verts.V2 ∨ w = Verts.V3 ∨ w = Verts.V4

theorem Konigsberg.setOf_odd_degree_eq :

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

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

The Königsberg graph is not Eulerian.