import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Card
import Mathlib.Data.Fintype.Basic
import Mathlib.Order.Preorder.Finite
import Mathlib.Tactic

--注释的中的题目为选做题
/-
Definition:
A tournament is a directed graph where between any two vertices there is exactly one edge.
A vertex v in a tournament is a king
if every other vertex can be reached from v by a (directed) path of length at most two.
-/

-- 定义顶点的类型（此处可以修改为任意你需要的类型）
abbrev Vertex := Nat

-- 定义顶点集合
abbrev VertexSet := Set Vertex

-- 定义边集合类型
abbrev EdgeSet := Set (Vertex × Vertex)

-- 定义有向图结构
structure DirectedGraph where
  (vertices : VertexSet)         -- 顶点集合
  (edges : EdgeSet)               -- 边集合，表示从一个顶点到另一个顶点的有向边

-- 判断一个有向图是否是 Tournament
def isTournament (G : DirectedGraph) : Prop :=
  -- 所有边都必须连接 G.vertices 中的两个不同顶点
  (∀ e : Vertex × Vertex,
    e ∈ G.edges →
      e.1 ∈ G.vertices ∧ e.2 ∈ G.vertices ∧ e.1 ≠ e.2)
  ∧
  -- 任意两个不同顶点之间，恰好有一个方向的边
  (∀ u v : Vertex,
    u ∈ G.vertices →
    v ∈ G.vertices →
    u ≠ v →
      (((u, v) ∈ G.edges ∧ (v, u) ∉ G.edges) ∨
       ((v, u) ∈ G.edges ∧ (u, v) ∉ G.edges)))
  ∧
  -- G非空
  G.vertices.Nonempty

-- 判断一个顶点是否是 King
def isKing (G : DirectedGraph) (v : Vertex) : Prop :=
  -- v 本身必须是图中的顶点
  v ∈ G.vertices
  ∧
  -- 对任意其他顶点 u，都可以从 v 在长度至多 2 的路径内到达 u
  (∀ u : Vertex,
    u ∈ G.vertices →
    u ≠ v →
      ((v, u) ∈ G.edges ∨
       ∃ w : Vertex,
         w ∈ G.vertices ∧
         (v, w) ∈ G.edges ∧
         (w, u) ∈ G.edges))

-- 定义有限Tournament
def isFiniteTournament (G : DirectedGraph) : Prop :=
  G.vertices.Finite  ∧ isTournament G

-- 定义无限Tournament
def isInfiniteTournament (G : DirectedGraph) : Prop :=
  (¬G.vertices.Finite ) ∧ isTournament G

-- 1.(a)证明每个有限Tournament中都存在一个King

/-解题思路：
考虑出度最大的v,
若存在u使得u->v,
若对v的所有的一步到达点，u都能一步到达，则u的出度大于v，矛盾
则存在一点w使得有v->w->u
则v为king
-/

-- 定义出邻居
def outNeighbors (G : DirectedGraph) (v : Vertex) : Set Vertex :=
  {u : Vertex | u ∈ G.vertices ∧ (v, u) ∈ G.edges}
-- 出邻居集的基数即为出度
noncomputable def outDegree (G : DirectedGraph) (v : Vertex) : Nat :=
  (outNeighbors G v).ncard

-- 出邻居集合有限
lemma outNeighbors_finite
    (G : DirectedGraph)
    (hfin : G.vertices.Finite)
    (v : Vertex) :
    (outNeighbors G v).Finite := by
  exact hfin.subset (by
    intro u hu
    exact hu.1
  )

-- 辅助定理：最大出度的顶点是 King
theorem max_outdegree_vertex_is_king
    (G : DirectedGraph)
    (hfin : G.vertices.Finite)
    (hT : isTournament G)
    (v : Vertex)
    (hv : v ∈ G.vertices)
    (hmax : ∀ u : Vertex, u ∈ G.vertices → outDegree G u ≤ outDegree G v) :
    isKing G v := by
  constructor
  · exact hv
  · intro u hu huv

    -- 如果 v 直接指向 u，那么已经到达
    by_cases hvu_edge : (v, u) ∈ G.edges
    · exact Or.inl hvu_edge

    -- 否则证明存在 w，使得 v → w 且 w → u
    · right

      by_contra hno_path

      -- 先证明 u → v
      have huv_edge : (u, v) ∈ G.edges := by
        have hdir := hT.2.1 v u hv hu (Ne.symm huv)
        rcases hdir with hvu | huv'
        · exact False.elim (hvu_edge hvu.1)
        · exact huv'.1

      -- 证明 outNeighbors v ⊆ outNeighbors u
      have hsubset : outNeighbors G v ⊆ outNeighbors G u := by
        intro w hw
        rcases hw with ⟨hwV, hvw_edge⟩

        -- w ≠ u，因为如果 w = u，则有 v → u，与 hvu_edge 矛盾
        have hwu : w ≠ u := by
          intro h_eq
          subst h_eq
          exact hvu_edge hvw_edge

        -- 在 tournament 中，w 和 u 之间必有一个方向
        have hdir := hT.2.1 w u hwV hu hwu

        -- 证明一定是 u → w
        have huw_edge : (u, w) ∈ G.edges := by
          rcases hdir with hwu_edge | huw
          · -- 如果 w → u，那么 v → w → u，矛盾
            exfalso
            apply hno_path
            exact ⟨w, hwV, hvw_edge, hwu_edge.1⟩
          · exact huw.1

        exact ⟨hwV, huw_edge⟩

      -- 证明 v ∈ outNeighbors u
      have hv_in_out_u : v ∈ outNeighbors G u := by
        exact ⟨hv, huv_edge⟩

      -- 证明 v ∉ outNeighbors v，因为 tournament 没有自环
      have hv_not_in_out_v : v ∉ outNeighbors G v := by
        intro hvout
        have h_edge_valid := hT.1 (v, v) hvout.2
        exact h_edge_valid.2.2 rfl

      -- 因此 outNeighbors v 是 outNeighbors u 的真子集
      have hproper : outNeighbors G v ⊂ outNeighbors G u := by
        constructor
        · exact hsubset
        · intro hreverse
          exact hv_not_in_out_v (hreverse hv_in_out_u)

      -- 所以 outDegree v < outDegree u
      have hlt : outDegree G v < outDegree G u := by
        unfold outDegree
        exact Set.ncard_lt_ncard hproper (outNeighbors_finite G hfin u)

      -- 但 v 是最大出度点，所以 outDegree u ≤ outDegree v，矛盾
      have hle : outDegree G u ≤ outDegree G v := hmax u hu

      exact (not_lt_of_ge hle) hlt

