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
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59

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

variable [LE α] [DecidableLE α]

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

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

/-- Predicate for a list being sorted -/
@[grind]
def sorted : List α → Prop
  -- An empty list is sorted
  | [] => True
  -- A list containing a single element is sorted
  | [_] => True
  -- A list with 2 or more elements is only sorted if all elements are ordered.
  | h :: h' :: t => h ≤ h' ∧ sorted (h' :: t)
/- This also works:
inductive sorted : List α → Prop where
  | nil : sorted []
  | single x : sorted [x]
  | cons_cons x x' xs : x ≤ x' → sorted (x' :: xs) → sorted (x :: x' :: xs)
-/

variable (l : List α)

/-- If a sorted list is passed to `sInsert`,
it will return a sorted list after inserting a new element. -/
theorem sInsert_sorted [Std.IsLinearOrder α] : sorted l → sorted (sInsert n l) := by
  induction l with
  | nil => grind
  | cons _ t => cases t <;> grind

theorem sort_sorted [Std.IsLinearOrder α] : 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.
We need `LawfulBEq` because grind uses it via `List.perm_iff_count`. -/
theorem sInsert_perm [BEq α] [LawfulBEq α] : (n :: l).Perm (sInsert n l) := by
  induction l <;> grind

/-- `sort` returns a permutation of the input list. -/
theorem sort_perm [BEq α] [LawfulBEq α] : l.Perm (sort l) := by
  induction l with
  | nil => grind
  | cons h t => grind [sInsert_perm (sort t) (n := h)]