Grace/Cumulus/GraphTheory/Walks.g17

Open in Workbench Download source

Imports

Basic

Declarations

• TwoStep predicate
• TwoStep.intro theorem derivation
• TwoStep.bounds theorem derivation
• TwoStep.symmetric theorem derivation
• TwoStep.common_neighbor theorem derivation
• TwoStep.of_common_neighbor theorem derivation
• TwoStep.backtrack theorem derivation
• Triangle predicate
• Triangle.distinct theorem derivation
• Triangle.rotate theorem derivation
• Triangle.reverse theorem derivation
• Triangle.two_step theorem derivation
• Triangle.of_two_step theorem derivation
• Triangle.subgraph theorem derivation

Source

1-- Short walks and triangles in simple graphs2-- 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.Walks8import Basic910predicate TwoStep (V E x y : Set) :=11  ∃ z ∈ V, Adjacent(E, x, z) ∧ Adjacent(E, z, y)1213theorem TwoStep.intro (V E x y z : Set)14  requires hz : z ∈ V15  requires first : Adjacent(E, x, z)16  requires second : Adjacent(E, z, y)17  shows TwoStep(V, E, x, y)18proof19  unfold TwoStep20  refine ⟨z, hz, first, second⟩2122theorem TwoStep.bounds (V E x y : Set)23  requires graph : SimpleGraph(V, E)24  requires walk : TwoStep(V, E, x, y)25  shows x ∈ V ∧ y ∈ V26proof27  rcases walk with ⟨z, hz, first, second⟩28  have firstBounds := Adjacent.bounds with graph, first29  have secondBounds := Adjacent.bounds with graph, second30  rcases firstBounds with ⟨hx, hz2⟩31  rcases secondBounds with ⟨hz3, hy⟩32  refine ⟨hx, hy⟩3334theorem TwoStep.symmetric (V E x y : Set)35  requires graph : SimpleGraph(V, E)36  requires walk : TwoStep(V, E, x, y)37  shows TwoStep(V, E, y, x)38proof39  rcases walk with ⟨z, hz, first, second⟩40  have back := Adjacent.symmetric with graph, second41  have front := Adjacent.symmetric with graph, first42  exact TwoStep.intro with hz, back, front4344theorem TwoStep.common_neighbor (V E x y : Set)45  requires walk : TwoStep(V, E, x, y)46  shows ∃ z ∈ neighbors(V, E, x), Adjacent(E, z, y)47proof48  rcases walk with ⟨z, hz, first, second⟩49  have member : z ∈ neighbors(V, E, x) := neighbors.membership.backward with ⟨hz, first⟩50  refine ⟨z, member, second⟩5152theorem TwoStep.of_common_neighbor (V E x y : Set)53  requires common : ∃ z ∈ neighbors(V, E, x), Adjacent(E, z, y)54  shows TwoStep(V, E, x, y)55proof56  rcases common with ⟨z, member, second⟩57  obtain ⟨hz, first⟩ := neighbors.membership.forward with member58  exact TwoStep.intro with hz, first, second5960theorem TwoStep.backtrack (V E x y : Set)61  requires graph : SimpleGraph(V, E)62  requires edge : Adjacent(E, x, y)63  shows TwoStep(V, E, x, x)64proof65  obtain ⟨hx, hy⟩ := Adjacent.bounds with graph, edge66  have reverse := Adjacent.symmetric with graph, edge67  exact TwoStep.intro with hy, edge, reverse6869predicate Triangle (E x y z : Set) :=70  Adjacent(E, x, y) ∧ Adjacent(E, y, z) ∧ Adjacent(E, z, x)7172theorem Triangle.distinct (V E x y z : Set)73  requires graph : SimpleGraph(V, E)74  requires triangle : Triangle(E, x, y, z)75  shows x ≠ y ∧ y ≠ z ∧ z ≠ x76proof77  rcases triangle with ⟨xy, yz, zx⟩78  have dxy := Adjacent.distinct with graph, xy79  have dyz := Adjacent.distinct with graph, yz80  have dzx := Adjacent.distinct with graph, zx81  refine ⟨dxy, dyz, dzx⟩8283theorem Triangle.rotate (E x y z : Set)84  requires triangle : Triangle(E, x, y, z)85  shows Triangle(E, y, z, x)86proof87  rcases triangle with ⟨xy, yz, zx⟩88  unfold Triangle89  refine ⟨yz, zx, xy⟩9091theorem Triangle.reverse (V E x y z : Set)92  requires graph : SimpleGraph(V, E)93  requires triangle : Triangle(E, x, y, z)94  shows Triangle(E, x, z, y)95proof96  rcases triangle with ⟨xy, yz, zx⟩97  have xz := Adjacent.symmetric with graph, zx98  have zy := Adjacent.symmetric with graph, yz99  have yx := Adjacent.symmetric with graph, xy100  unfold Triangle101  refine ⟨xz, zy, yx⟩102103theorem Triangle.two_step (V E x y z : Set)104  requires graph : SimpleGraph(V, E)105  requires triangle : Triangle(E, x, y, z)106  shows TwoStep(V, E, x, z)107proof108  rcases triangle with ⟨xy, yz, zx⟩109  obtain ⟨hx, hy⟩ := Adjacent.bounds with graph, xy110  exact TwoStep.intro with hy, xy, yz111112theorem Triangle.of_two_step (V E x y : Set)113  requires graph : SimpleGraph(V, E)114  requires walk : TwoStep(V, E, x, y)115  requires closing : Adjacent(E, y, x)116  shows ∃ z ∈ V, Triangle(E, x, z, y)117proof118  rcases walk with ⟨z, hz, first, second⟩119  have triangle : Triangle(E, x, z, y)120    unfold Triangle121    refine ⟨first, second, closing⟩122  refine ⟨z, hz, triangle⟩123124theorem Triangle.subgraph (V E W F x y z : Set)125  requires sub : Subgraph(V, E, W, F)126  requires triangle : Triangle(F, x, y, z)127  shows Triangle(E, x, y, z)128proof129  rcases triangle with ⟨xy, yz, zx⟩130  have exy := Subgraph.adjacent with sub, xy131  have eyz := Subgraph.adjacent with sub, yz132  have ezx := Subgraph.adjacent with sub, zx133  unfold Triangle134  refine ⟨exy, eyz, ezx⟩135