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 :=
  by sorry

-- 请你完成：判断一个顶点是否是King
def isKing (G : DirectedGraph) (v : Vertex) : Prop :=
  by sorry

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

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

-- 定义出邻居
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

-- 定义入邻居
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

-- 1.(a)证明每个有限Tournament中都存在一个King
-- Hint：考虑证明出度最大的节点是King
theorem king_in_finite_tournament (G : DirectedGraph) (h : isFiniteTournament G) :
  ∃ v : Vertex, isKing G v :=
  sorry

-- 1.(b)证明存在没有King的无限Tournament
theorem infinite_tournament_without_king :
  ∃ G : DirectedGraph, isInfiniteTournament G ∧
    (∀ v : Vertex, ¬ isKing G v) :=
    by sorry

-- 2.(a)

-- 请你证明：存在一个常数 N，当 n 大于 N 时，在 n 个顶点的 Tournament 中，每个顶点都是King
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
  sorry


-- 2.(b)请思考是否存在一个每个顶点都是King的无限Tournament，给出你的命题并证明
/-
如果是，请完成：
theorem all_kings_in_infinite_tournament :
  ∃ G : DirectedGraph, isInfiniteTournament G ∧ (∀ v : Vertex, v ∈ G.vertices → isKing G v) :=
  by sorry
如果不是，请完成：
theorem neg_all_kings_in_infinite_tournament :
  ∀ G : DirectedGraph, isInfiniteTournament G ∧ (∃ v : Vertex, v ∈ G.vertices ∧ ¬isKing G v) :=
  by sorry
-/
-- 3.假设在一个无限的Tournament中，每个顶点都有有限的“in-degree”（即只有有限多的边指向该顶点）。证明在其中存在一个King。
-- Hint：利用Compactness Theorem
-- 你也可以不使用Compactness Theorem而直接对诱导子图的king验证其为原图的king

-- 判断顶点有有限的入度（你也可以自己定义一个判定条件）
def finite_indegree (G : DirectedGraph) (v : Vertex) (m : Nat) : Prop :=
  let count := {u : Vertex | (u, v) ∈ G.edges}.ncard;  -- 计算指向 v 的所有顶点数
  count < m  -- 确保指向 v 的顶点数小于 m

def finite_indegree_in_infinite_tournament :
  ∀ G : DirectedGraph, isInfiniteTournament G → (∀ v : Vertex, v ∈ G.vertices → (∃ m : Nat, finite_indegree G v m)) →
  ∃ v : Vertex, isKing G v :=
  by sorry

-- 4.(a)证明或反驳：一个有限Tournament有一个source（入度为零的顶点），当且仅当有一个 sink（出度为零的顶点）。
-- 判断顶点有有限的出度（你也可以自己定义一个判定条件）
def finite_outdegree (G : DirectedGraph) (u : Vertex) (m : Nat) : Prop :=
  let count := {v : Vertex | (u, v) ∈ G.edges}.ncard;  -- 计算 u 指向的所有顶点数
  count < m  -- 确保 u 指向的顶点数小于 m

-- 判断一个顶点是否是Source
def isSource (G : DirectedGraph) (v : Vertex) : Prop :=
  finite_indegree G v 1

-- 判断一个顶点是否是Sink
def isSink (G : DirectedGraph) (v : Vertex) : Prop :=
  finite_outdegree G v 1


--如果你同意，请完成：
theorem source_and_sink_equivalence :
  ∀ G : DirectedGraph, isFiniteTournament G →
    (∃ v : Vertex, isSource G v) ↔ (∃ v : Vertex, isSink G v) :=
    by sorry
--如果你不同意，请完成：
theorem neg_source_and_sink_equivalence :
  ∃ G : DirectedGraph, isFiniteTournament G ∧
    ¬((∃ v : Vertex, isSource G v) ↔ (∃ v : Vertex, isSink G v)) :=
    by sorry

-- 4.(b)对于无限Tournament呢？
/-
如果你同意，请完成：
theorem source_and_sink_equivalence_in_infinite_tournament :
  ∀ G : DirectedGraph, isInfiiniteTournament G →
    (∃ v : Vertex, isSource G v) ↔ (∃ v : Vertex, isSink G v) :=
    by sorry
如果你不同意，请完成：
theorem neg_source_and_sink_equivalence_in_infinite_tournament :
  ∃ G : DirectedGraph, isInfiiniteTournament G ∧
    ¬((∃ v : Vertex, isSource G v) ↔ (∃ v : Vertex, isSink G v)) :=
    by sorry
-/