theorem king_in_finite_tournament
    (G : DirectedGraph)
    (h : isFiniteTournament G) :
    ∃ v : Vertex, isKing G v := by
  classical

  -- 拆开有限 tournament 的条件
  rcases h with ⟨hfin, hT⟩

  -- tournament 非空
  have hnonempty : G.vertices.Nonempty := hT.2.2

  -- 在有限非空顶点集中，存在出度最大的顶点
  obtain ⟨v, hvmax⟩ :=
    Set.Finite.exists_maximalFor
      (fun x : Vertex => outDegree G x)
      G.vertices
      hfin
      hnonempty

  -- 从 MaximalFor 推出真正的最大出度性质
  have hmax :
      ∀ u : Vertex, u ∈ G.vertices → outDegree G u ≤ outDegree G v := by
    intro u hu
    by_cases hle : outDegree G v ≤ outDegree G u
    · exact hvmax.2 hu hle
    · exact le_of_not_ge hle

  -- 使用辅助定理：最大出度顶点是 king
  exact ⟨v, max_outdegree_vertex_is_king G hfin hT v hvmax.1 hmax⟩

-- 1.(b)证明存在没有King的无限Tournament
/-
证明思路：我们构造自然数集，对于点a<b，存在道路b->a
则对于任意v，无法两步到达v+1
-/
-- 构造顶点是所有自然数，边从大的数指向小的数的无限Tournament
def descendingNatTournament : DirectedGraph where
  vertices := Set.univ
  edges := {e : Vertex × Vertex | e.1 > e.2}


theorem infinite_tournament_without_king :
  ∃ G : DirectedGraph, isInfiniteTournament G ∧
    (∀ v : Vertex, ¬ isKing G v) := by
  classical

  refine ⟨descendingNatTournament, ?_, ?_⟩

  · -- 先证明它是一个无限 Tournament
    constructor

    · -- 顶点集是 Nat 全体，所以无限
      have hInf : (Set.univ : Set Vertex).Infinite := Set.infinite_univ
      simpa [descendingNatTournament] using hInf

    · -- 证明它满足 Tournament 定义
      constructor

      · -- 每条边都连接两个不同的顶点，并且端点都在顶点集中
        intro e he

        have hgt : e.1 > e.2 := by
          simpa [descendingNatTournament] using he

        constructor
        · simp [descendingNatTournament]
        · constructor
          · simp [descendingNatTournament]
          · exact ne_of_gt hgt

      · constructor

        · -- 任意两个不同顶点之间，恰好有一个方向的边
          intro u v hu hv huv

          have hcases : u < v ∨ v < u := lt_or_gt_of_ne huv

          rcases hcases with huvlt | hvult

          · -- 情况一：u < v，所以 v → u
            right
            constructor

            · -- 证明 (v, u) 是边
              simpa [descendingNatTournament] using huvlt

            · -- 证明 (u, v) 不是边
              intro huv_edge
              have hvltu : v < u := by
                simpa [descendingNatTournament] using huv_edge
              exact (not_lt_of_ge (le_of_lt huvlt)) hvltu

          · -- 情况二：v < u，所以 u → v
            left
            constructor

            · -- 证明 (u, v) 是边
              simpa [descendingNatTournament] using hvult

            · -- 证明 (v, u) 不是边
              intro hvu_edge
              have hultv : u < v := by
                simpa [descendingNatTournament] using hvu_edge
              exact (not_lt_of_ge (le_of_lt hvult)) hultv

        · -- 顶点集非空
          exact ⟨0, by simp [descendingNatTournament]⟩

  · -- 证明没有任何顶点是 King
    intro v hvKing

    rcases hvKing with ⟨hv_mem, hreach⟩

    -- 取 u = v + 1
    -- 它是顶点，并且 u ≠ v
    have hsucc_mem : v + 1 ∈ descendingNatTournament.vertices := by
      simp [descendingNatTournament]

    have hsucc_ne : v + 1 ≠ v := by
      simp

    -- 如果 v 是 king，那么 v 应该能在两步内到达 v + 1
    have hreach_succ :=
      hreach (v + 1) hsucc_mem hsucc_ne

    rcases hreach_succ with hv_direct | hv_two_step

    · -- 情况一：假设 v → v+1
      -- 但边只能从大的数指向小的数，所以这会推出 v+1 < v，矛盾
      have hlt : v + 1 < v := by
        simpa [descendingNatTournament] using hv_direct

      have hle : v + 1 ≤ v := Nat.le_of_lt hlt

      have hle' : Nat.succ v ≤ v := by
        simpa [Nat.succ_eq_add_one] using hle

      exact (Nat.not_succ_le_self v) hle'

    · -- 情况二：假设存在 w，使得 v → w → v+1
      rcases hv_two_step with ⟨w, hw_mem, hvw_edge, hw_succ_edge⟩

      -- v → w 说明 w < v
      have hw_lt_v : w < v := by
        simpa [descendingNatTournament] using hvw_edge

      -- w → v+1 说明 v+1 < w
      have hsucc_lt_w : v + 1 < w := by
        simpa [descendingNatTournament] using hw_succ_edge

      -- 所以 v+1 < w < v，从而 v+1 ≤ v，矛盾
      have hle : v + 1 ≤ v :=
        le_trans (Nat.le_of_lt hsucc_lt_w) (Nat.le_of_lt hw_lt_v)

      have hle' : Nat.succ v ≤ v := by
        simpa [Nat.succ_eq_add_one] using hle

      exact (Nat.not_succ_le_self v) hle'

