插入排序与数组可变性

虽然插入排序的最差时间复杂度并不是最优，但它仍然有一些有用的属性：

• 它简单明了，易于实现和理解
• 它是一种原地排序算法，不需要额外的空间来运行
• 它是一种稳定排序
• 当输入已经排序得差不多时，它很快

原地算法在 Lean 中特别有用，因为它管理内存的方式。 在某些情况下，会复制数组的操作通常可以优化为直接修改。这包括交换数组中的元素。

大多数语言和具有自动内存管理的运行时系统，包括 JavaScript、JVM 和 .NET，都使用跟踪垃圾回收。 当需要回收内存时，系统从许多 根（例如调用栈和全局值）开始， 然后通过递归地追踪指针来确定可以到达哪些值。任何无法到达的值都会被释放，从而释放内存。

引用计数是追踪式垃圾回收的替代方法，它被许多语言使用，包括 Python、Swift 和 Lean。 在引用计数系统中，内存中的每个对象都有一个字段来跟踪对它的引用数。 当建立一个新引用时，计数器会增加。当一个引用不再存在时，计数器会减少。 当计数器达到零时，对象会立即被释放。

与追踪式垃圾回收器相比，引用计数有一个主要的缺点：循环引用会导致内存泄漏。 如果对象 \( A \) 引用对象 \( B \)，而对象 \( B \) 引用对象 \( A \)， 它们将永远不会被释放，即使程序中没有其他内容引用 \( A \) 或 \( B \)。 循环引用要么是由不受控制的递归引起的，要么是由可变引用引起的。由于 Lean 不支持这两者， 因此不可能构造循环引用。

引用计数意味着 Lean 运行时系统用于分配和释放数据结构的原语可以检查引用计数是否即将降至零， 并重新使用现有对象而非分配一个新对象。当使用大型数组时，这一点尤其重要。

针对 Lean 数组的插入排序的实现应满足以下条件：

1. Lean 应当接受没有 partial 标注的函数
2. 若传递了一个没有其他引用的数组，它应原地修改数组，而非分配一个新数组

第一个条件很容易检查：如果 Lean 接受该定义，则满足该条件。 然而，第二个条件需要一种测试方法。Lean 提供了一个名为 dbgTraceIfShared 的内置函数，其签名如下：

#check dbgTraceIfShared

dbgTraceIfShared.{u} {α : Type u} (s : String) (a : α) : α

它以一个字符串和一个值作为参数，如果该值有多个引用，则使用该字符串打印一条消息到标准错误， 并返回该值。严格来说，它不是一个纯函数。 但是，它仅在开发期间用于检查函数实际上能够重用内存而非分配和复制。

在学习使用 dbgTraceIfShared 时，重要的是要知道 #eval 会报告的值比已编译的代码中共享的值更多， 这可能会令人困惑。重要的是使用 lake 构建可执行文件，而非在编辑器中进行实验。

插入排序由两个循环组成。外层循环将指针从左向右移动到要排序的数组中。 每次迭代后，指针左边的数组区域都会被排序，而右边的区域可能尚未被排序。 内层循环获取指针指向的元素，并将其向左移动，直到找到合适的位置并恢复循环不变式。 换句话说，每次迭代都会将数组的下一个元素插入到已排序区域的合适位置。

内层循环

插入排序的内层循环可以实现为一个尾递归函数，该函数将数组和要插入的元素的索引作为参数。 要插入的元素会与它左边的元素反复交换，直到左边的元素更小或到达数组的开头。 内层循环会在用来索引数组的 Fin 中的 Nat 上进行结构化递归：

