-- Ramsey's theorem for triangles: among six people, three are mutual
-- acquaintances or three are mutual strangers, so R(3, 3) ≤ 6.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.GraphTheory.Ramsey
import Complement
import Cardinal.InclusionExclusion

theorem ne.symmetric (x y : Set)
  requires distinct : x ≠ y
  shows y ≠ x
proof
  intro same
  symm at same
  exact distinct with same

-- A finite set of positive size has a member.
theorem Finite.member_of_positive (S : Set)
  requires finite : Finite(S)
  requires positive : 0 < cardinality(S)
  shows ∃ a, a ∈ S
proof
  have alternatives : (∃ a, a ∈ S) ∨ ¬(∃ a, a ∈ S) by tauto
  rcases alternatives with some | none
  . exact some
  . have empty : S = ∅
      ext x
      constructor
      . intro hx
        have witness : ∃ a, a ∈ S := ⟨x, hx⟩
        exfalso
        exact none with witness
      . intro hx
        exfalso
        exact set.empty with hx
    have counted := HasCardinality.empty_set
    rw ← empty at counted
    have zero := cardinality.eq_of_has with counted
    rw zero at positive
    have irreflexive := Less.irreflexive at 0
    exfalso
    exact irreflexive with positive

-- A finite set of size at least three has three distinct members.
theorem Finite.three_members (S : Set)
  requires finite : Finite(S)
  requires large : 3 ≤ cardinality(S)
  shows ∃ a ∈ S, ∃ b ∈ S, ∃ c ∈ S, a ≠ b ∧ a ≠ c ∧ b ≠ c
proof
  have natS := cardinality.nat with finite
  have positiveS : 0 < cardinality(S) by arith
  obtain ⟨a, ha⟩ := Finite.member_of_positive with finite, positiveS
  have removeA := cardinality.remove with finite, ha
  have subsetA := difference.subset_left at S, {a} with *
  have finiteA := Finite.subset with finite, subsetA
  have natA := cardinality.nat with finiteA
  have positiveA : 0 < cardinality(S ∖ {a}) by arith
  obtain ⟨b, hb⟩ := Finite.member_of_positive with finiteA, positiveA
  have bFacts := difference.singleton_membership.forward with hb
  rcases bFacts with ⟨bInS, bNotA⟩
  have removeB := cardinality.remove with finiteA, hb
  have subsetB := difference.subset_left at S ∖ {a}, {b} with *
  have finiteB := Finite.subset with finiteA, subsetB
  have natB := cardinality.nat with finiteB
  have positiveB : 0 < cardinality((S ∖ {a}) ∖ {b}) by arith
  obtain ⟨c, hc⟩ := Finite.member_of_positive with finiteB, positiveB
  have cFacts := difference.singleton_membership.forward with hc
  rcases cFacts with ⟨cInA, cNotB⟩
  have cInner := difference.singleton_membership.forward with cInA
  rcases cInner with ⟨cInS, cNotA⟩
  have ab := ne.symmetric with bNotA
  have ac := ne.symmetric with cNotA
  have bc := ne.symmetric with cNotB
  exact ⟨a, ha, b, bInS, c, cInS, ab, ac, bc⟩

-- Three mutually adjacent or three mutually non-adjacent vertices.
predicate MonochromaticTriangle (E a b c : Set) :=
  (Adjacent(E, a, b) ∧ Adjacent(E, a, c) ∧ Adjacent(E, b, c)) ∨
  (¬Adjacent(E, a, b) ∧ ¬Adjacent(E, a, c) ∧ ¬Adjacent(E, b, c))

-- Three neighbours of a vertex give a monochromatic triangle: an edge among
-- them closes a triangle with the vertex, and otherwise they are independent.
theorem ramsey.of_neighbors (V E v a b c : Set)
  requires graph : SimpleGraph(V, E)
  requires hv : v ∈ V
  requires ha : a ∈ V
  requires hb : b ∈ V
  requires hc : c ∈ V
  requires va : Adjacent(E, v, a)
  requires vb : Adjacent(E, v, b)
  requires vc : Adjacent(E, v, c)
  requires ab : a ≠ b
  requires ac : a ≠ c
  requires bc : b ≠ c
  shows ∃ x ∈ V, ∃ y ∈ V, ∃ z ∈ V,
    x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ MonochromaticTriangle(E, x, y, z)