-- 2.(a)

-- 请你证明：存在一个常数 N，当 n 大于 N 时，存在有 n 个顶点的每个顶点都是King 的 Tournament

/-
构造思路：

可以取 N = 5。然后分奇偶讨论。

一、n 为奇数，设 n = 2k + 1，其中 k ≥ 2。
取顶点集：V = {0, 1, ..., 2k}。
定义边：i → j  当且仅当  j - i (mod 2k+1) ∈ {1, 2, ..., k}，这是一个 tournament：
任意两个不同点 i,j，令 d = j - i (mod 2k+1)。
若 d ∈ {1,...,k}，则 i → j；
若 d ∈ {k+1,...,2k}，则 j → i。
所以任意两个不同顶点之间恰好有一个方向的边。

每个顶点都是 king：
任取 i,j。
若 j - i (mod 2k+1) ∈ {1,...,k}，则 i → j，一步到达。
否则取中间点 w = i + k (mod 2k+1)。
则 i → w，且 w → j。
所以 i 可以在两步内到达 j。
因此奇数个顶点时构造成立。

二、n 为偶数，设 n = 2k，其中 k ≥ 3。先构造 2k - 1 个旧顶点：0, 1, ..., 2k - 2。
旧顶点之间按照上面的奇数循环 tournament 连边：i → j  当且仅当  j - i (mod 2k - 1) ∈ {1, 2, ..., k - 1}，然后加入一个新顶点，记作 ∞。
定义新顶点与旧顶点之间的边：
  ∞ → i  当且仅当 i 是偶数；
  i → ∞  当且仅当 i 是奇数。

这是一个 tournament：
旧点之间已经是 tournament；
∞ 和每个旧点之间也恰好有一个方向。

每个顶点都是 king：

1. 旧点到旧点：
   由 2k - 1 个旧点上的奇数循环 tournament 保证。

2. ∞ 到旧点 j：
   若 j 是偶数，则 ∞ → j。
   若 j 是奇数，则取 w = j - 1。
   因为 w 是偶数，所以 ∞ → w；
   又因为 w → j，所以 ∞ → w → j。

3. 旧点 i 到 ∞：
   若 i 是奇数，则 i → ∞。
   若 i 是偶数，通常取 w = i + 1。
   因为 w 是奇数，所以 w → ∞；
   又因为 i → w，所以 i → w → ∞。
   边界情况 i = 2k - 2 时，取 w = 1。
   此时 2k - 2 → 1，且 1 → ∞。

因此偶数个顶点时也构造成立。

综上，对所有 n ≥ 5，都存在一个 n 个顶点的 tournament，
其中每个顶点都是 king。
所以原命题成立，可以取 N = 5。
-/

-- 自然数要么偶，要么奇
lemma nat_even_or_odd (n : Nat) : Even n ∨ Odd n := by
  induction n with
  | zero =>
      left
      use 0
  | succ n ih =>
      rcases ih with hEven | hOdd
      · right
        rcases hEven with ⟨k, hk⟩
        use k
        omega
      · left
        rcases hOdd with ⟨k, hk⟩
        use k + 1
        omega

-- 循环边
def cyclicEdge (m r i j : Nat) : Prop :=
  i < m ∧
  j < m ∧
  i ≠ j ∧
  let d := (j + m - i) % m
  1 ≤ d ∧ d ≤ r

-- 奇数构造
def oddCyclicTournament (k : Nat) : DirectedGraph where
  vertices := {v : Vertex | v < 2 * k + 1}
  edges :=
    {e : Vertex × Vertex |
      cyclicEdge (2 * k + 1) k e.1 e.2}

-- 偶数构造
def evenExtendedTournament (k : Nat) : DirectedGraph where
  vertices := {v : Vertex | v < 2 * k}
  edges :=
    {e : Vertex × Vertex |
      (e.1 < 2 * k - 1 ∧
       e.2 < 2 * k - 1 ∧
       cyclicEdge (2 * k - 1) (k - 1) e.1 e.2)
      ∨
      (e.1 = 2 * k - 1 ∧
       e.2 < 2 * k - 1 ∧
       Even e.2)
      ∨
      (e.1 < 2 * k - 1 ∧
       e.2 = 2 * k - 1 ∧
       Odd e.1)}

-- 奇数构造正确性（太过复杂）
lemma oddCyclicTournament_all_kings
    (k : Nat)
    (hk : 2 ≤ k) :
    isTournament (oddCyclicTournament k) ∧
    (oddCyclicTournament k).vertices.ncard = 2 * k + 1 ∧
    ∀ v : Vertex,
      v ∈ (oddCyclicTournament k).vertices →
      isKing (oddCyclicTournament k) v := by
  sorry

-- 偶数构造正确性（太过复杂）
lemma evenExtendedTournament_all_kings
    (k : Nat)
    (hk : 3 ≤ k) :
    isTournament (evenExtendedTournament k) ∧
    (evenExtendedTournament k).vertices.ncard = 2 * k ∧
    ∀ v : Vertex,
      v ∈ (evenExtendedTournament k).vertices →
      isKing (evenExtendedTournament k) v := by
  sorry

