Grace/Cumulus/GraphTheory/Basic.g17

Open in Workbench Download source

Imports

Relation

Declarations

Source

1-- Simple graphs and their local structure2-- 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.Basic8import Relation910-- Edges are ordered pairs; symmetry makes their orientation immaterial.11predicate SimpleGraph (V E : Set) :=12  RelationOn(E, V) ∧ SymmetricOn(V, E) ∧ IrreflexiveOn(V, E)1314predicate Adjacent (E x y : Set) := relates(E, x, y)1516theorem SimpleGraph.relation (V E : Set)17  requires graph : SimpleGraph(V, E)18  shows RelationOn(E, V)19proof20  simp [SimpleGraph]2122theorem SimpleGraph.symmetric (V E : Set)23  requires graph : SimpleGraph(V, E)24  shows SymmetricOn(V, E)25proof26  simp [SimpleGraph]2728theorem SimpleGraph.irreflexive (V E : Set)29  requires graph : SimpleGraph(V, E)30  shows IrreflexiveOn(V, E)31proof32  simp [SimpleGraph]3334theorem Adjacent.bounds (V E x y : Set)35  requires graph : SimpleGraph(V, E)36  requires edge : Adjacent(E, x, y)37  shows x ∈ V ∧ y ∈ V38proof39  unfold Adjacent at edge40  have relation := SimpleGraph.relation with graph41  unfold RelationOn at relation42  exact RelationBetween.bounds with relation, edge4344theorem Adjacent.symmetric (V E x y : Set)45  requires graph : SimpleGraph(V, E)46  requires edge : Adjacent(E, x, y)47  shows Adjacent(E, y, x)48proof49  obtain ⟨hx, hy⟩ := Adjacent.bounds with graph, edge50  have symmetric := SimpleGraph.symmetric with graph51  unfold Adjacent52  exact symmetric with x, hx, y, hy, edge5354theorem Adjacent.distinct (V E x y : Set)55  requires graph : SimpleGraph(V, E)56  requires edge : Adjacent(E, x, y)57  shows x ≠ y58proof59  intro equal60  obtain ⟨hx, hy⟩ := Adjacent.bounds with graph, edge61  have noLoop := SimpleGraph.irreflexive with graph62  have contradiction := noLoop with x, hx63  rw ← equal at edge64  apply contradiction65  exact edge6667-- All neighbors lie in V; this is a set by separation.68def neighbors (V E x : Set) : Set := { y ∈ V | Adjacent(E, x, y) }6970theorem neighbors.symmetric (V E x y : Set)71  requires graph : SimpleGraph(V, E)72  requires hx : x ∈ V73  requires hy : y ∈ neighbors(V, E, x)74  shows x ∈ neighbors(V, E, y)75proof76  simp [neighbors.membership] at hy77  rcases hy with ⟨hyV, edge⟩78  apply neighbors.membership.backward79  constructor80  . exact hx81  . exact Adjacent.symmetric with graph, edge8283theorem neighbors.excludes_self (V E x : Set)84  requires graph : SimpleGraph(V, E)85  shows ¬(x ∈ neighbors(V, E, x))86proof87  intro member88  simp [neighbors.membership] at member89  rcases member with ⟨hx, edge⟩90  have distinct := Adjacent.distinct with graph, edge91  apply distinct92  rfl9394-- A subgraph can delete vertices and edges independently.95predicate Subgraph (V E W F : Set) :=96  SimpleGraph(W, F) ∧ W ⊆ V ∧ F ⊆ E9798theorem Subgraph.vertices (V E W F : Set)99  requires sub : Subgraph(V, E, W, F)100  shows W ⊆ V101proof102  simp [Subgraph]103104theorem Subgraph.edges (V E W F : Set)105  requires sub : Subgraph(V, E, W, F)106  shows F ⊆ E107proof108  simp [Subgraph]109110theorem Subgraph.adjacent (V E W F x y : Set)111  requires sub : Subgraph(V, E, W, F)112  requires edge : Adjacent(F, x, y)113  shows Adjacent(E, x, y)114proof115  have included := Subgraph.edges with sub116  unfold Adjacent at edge117  unfold Adjacent118  unfold relates119  exact included with (x, y), edge120121-- Restriction to a vertex set keeps precisely the edges with both ends there.122def inducedEdges (E W : Set) : Set := E ∩ (W × W)123124theorem inducedEdges.membership (E W x y : Set)125  shows relates(inducedEdges(E, W), x, y) ↔126    (relates(E, x, y) ∧ x ∈ W ∧ y ∈ W)127proof128  constructor129  . intro h130    unfold relates at h131    unfold inducedEdges at h132    simp [intersection.membership] at h133    rcases h with ⟨edge, pair⟩134    obtain ⟨bounded, a, ha, b, hb, equality⟩ := product.membership.forward with pair135    obtain ⟨xa, yb⟩ := orderedPair.injective with equality136    rw ← xa at ha137    rw ← yb at hb138    constructor139      exact edge140    . constructor141      . exact ha142      . exact hb143  . intro h144    rcases h with ⟨edge, hx, hy⟩145    unfold relates146    unfold inducedEdges147    apply intersection.membership.backward148    have pair := product.pair with hx, hy149    refine ⟨edge, pair⟩150151theorem inducedEdges.graph (V E W : Set)152  requires graph : SimpleGraph(V, E)153  requires vertices : W ⊆ V154  shows SimpleGraph(W, inducedEdges(E, W))155proof156  constructor157    intros p hp158    unfold inducedEdges at hp159    simp [intersection.membership] at hp160    rcases hp with ⟨edge, pair⟩161    exact pair162  . constructor163      intros x hx y hy edge164      obtain ⟨original, wx, wy⟩ := inducedEdges.membership.forward with edge165      have symmetric := SimpleGraph.symmetric with graph166      have xInV := vertices with x, hx167      have yInV := vertices with y, hy168      have old := symmetric with x, xInV, y, yInV, original169      exact inducedEdges.membership.backward with ⟨old, hy, hx⟩170      intros x hx edge171      obtain ⟨original, wx, wy⟩ := inducedEdges.membership.forward with edge172      have noLoop := SimpleGraph.irreflexive with graph173      have xInV := vertices with x, hx174      have impossible := noLoop with x, xInV175      apply impossible176      exact original177178theorem inducedEdges.subgraph (V E W : Set)179  requires graph : SimpleGraph(V, E)180  requires vertices : W ⊆ V181  shows Subgraph(V, E, W, inducedEdges(E, W))182proof183  constructor184  . exact inducedEdges.graph with graph, vertices185  . constructor186    . exact vertices187    . unfold inducedEdges188      exact intersection.subset_left189