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

import Mathlib

variable [LinearOrder α]

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

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)

theorem insCorrect x (xs : List α) : (Sorted xs → Sorted (ins x xs)) ∧ (x :: xs).Perm (ins x xs) := by
  constructor
  · intro h
    unfold ins
    grind
    induction xs <;> grind
    try?
    hint
    sorry
  · sorry

-- WARNING: This will uninstall Lean!
-- #eval do
  -- IO.FS.removeDirAll
    -- <| .mk <$> (← IO.getEnv "ELAN_HOME") |>.getD
    -- <| (← Std.Internal.IO.Async.System.getHomeDir) / ".elan"