Prove perm_ICan'tBelieveItCanSort Used the fix at https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/mvcgen.20doesn't.20produce.20any.20invariant.20goals/with/546177611

Changes

1 changed files (+45/-5)

• Sort.lean
  • @@ -2,12 +2,12 @@ import Std.Tactic.Do
    import Mathlib def BubbleSort [LT α] [DecidableLT α] (A : Array α) := Id.run do - let n := A.size + 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 + 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 + if A[j + 1] < A[j] then A := A.swap j (j + 1) return A.toArray
  • @@ -22,7 +22,47 @@ def ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) := Id.run do
    open Std.Do - theorem SortCorrect [LT α] [DecidableLT α] (A : Array α) : Multiset.ofList A.toList = Multiset.ofList (ICan'tBelieveItCanSort A).toList := by + theorem perm_ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) : ICan'tBelieveItCanSort.{0} A |>.Perm A := by + suffices Multiset.ofList (ICan'tBelieveItCanSort.{0} A).toList = A.toList by + rw [Multiset.coe_eq_coe] at this + exact { toList := this } + generalize h : ICan'tBelieveItCanSort A = x + apply Id.of_wp_run_eq h + mvcgen + case inv1 => exact ⇓⟨_, A'⟩ => ⌜Multiset.ofList A.toList = A'.toList⌝ + all_goals try grind + case vc1.step.isTrue => + expose_names + mleave + simp_all only [Multiset.coe_eq_coe] + have h₁ := Membership.get_elem_helper (Spec.forIn'_range._proof_4 pref cur suff h_1) rfl + have h₂ := Membership.get_elem_helper (Spec.forIn'_range._proof_4 pref_1 cur_1 suff_1 h_3) rfl + exact h_5.trans <| .symm <| Vector.perm_iff_toList_perm.mp <| Vector.swap_perm h₁ h₂ + + theorem sorted_ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) : ICan'tBelieveItCanSort.{0} A |>.Pairwise (¬ · > ·) := by generalize h : ICan'tBelieveItCanSort A = x apply Id.of_wp_run_eq h mvcgen + case inv1 => exact ⇓⟨xs, A'⟩ => ⌜A'.take xs.prefix.length |>.toArray.Pairwise (¬ · > ·)⌝ + case vc1.step.isTrue => + expose_names + simp_all + grind + sorry + case vc2.step.isFalse => + expose_names + simp_all + grind + sorry + case vc3.step.pre => grind + case vc4.step.post.success => + expose_names + simp_all + grind + sorry + case vc5.a.pre => grind + case vc6.a.post.success => + expose_names + simp_all + have : r.toArray = r.toArray.extract 0 N := by grind + rwa [this]