-- 主定理
theorem all_kings_for_large_n :
  ∃ N : Nat, ∀ n ≥ N, ∃ G : DirectedGraph,
    isTournament G ∧
    G.vertices.ncard = n ∧
    ∀ v : Vertex, v ∈ G.vertices → isKing G v := by
  refine ⟨5, ?_⟩

  intro n hn

  have hparity : Even n ∨ Odd n := nat_even_or_odd n

  rcases hparity with heven | hodd

  · rcases heven with ⟨k, hk⟩

    have hk3 : 3 ≤ k := by
      omega

    refine ⟨evenExtendedTournament k, ?_, ?_, ?_⟩

    · exact (evenExtendedTournament_all_kings k hk3).1

    · have hcard :
        (evenExtendedTournament k).vertices.ncard = 2 * k :=
        (evenExtendedTournament_all_kings k hk3).2.1
      omega

    · exact (evenExtendedTournament_all_kings k hk3).2.2

  · rcases hodd with ⟨k, hk⟩

    have hk2 : 2 ≤ k := by
      omega

    refine ⟨oddCyclicTournament k, ?_, ?_, ?_⟩

    · exact (oddCyclicTournament_all_kings k hk2).1

    · have hcard :
        (oddCyclicTournament k).vertices.ncard = 2 * k + 1 :=
        (oddCyclicTournament_all_kings k hk2).2.1
      omega

    · exact (oddCyclicTournament_all_kings k hk2).2.2

-- 2.(b)请思考是否存在一个每个顶点都是King的无限Tournament，给出你的命题并证明
/-
解题思路：
构造点m、n，满足下面构造要求
m<n，n-m为奇数，m->n
m>n，m-n为偶数，m->n
验证即可
（如果你将点改为Int类型可以直接用奇偶性进行区分）
-/

-- 奇数和偶数不能同时成立
lemma odd_even_false {n : Nat} (hOdd : Odd n) (hEven : Even n) : False := by
  rcases hOdd with ⟨a, ha⟩
  rcases hEven with ⟨b, hb⟩
  omega

lemma odd_one_nat : Odd (1 : Nat) := by
  use 0
  norm_num

-- 若 n 是正偶数，则 n - 1 是奇数
lemma odd_sub_one_of_even_pos {n : Nat}
    (hpos : 0 < n)
    (hEven : Even n) :
    Odd (n - 1) := by
  rcases hEven with ⟨k, hk⟩
  use k - 1
  omega

-- 若 n 是奇数，则 n + 1 是偶数
lemma even_add_one_of_odd {n : Nat}
    (hOdd : Odd n) :
    Even (n + 1) := by
  rcases hOdd with ⟨k, hk⟩
  use k + 1
  omega

-- 如果 v < u 且 u - v 是偶数，那么 v < u - 1
lemma lt_pred_of_lt_even_sub {v u : Nat}
    (hvu : v < u)
    (hEven : Even (u - v)) :
    v < u - 1 := by
  rcases hEven with ⟨k, hk⟩
  omega

-- 如果 v < u 且 u - v 是偶数，那么 (u - 1) - v 是奇数
lemma odd_pred_sub_of_even_sub {v u : Nat}
    (hvu : v < u)
    (hEven : Even (u - v)) :
    Odd ((u - 1) - v) := by
  have hpos : 0 < u - v := Nat.sub_pos_of_lt hvu
  have hOdd : Odd ((u - v) - 1) :=
    odd_sub_one_of_even_pos hpos hEven
  convert hOdd using 1
  omega

-- 如果 u < v 且 v - u 是奇数，那么 (v + 1) - u 是偶数
lemma even_succ_sub_of_odd_sub {u v : Nat}
    (huv : u < v)
    (hOdd : Odd (v - u)) :
    Even ((v + 1) - u) := by
  have hEven : Even ((v - u) + 1) :=
    even_add_one_of_odd hOdd
  convert hEven using 1
  omega

-- 构造无限 Tournament：
-- m → n 当且仅当：
-- 1. m < n 且 n - m 为奇数；
-- 或者
-- 2. n < m 且 m - n 为偶数。
def oddStepTournament : DirectedGraph where
  vertices := Set.univ
  edges :=
    {e : Vertex × Vertex |
      (e.1 < e.2 ∧ Odd (e.2 - e.1)) ∨
      (e.2 < e.1 ∧ Even (e.1 - e.2))}

