Grace/Cumulus/GraphTheory/Konigsberg.g17

Open in Workbench Download source

Imports

Multigraph · Nat.Mod

Declarations

Source

1-- The seven bridges of Königsberg, with distinct bridge identities.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.GraphTheory.Konigsberg8import Multigraph9import Nat.Mod1011-- Endpoint table follows Grant Passmore's Imandra Top 100 development:12-- https://github.com/imandra-ai/imandra-100-theorems/blob/main/src/konigsberg.iml13-- Regions 0,1,2,3 represent L1,L2,I1,I2; bridge i represents B(i+1).14-- Edges: (0,2), (0,2), (0,3), (1,2), (1,2), (1,3), (2,3).1516theorem bridge_cases (i : Set)17  shows i ∈ 7 ↔ (i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6)18proof19  have s1 := membership.successor_set{n := 1} at i with *20  have s2 := membership.successor_set{n := 2} at i with *21  have s3 := membership.successor_set{n := 3} at i with *22  have s4 := membership.successor_set{n := 4} at i with *23  have s5 := membership.successor_set{n := 5} at i with *24  have s6 := membership.successor_set{n := 6} at i with *25  have first := membership.one at i26  tauto2728theorem region029  shows 0 ∈ 430proof31  simp [next.natural, next.membership, Naturals.constructor.zero, Naturals.constructor.succ]3233theorem region134  shows 1 ∈ 435proof36  simp [next.natural, next.membership, Naturals.constructor.zero, Naturals.constructor.succ]3738theorem region239  shows 2 ∈ 440proof41  simp [next.natural, next.membership, Naturals.constructor.zero, Naturals.constructor.succ]4243theorem region344  shows 3 ∈ 445proof46  simp [next.natural, next.membership, Naturals.constructor.zero, Naturals.constructor.succ]4748def leftValue (i : Set) : Set :=49  chooseNat(equalNat(i, 6), 2,50    chooseNat(equalNat(i, 3), 1, chooseNat(equalNat(i, 4), 1, chooseNat(equalNat(i, 5), 1, 0))))5152def rightValue (i : Set) : Set :=53  chooseNat(equalNat(i, 2), 3, chooseNat(equalNat(i, 5), 3, chooseNat(equalNat(i, 6), 3, 2)))5455defgraph bridgeLeft (i ∈ 7) : 4 := leftValue(i)56proof57  have alternatives := bridge_cases.forward at i with member58  rcases alternatives with h0 | h1 | h2 | h3 | h4 | h5 | h659  . rw h060    have value : leftValue(0) = 061      compute62    rw value63    exact region064  . rw h165    have value : leftValue(1) = 066      compute67    rw value68    exact region069  . rw h270    have value : leftValue(2) = 071      compute72    rw value73    exact region074  . rw h375    have value : leftValue(3) = 176      compute77    rw value78    exact region179  . rw h480    have value : leftValue(4) = 181      compute82    rw value83    exact region184  . rw h585    have value : leftValue(5) = 186      compute87    rw value88    exact region189  . rw h690    have value : leftValue(6) = 291      compute92    rw value93    exact region29495defgraph bridgeRight (i ∈ 7) : 4 := rightValue(i)96proof97  have alternatives := bridge_cases.forward at i with member98  rcases alternatives with h0 | h1 | h2 | h3 | h4 | h5 | h699  . rw h0100    have value : rightValue(0) = 2101      compute102    rw value103    exact region2104  . rw h1105    have value : rightValue(1) = 2106      compute107    rw value108    exact region2109  . rw h2110    have value : rightValue(2) = 3111      compute112    rw value113    exact region3114  . rw h3115    have value : rightValue(3) = 2116      compute117    rw value118    exact region2119  . rw h4120    have value : rightValue(4) = 2121      compute122    rw value123    exact region2124  . rw h5125    have value : rightValue(5) = 3126      compute127    rw value128    exact region3129  . rw h6130    have value : rightValue(6) = 3131      compute132    rw value133    exact region3134135theorem graph136  shows Multigraph.Graph(4, 7, bridgeLeft, bridgeRight)137proof138  unfold Multigraph.Graph139  refine ⟨bridgeLeft.function, bridgeRight.function⟩140141theorem leftValue.table142  shows leftValue(0) = 0 ∧ leftValue(1) = 0 ∧ leftValue(2) = 0 ∧ leftValue(3) = 1 ∧ leftValue(4) = 1 ∧ leftValue(5) = 1 ∧ leftValue(6) = 2143proof144  refine ⟨_, _, _, _, _, _, _⟩145  . compute146  . compute147  . compute148  . compute149  . compute150  . compute151  . compute152153theorem rightValue.table154  shows rightValue(0) = 2 ∧ rightValue(1) = 2 ∧ rightValue(2) = 3 ∧ rightValue(3) = 2 ∧ rightValue(4) = 2 ∧ rightValue(5) = 3 ∧ rightValue(6) = 3155proof156  refine ⟨_, _, _, _, _, _, _⟩157  . compute158  . compute159  . compute160  . compute161  . compute162  . compute163  . compute164165-- The complete degree table, with each bridge identity counted separately.166theorem degree_formula (x : Set)167  shows Multigraph.incidences(bridgeLeft, bridgeRight, identity(7), x, 7) =168    add(add(mul(3, indicator({x}, 0)), mul(3, indicator({x}, 1))),169      add(mul(5, indicator({x}, 2)), mul(3, indicator({x}, 3))))170proof171  have member0 : 0 ∈ 7172    have shape := bridge_cases at 0173    have same : 0 = 0 by rfl174    tauto175  have member1 : 1 ∈ 7176    have shape := bridge_cases at 1177    have same : 1 = 1 by rfl178    tauto179  have member2 : 2 ∈ 7180    have shape := bridge_cases at 2181    have same : 2 = 2 by rfl182    tauto183  have member3 : 3 ∈ 7184    have shape := bridge_cases at 3185    have same : 3 = 3 by rfl186    tauto187  have member4 : 4 ∈ 7188    have shape := bridge_cases at 4189    have same : 4 = 4 by rfl190    tauto191  have member5 : 5 ∈ 7192    have shape := bridge_cases at 5193    have same : 5 = 5 by rfl194    tauto195  have member6 : 6 ∈ 7196    have shape := bridge_cases at 6197    have same : 6 = 6 by rfl198    tauto199  obtain ⟨l0, l1, l2, l3, l4, l5, l6⟩ := leftValue.table200  obtain ⟨r0, r1, r2, r3, r4, r5, r6⟩ := rightValue.table201  simp [Multigraph.incidences, identity.apply, bridgeLeft.value, bridgeRight.value, mul, add.right_unit]202  ring203204theorem degree_land1205  shows Multigraph.incidences(bridgeLeft, bridgeRight, identity(7), 0, 7) = 3206proof207  rw degree_formula208  have different1 : 0 ≠ 1 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]209  have different2 : 0 ≠ 2 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]210  have different3 : 0 ≠ 3 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]211  simp [indicator.singleton_self, indicator.singleton_other]212213theorem degree_land2214  shows Multigraph.incidences(bridgeLeft, bridgeRight, identity(7), 1, 7) = 3215proof216  rw degree_formula217  have different0 : 1 ≠ 0218    have reversed : 0 ≠ 1 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]219    intro same220    cc221  have different2 : 1 ≠ 2 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]222  have different3 : 1 ≠ 3 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]223  simp [indicator.singleton_self, indicator.singleton_other]224225theorem degree_island1226  shows Multigraph.incidences(bridgeLeft, bridgeRight, identity(7), 2, 7) = 5227proof228  rw degree_formula229  have different0 : 2 ≠ 0230    have reversed : 0 ≠ 2 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]231    intro same232    cc233  have different1 : 2 ≠ 1234    have reversed : 1 ≠ 2 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]235    intro same236    cc237  have different3 : 2 ≠ 3 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]238  simp [indicator.singleton_self, indicator.singleton_other]239240theorem degree_island2241  shows Multigraph.incidences(bridgeLeft, bridgeRight, identity(7), 3, 7) = 3242proof243  rw degree_formula244  have different0 : 3 ≠ 0245    have reversed : 0 ≠ 3 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]246    intro same247    cc248  have different1 : 3 ≠ 1249    have reversed : 1 ≠ 3 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]250    intro same251    cc252  have different2 : 3 ≠ 2253    have reversed : 2 ≠ 3 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]254    intro same255    cc256  simp [indicator.singleton_self, indicator.singleton_other]257258-- No start, finish, length, or ordering can traverse every bridge exactly once.259theorem no_euler_trail (edges vertices : Set, n : Nat)260  shows ¬Multigraph.EulerTrail(4, 7, bridgeLeft, bridgeRight, edges, vertices, n)261proof262  have enumeration := identity.bijective at 7263  have distinct01 : 0 ≠ 1 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]264  have distinct03 : 0 ≠ 3 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]265  have distinct13 : 1 ≠ 3 by simp [Naturals.disjoint.zero.succ, Naturals.injective.succ]266  have degree0 : Odd(Multigraph.incidences(bridgeLeft, bridgeRight, identity(7), 0, 7))267    rw degree_land1268    exact Odd.three269  have degree1 : Odd(Multigraph.incidences(bridgeLeft, bridgeRight, identity(7), 1, 7))270    rw degree_land2271    exact Odd.three272  have degree3 : Odd(Multigraph.incidences(bridgeLeft, bridgeRight, identity(7), 3, 7))273    rw degree_island2274    exact Odd.three275  exact Multigraph.EulerTrail.three_odd_obstruction at 4, 7, bridgeLeft, bridgeRight,276    edges, vertices, identity(7), 0, 1, 3, n, 7 with *277278279theorem no_euler_trail_exists280  shows ¬(∃ n ∈ ℕ, ∃ edges, ∃ vertices,281    Multigraph.EulerTrail(4, 7, bridgeLeft, bridgeRight, edges, vertices, n))282proof283  intro exists284  rcases exists with ⟨n, member, edges, vertices, trail⟩285  have natural := nat.omega.backward with member286  exact no_euler_trail with trail287