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
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69

import Mathlib

variable [LE α] [DecidableLE α] [Std.IsLinearOrder α] (xs : List α)

def ins (a : α)
  | [] => [a]
  | x :: xs =>
    if a ≤ x then a :: x :: xs else x :: ins a xs

def List.insSort : List α → List α
  | [] => []
  | x :: xs => ins x xs.insSort

def Sorted : List α → Prop
  | [] | [_] => True
  | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs)

noncomputable section AristotleLemmas

/-
Inserting an element `x` into a list `xs` results in a permutation of `x :: xs`.
-/
theorem ins_perm (x : α) (xs : List α) : List.Perm (ins x xs) (x :: xs) := by
  -- By definition of `ins`, we know that `ins x [] = [x]`.
  have h_base : List.Perm (ins x []) (x :: []) := by
    rfl;
  induction xs <;> simp_all +decide [ List.Perm ];
  -- By definition of `ins`, we know that `ins x (head :: tail)` is either `x :: head :: tail` or `head :: ins x tail`.
  have h_cases : ins x (‹α› :: ‹List α›) = if x ≤ ‹α› then x :: ‹α› :: ‹List α› else ‹α› :: ins x ‹List α› := by
    exact?;
  split_ifs at h_cases <;> simp_all +decide [ List.Perm.swap ];
  rename_i k hk ih;
  exact List.Perm.trans ( List.Perm.cons _ hk ) ( List.Perm.swap .. )

/-
Inserting an element into a sorted list preserves sortedness.
-/
theorem ins_sorted [LE α] [DecidableLE α] [Std.IsLinearOrder α] (x : α) (xs : List α) (h : Sorted xs) : Sorted (ins x xs) := by
  revert x xs;
  intro x y;
  induction y <;> simp_all +decide [ ins ];
  · tauto;
  · rename_i k hk ih;
    split_ifs with h;
    · exact fun h' => ⟨ h, h' ⟩;
    · rcases hk with ( _ | ⟨ y, hk ⟩ ) <;> simp_all +decide [ Sorted ];
      · constructor;
        · exact?;
        · trivial;
      · -- Since $k \leq y$ and $y \leq x$, we have $k \leq x$.
        have h_kx : k ≤ x := by
          exact?;
        rcases n : ins x ( y :: hk ) with ( _ | ⟨ z, _ | ⟨ w, l ⟩ ⟩ ) <;> simp_all +decide [ Sorted ];
        · unfold ins at n; aesop;
        · unfold ins at n; aesop;

end AristotleLemmas

theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort := by
  constructor;
  · induction xs <;> simp_all +decide [ List.insSort ];
    · trivial;
    · exact?;
  · induction xs;
    · rfl;
    · -- By definition of `ins`, we have `ins head (tail.insSort) = head :: tail.insSort` if `head ≤ tail.insSort`.
      have h_insert : List.Perm (ins ‹α› (‹List α›.insSort)) (‹α› :: ‹List α›.insSort) := by
        exact?;
      exact List.Perm.trans ( List.Perm.cons _ ‹_› ) h_insert.symm