lemma oddStepTournament_isTournament :
    isTournament oddStepTournament := by
  constructor

  · -- 边的两个端点都在顶点集中，且没有自环
    intro e he
    have he' :
        (e.1 < e.2 ∧ Odd (e.2 - e.1)) ∨
        (e.2 < e.1 ∧ Even (e.1 - e.2)) := by
      simpa [oddStepTournament] using he

    constructor
    · simp [oddStepTournament]
    · constructor
      · simp [oddStepTournament]
      · rcases he' with h | h
        · exact ne_of_lt h.1
        · exact ne_of_gt h.1

  · constructor

    · -- 任意两个不同顶点之间，恰好有一个方向的边
      intro u v hu hv huv

      have hcases : u < v ∨ v < u := lt_or_gt_of_ne huv

      rcases hcases with huvlt | hvult

      · -- 情况一：u < v
        have hparity : Even (v - u) ∨ Odd (v - u) :=
          nat_even_or_odd (v - u)

        rcases hparity with hEven | hOdd

        · -- 若 v - u 为偶数，则 v → u
          right
          constructor

          · -- 证明 (v,u) 是边
            change
              (v < u ∧ Odd (u - v)) ∨
              (u < v ∧ Even (v - u))
            exact Or.inr ⟨huvlt, hEven⟩

          · -- 证明 (u,v) 不是边
            intro hEdge
            have hEdge' :
                (u < v ∧ Odd (v - u)) ∨
                (v < u ∧ Even (u - v)) := by
              simpa [oddStepTournament] using hEdge

            rcases hEdge' with h1 | h2
            · exact odd_even_false h1.2 hEven
            · exact (not_lt_of_ge (le_of_lt huvlt)) h2.1

        · -- 若 v - u 为奇数，则 u → v
          left
          constructor

          · -- 证明 (u,v) 是边
            change
              (u < v ∧ Odd (v - u)) ∨
              (v < u ∧ Even (u - v))
            exact Or.inl ⟨huvlt, hOdd⟩

          · -- 证明 (v,u) 不是边
            intro hEdge
            have hEdge' :
                (v < u ∧ Odd (u - v)) ∨
                (u < v ∧ Even (v - u)) := by
              simpa [oddStepTournament] using hEdge

            rcases hEdge' with h1 | h2
            · exact (not_lt_of_ge (le_of_lt huvlt)) h1.1
            · exact odd_even_false hOdd h2.2

      · -- 情况二：v < u
        have hparity : Even (u - v) ∨ Odd (u - v) :=
          nat_even_or_odd (u - v)

        rcases hparity with hEven | hOdd

        · -- 若 u - v 为偶数，则 u → v
          left
          constructor

          · -- 证明 (u,v) 是边
            change
              (u < v ∧ Odd (v - u)) ∨
              (v < u ∧ Even (u - v))
            exact Or.inr ⟨hvult, hEven⟩

          · -- 证明 (v,u) 不是边
            intro hEdge
            have hEdge' :
                (v < u ∧ Odd (u - v)) ∨
                (u < v ∧ Even (v - u)) := by
              simpa [oddStepTournament] using hEdge

            rcases hEdge' with h1 | h2
            · exact odd_even_false h1.2 hEven
            · exact (not_lt_of_ge (le_of_lt hvult)) h2.1

        · -- 若 u - v 为奇数，则 v → u
          right
          constructor

          · -- 证明 (v,u) 是边
            change
              (v < u ∧ Odd (u - v)) ∨
              (u < v ∧ Even (v - u))
            exact Or.inl ⟨hvult, hOdd⟩

          · -- 证明 (u,v) 不是边
            intro hEdge
            have hEdge' :
                (u < v ∧ Odd (v - u)) ∨
                (v < u ∧ Even (u - v)) := by
              simpa [oddStepTournament] using hEdge

            rcases hEdge' with h1 | h2
            · exact (not_lt_of_ge (le_of_lt hvult)) h1.1
            · exact odd_even_false hOdd h2.2

    · -- 顶点集非空
      exact ⟨0, by simp [oddStepTournament]⟩


-- 2.(b) 存在一个每个顶点都是 King 的无限 Tournament
theorem all_kings_in_infinite_tournament :
  ∃ G : DirectedGraph,
    isInfiniteTournament G ∧
      (∀ v : Vertex, v ∈ G.vertices → isKing G v) := by
  classical

  refine ⟨oddStepTournament, ?_, ?_⟩

  · -- 证明这是一个无限 Tournament
    constructor

    · -- 顶点集是 Nat 全体，所以无限
      have hInf : (Set.univ : Set Vertex).Infinite := Set.infinite_univ
      simpa [oddStepTournament] using hInf

    · -- 证明它是 Tournament
      exact oddStepTournament_isTournament

  · -- 证明每个顶点都是 King
    intro v hv

    constructor
    · exact hv

    · intro u hu huv

      have hcases : u < v ∨ v < u := lt_or_gt_of_ne huv

      rcases hcases with huvlt | hvult

      · -- 情况一：u < v
        have hparity : Even (v - u) ∨ Odd (v - u) :=
          nat_even_or_odd (v - u)

        rcases hparity with hEven | hOdd

        · -- 若 v - u 为偶数，则 v 可以一步到达 u
          left
          change
            (v < u ∧ Odd (u - v)) ∨
            (u < v ∧ Even (v - u))
          exact Or.inr ⟨huvlt, hEven⟩

        · -- 若 v - u 为奇数，则取 w = v + 1
          right
          refine ⟨v + 1, ?_, ?_, ?_⟩

          · simp [oddStepTournament]

          · -- v → v+1
            change
              (v < v + 1 ∧ Odd ((v + 1) - v)) ∨
              (v + 1 < v ∧ Even (v - (v + 1)))
            left
            constructor
            · exact Nat.lt_succ_self v
            · have hdiff : (v + 1) - v = 1 := by
                simpa [Nat.add_comm] using (Nat.add_sub_cancel_right 1 v)
              rw [hdiff]
              exact odd_one_nat

          · -- v+1 → u
            change
              (v + 1 < u ∧ Odd (u - (v + 1))) ∨
              (u < v + 1 ∧ Even ((v + 1) - u))
            right
            constructor
            · exact lt_trans huvlt (Nat.lt_succ_self v)
            · exact even_succ_sub_of_odd_sub huvlt hOdd

      · -- 情况二：v < u
        have hparity : Even (u - v) ∨ Odd (u - v) :=
          nat_even_or_odd (u - v)

        rcases hparity with hEven | hOdd

        · -- 若 u - v 为偶数，则取 w = u - 1
          right
          refine ⟨u - 1, ?_, ?_, ?_⟩

          · simp [oddStepTournament]

          · -- v → u-1
            change
              (v < u - 1 ∧ Odd ((u - 1) - v)) ∨
              (u - 1 < v ∧ Even (v - (u - 1)))
            left
            constructor
            · exact lt_pred_of_lt_even_sub hvult hEven
            · exact odd_pred_sub_of_even_sub hvult hEven

          · -- u-1 → u
            change
              (u - 1 < u ∧ Odd (u - (u - 1))) ∨
              (u < u - 1 ∧ Even ((u - 1) - u))
            left
            constructor
            · cases u with
              | zero =>
                  exact False.elim (Nat.not_lt_zero v hvult)
              | succ u =>
                  simp
            · have hdiff : u - (u - 1) = 1 := by
                cases u with
                | zero =>
                    exact False.elim (Nat.not_lt_zero v hvult)
                | succ u =>
                    simp
              rw [hdiff]
              exact odd_one_nat

        · -- 若 u - v 为奇数，则 v 可以一步到达 u
          left
          change
            (v < u ∧ Odd (u - v)) ∨
            (u < v ∧ Even (v - u))
          exact Or.inl ⟨hvult, hOdd⟩


