Almost done with annoying Kadane proof

Changes

2 changed files (+108/-1)

• Count.lean
  • @@ -4,7 +4,7 @@ def Main := do
    let A := Array.replicate 10 0 |>.append (Array.replicate 8 1) |>.append (Array.replicate 6 2) let N := A.size let mut cnt := 0 - for ha : a in [0:N] do + for ha : a in [:N] do for hb : b in [a + 1:N] do for hc : c in [b + 1:N] do for hd : d in [c + 1:N] do
• Sort.lean (new)
  • @@ -0,0 +1,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