1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28

import Std.Tactic.Do
import Mathlib

def BubbleSort [LT α] [DecidableLT α] (A : Array α) := Id.run do
  let n := A.size
  let mut A := A.toVector
  for i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      have := List.mem_range.mp hj
      if A[j] > A[j + 1] then
        A := A.swap j (j + 1)
  return A.toArray

def ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) := Id.run do
  let N := A.size
  let mut A := A.toVector
  for hi : i in [:N] do
    for hj : j in [:N] do
      if A[i] < A[j] then
        A := A.swap i j
  return A.toArray

open Std.Do

theorem SortCorrect [LT α] [DecidableLT α] (A : Array α) : Multiset.ofList A.toList = Multiset.ofList (ICan'tBelieveItCanSort A).toList := by
  generalize h : ICan'tBelieveItCanSort A = x
  apply Id.of_wp_run_eq h
  mvcgen