-- Short walks and triangles in simple graphs
-- 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.Walks
import Basic

predicate TwoStep (V E x y : Set) :=
  ∃ z ∈ V, Adjacent(E, x, z) ∧ Adjacent(E, z, y)

theorem TwoStep.intro (V E x y z : Set)
  requires hz : z ∈ V
  requires first : Adjacent(E, x, z)
  requires second : Adjacent(E, z, y)
  shows TwoStep(V, E, x, y)
proof
  unfold TwoStep
  refine ⟨z, hz, first, second⟩

theorem TwoStep.bounds (V E x y : Set)
  requires graph : SimpleGraph(V, E)
  requires walk : TwoStep(V, E, x, y)
  shows x ∈ V ∧ y ∈ V
proof
  rcases walk with ⟨z, hz, first, second⟩
  have firstBounds := Adjacent.bounds with graph, first
  have secondBounds := Adjacent.bounds with graph, second
  rcases firstBounds with ⟨hx, hz2⟩
  rcases secondBounds with ⟨hz3, hy⟩
  refine ⟨hx, hy⟩

theorem TwoStep.symmetric (V E x y : Set)
  requires graph : SimpleGraph(V, E)
  requires walk : TwoStep(V, E, x, y)
  shows TwoStep(V, E, y, x)
proof
  rcases walk with ⟨z, hz, first, second⟩
  have back := Adjacent.symmetric with graph, second
  have front := Adjacent.symmetric with graph, first
  exact TwoStep.intro with hz, back, front

theorem TwoStep.common_neighbor (V E x y : Set)
  requires walk : TwoStep(V, E, x, y)
  shows ∃ z ∈ neighbors(V, E, x), Adjacent(E, z, y)
proof
  rcases walk with ⟨z, hz, first, second⟩
  have member : z ∈ neighbors(V, E, x) := neighbors.membership.backward with ⟨hz, first⟩
  refine ⟨z, member, second⟩

theorem TwoStep.of_common_neighbor (V E x y : Set)
  requires common : ∃ z ∈ neighbors(V, E, x), Adjacent(E, z, y)
  shows TwoStep(V, E, x, y)
proof
  rcases common with ⟨z, member, second⟩
  obtain ⟨hz, first⟩ := neighbors.membership.forward with member
  exact TwoStep.intro with hz, first, second

theorem TwoStep.backtrack (V E x y : Set)
  requires graph : SimpleGraph(V, E)
  requires edge : Adjacent(E, x, y)
  shows TwoStep(V, E, x, x)
proof
  obtain ⟨hx, hy⟩ := Adjacent.bounds with graph, edge
  have reverse := Adjacent.symmetric with graph, edge
  exact TwoStep.intro with hy, edge, reverse

predicate Triangle (E x y z : Set) :=
  Adjacent(E, x, y) ∧ Adjacent(E, y, z) ∧ Adjacent(E, z, x)

theorem Triangle.distinct (V E x y z : Set)
  requires graph : SimpleGraph(V, E)
  requires triangle : Triangle(E, x, y, z)
  shows x ≠ y ∧ y ≠ z ∧ z ≠ x
proof
  rcases triangle with ⟨xy, yz, zx⟩
  have dxy := Adjacent.distinct with graph, xy
  have dyz := Adjacent.distinct with graph, yz
  have dzx := Adjacent.distinct with graph, zx
  refine ⟨dxy, dyz, dzx⟩

theorem Triangle.rotate (E x y z : Set)
  requires triangle : Triangle(E, x, y, z)
  shows Triangle(E, y, z, x)
proof
  rcases triangle with ⟨xy, yz, zx⟩
  unfold Triangle
  refine ⟨yz, zx, xy⟩

theorem Triangle.reverse (V E x y z : Set)
  requires graph : SimpleGraph(V, E)
  requires triangle : Triangle(E, x, y, z)
  shows Triangle(E, x, z, y)
proof
  rcases triangle with ⟨xy, yz, zx⟩
  have xz := Adjacent.symmetric with graph, zx
  have zy := Adjacent.symmetric with graph, yz
  have yx := Adjacent.symmetric with graph, xy
  unfold Triangle
  refine ⟨xz, zy, yx⟩

theorem Triangle.two_step (V E x y z : Set)
  requires graph : SimpleGraph(V, E)
  requires triangle : Triangle(E, x, y, z)
  shows TwoStep(V, E, x, z)
proof
  rcases triangle with ⟨xy, yz, zx⟩
  obtain ⟨hx, hy⟩ := Adjacent.bounds with graph, xy
  exact TwoStep.intro with hy, xy, yz

theorem Triangle.of_two_step (V E x y : Set)
  requires graph : SimpleGraph(V, E)
  requires walk : TwoStep(V, E, x, y)
  requires closing : Adjacent(E, y, x)
  shows ∃ z ∈ V, Triangle(E, x, z, y)
proof
  rcases walk with ⟨z, hz, first, second⟩
  have triangle : Triangle(E, x, z, y)
    unfold Triangle
    refine ⟨first, second, closing⟩
  refine ⟨z, hz, triangle⟩

theorem Triangle.subgraph (V E W F x y z : Set)
  requires sub : Subgraph(V, E, W, F)
  requires triangle : Triangle(F, x, y, z)
  shows Triangle(E, x, y, z)
proof
  rcases triangle with ⟨xy, yz, zx⟩
  have exy := Subgraph.adjacent with sub, xy
  have eyz := Subgraph.adjacent with sub, yz
  have ezx := Subgraph.adjacent with sub, zx
  unfold Triangle
  refine ⟨exy, eyz, ezx⟩