-- 3.假设在一个无限的Tournament中，每个顶点都有有限的“in-degree”（即只有有限多的边指向该顶点）。证明在其中存在一个King。（Hint：利用Compactness Theorem）

-- 定义入邻居
def inNeighbors (G : DirectedGraph) (v : Vertex) : Set Vertex :=
  {u : Vertex | u ∈ G.vertices ∧ (u,v) ∈ G.edges}
-- 入邻居集的基数即为入度
noncomputable def inDegree (G : DirectedGraph) (v : Vertex) : Nat :=
  (inNeighbors G v).ncard

-- 判断顶点有有限的入度（你也可以自己定义一个判定条件）
def hasFiniteIndegree (G : DirectedGraph) (v : Vertex) : Prop :=
  (inNeighbors G v).Finite

-- 诱导子图：在顶点子集 S 上保留原图中的边
def inducedSubgraph (G : DirectedGraph) (S : Set Vertex) : DirectedGraph where
  vertices := S
  edges := {e : Vertex × Vertex | e ∈ G.edges ∧ e.1 ∈ S ∧ e.2 ∈ S}

-- 诱导子图仍然是 tournament
lemma inducedSubgraph_isTournament
    (G : DirectedGraph)
    (S : Set Vertex)
    (hT : isTournament G)
    (hsub : S ⊆ G.vertices)
    (hSnonempty : S.Nonempty) :
    isTournament (inducedSubgraph G S) := by
  constructor

  · -- 每条边都连接诱导子图中的两个不同顶点
    intro e he
    rcases he with ⟨heG, he1S, he2S⟩

    have hvalid := hT.1 e heG

    constructor
    · exact he1S
    · constructor
      · exact he2S
      · exact hvalid.2.2

  · constructor

    · -- 任意两个不同顶点之间恰好有一个方向的边
      intro u v huS hvS huv

      have huG : u ∈ G.vertices := hsub huS
      have hvG : v ∈ G.vertices := hsub hvS

      have hdir := hT.2.1 u v huG hvG huv

      rcases hdir with huv_edge | hvu_edge

      · left
        constructor

        · exact ⟨huv_edge.1, huS, hvS⟩

        · intro hvu_in_induced
          exact huv_edge.2 hvu_in_induced.1

      · right
        constructor

        · exact ⟨hvu_edge.1, hvS, huS⟩

        · intro huv_in_induced
          exact hvu_edge.2 huv_in_induced.1

    · -- 非空
      exact hSnonempty

-- 如果某个顶点没有入邻居，那么它是 king
lemma vertex_is_king_if_no_inNeighbors
    (G : DirectedGraph)
    (hT : isTournament G)
    (v : Vertex)
    (hv : v ∈ G.vertices)
    (hempty : inNeighbors G v = ∅) :
    isKing G v := by
  constructor

  · exact hv

  · intro u hu huv

    -- 因为 u ≠ v，所以 tournament 中 v,u 之间有且仅有一个方向
    have hdir := hT.2.1 v u hv hu (Ne.symm huv)

    rcases hdir with hvu_edge | huv_edge

    · -- 如果 v → u，则一步到达
      exact Or.inl hvu_edge.1

    · -- 如果 u → v，则 u 是 v 的入邻居，矛盾
      exfalso

      have hu_in : u ∈ inNeighbors G v := by
        exact ⟨hu, huv_edge.1⟩

      rw [hempty] at hu_in
      simp at hu_in


