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 Std.Tactic.Do
import Mathlib.Algebra.Order.Group.Nat

variable [LinearOrder α] (A : Array α)

def Array.insSort := Id.run do
  let N := A.size
  let mut A := A.toVector
  for hi : i in [:N] do
    for hj : j in [:i] do
      have := Membership.get_elem_helper hi rfl
      if A[i - j] < A[i - j - 1] then
        A := A.swap (i - j - 1) (i - j)
      else
        break
  return A.toArray

open Std.Do

theorem insSortPerm : A.insSort.Perm A := by
  generalize h : A.insSort = x
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · ⇓⟨_, A'⟩ => ⌜A.Perm A'.toArray⌝
  · ⇓⟨_, A'⟩ => ⌜A.Perm A'.toArray⌝
  with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm]

abbrev Sorted := ∀ i (_ : 0 ≤ i ∧ i < A.size - 1), A[i] ≤ A[i + 1]

abbrev SortedRange (l r : ℕ) (_ : l ≤ A.size) (_ : r ≤ A.size) :=
  ∀ i (_ : l ≤ i ∧ i < r - 1), A[i] ≤ A[i + 1]

theorem insSortSorted : Sorted A.insSort := by
  generalize h : A.insSort = x
  apply Id.of_wp_run_eq h
  mvcgen <;> expose_names
  case inv1 => exact ⇓⟨xs, A'⟩ => ⌜SortedRange A'.toArray 0 xs.pos (by grind) (by grind [List.length_append, xs.property])⌝
  case inv2 =>
    exact ⇓⟨xs, A'⟩ => ⌜SortedRange A'.toArray 0 (cur - xs.pos) (by grind) (by grind)
      ∧ SortedRange A'.toArray (cur - xs.pos) (cur + 1) (by grind) (by grind)
      ∧ ((_ : 0 < xs.pos ∧ xs.pos < cur) → A'[cur - xs.pos - 1]'(by grind) ≤ A'[cur - xs.pos + 1]'(by grind))⌝
  case vc1.step.isTrue =>
    simp at h_5 ⊢
    and_intros
    · grind
    · intro i hi
      by_cases i = cur - cur_1 - 1 ∨ i = cur - cur_1
      · grind
      · grind [h_5.2.1 i (by grind)]
    · intro _
      grind [h_5.1 (cur - cur_1 - 2) (by grind)]
  case vc2.step.isFalse =>
    simp_all
    and_intros
    · grind
    · intro i hi
      by_cases i < cur - cur_1 - 1
      · exact h_5.1 i (by grind)
      · by_cases cur - cur_1 ≤ i
        · exact h_5.2.1 i (by grind)
        · grind
    · grind
  case vc4.step.post.success =>
    simp at h_3 ⊢
    grind
  all_goals grind

theorem insSortCorrect : A.insSort.Perm A ∧ Sorted A.insSort :=
  ⟨insSortPerm A, insSortSorted A⟩