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

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]

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 =>
    obtain ⟨h₁, h₂, h₃⟩ := ih
    expose_names
    and_intros
    · grind
    · by_cases h₄ : cur ≤ b.snd + cur
      · obtain ⟨i, hi⟩ := h₁
        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
    · intro i hi
      rw [concat_drop_sum pref [cur] (by grind)]
      by_cases h₄ : i < pref.length
      · grind
      · have : i = pref.length := by grind
        grind
    · by_cases h₄ : b.fst ≤ cur_1
      · obtain ⟨i, _⟩ := h₁
        use i, (by grind), pref.length + 1
        constructor
        · grind
        · sorry -- obvious
      · unfold is_max_subarray at h₃
        obtain ⟨i, hi, j, hj, _⟩ := h₃.1
        use i, (by grind), j, (by grind)
        sorry
    · intro i hi j hj
      by_cases h₄ : i ≤ pref.length
      · by_cases h₅ : j ≤ pref.length
        · sorry
        · sorry
      · by_cases h₅ : j ≤ pref.length
        · sorry
        · have : j - i = 0 := by grind
          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