编辑“︁Lean优先队列”︁（章节）

== Lean中的实现 ==

以下是一个基于二叉堆的Lean优先队列实现示例：

<syntaxhighlight lang="lean">
-- 定义优先队列结构
structure PriorityQueue (α : Type) [LE α] where
  heap : List α
  deriving Repr

-- 空优先队列
def PriorityQueue.empty : PriorityQueue α :=
  { heap := [] }

-- 插入元素
def PriorityQueue.insert (pq : PriorityQueue α) (x : α) : PriorityQueue α :=
  let newHeap := x :: pq.heap
  { heap := bubbleUp newHeap (newHeap.length - 1) }

-- 辅助函数：上浮操作
def bubbleUp (heap : List α) (idx : Nat) : List α :=
  match idx with
  | 0 => heap
  | i+1 =>
    let parentIdx := (i - 1) / 2
    if heap[i] ≤ heap[parentIdx] then heap
    else
      let swapped := heap.swap i parentIdx
      bubbleUp swapped parentIdx
</syntaxhighlight>

=== 操作示例 ===
输入：
<syntaxhighlight lang="lean">
let pq := PriorityQueue.empty
let pq := pq.insert 5
let pq := pq.insert 3
let pq := pq.insert 8
</syntaxhighlight>

输出队列内部表示：
<pre>
{ heap := [8, 3, 5] }
</pre>