Grace/Cumulus/GraphTheory/Complement.g17

Open in Workbench Download source

Imports

Walks · Cardinal.Countable

Declarations

Source

1-- Complete graphs, complements, cliques, and independent sets.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.Complement8import Walks9import Cardinal.Countable1011-- Separation from V × V makes this a set, even for infinite V.12def completeEdges (V : Set) : Set :=13  { p ∈ V × V | ∃ x ∈ V, ∃ y ∈ V, p = (x, y) ∧ x ≠ y }1415theorem completeEdges.adjacent (V x y : Set)16  shows Adjacent(completeEdges(V), x, y) ↔17    (x ∈ V ∧ y ∈ V ∧ x ≠ y)18proof19  constructor20  . intro edge21    unfold Adjacent at edge22    unfold relates at edge23    simp [completeEdges] at edge24    rcases edge with ⟨pair, a, ha, b, hb, equality, distinct⟩25    obtain ⟨xa, yb⟩ := orderedPair.injective with equality26    rw ← xa at ha27    rw ← yb at hb28    rw [← xa, ← yb] at distinct29    refine ⟨ha, hb, distinct⟩30  . intro h31    rcases h with ⟨hx, hy, distinct⟩32    unfold Adjacent33    unfold relates34    simp [completeEdges]35    have pair := product.pair with hx, hy36    refine ⟨pair, x, hx, y, hy, rfl, distinct⟩3738theorem completeEdges.graph (V : Set)39  shows SimpleGraph(V, completeEdges(V))40proof41  constructor42    intros p hp43    simp [completeEdges] at hp44    rcases hp with ⟨pair, witness⟩45    exact pair46  . constructor47      intros x hx y hy edge48      have adjacent : Adjacent(completeEdges(V), x, y) by exact edge49      obtain ⟨hx2, hy2, distinct⟩ := completeEdges.adjacent.forward with adjacent50      have symmetricEdge : Adjacent(completeEdges(V), y, x)51        apply completeEdges.adjacent.backward52        constructor53        . exact hy54        . constructor55          . exact hx56          . intro equal57            apply distinct58            rw equal59            rfl60      exact symmetricEdge61      intros x hx edge62      have adjacent : Adjacent(completeEdges(V), x, x) by exact edge63      obtain ⟨hx2, hx3, distinct⟩ := completeEdges.adjacent.forward with adjacent64      apply distinct65      rfl6667theorem SimpleGraph.edges_in_complete (V E : Set)68  requires graph : SimpleGraph(V, E)69  shows E ⊆ completeEdges(V)70proof71  intros p hp72  have relation := SimpleGraph.relation with graph73  unfold RelationOn at relation74  unfold RelationBetween at relation75  have pair := relation with p, hp76  obtain ⟨bounded, x, hx, y, hy, equality⟩ := product.membership.forward with pair77  have edge : Adjacent(E, x, y)78    unfold Adjacent79    unfold relates80    rwa ← equality81  have distinct := Adjacent.distinct with graph, edge82  have complete : Adjacent(completeEdges(V), x, y) := completeEdges.adjacent.backward with ⟨hx, hy, distinct⟩83  unfold Adjacent at complete84  unfold relates at complete85  rwa equality8687def complementEdges (V E : Set) : Set := completeEdges(V) ∖ E8889theorem complementEdges.membership (V E x y : Set)90  shows Adjacent(complementEdges(V, E), x, y) ↔91    (x ∈ V ∧ y ∈ V ∧ x ≠ y ∧ ¬Adjacent(E, x, y))92proof93  constructor94  . intro edge95    unfold Adjacent at edge96    unfold relates at edge97    unfold complementEdges at edge98    simp [difference.membership] at edge99    rcases edge with ⟨complete, absent⟩100    have adjacent : Adjacent(completeEdges(V), x, y)101      unfold Adjacent102      exact complete103    obtain ⟨hx, hy, distinct⟩ := completeEdges.adjacent.forward with adjacent104    constructor105    . exact hx106    . constructor107      . exact hy108      . constructor109        . exact distinct110        . intro edge111          unfold Adjacent at edge112          apply absent113          exact edge114  . intro h115    rcases h with ⟨hx, hy, distinct, absent⟩116    have complete : Adjacent(completeEdges(V), x, y) := completeEdges.adjacent.backward with ⟨hx, hy, distinct⟩117    unfold Adjacent at complete118    unfold Adjacent119    unfold relates120    unfold complementEdges121    apply difference.membership.backward122    constructor123    . exact complete124    . intro edge125      apply absent126      unfold Adjacent127      exact edge128129theorem complementEdges.graph (V E : Set)130  requires graph : SimpleGraph(V, E)131  shows SimpleGraph(V, complementEdges(V, E))132proof133  constructor134    intros p hp135    unfold complementEdges at hp136    simp [difference.membership] at hp137    rcases hp with ⟨complete, absent⟩138    have relation := SimpleGraph.relation at V, completeEdges(V) with completeEdges.graph at V139    unfold RelationOn at relation140    unfold RelationBetween at relation141    exact relation with p, complete142  . constructor143      intros x hx y hy edge144      have adjacent : Adjacent(complementEdges(V, E), x, y) by exact edge145      obtain ⟨hx2, hy2, distinct, absent⟩ := complementEdges.membership.forward with adjacent146      have reverseEdge : Adjacent(complementEdges(V, E), y, x)147        apply complementEdges.membership.backward148        constructor149        . exact hy150        . constructor151          . exact hx152          . constructor153            . intro equal154              apply distinct155              rw equal156              rfl157            . intro reverse158              have forward := Adjacent.symmetric with graph, reverse159              apply absent160              exact forward161      exact reverseEdge162      intros x hx edge163      have adjacent : Adjacent(complementEdges(V, E), x, x) by exact edge164      obtain ⟨hx2, hx3, distinct, absent⟩ := complementEdges.membership.forward with adjacent165      apply distinct166      rfl167168predicate Clique (V E S : Set) :=169  S ⊆ V ∧ (∀ x ∈ S, ∀ y ∈ S, x ≠ y → Adjacent(E, x, y))170171predicate Independent (V E S : Set) :=172  S ⊆ V ∧ (∀ x ∈ S, ∀ y ∈ S, ¬Adjacent(E, x, y))173174theorem Independent.in_complement (V E S : Set)175  requires independent : Independent(V, E, S)176  shows Clique(V, complementEdges(V, E), S)177proof178  rcases independent with ⟨included, noEdges⟩179  constructor180  . exact included181  . intros x hx y hy distinct182    have xInV := included with x, hx183    have yInV := included with y, hy184    have absent := noEdges with x, hx, y, hy185    exact complementEdges.membership.backward with ⟨xInV, yInV, distinct, absent⟩186187theorem Clique.in_complement (V E S : Set)188  requires clique : Clique(V, complementEdges(V, E), S)189  requires graph : SimpleGraph(V, E)190  shows Independent(V, E, S)191proof192  rcases clique with ⟨included, allEdges⟩193  constructor194  . exact included195  . intros x hx y hy edge196    have distinct := Adjacent.distinct with graph, edge197    have complementary := allEdges with x, hx, y, hy, distinct198    obtain ⟨xInV, yInV, d, absent⟩ := complementEdges.membership.forward with complementary199    apply absent200    exact edge201202theorem complementEdges.involution (V E : Set)203  requires graph : SimpleGraph(V, E)204  shows complementEdges(V, complementEdges(V, E)) = E205proof206  ext p207  have included := SimpleGraph.edges_in_complete with graph208  have membership : p ∈ E → p ∈ completeEdges(V)209    intro hp210    exact included with p, hp211  constructor212  . intro h213    unfold complementEdges at h214    obtain ⟨inComplete, notInner⟩ := difference.membership.forward with h215    have cases : p ∈ E ∨ ¬(p ∈ E) by tauto216    cases cases with yes | no217    . exact yes218    . exfalso219      apply notInner220      exact difference.membership.backward with ⟨inComplete, no⟩221  . intro he222    unfold complementEdges223    apply difference.membership.backward224    constructor225    . exact membership with he226    . intro inner227      obtain ⟨inComplete, absent⟩ := difference.membership.forward with inner228      apply absent229      exact he230231def independentSets (V E : Set) : Set :=232  { S ∈ 𝒫(V) | Independent(V, E, S) }233234theorem independentSets.empty_graph (V : Set)235  shows independentSets(V, empty) = 𝒫(V)236proof237  ext S238  constructor239  . intro h240    simp [independentSets] at h241    rcases h with ⟨inPower, independent⟩242    exact inPower243  . intro inPower244    have subset := set.powerset.forward with inPower245    simp [independentSets]246    constructor247    . exact inPower248      constructor249      . unfold Subset250        exact subset251      . intros x hx y hy edge252        unfold Adjacent at edge253        unfold relates at edge254        exact set.empty with edge255256-- Cantor's diagonal argument has a graph-theoretic consequence even when257-- there are no edges: the independent vertex subsets cannot be enumerated258-- by the vertices themselves.259theorem Independent.no_surjection_from_vertices (V f : Set)260  shows ¬SurjectiveBetween(f, V, independentSets(V, empty))261proof262  intro onto263  have allSubsets := independentSets.empty_graph at V264  rw allSubsets at onto265  exact Cantor.no_surjection_onto_powerset with onto266