theorem finite_indegree_in_infinite_tournament :
  ∀ G : DirectedGraph,
    isInfiniteTournament G →
    (∀ v : Vertex, v ∈ G.vertices → hasFiniteIndegree G v) →
    ∃ v : Vertex, isKing G v := by
  intro G hG hFiniteIn

  rcases hG with ⟨hInfinite, hT⟩

  -- 先任取一个顶点 a
  rcases hT.2.2 with ⟨a, ha⟩

  let S : Set Vertex := inNeighbors G a

  -- S 是有限集，因为 a 的入度有限
  have hSfinite : S.Finite := by
    simpa [S, hasFiniteIndegree] using hFiniteIn a ha

  -- S 中的点当然都是 G 的顶点
  have hSsub : S ⊆ G.vertices := by
    intro x hx
    exact hx.1

  -- 分情况：S 是否为空
  by_cases hSempty : S = ∅

  · -- 如果 a 没有入邻居，那么 a 是 source，所以 a 是 king
    have haKing : isKing G a := by
      apply vertex_is_king_if_no_inNeighbors G hT a ha
      simpa [S] using hSempty

    exact ⟨a, haKing⟩

  · -- 如果 S 非空，则考虑 G 在 S 上的有限诱导子 tournament
    have hSnonempty : S.Nonempty := by
      by_contra hno
      apply hSempty
      ext x
      constructor

      · intro hx
        exact False.elim (hno ⟨x, hx⟩)

      · intro hx
        simp at hx

    let H : DirectedGraph := inducedSubgraph G S

    have hHfinite : H.vertices.Finite := by
      simpa [H, inducedSubgraph] using hSfinite

    have hHtournament : isTournament H := by
      simpa [H] using
        inducedSubgraph_isTournament G S hT hSsub hSnonempty

    have hHfiniteTournament : isFiniteTournament H := by
      exact ⟨hHfinite, hHtournament⟩

    -- 由 1(a)，有限 tournament H 中存在 king
    obtain ⟨k, hkH⟩ := king_in_finite_tournament H hHfiniteTournament

    -- 证明这个 k 也是原图 G 的 king
    have hkS : k ∈ S := by
      simpa [H, inducedSubgraph] using hkH.1

    have hkG : k ∈ G.vertices := hkS.1

    refine ⟨k, ?_⟩

    constructor

    · exact hkG

    · intro u hu huk

      by_cases hua : u = a

      · -- 如果 u = a，因为 k ∈ inNeighbors G a，所以 k → a
        subst hua
        exact Or.inl hkS.2

      · by_cases huS : u ∈ S

        · -- 如果 u ∈ S，那么在有限子 tournament H 中，k 两步内可达 u
          have hreachH := hkH.2 u (by simpa [H, inducedSubgraph] using huS) huk

          rcases hreachH with hku | htwo

          · -- H 中的一步边也是 G 中的一步边
            exact Or.inl hku.1

          · -- H 中的两步路径也是 G 中的两步路径
            right
            rcases htwo with ⟨w, hwH, hkw, hwu⟩

            have hwS : w ∈ S := by
              simpa [H, inducedSubgraph] using hwH

            exact ⟨w, hwS.1, hkw.1, hwu.1⟩

        · -- 如果 u ∉ S，则 u 不是 a 的入邻居
          -- 又因为 u ≠ a，所以 tournament 中只能有 a → u
          right

          have hau : (a, u) ∈ G.edges := by
            have hau_or_hua := hT.2.1 a u ha hu (by
              intro hau_eq
              apply hua
              exact hau_eq.symm
            )

            rcases hau_or_hua with hau_edge | hua_edge

            · exact hau_edge.1

            · exfalso
              apply huS
              exact ⟨hu, hua_edge.1⟩

          -- k → a，因为 k ∈ inNeighbors G a；再 a → u
          exact ⟨a, ha, hkS.2, hau⟩

-- 4.(a)证明或反驳：一个有限Tournament有一个source（入度为零的顶点），当且仅当有一个 sink（出度为零的顶点）。
/-
反驳：
4点abcd
a->b,a->c,a->d,b->c,c->d,d->b
有一个source但是没有sink
-/

-- source：顶点在图中，并且入邻居为空
def isSource (G : DirectedGraph) (v : Vertex) : Prop :=
  v ∈ G.vertices ∧ inNeighbors G v = ∅

-- sink：顶点在图中，并且出邻居为空
def isSink (G : DirectedGraph) (v : Vertex) : Prop :=
  v ∈ G.vertices ∧ outNeighbors G v = ∅

def fourVertexTournament : DirectedGraph where
  vertices := ({0, 1, 2, 3} : Set Vertex)
  edges :=
    ({(0, 1), (0, 2), (0, 3), (1, 2), (2, 3), (3, 1)}
      : Set (Vertex × Vertex))

lemma fourVertexTournament_isTournament :
    isTournament fourVertexTournament := by
  constructor

  · -- 所有边都连接图中的两个不同顶点
    intro e he
    rcases e with ⟨x, y⟩

    simp [fourVertexTournament] at he ⊢

    rcases he with h | h | h | h | h | h <;>
      rcases h with ⟨rfl, rfl⟩ <;>
      norm_num

  · constructor

    · -- 任意两个不同顶点之间恰好有一个方向的边
      intro u v hu hv huv

      simp [fourVertexTournament] at hu hv ⊢

      rcases hu with rfl | rfl | rfl | rfl
      · rcases hv with rfl | rfl | rfl | rfl
        · contradiction
        · simp
        · simp
        · simp

      · rcases hv with rfl | rfl | rfl | rfl
        · simp
        · contradiction
        · simp
        · simp

      · rcases hv with rfl | rfl | rfl | rfl
        · simp
        · simp
        · contradiction
        · simp

      · rcases hv with rfl | rfl | rfl | rfl
        · simp
        · simp
        · simp
        · contradiction

    · -- 非空
      exact ⟨0, by simp [fourVertexTournament]⟩

lemma fourVertexTournament_finite :
    fourVertexTournament.vertices.Finite := by
  simp [fourVertexTournament]

-- 0 是 source
lemma zero_is_source_in_fourVertexTournament :
    isSource fourVertexTournament 0 := by
  constructor

  · -- 0 是顶点
    simp [fourVertexTournament]

  · -- 0 的入邻居为空
    ext u
    simp [inNeighbors, fourVertexTournament]

