Simplify the sort proofs even more

Changes

1 changed files (+7/-25)

• Sort.lean
  • @@ -4,16 +4,6 @@ import Mathlib.Data.Nat.Basic
    variable [LinearOrder α] (A : Array α) - def BubbleSort := Id.run 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 + 1] < A[j] then - A := A.swap j (j + 1) - return A.toArray - def ICan'tBelieveItCanSort := Id.run do let N := A.size let mut A := A.toVector
  • @@ -43,26 +33,18 @@ theorem sorted : ICan'tBelieveItCanSort A |>.Pairwise (· ≤ ·) := by
    mvcgen <;> expose_names case inv1 => exact ⇓⟨xs, A'⟩ => ⌜A'.take xs.pos |>.toArray.Pairwise (· ≤ ·)⌝ case inv2 => - exact ⇓⟨xs, A'⟩ => ⌜(A'.take cur).toArray.Pairwise (· ≤ ·) ∧ ∀ i (_ : i < xs.pos), A'[i]'(by - have : xs.prefix.length + xs.suffix.length = N := by simp [← List.length_append, xs.property] - grind - ) ≤ A'[cur]'(by grind)⌝ + exact ⇓⟨xs, A'⟩ => ⌜(A'.take cur).toArray.Pairwise (· ≤ ·) + ∧ ∀ i (_ : i < xs.pos), A'[i]'(by grind [List.length_append, xs.property]) ≤ A'[cur]'(by grind)⌝ case vc1.step.isTrue => - simp_all - constructor - · rw [Array.pairwise_iff_getElem] at h_5 ⊢ - grind - · grind - case vc2.step.isFalse => grind - case vc3.step.pre => grind + simp [Array.pairwise_iff_getElem] at h_5 ⊢ + grind case vc4.step.post.success => - simp_all - rw [Array.pairwise_iff_getElem] at h_3 ⊢ + simp [Array.pairwise_iff_getElem] at h_3 ⊢ grind - case vc5.a.pre => grind case vc6.a.post.success => - simp_all + simp at h_1 exact (show r.toArray = r.toArray.extract 0 N by grind) ▸ h_1 + all_goals grind theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort A).Perm A ∧ (ICan'tBelieveItCanSort A).Pairwise (· ≤ ·) :=