New mvcgen invariants syntax

Changes

1 changed files (+3/-5)

• Kadane.lean
  • @@ -26,11 +26,9 @@ open Std.Do
    theorem kadane_correct : 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 guarantee ∀ 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 + mvcgen invariants + · -- cur might be negative so the loop invariant can only guarantee ∀ i < xs.prefix.length + ⇓⟨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⌝ case vc1.step ih => expose_names have cur_1_exists : ∃ i ≤ (pref ++ [cur]).length, (List.drop i (pref ++ [cur])).sum = cur_1 := by