proof
  have vNotA := Adjacent.distinct with graph, va
  have vNotB := Adjacent.distinct with graph, vb
  have vNotC := Adjacent.distinct with graph, vc
  have firstCase : Adjacent(E, a, b) ∨ ¬Adjacent(E, a, b) by tauto
  rcases firstCase with abEdge | abNone
  . refine ⟨v, hv, a, ha, b, hb, vNotA, vNotB, ab, _⟩
    unfold MonochromaticTriangle
    left
    exact ⟨va, vb, abEdge⟩
  have secondCase : Adjacent(E, a, c) ∨ ¬Adjacent(E, a, c) by tauto
  rcases secondCase with acEdge | acNone
  . refine ⟨v, hv, a, ha, c, hc, vNotA, vNotC, ac, _⟩
    unfold MonochromaticTriangle
    left
    exact ⟨va, vc, acEdge⟩
  have thirdCase : Adjacent(E, b, c) ∨ ¬Adjacent(E, b, c) by tauto
  rcases thirdCase with bcEdge | bcNone
  . refine ⟨v, hv, b, hb, c, hc, vNotB, vNotC, bc, _⟩
    unfold MonochromaticTriangle
    left
    exact ⟨vb, vc, bcEdge⟩
  refine ⟨a, ha, b, hb, c, hc, ab, ac, bc, _⟩
  unfold MonochromaticTriangle
  right
  exact ⟨abNone, acNone, bcNone⟩

-- Three non-neighbours of a vertex, the mirror image of the previous case.
theorem ramsey.of_strangers (V E v a b c : Set)
  requires graph : SimpleGraph(V, E)
  requires hv : v ∈ V
  requires ha : a ∈ V
  requires hb : b ∈ V
  requires hc : c ∈ V
  requires va : ¬Adjacent(E, v, a)
  requires vb : ¬Adjacent(E, v, b)
  requires vc : ¬Adjacent(E, v, c)
  requires vNotA : v ≠ a
  requires vNotB : v ≠ b
  requires vNotC : v ≠ c
  requires ab : a ≠ b
  requires ac : a ≠ c
  requires bc : b ≠ c
  shows ∃ x ∈ V, ∃ y ∈ V, ∃ z ∈ V,
    x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ MonochromaticTriangle(E, x, y, z)
proof
  have firstCase : Adjacent(E, a, b) ∨ ¬Adjacent(E, a, b) by tauto
  rcases firstCase with abEdge | abNone
  . have secondCase : Adjacent(E, a, c) ∨ ¬Adjacent(E, a, c) by tauto
    rcases secondCase with acEdge | acNone
    . have thirdCase : Adjacent(E, b, c) ∨ ¬Adjacent(E, b, c) by tauto
      rcases thirdCase with bcEdge | bcNone
      . refine ⟨a, ha, b, hb, c, hc, ab, ac, bc, _⟩
        unfold MonochromaticTriangle
        left
        exact ⟨abEdge, acEdge, bcEdge⟩
      . refine ⟨v, hv, b, hb, c, hc, vNotB, vNotC, bc, _⟩
        unfold MonochromaticTriangle
        right
        exact ⟨vb, vc, bcNone⟩
    . refine ⟨v, hv, a, ha, c, hc, vNotA, vNotC, ac, _⟩
      unfold MonochromaticTriangle
      right
      exact ⟨va, vc, acNone⟩
  . refine ⟨v, hv, a, ha, b, hb, vNotA, vNotB, ab, _⟩
    unfold MonochromaticTriangle
    right
    exact ⟨va, vb, abNone⟩

-- A vertex outside the neighbourhood of v is not adjacent to v.
theorem neighbors.not_adjacent (V E v a : Set)
  requires inV : a ∈ V
  requires outside : ¬(a ∈ neighbors(V, E, v))
  shows ¬Adjacent(E, v, a)
proof
  intro edge
  have inside : a ∈ neighbors(V, E, v)
    apply neighbors.membership.backward
    exact ⟨inV, edge⟩
  exact outside with inside

-- Ramsey's theorem for triangles: a graph on six vertices has three mutually
-- adjacent vertices or three mutually non-adjacent ones.
theorem ramsey.three_three (V E : Set)
  requires graph : SimpleGraph(V, E)
  requires six : HasCardinality(V, 6)
  shows ∃ x ∈ V, ∃ y ∈ V, ∃ z ∈ V,
    x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ MonochromaticTriangle(E, x, y, z)