-- 没有 sink
lemma no_sink_in_fourVertexTournament :
    ¬ ∃ v : Vertex, isSink fourVertexTournament v := by
  intro h
  rcases h with ⟨v, hvSink⟩
  rcases hvSink with ⟨hv_mem, hv_no_out⟩

  simp [fourVertexTournament] at hv_mem

  rcases hv_mem with rfl | rfl | rfl | rfl

  · -- v = 0，有出边 0 → 1
    have hmem : 1 ∈ outNeighbors fourVertexTournament 0 := by
      simp [outNeighbors, fourVertexTournament]

    rw [hv_no_out] at hmem
    simp at hmem

  · -- v = 1，有出边 1 → 2
    have hmem : 2 ∈ outNeighbors fourVertexTournament 1 := by
      simp [outNeighbors, fourVertexTournament]

    rw [hv_no_out] at hmem
    simp at hmem

  · -- v = 2，有出边 2 → 3
    have hmem : 3 ∈ outNeighbors fourVertexTournament 2 := by
      simp [outNeighbors, fourVertexTournament]

    rw [hv_no_out] at hmem
    simp at hmem

  · -- v = 3，有出边 3 → 1
    have hmem : 1 ∈ outNeighbors fourVertexTournament 3 := by
      simp [outNeighbors, fourVertexTournament]

    rw [hv_no_out] at hmem
    simp at hmem

-- 不同意
theorem neg_source_and_sink_equivalence :
  ∃ G : DirectedGraph, isFiniteTournament G ∧
    ¬ ((∃ v : Vertex, isSource G v) ↔
       (∃ v : Vertex, isSink G v)) := by
  refine ⟨fourVertexTournament, ?_, ?_⟩

  · -- 它是有限 tournament
    constructor

    · exact fourVertexTournament_finite

    · exact fourVertexTournament_isTournament

  · -- 它有 source，但没有 sink，所以 iff 不成立
    intro hiff

    have hSource : ∃ v : Vertex, isSource fourVertexTournament v := by
      exact ⟨0, zero_is_source_in_fourVertexTournament⟩

    have hSink : ∃ v : Vertex, isSink fourVertexTournament v :=
      hiff.mp hSource

    exact no_sink_in_fourVertexTournament hSink


-- 4.(b)对于无限Tournament呢？反驳！
/-
反对
自然数集
小指向大
有source但是没有sink
-/


-- 无限反例：
-- 顶点是所有自然数，边从小的自然数指向大的自然数
def increasingNatTournament : DirectedGraph where
  vertices := Set.univ
  edges := {e : Vertex × Vertex | e.1 < e.2}

lemma increasingNatTournament_isTournament :
    isTournament increasingNatTournament := by
  constructor

  · -- 每条边都连接两个图中不同的顶点
    intro e he

    have hlt : e.1 < e.2 := by
      simpa [increasingNatTournament] using he

    constructor
    · simp [increasingNatTournament]
    · constructor
      · simp [increasingNatTournament]
      · exact ne_of_lt hlt

  · constructor

    · -- 任意两个不同顶点之间，恰好有一个方向的边
      intro u v hu hv huv

      have hcases : u < v ∨ v < u := lt_or_gt_of_ne huv

      rcases hcases with huvlt | hvult

      · -- 情况一：u < v，所以 u → v
        left
        constructor

        · -- (u,v) 是边
          simpa [increasingNatTournament] using huvlt

        · -- (v,u) 不是边
          intro hvu_edge
          have hvu_lt : v < u := by
            simpa [increasingNatTournament] using hvu_edge
          exact (not_lt_of_ge (le_of_lt huvlt)) hvu_lt

      · -- 情况二：v < u，所以 v → u
        right
        constructor

        · -- (v,u) 是边
          simpa [increasingNatTournament] using hvult

        · -- (u,v) 不是边
          intro huv_edge
          have huv_lt : u < v := by
            simpa [increasingNatTournament] using huv_edge
          exact (not_lt_of_ge (le_of_lt hvult)) huv_lt

    · -- 顶点集非空
      exact ⟨0, by simp [increasingNatTournament]⟩

-- 0 是 source，因为没有自然数小于 0
lemma zero_is_source_in_increasingNatTournament :
    isSource increasingNatTournament 0 := by
  constructor

  · -- 0 是顶点
    simp [increasingNatTournament]

  · -- 0 的入邻居为空
    ext u
    simp [inNeighbors, increasingNatTournament]

-- 没有 sink，因为任意 v 都有出边 v → v+1
lemma no_sink_in_increasingNatTournament :
    ¬ ∃ v : Vertex, isSink increasingNatTournament v := by
  intro h

  rcases h with ⟨v, hvSink⟩
  rcases hvSink with ⟨hv_mem, hout_empty⟩

  -- v+1 是 v 的出邻居
  have hmem : v + 1 ∈ outNeighbors increasingNatTournament v := by
    dsimp [outNeighbors, increasingNatTournament]
    constructor
    · simp
    · exact Nat.lt_succ_self v

  -- 但如果 v 是 sink，则 outNeighbors v = ∅，矛盾
  have hnot : v + 1 ∉ outNeighbors increasingNatTournament v := by
    rw [hout_empty]
    simp

  exact hnot hmem

theorem neg_source_and_sink_equivalence_in_infinite_tournament :
  ∃ G : DirectedGraph, isInfiniteTournament G ∧
    ¬ ((∃ v : Vertex, isSource G v) ↔
       (∃ v : Vertex, isSink G v)) := by
  refine ⟨increasingNatTournament, ?_, ?_⟩

  · -- 证明它是无限 tournament
    constructor

    · -- 顶点集是 Nat 全体，所以无限
      have hInf : (Set.univ : Set Vertex).Infinite := Set.infinite_univ
      simpa [increasingNatTournament] using hInf

    · -- 它是 tournament
      exact increasingNatTournament_isTournament

  · -- 它有 source，但没有 sink，因此 iff 不成立
    intro hiff

    have hSource : ∃ v : Vertex, isSource increasingNatTournament v := by
      exact ⟨0, zero_is_source_in_increasingNatTournament⟩

    have hSink : ∃ v : Vertex, isSink increasingNatTournament v :=
      hiff.mp hSource

    exact no_sink_in_increasingNatTournament hSink