Grace/Cumulus/GraphTheory/Ramsey.g17

Open in Workbench Download source

Imports

Complement · Cardinal.InclusionExclusion

Declarations

Source

1-- Ramsey's theorem for triangles: among six people, three are mutual2-- acquaintances or three are mutual strangers, so R(3, 3) ≤ 6.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.GraphTheory.Ramsey9import Complement10import Cardinal.InclusionExclusion1112theorem ne.symmetric (x y : Set)13  requires distinct : x ≠ y14  shows y ≠ x15proof16  intro same17  symm at same18  exact distinct with same1920-- A finite set of positive size has a member.21theorem Finite.member_of_positive (S : Set)22  requires finite : Finite(S)23  requires positive : 0 < cardinality(S)24  shows ∃ a, a ∈ S25proof26  have alternatives : (∃ a, a ∈ S) ∨ ¬(∃ a, a ∈ S) by tauto27  rcases alternatives with some | none28  . exact some29  . have empty : S = ∅30      ext x31      constructor32      . intro hx33        have witness : ∃ a, a ∈ S := ⟨x, hx⟩34        exfalso35        exact none with witness36      . intro hx37        exfalso38        exact set.empty with hx39    have counted := HasCardinality.empty_set40    rw ← empty at counted41    have zero := cardinality.eq_of_has with counted42    rw zero at positive43    have irreflexive := Less.irreflexive at 044    exfalso45    exact irreflexive with positive4647-- A finite set of size at least three has three distinct members.48theorem Finite.three_members (S : Set)49  requires finite : Finite(S)50  requires large : 3 ≤ cardinality(S)51  shows ∃ a ∈ S, ∃ b ∈ S, ∃ c ∈ S, a ≠ b ∧ a ≠ c ∧ b ≠ c52proof53  have natS := cardinality.nat with finite54  have positiveS : 0 < cardinality(S) by arith55  obtain ⟨a, ha⟩ := Finite.member_of_positive with finite, positiveS56  have removeA := cardinality.remove with finite, ha57  have subsetA := difference.subset_left at S, {a} with *58  have finiteA := Finite.subset with finite, subsetA59  have natA := cardinality.nat with finiteA60  have positiveA : 0 < cardinality(S ∖ {a}) by arith61  obtain ⟨b, hb⟩ := Finite.member_of_positive with finiteA, positiveA62  have bFacts := difference.singleton_membership.forward with hb63  rcases bFacts with ⟨bInS, bNotA⟩64  have removeB := cardinality.remove with finiteA, hb65  have subsetB := difference.subset_left at S ∖ {a}, {b} with *66  have finiteB := Finite.subset with finiteA, subsetB67  have natB := cardinality.nat with finiteB68  have positiveB : 0 < cardinality((S ∖ {a}) ∖ {b}) by arith69  obtain ⟨c, hc⟩ := Finite.member_of_positive with finiteB, positiveB70  have cFacts := difference.singleton_membership.forward with hc71  rcases cFacts with ⟨cInA, cNotB⟩72  have cInner := difference.singleton_membership.forward with cInA73  rcases cInner with ⟨cInS, cNotA⟩74  have ab := ne.symmetric with bNotA75  have ac := ne.symmetric with cNotA76  have bc := ne.symmetric with cNotB77  exact ⟨a, ha, b, bInS, c, cInS, ab, ac, bc⟩7879-- Three mutually adjacent or three mutually non-adjacent vertices.80predicate MonochromaticTriangle (E a b c : Set) :=81  (Adjacent(E, a, b) ∧ Adjacent(E, a, c) ∧ Adjacent(E, b, c)) ∨82  (¬Adjacent(E, a, b) ∧ ¬Adjacent(E, a, c) ∧ ¬Adjacent(E, b, c))8384-- Three neighbours of a vertex give a monochromatic triangle: an edge among85-- them closes a triangle with the vertex, and otherwise they are independent.86theorem ramsey.of_neighbors (V E v a b c : Set)87  requires graph : SimpleGraph(V, E)88  requires hv : v ∈ V89  requires ha : a ∈ V90  requires hb : b ∈ V91  requires hc : c ∈ V92  requires va : Adjacent(E, v, a)93  requires vb : Adjacent(E, v, b)94  requires vc : Adjacent(E, v, c)95  requires ab : a ≠ b96  requires ac : a ≠ c97  requires bc : b ≠ c98  shows ∃ x ∈ V, ∃ y ∈ V, ∃ z ∈ V,99    x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ MonochromaticTriangle(E, x, y, z)100proof101  have vNotA := Adjacent.distinct with graph, va102  have vNotB := Adjacent.distinct with graph, vb103  have vNotC := Adjacent.distinct with graph, vc104  have firstCase : Adjacent(E, a, b) ∨ ¬Adjacent(E, a, b) by tauto105  rcases firstCase with abEdge | abNone106  . refine ⟨v, hv, a, ha, b, hb, vNotA, vNotB, ab, _⟩107    unfold MonochromaticTriangle108    left109    exact ⟨va, vb, abEdge⟩110  have secondCase : Adjacent(E, a, c) ∨ ¬Adjacent(E, a, c) by tauto111  rcases secondCase with acEdge | acNone112  . refine ⟨v, hv, a, ha, c, hc, vNotA, vNotC, ac, _⟩113    unfold MonochromaticTriangle114    left115    exact ⟨va, vc, acEdge⟩116  have thirdCase : Adjacent(E, b, c) ∨ ¬Adjacent(E, b, c) by tauto117  rcases thirdCase with bcEdge | bcNone118  . refine ⟨v, hv, b, hb, c, hc, vNotB, vNotC, bc, _⟩119    unfold MonochromaticTriangle120    left121    exact ⟨vb, vc, bcEdge⟩122  refine ⟨a, ha, b, hb, c, hc, ab, ac, bc, _⟩123  unfold MonochromaticTriangle124  right125  exact ⟨abNone, acNone, bcNone⟩126127-- Three non-neighbours of a vertex, the mirror image of the previous case.128theorem ramsey.of_strangers (V E v a b c : Set)129  requires graph : SimpleGraph(V, E)130  requires hv : v ∈ V131  requires ha : a ∈ V132  requires hb : b ∈ V133  requires hc : c ∈ V134  requires va : ¬Adjacent(E, v, a)135  requires vb : ¬Adjacent(E, v, b)136  requires vc : ¬Adjacent(E, v, c)137  requires vNotA : v ≠ a138  requires vNotB : v ≠ b139  requires vNotC : v ≠ c140  requires ab : a ≠ b141  requires ac : a ≠ c142  requires bc : b ≠ c143  shows ∃ x ∈ V, ∃ y ∈ V, ∃ z ∈ V,144    x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ MonochromaticTriangle(E, x, y, z)145proof146  have firstCase : Adjacent(E, a, b) ∨ ¬Adjacent(E, a, b) by tauto147  rcases firstCase with abEdge | abNone148  . have secondCase : Adjacent(E, a, c) ∨ ¬Adjacent(E, a, c) by tauto149    rcases secondCase with acEdge | acNone150    . have thirdCase : Adjacent(E, b, c) ∨ ¬Adjacent(E, b, c) by tauto151      rcases thirdCase with bcEdge | bcNone152      . refine ⟨a, ha, b, hb, c, hc, ab, ac, bc, _⟩153        unfold MonochromaticTriangle154        left155        exact ⟨abEdge, acEdge, bcEdge⟩156      . refine ⟨v, hv, b, hb, c, hc, vNotB, vNotC, bc, _⟩157        unfold MonochromaticTriangle158        right159        exact ⟨vb, vc, bcNone⟩160    . refine ⟨v, hv, a, ha, c, hc, vNotA, vNotC, ac, _⟩161      unfold MonochromaticTriangle162      right163      exact ⟨va, vc, acNone⟩164  . refine ⟨v, hv, a, ha, b, hb, vNotA, vNotB, ab, _⟩165    unfold MonochromaticTriangle166    right167    exact ⟨va, vb, abNone⟩168169-- A vertex outside the neighbourhood of v is not adjacent to v.170theorem neighbors.not_adjacent (V E v a : Set)171  requires inV : a ∈ V172  requires outside : ¬(a ∈ neighbors(V, E, v))173  shows ¬Adjacent(E, v, a)174proof175  intro edge176  have inside : a ∈ neighbors(V, E, v)177    apply neighbors.membership.backward178    exact ⟨inV, edge⟩179  exact outside with inside180181-- Ramsey's theorem for triangles: a graph on six vertices has three mutually182-- adjacent vertices or three mutually non-adjacent ones.183theorem ramsey.three_three (V E : Set)184  requires graph : SimpleGraph(V, E)185  requires six : HasCardinality(V, 6)186  shows ∃ x ∈ V, ∃ y ∈ V, ∃ z ∈ V,187    x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ MonochromaticTriangle(E, x, y, z)188proof189  have finite := Finite.from_cardinality with six190  have count := cardinality.eq_of_has with six191  have positive : 0 < cardinality(V)192    rw count193    arith194  obtain ⟨v, hv⟩ := Finite.member_of_positive with finite, positive195  have removeV := cardinality.remove with finite, hv196  have restSubset := difference.subset_left at V, {v} with *197  have finiteRest := Finite.subset with finite, restSubset198  have natRest := cardinality.nat with finiteRest199  -- The neighbours of v and the other vertices split the rest of V.200  have neighborsSubset : neighbors(V, E, v) ⊆ V ∖ {v}201    intros y hy202    have facts := neighbors.membership.forward with hy203    rcases facts with ⟨yInV, edge⟩204    have vNotY := Adjacent.distinct with graph, edge205    have distinct := ne.symmetric with vNotY206    apply difference.singleton_membership.backward207    exact ⟨yInV, distinct⟩208  have finiteNeighbors := Finite.subset with finiteRest, neighborsSubset209  have natNeighbors := cardinality.nat with finiteNeighbors210  have strangersSubset := difference.subset_left at V ∖ {v}, neighbors(V, E, v)211    with *212  have finiteStrangers := Finite.subset with finiteRest, strangersSubset213  have natStrangers := cardinality.nat with finiteStrangers214  have split := difference.union2_of_subset with neighborsSubset215  have disjoint : Disjoint(neighbors(V, E, v), (V ∖ {v}) ∖ neighbors(V, E, v))216    unfold Disjoint217    ext x218    simp219  have sum := cardinality.union_disjoint with220    finiteNeighbors, finiteStrangers, disjoint221  rw split at sum222  rw count at removeV223  -- Five other vertices split into neighbours and strangers of v, so one of224  -- the two parts has at least three members.225  have trichotomy := Less.trichotomy at 2, cardinality(neighbors(V, E, v))226    with *227  have parts : 3 ≤ cardinality(neighbors(V, E, v)) ∨228      3 ≤ cardinality((V ∖ {v}) ∖ neighbors(V, E, v))229    rcases trichotomy with more | same | fewer230    . left231      arith232    . right233      arith234    . right235      arith236  rcases parts with manyNeighbors | manyStrangers237  . obtain ⟨a, ha, b, hb, c, hc, ab, ac, bc⟩ :=238      Finite.three_members with finiteNeighbors, manyNeighbors239    have aFacts := neighbors.membership.forward with ha240    have bFacts := neighbors.membership.forward with hb241    have cFacts := neighbors.membership.forward with hc242    rcases aFacts with ⟨aInV, va⟩243    rcases bFacts with ⟨bInV, vb⟩244    rcases cFacts with ⟨cInV, vc⟩245    exact ramsey.of_neighbors with graph, hv, aInV, bInV, cInV, va, vb, vc,246      ab, ac, bc247  . obtain ⟨a, ha, b, hb, c, hc, ab, ac, bc⟩ :=248      Finite.three_members with finiteStrangers, manyStrangers249    have aFacts := difference.membership.forward with ha250    have bFacts := difference.membership.forward with hb251    have cFacts := difference.membership.forward with hc252    rcases aFacts with ⟨aRest, aOutside⟩253    rcases bFacts with ⟨bRest, bOutside⟩254    rcases cFacts with ⟨cRest, cOutside⟩255    have aIn := difference.singleton_membership.forward with aRest256    have bIn := difference.singleton_membership.forward with bRest257    have cIn := difference.singleton_membership.forward with cRest258    rcases aIn with ⟨aInV, aNotV⟩259    rcases bIn with ⟨bInV, bNotV⟩260    rcases cIn with ⟨cInV, cNotV⟩261    have va := neighbors.not_adjacent with aInV, aOutside262    have vb := neighbors.not_adjacent with bInV, bOutside263    have vc := neighbors.not_adjacent with cInV, cOutside264    have vNotA := ne.symmetric with aNotV265    have vNotB := ne.symmetric with bNotV266    have vNotC := ne.symmetric with cNotV267    exact ramsey.of_strangers with graph, hv, aInV, bInV, cInV, va, vb, vc,268      vNotA, vNotB, vNotC, ab, ac, bc269