proof
  have finite := Finite.from_cardinality with six
  have count := cardinality.eq_of_has with six
  have positive : 0 < cardinality(V)
    rw count
    arith
  obtain ⟨v, hv⟩ := Finite.member_of_positive with finite, positive
  have removeV := cardinality.remove with finite, hv
  have restSubset := difference.subset_left at V, {v} with *
  have finiteRest := Finite.subset with finite, restSubset
  have natRest := cardinality.nat with finiteRest
  -- The neighbours of v and the other vertices split the rest of V.
  have neighborsSubset : neighbors(V, E, v) ⊆ V ∖ {v}
    intros y hy
    have facts := neighbors.membership.forward with hy
    rcases facts with ⟨yInV, edge⟩
    have vNotY := Adjacent.distinct with graph, edge
    have distinct := ne.symmetric with vNotY
    apply difference.singleton_membership.backward
    exact ⟨yInV, distinct⟩
  have finiteNeighbors := Finite.subset with finiteRest, neighborsSubset
  have natNeighbors := cardinality.nat with finiteNeighbors
  have strangersSubset := difference.subset_left at V ∖ {v}, neighbors(V, E, v)
    with *
  have finiteStrangers := Finite.subset with finiteRest, strangersSubset
  have natStrangers := cardinality.nat with finiteStrangers
  have split := difference.union2_of_subset with neighborsSubset
  have disjoint : Disjoint(neighbors(V, E, v), (V ∖ {v}) ∖ neighbors(V, E, v))
    unfold Disjoint
    ext x
    simp
  have sum := cardinality.union_disjoint with
    finiteNeighbors, finiteStrangers, disjoint
  rw split at sum
  rw count at removeV
  -- Five other vertices split into neighbours and strangers of v, so one of
  -- the two parts has at least three members.
  have trichotomy := Less.trichotomy at 2, cardinality(neighbors(V, E, v))
    with *
  have parts : 3 ≤ cardinality(neighbors(V, E, v)) ∨
      3 ≤ cardinality((V ∖ {v}) ∖ neighbors(V, E, v))
    rcases trichotomy with more | same | fewer
    . left
      arith
    . right
      arith
    . right
      arith
  rcases parts with manyNeighbors | manyStrangers
  . obtain ⟨a, ha, b, hb, c, hc, ab, ac, bc⟩ :=
      Finite.three_members with finiteNeighbors, manyNeighbors
    have aFacts := neighbors.membership.forward with ha
    have bFacts := neighbors.membership.forward with hb
    have cFacts := neighbors.membership.forward with hc
    rcases aFacts with ⟨aInV, va⟩
    rcases bFacts with ⟨bInV, vb⟩
    rcases cFacts with ⟨cInV, vc⟩
    exact ramsey.of_neighbors with graph, hv, aInV, bInV, cInV, va, vb, vc,
      ab, ac, bc
  . obtain ⟨a, ha, b, hb, c, hc, ab, ac, bc⟩ :=
      Finite.three_members with finiteStrangers, manyStrangers
    have aFacts := difference.membership.forward with ha
    have bFacts := difference.membership.forward with hb
    have cFacts := difference.membership.forward with hc
    rcases aFacts with ⟨aRest, aOutside⟩
    rcases bFacts with ⟨bRest, bOutside⟩
    rcases cFacts with ⟨cRest, cOutside⟩
    have aIn := difference.singleton_membership.forward with aRest
    have bIn := difference.singleton_membership.forward with bRest
    have cIn := difference.singleton_membership.forward with cRest
    rcases aIn with ⟨aInV, aNotV⟩
    rcases bIn with ⟨bInV, bNotV⟩
    rcases cIn with ⟨cInV, cNotV⟩
    have va := neighbors.not_adjacent with aInV, aOutside
    have vb := neighbors.not_adjacent with bInV, bOutside
    have vc := neighbors.not_adjacent with cInV, cOutside
    have vNotA := ne.symmetric with aNotV
    have vNotB := ne.symmetric with bNotV
    have vNotC := ne.symmetric with cNotV
    exact ramsey.of_strangers with graph, hv, aInV, bInV, cInV, va, vb, vc,
      vNotA, vNotB, vNotC, ab, ac, bc