def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
  match i with
  | ⟨0, _⟩ => arr
  | ⟨i' + 1, _⟩ =>
    have : i' < arr.size := by
      simp [Nat.lt_of_succ_lt, *]
    match Ord.compare arr[i'] arr[i] with
    | .lt | .eq => arr
    | .gt =>
      insertSorted (arr.swap ⟨i', by assumption⟩ i) ⟨i', by simp [*]⟩

若索引 i 为 0，则插入到已排序区域的元素已到达该区域的开头，并且是最小的。 若索引为 i' + 1，则应将 i' 处的元素与 i 处的元素进行比较。 请注意，虽然 i 是 Fin arr.size，但 i' 只是一个 Nat，因为它是由 i 的 val 字段产生的。 因此，在使用 i' 对 arr 进行索引之前，有必要证明 i' < arr.size。

省略带有证明 i' < arr.size 的 have 表达式，将显示以下目标：

unsolved goals
α : Type ?u.7
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
i' : Nat
isLt✝ : i' + 1 < Array.size arr
⊢ i' < Array.size arr

提示 Nat.lt_of_succ_lt 是 Lean 标准库中的一个定理。 它的签名可以通过 #check Nat.lt_of_succ_lt 查看：

Nat.lt_of_succ_lt {n m : Nat} (a✝ : Nat.succ n < m) : n < m

换句话说，它指出如果 n + 1 < m，则 n < m。传递给 simp 的 * 会使其将 Nat.lt_of_succ_lt 与 i 中的 isLt 字段结合起来以获得最终证明。

在确定 i' 可用于查找要插入元素左侧的元素后，就要查找并比较这两个元素。 若左侧元素小于或等于要插入的元素，则循环结束并且不变量被恢复。 若左侧元素大于要插入的元素，则交换元素并重新开始内层循环。 Array.swap 将其两个索引都作为 Fin，并且利用 have 建立 i' < arr.size 的 by assumption。 在内层循环的下一轮中要检查的索引也是 i'，但在这种情况下 by assumption 并足够。 这是因为该证明是针对原始数组 arr 编写的，而非交换两个元素的结果。 simp 策略的数据库包含这样一个事实：交换数组的两个元素不会改变其大小， 并且 [*] 参数会指示它额外使用 have 引入的假设。

外层循环

插入排序的外层循环将指针从左向右移动，在每次迭代中调用 insertSorted 将指针处的元素插入到数组中正确的位置。循环的基本形式类似于 Array.map 的实现：

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr

它产生的错误也与在 Array.map 上没有 termination_by 子句时发生的错误相同， 因为没有在每次递归调用时都会减少的参数：

fail to show termination for
  insertionSortLoop
with errors
argument #4 was not used for structural recursion
  failed to eliminate recursive application
    insertionSortLoop (insertSorted arr { val := i, isLt := h }) (i + 1)

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

在构建停机证明之前，可以使用 partial 修饰符测试定义以确保它返回预期的答案：

partial def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr

#eval insertionSortLoop #[5, 17, 3, 8] 0

#[3, 5, 8, 17]

#eval insertionSortLoop #["metamorphic", "igneous", "sedentary"] 0

#["igneous", "metamorphic", "sedentary"]

停机性

同样，该函数会停机是因为正在处理的索引和数组大小之差在每次递归调用时都会减小。 然而，这一次，Lean 不接受 termination_by：

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr
termination_by insertionSortLoop arr i => arr.size - i

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Nat
h : i < Array.size arr
⊢ Array.size (insertSorted arr { val := i, isLt := h }) - (i + 1) < Array.size arr - i

问题在于 Lean 无法知道 insertSorted 返回的数组与传递给它的数组大小相同。 为了证明 insertionSortLoop 会停机，首先有必要证明 insertSorted 不会改变数组的大小。 将未经证明的停机条件从错误消息复制到函数中，并使用 sorry「证明」它，可以暂时接受该函数：

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
      sorry
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr
termination_by insertionSortLoop arr i => arr.size - i

declaration uses 'sorry'

由于 insertSorted 在要插入的元素的索引上是结构化递归的，所以应该通过索引归纳进行证明。 在基本情况下，数组返回不变，因此其长度肯定不会改变。对于归纳步骤， 归纳假设是在下一个更小的索引上的递归调用不会改变数组的长度。 这里有两种情况需要考虑：要么元素已完全插入到已排序区域中，并且数组返回不变， 在这种情况下长度也不会改变，要么元素在递归调用之前与下一个元素交换。 然而，在数组中交换两个元素不会改变它的大小， 并且归纳假设指出以下一个索引的递归调用返回的数组与其参数大小相同。因此，大小仍然保持不变。

将自然语言的定理陈述翻译为 Lean，并使用本章中的技术进行操作，足以证明基本情况并在归纳步骤中取得进展：

theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
    (insertSorted arr i).size = arr.size := by
  match i with
  | ⟨j, isLt⟩ =>
    induction j with
    | zero => simp [insertSorted]
    | succ j' ih =>
      simp [insertSorted]

在归纳步骤中使用 insertSorted 的简化揭示了 insertSorted 中的模式匹配：

unsolved goals
case succ
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
⊢ Array.size
      (match compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] with
      | Ordering.lt => arr
      | Ordering.eq => arr
      | Ordering.gt =>
        insertSorted
          (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) } { val := Nat.succ j', isLt := isLt })
          { val := j',
            isLt :=
              (_ :
                j' <
                  Array.size
                    (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) }
                      { val := Nat.succ j', isLt := isLt })) }) =
    Array.size arr

当面对包含 if 或 match 的目标时，split 策略（不要与归并排序定义中使用的 split 函数混淆） 会用一个新目标替换原目标，用于控制流的每条路径：

theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
    (insertSorted arr i).size = arr.size := by
  match i with
  | ⟨j, isLt⟩ =>
    induction j with
    | zero => simp [insertSorted]
    | succ j' ih =>
      simp [insertSorted]
      split

此外，每个新目标都有一个假设，表明哪个分支导致了该目标，在本例中命名为 heq✝：

unsolved goals
case succ.h_1
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.lt
⊢ Array.size arr = Array.size arr

case succ.h_2
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.eq
⊢ Array.size arr = Array.size arr

case succ.h_3
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) } { val := Nat.succ j', isLt := isLt })
        { val := j',
          isLt :=
            (_ :
              j' <
                Array.size
                  (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) }
                    { val := Nat.succ j', isLt := isLt })) }) =
    Array.size arr

与其为这两个简单情况编写证明，不如在 split 后添加 <;> try rfl， 这样这两个直接的情况会立即消失，只留下一个目标：

theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
    (insertSorted arr i).size = arr.size := by
  match i with
  | ⟨j, isLt⟩ =>
    induction j with
    | zero => simp [insertSorted]
    | succ j' ih =>
      simp [insertSorted]
      split <;> try rfl

unsolved goals
case succ.h_3
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) } { val := Nat.succ j', isLt := isLt })
        { val := j',
          isLt :=
            (_ :
              j' <
                Array.size
                  (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) }
                    { val := Nat.succ j', isLt := isLt })) }) =
    Array.size arr

不幸的是，归纳假设不足以证明这个目标。归纳假设指出对 arr 调用 insertSorted 不会改变大小， 但证明目标是要证明用交换的结果来进行递归调用的结果不会改变大小。成功完成证明需要一个归纳假设， 该假设适用于传递给 insertSorted 的任何数组，以及作为参数的更小的索引。

可以使用 induction 策略的 generalizing 选项来获得强归纳假设。 此选项会将语境中的附加假设引入到一个语句中，该语句用于生成基本情况、归纳假设和在归纳步骤中显示的目标。 对 arr 进行推广会产生更强的假设：

theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
    (insertSorted arr i).size = arr.size := by
  match i with
  | ⟨j, isLt⟩ =>
    induction j generalizing arr with
    | zero => simp [insertSorted]
    | succ j' ih =>
      simp [insertSorted]
      split <;> try rfl

在生成的证明目标中，arr 现在是归纳假设中「对于所有」语句的一部分：

unsolved goals
case succ.h_3
α : Type u_1
inst✝ : Ord α
j' : Nat
ih :
  ∀ (arr : Array α),
    Fin (Array.size arr) →
      ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
arr : Array α
i : Fin (Array.size arr)
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) } { val := Nat.succ j', isLt := isLt })
        { val := j',
          isLt :=
            (_ :
              j' <
                Array.size
                  (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) }
                    { val := Nat.succ j', isLt := isLt })) }) =
    Array.size arr

然而，整个证明开始变得难以控制。下一步是引入一个变量表示交换结果的长度， 证明它等于 arr.size，然后证明这个变量也等于递归调用产生的数组的长度。 之后可以将这些相等语句链接在一起来证明目标。 然而，仔细地重新表述定理的陈述要容易得多，这样归纳假设就能自动变得足够强，变量也会被引入。 重新表述的陈述如下：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → arr.size = len →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  skip

这个版本的定理陈述更容易证明，原因有以下几个：

1. 与其将索引及其有效性证明捆绑在 Fin 中，不如将索引放在数组之前。 这使得归纳假设可以自然地推广到整个数组，并证明 i 在范围内。
2. 引入了一个抽象长度 len 来表示 array.size。证明自动化通常更擅长处理显式相等性陈述。

生成的证明状态显示了将要用于生成归纳假设的语句，以及基本情况和归纳步骤的目标：

unsolved goals
α : Type u_1
inst✝ : Ord α
len i : Nat
⊢ ∀ (arr : Array α) (isLt : i < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i, isLt := isLt }) = len

将该语句与 induction 策略产生的目标进行比较：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → arr.size = len →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero => skip
  | succ i' ih => skip

在基本情况下，每个 i 的出现都会被替换为 0。使用 intro 引入每个假设， 然后使用 insertSorted 简化就能证明目标，因为在索引 zero 处的 insertSorted 会返回其参数不变：

unsolved goals
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
⊢ ∀ (arr : Array α) (isLt : Nat.zero < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := Nat.zero, isLt := isLt }) = len

在归纳步骤中，归纳假设具有恰当的强度。它对 任何 数组都适用，只要该数组的长度为 len：

unsolved goals
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
⊢ ∀ (arr : Array α) (isLt : Nat.succ i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := Nat.succ i', isLt := isLt }) = len

在基本情况下，simp 将目标简化为 arr.size = len：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → arr.size = len →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted]
  | succ i' ih => skip

unsolved goals
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
arr : Array α
isLt : Nat.zero < Array.size arr
hLen : Array.size arr = len
⊢ Array.size arr = len

这可以使用假设 hLen 来证明。向 simp 添加 * 参数指示它额外使用假设，这解决了目标：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → arr.size = len →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih => skip

在归纳步骤中，引入假设并简化目标会再次产生包含模式匹配的目标：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]

unsolved goals
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size
      (match compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] with
      | Ordering.lt => arr
      | Ordering.eq => arr
      | Ordering.gt =>
        insertSorted
          (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
          { val := i',
            isLt :=
              (_ :
                i' <
                  Array.size
                    (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                      { val := Nat.succ i', isLt := isLt })) }) =
    len

使用 split 策略会为每个模式生成一个目标。同样，前两个目标来自没有递归调用的分支，因此不需要归纳假设：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]
    split

unsolved goals
case succ.h_1
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
x✝ : Ordering
heq✝ : compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] = Ordering.lt
⊢ Array.size arr = len

case succ.h_2
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
x✝ : Ordering
heq✝ : compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] = Ordering.eq
⊢ Array.size arr = len

case succ.h_3
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
x✝ : Ordering
heq✝ : compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
        { val := i',
          isLt :=
            (_ :
              i' <
                Array.size
                  (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                    { val := Nat.succ i', isLt := isLt })) }) =
    len

在 split 产生的每个目标中运行 try assumption 会消除两个非递归目标：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]
    split <;> try assumption

unsolved goals
case succ.h_3
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
x✝ : Ordering
heq✝ : compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
        { val := i',
          isLt :=
            (_ :
              i' <
                Array.size
                  (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                    { val := Nat.succ i', isLt := isLt })) }) =
    len

对于证明目标的全新表述，其中常量 len 用于递归函数中涉及的所有数组的长度， 恰好属于 simp 可以解决的问题类型。最终的证明目标可以通过 simp [*] 来解决， 因为将数组的长度与 len 联系起来的假设很重要：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]
    split <;> try assumption
    simp [*]

最后，因为 simp [*] 可以使用假设，所以 try assumption 一行可以用 simp [*] 替换来缩短证明：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]
    split <;> simp [*]

现在可以使用这个证明来替换 insertionSortLoop 中的 sorry。 将 arr.size 作为定理的 len 参数会导致最终结论为 (insertSorted arr ⟨i, isLt⟩).size = arr.size， 因此重写以一个非常易于管理的证明目标结束：

  def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
    if h : i < arr.size then
      have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
        rw [insert_sorted_size_eq arr.size i arr h rfl]
      insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
    else
      arr
termination_by insertionSortLoop arr i => arr.size - i

unsolved goals
α : Type ?u.22173
inst✝ : Ord α
arr : Array α
i : Nat
h : i < Array.size arr
⊢ Array.size arr - (i + 1) < Array.size arr - i

证明 Nat.sub_succ_lt_self 是 Lean 标准库的一部分，其类型为 ∀ (a i : Nat), i < a → a - (i + 1) < a - i 它刚好就是我们所需要的：

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
      rw [insert_sorted_size_eq arr.size i arr h rfl]
      simp [Nat.sub_succ_lt_self, *]
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr
termination_by insertionSortLoop arr i => arr.size - i

驱动函数

插入排序本身会调用 insertionSortLoop，以将数组中已排序区域与未排序区域的分界索引初始化为 0：

def insertionSort [Ord α] (arr : Array α) : Array α :=
   insertionSortLoop arr 0

一些快速测试表明该函数至少不是明显错误的：

#eval insertionSort #[3, 1, 7, 4]

#[1, 3, 4, 7]

#eval insertionSort #[ "quartz", "marble", "granite", "hematite"]

#["granite", "hematite", "marble", "quartz"]

它真的是插入排序吗？

插入排序被 定义 为原地排序算法。尽管它具有二次最差运行时间，但它仍然有用， 因为它是一种稳定的排序算法，不会分配额外的空间，并且可以有效处理几乎已排序的数据。 如果内层循环的每次迭代都分配一个新数组，那么该算法就不会真正成为插入排序。

Lean 的数组操作（例如 Array.set 和 Array.swap）会检查所讨论的数组的引用计数是否大于 1。 如果是，则该数组对代码的多个部分可见，这意味着它必须被复制。 否则，Lean 将不再是一种纯函数式语言。但是，当引用计数恰好为 1 时，没有其他潜在的值观察者。 在这种情况下，数组原语会就地改变数组。程序其他不知道的部分不会对它造成破坏。

Lean 的证明逻辑在纯函数式程序的级别上，而非在底层实现上工作。 这意味着发现程序是否不必要地复制了数据的最好方法是测试它。 在需要改变的每个点添加对 dbgTraceIfShared 的调用，当所讨论的值有多个引用时， 它会将提供的消息打印到 stderr。

插入排序刚好有一个地方有复制而非改变的风险：调用 Array.swap。将 arr.swap ⟨i', by assumption⟩ i 替换为 ((dbgTraceIfShared "array to swap" arr).swap ⟨i', by assumption⟩ i) 会让程序在无法改变数组时发出 shared RC array to swap。然而，对程序的这一更改也会更改证明， 因为现在调用了一个附加函数。由于 dbgTraceIfShared 直接返回其第二个参数， 因此将其添加到对 simp 的调用中足以修复证明。

插入排序的完整形式化验证代码为：

def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
  match i with
  | ⟨0, _⟩ => arr
  | ⟨i' + 1, _⟩ =>
    have : i' < arr.size := by
      simp [Nat.lt_of_succ_lt, *]
    match Ord.compare arr[i'] arr[i] with
    | .lt | .eq => arr
    | .gt =>
      insertSorted
        ((dbgTraceIfShared "array to swap" arr).swap ⟨i', by assumption⟩ i)
        ⟨i', by simp [dbgTraceIfShared, *]⟩

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted, dbgTraceIfShared]
    split <;> simp [*]

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
      rw [insert_sorted_size_eq arr.size i arr h rfl]
      simp [Nat.sub_succ_lt_self, *]
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr
termination_by insertionSortLoop arr i => arr.size - i

def insertionSort [Ord α] (arr : Array α) : Array α :=
  insertionSortLoop arr 0

要检查形式化验证是否实际起作用，需要一点技巧。首先，当所有参数在编译时都已知时， Lean 编译器会积极地优化函数调用。仅仅编写一个将 insertionSort 应用于大数组的程序是不够的， 因为生成的编译代码可能只包含已排序的数组作为常量。确保编译器不会优化排序例程的最简单方法是从 stdin 读取数组。其次，编译器会执行死代码消除。如果从未使用 let 绑定的变量， 则向程序中添加额外的 let 并不一定会导致运行代码中更多的引用。为了确保不会完全消除额外的引用， 重点在于确保以某种方式使用了额外的引用。

测试形式化验证代码的第一步是编写 getLines，它从标准输入读取一行数组：

def getLines : IO (Array String) := do
  let stdin ← IO.getStdin
  let mut lines : Array String := #[]
  let mut currLine ← stdin.getLine
  while !currLine.isEmpty do
     -- Drop trailing newline:
    lines := lines.push (currLine.dropRight 1)
    currLine ← stdin.getLine
  pure lines

IO.FS.Stream.getLine 返回一行完整的文本，包括结尾的换行。当到达文件结尾标记时，它返回空字符串 ""。

接下来，需要两个单独的 main 例程。两者都从标准输入读取要排序的数组， 确保在编译时不会用它们的返回值替换对 insertionSort 的调用。然后两者都打印到控制台， 确保对 insertionSort 的调用不会被完全优化掉。其中一个只打印排序后的数组， 而另一个同时打印排序后的数组和原始数组。第二个函数应该触发一个警告， 即 Array.swap 必须分配一个新数组：

def mainUnique : IO Unit := do
  let lines ← getLines
  for line in insertionSort lines do
    IO.println line

def mainShared : IO Unit := do
  let lines ← getLines
  IO.println "--- Sorted lines: ---"
  for line in insertionSort lines do
    IO.println line

  IO.println ""
  IO.println "--- Original data: ---"
  for line in lines do
    IO.println line

实际的 main 只需根据提供的命令行参数选择两个 main 活动二者之一：

def main (args : List String) : IO UInt32 := do
  match args with
  | ["--shared"] => mainShared; pure 0
  | ["--unique"] => mainUnique; pure 0
  | _ =>
    IO.println "Expected single argument, either \"--shared\" or \"--unique\""
    pure 1

在没有参数的情况下运行它会产生预期的用法信息：

$ sort
Expected single argument, either "--shared" or "--unique"

test-data 文件包含以下岩石：

schist
feldspar
diorite
pumice
obsidian
shale
gneiss
marble
flint

对这些岩石使用形式化验证的插入排序，结果按字母顺序打印出来：

$ sort --unique < test-data
diorite
feldspar
flint
gneiss
marble
obsidian
pumice
schist
shale

然而，保留对原始数组的引用的版本会导致对 Array.swap 的第一次调用在 stderr 上发出通知（即 shared RC array to swap）：

$ sort --shared < test-data
shared RC array to swap
--- Sorted lines: ---
diorite
feldspar
flint
gneiss
marble
obsidian
pumice
schist
shale

--- Original data: ---
schist
feldspar
diorite
pumice
obsidian
shale
gneiss
marble
flint

仅出现一个 shared RC 通知这一事实意味着数组仅被复制了一次。 这是因为由对 Array.swap 的调用产生的副本本身是唯一的，因此不需要进行进一步的复制。 在命令式语言中，由于忘记在按引用传递数组之前显式复制数组，可能会导致微妙的 Bug。 在运行 sort --shared 时，数组会安需复制，以保持 Lean 程序的纯函数语义，但仅此而已。

其他可变性的机会

当引用唯一时，使用修改而非复制并不仅限于数组更新操作。 Lean 还会尝试「回收」引用计数即将降至零的构造函数，重新使用它们而不是分配新数据。 这意味着，例如，List.map 将原地修改链表，至少在无人能注意到的情况下。 优化 Lean 代码中的热循环最重要的步骤之一是确保被修改的数据不会被从多个位置引用。

练习

• 编写一个反转数组的函数。测试如果输入数组的引用计数为一，则你的函数不会分配一个新数组。

• 为数组实现归并排序或快速排序。证明你的实现会停机，并测试它不会分配比预期更多的数组。 这是一个具有挑战性的练习！