编辑“︁Lean图结构”︁（章节）

= Lean图结构 =

图（Graph）是计算机科学中最重要的数据结构之一，用于表示对象及其关系。在Lean定理证明器中，图结构可以通过多种方式实现，并用于形式化验证算法或建模复杂系统。

== 基本概念 ==

图由'''顶点'''（Vertices/Nodes）和'''边'''（Edges）组成，数学上表示为 <math>G = (V, E)</math>：
* <math>V</math> 是顶点集合
* <math>E \subseteq V \times V</math> 是边集合

'''类型分类'''：
* '''有向图'''：边有方向（箭头表示）
* '''无向图'''：边无方向（可视为双向）
* '''加权图'''：边带有权值
* '''连通图'''：任意两顶点间存在路径

<mermaid>
graph LR
    A --> B
    B --> C
    C --> A
    D --> E
</mermaid>

== Lean中的实现 ==

在Lean中，图可以通过以下方式表示：

=== 邻接列表表示法 ===
<syntaxhighlight lang="lean">
structure Graph (V : Type) where
  adjList : V → List V  -- 每个顶点对应的邻接顶点列表

-- 示例：有向图
def sampleGraph : Graph Nat := {
  adjList := fun
    | 1 => [2, 3]
    | 2 => [4]
    | 3 => [4]
    | 4 => []
    | _ => []
}
</syntaxhighlight>

=== 边集表示法 ===
<syntaxhighlight lang="lean">
structure Edge (V : Type) :=
  (src : V) (dest : V)

structure Graph (V : Type) where
  vertices : List V
  edges : List (Edge V)

-- 示例：无向图（每条边需要添加双向）
def undirectedGraph : Graph Nat := {
  vertices := [1, 2, 3, 4],
  edges := [
    Edge.mk 1 2, Edge.mk 2 1,
    Edge.mk 2 3, Edge.mk 3 2,
    Edge.mk 3 4, Edge.mk 4 3
  ]
}
</syntaxhighlight>

== 基本操作 ==

=== 添加顶点 ===
<syntaxhighlight lang="lean">
def addVertex (g : Graph V) (v : V) : Graph V :=
  { g with vertices := v :: g.vertices }
</syntaxhighlight>

=== 添加边 ===
<syntaxhighlight lang="lean">
def addEdge (g : Graph V) (e : Edge V) : Graph V :=
  { g with edges := e :: g.edges }
</syntaxhighlight>

=== 深度优先搜索（DFS） ===
<syntaxhighlight lang="lean">
partial def dfs [DecidableEq V] (g : Graph V) (start : V) : List V :=
  let rec visit (visited : List V) (current : V) : List V :=
    if current ∈ visited then visited
    else
      let neighbors := g.adjList current
      neighbors.foldl visit (current :: visited)
  visit [] start

-- 示例输出：
-- #eval dfs sampleGraph 1  -- [4, 2, 3, 1]
</syntaxhighlight>

== 形式化验证案例 ==

验证"图中从顶点u到v存在路径"的性质：

<syntaxhighlight lang="lean">
inductive Path {V : Type} (g : Graph V) : V → V → Prop
| nil (u : V) : Path g u u
| cons (u v w : V) : Edge g u v → Path g v w → Path g u w

theorem path_exists (g : Graph Nat) (u v : Nat) :
  (∃ path : List Nat, isPath g u v path) ↔ Reachable g u v := by
  constructor
  { intro ⟨p, hp⟩; induction hp <;> simp [Reachable] }
  { intro h; induction h <;> simp [isPath] }
</syntaxhighlight>

== 应用场景 ==

1. '''社交网络分析'''：顶点表示用户，边表示关系
2. '''路由算法'''：网络拓扑建模
3. '''依赖解析'''：如构建系统的模块依赖
4. '''状态机建模'''：顶点表示状态，边表示转移

=== 最短路径案例 ===
<mermaid>
graph LR
    A --5--> B
    A --1--> C
    B --2--> D
    C --4--> D
    D --3--> E
</mermaid>

<syntaxhighlight lang="lean">
def shortestPath (g : Graph Nat) (start end : Nat) : Option Nat :=
  -- 使用Dijkstra算法实现
  -- 返回最短路径长度
  sorry  -- 实际实现需要优先队列
</syntaxhighlight>

== 进阶主题 ==

* '''图同构验证'''：证明两个图结构相同
* '''平面性检测'''：形式化验证图是否可平面绘制
* '''着色问题'''：形式化四色定理等图着色性质
* '''流网络'''：验证最大流最小割定理

== 练习建议 ==

1. 实现广度优先搜索（BFS）算法
2. 证明无向图中顶点度数和等于边数的两倍
3. 形式化树是连通无环图的定义
4. 实现拓扑排序算法并验证其正确性

通过Lean的形式化验证能力，可以确保图算法的正确性，这是传统编程语言难以实现的独特优势。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean数据结构]]