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
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48

-- Simplified version of https://jamesoswald.dev/posts/lean4-insertion-sort/
-- Also inspired by https://gist.github.com/Kha/96d67c8b947b48f8786aea90857fbb5c

/-- Inserts a natural number n into a sorted list. -/
@[grind]
def sInsert (n : Nat) : List Nat → List Nat
  | [] => [n]
  | h :: t =>
    if n ≤ h then
      n :: h :: t
    else
      h :: sInsert n t

/-- Insertion sort -/
@[grind]
def sort : List Nat → List Nat
  | [] => []
  | h :: t => sInsert h (sort t)

/-- Predicate for a list being sorted -/
@[grind]
def sorted : List Nat → Prop
  -- An empty list is sorted
  | [] => True
  -- A list containing a single element is sorted
  | [_] => True
  -- A list with more than 2 elements is only sorted if all elements are ordered.
  | h1 :: h2 :: t => h1 ≤ h2 ∧ sorted (h2 :: t)

/-- If a sorted list is passed to sInsert,
it will return a sorted list after inserting a new elm. -/
theorem sInsert_sorted (l : List Nat) (n : Nat) : sorted l → sorted (sInsert n l) := by
  induction l with
  | nil => grind
  | cons _ t1 => cases t1 <;> grind

theorem sort_sorted (l : List Nat) : sorted (sort l) := by
  induction l <;> grind [sInsert_sorted]

/-- A list l with n is a permutation of a list the list with n inserted into it. -/
theorem sInsert_perm (l : List Nat) (n : Nat) : (n :: l).Perm (sInsert n l) := by
  induction l <;> grind

/-- Sort returns a permutation of the input list. -/
theorem sort_perm (l : List Nat) : l.Perm (sort l) := by
  induction l with
  | nil => simp [sort]
  | cons h t ih => grind [sInsert_perm (sort t) h]