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
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115
116. 116
117. 117

import Std.Tactic.Do
import Mathlib

open Std.Do

def kadane (A : Array ℤ) := Id.run do
  let mut cur := 0
  let mut ans := 0
  for x in A do
    cur := max x (cur + x)
    ans := max ans cur
  return ans

def is_max_subarray (xs : List ℤ) m :=
  (∃ i ≤ xs.length, ∃ j ≤ xs.length, (xs.extract i j).sum = m) ∧ ∀ i ≤ xs.length, ∀ j ≤ xs.length, (xs.extract i j).sum ≤ m

lemma concat_drop (xs ys : List α) (hi : i ≤ xs.length) : (xs ++ ys).drop i = (xs.drop i) ++ ys := by
  fun_induction List.drop <;> grind

lemma concat_drop_sum [AddMonoid α] (xs ys : List α) (hi : i ≤ xs.length) : (xs ++ ys |>.drop i).sum = (xs.drop i).sum + ys.sum := by
  rw [concat_drop xs ys hi, List.sum_append]

lemma extract_end_drop (xs : List α) i j (h : j = xs.length) : xs.extract i j = xs.drop i := by
  simp [h]

lemma extract_in_bounds (xs ys : List α) (hi : i ≤ xs.length) (hj : j ≤ xs.length) : (xs ++ ys).extract i j = xs.extract i j := by
  simp
  rw [concat_drop xs ys hi]
  exact List.take_append_of_le_length (by grind)

theorem kadane_correct A : is_max_subarray A.toList (kadane A) := by
  generalize h : kadane A = x
  apply Id.of_wp_run_eq h
  mvcgen
  case inv1 =>
    -- cur might be negative so the loop invariant can only guarentee ∀ i < xs.prefix.length
    exact ⇓⟨xs, ans, cur⟩ => ⌜0 ≤ ans ∧ (∃ i ≤ xs.prefix.length, (xs.prefix.drop i).sum = cur) ∧ (∀ i < xs.prefix.length, (xs.prefix.drop i).sum ≤ cur) ∧ is_max_subarray xs.prefix ans⌝
  all_goals mleave
  case vc1.step ih =>
    expose_names
    have cur_1_exists : ∃ i ≤ (pref ++ [cur]).length, (List.drop i (pref ++ [cur])).sum = cur_1 := by
      by_cases cur ≤ b.snd + cur
      · obtain ⟨i, hi⟩ := ih.2.1
        use i
        rw [concat_drop_sum pref [cur] hi.1, hi.2]
        grind
      · use pref.length
        rw [concat_drop_sum pref [cur] (Nat.le_refl pref.length)]
        grind
    have cur_1_max : ∀ i < (pref ++ [cur]).length, (List.drop i (pref ++ [cur])).sum ≤ cur_1 := by
      intro i hi
      rw [concat_drop_sum pref [cur] (by grind)]
      by_cases i = pref.length <;> grind
    and_intros
    · grind
    · exact cur_1_exists
    · exact cur_1_max
    · by_cases b.fst ≤ cur_1
      · obtain ⟨i, hi⟩ := cur_1_exists
        use i, (by grind), pref.length + 1
        constructor
        · grind
        · rw [extract_end_drop (pref ++ [cur]) i (pref.length + 1) (by grind)]
          grind
      · obtain ⟨i, hi, j, hj, _⟩ := ih.2.2.2.1
        use i, (by grind), j, (by grind)
        rw [extract_in_bounds pref [cur] hi hj]
        grind
    · intro i hi j hj
      by_cases hi₂ : i ≤ pref.length
      · by_cases hj₂ : j ≤ pref.length
        · rw [extract_in_bounds pref [cur] hi₂ hj₂]
          grw [ih.2.2.2.2 i hi₂ j hj₂]
          exact Int.le_max_left b.fst cur_1
        · rw [extract_end_drop (pref ++ [cur]) i j (by grind)]
          grw [cur_1_max i (by grind)]
          exact Int.le_max_right b.fst cur_1
      · grind
  case vc2.a.pre =>
    simp [is_max_subarray]
  case vc3.a.post =>
    grind


def BubbleSort [LT α] [DecidableLT α] (A : Array α) : Id (Array α) := do
  let n := A.size
  let mut A := A.toVector
  for i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      have := List.mem_range.mp hj
      if A[j] > A[j + 1] then
        A := A.swap j (j + 1)
  return A.toArray

def ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) : Id (Array α) := do
  let N := A.size
  let mut A := A.toVector
  for hi : i in [:N] do
    for hj : j in [:N] do
      if A[i] < A[j] then
        A := A.swap i j
  return A.toArray



theorem SortCorrect [LT α] [DecidableLT α] (A : Array α) : Multiset.ofList A.toList = Multiset.ofList (ICan'tBelieveItCanSort A).toList := by
  generalize h : ICan'tBelieveItCanSort A = x
  apply Id.of_wp_run_eq h
  mvcgen




theorem SortCorrect [LT α] [DecidableLT α] (A : Array α) : ⦃⌜True⌝⦄ BubbleSort A ⦃⇓ r => ⌜Multiset.ofList r.toList = Multiset.ofList A.toList⌝⦄ := by
  -- generalize h : ICan'tBelieveItCanSort A = x
  -- apply Id.of_wp_run_eq h
  mvcgen