Is there code for "Reasonable proof of bubble sort"?

Stream: Is there code for X?

[chenjulang]

Something like this , it is only pseudocode:

open nat

-- 冒泡排序
def bubbleSort : list ℕ → list ℕ
| [] := []
| (x :: xs) :=
  let fix swapAdjacent : list ℕ → list ℕ
  | [] := []
  | [y] := [y]
  | (y1 :: y2 :: ys) := if y1 > y2 then y2 :: swapAdjacent (y1 :: ys)
                        else y1 :: swapAdjacent (y2 :: ys) in
  let sortedRest := bubbleSort xs in
  swapAdjacent (x :: sortedRest)

-- 冒泡排序的合理性证明
theorem bubbleSort_correct (lst : list ℕ) :
  bubbleSort lst = lst.sort (≤) :=
begin
  -- 使用列表长度的归纳法证明
  induction lst with x xs IH,
  -- 基础情况：空列表已经是排好序的
  { refl },
  -- 归纳情况
  { simp [bubbleSort, IH],
    -- 需要证明的目标是 swapAdjacent (x :: bubbleSort xs) = insert x (bubbleSort xs).sort (≤)
    -- 先证明一个引理：swapAdjacent 返回的列表最后一个元素是最大的元素
    have max_at_last : ∀ ys, ys ≠ [] → last (swapAdjacent ys) (cons_ne_nil _ _),
    { intros ys h,
      induction ys with y1 ys IH,
      { contradiction },
      { cases ys with y2 ys,
        { simp [swapAdjacent] },
        { by_cases h' : y1 > y2,
          { simp [swapAdjacent, h'],
            -- 使用 IH 来进行归纳推理，得到 ys 的最大元素将被放在列表最后一个位置上
            have h'' : last (swapAdjacent (y1 :: y2 :: ys)) (cons_ne_nil _ _)
              := max_at_last (y1 :: ys) (cons_ne_nil _ _),
            rw last_cons (cons_ne_nil _ _) at h'',
            rw last_cons (cons_ne_nil _ _),
            rwa last_cons (cons_ne_nil _ _) } ,
          { simp [swapAdjacent, h'],
            cases ys with y3 ys,
            { simp [insert] },
            { -- 此时 y1 ≤ y2，因此继续使用 IH 进行归纳推理
              have h'' : last (swapAdjacent (y2 :: y3 :: ys)) (cons_ne_nil _ _)
                := max_at_last (y2 :: ys) (cons_ne_nil _ _),
              rw last_cons (cons_ne_nil _ _) at h'',
              cases h'' with h'' h''',
              -- 根据归纳假设，swapAdjacent (y2 :: ys) = (y2 :: ys).sort (≤)
              rw IH (y2 :: ys),
              -- 使用列表的反转引理将等式转化为与 insert 一致的形式
              rw reverse_reverse (insert x (y2 :: ys).sort (≤)),
              rw ←reverse_cons h''',
              rw ←reverse_cons h''',
              rw insert_eq_insert_sorted,
              rw reverse_cons,
              rw reverse_cons } } } },
    -- 使用之前证明的引理，将 swapAdjacent (x :: bubbleSort xs) 的最后一个元素替换为 x
    have h : last (swapAdjacent (x :: bubbleSort xs)) (cons_ne_nil _ _) = x,
    { rw last_cons (cons_ne_nil _ _),
      exact max_at_last (x :: bubbleSort xs) (cons_ne_nil _ _) },
    -- 由于交换相邻元素的操作只改变了最后一个元素的位置，因此 swapAdjacent 产生的列表与 insert 的结果相同
    rw [insert_eq_insert_sorted, ←reverse_cons h],
    -- 继续使用 IH 进行归纳推理
    rw IH (x :: xs) }
end

[chenjulang]

And all the algorithm theorems in the book “Introduction to Algorithms” ，
Can we find the proofs in LEAN?

[Kim Morrison]

I would guess that you would have a much easier time proving that the result of your algorithm is sorted, rather then directly proving its output is equal to the output of a different sorting algorithm.

[Kim Morrison]

Also, this looks like Lean 3 code! You really should move to Lean 4 if at all possible.