Simplify proof slightly, add ! to end of name yay

Changes

1 changed files (+10/-14)

• Sort.lean
  • @@ -11,7 +11,7 @@ def BubbleSort [LinearOrder α] (A : Array α) := Id.run do
    A := A.swap j (j + 1) return A.toArray - def ICan'tBelieveItCanSort [LinearOrder α] (A : Array α) := Id.run do + def ICan'tBelieveItCanSort! [LinearOrder α] (A : Array α) := Id.run do let N := A.size let mut A := A.toVector for hi : i in [:N] do
  • @@ -21,14 +21,14 @@ def ICan'tBelieveItCanSort [LinearOrder α] (A : Array α) := Id.run do
    return A.toArray #guard let A := #[69, 420, 13, 1, 65536] - ICan'tBelieveItCanSort A = A.qsort + ICan'tBelieveItCanSort! A = A.qsort open Std.Do - theorem perm_ICan'tBelieveItCanSort [LinearOrder α] (A : Array α) : ICan'tBelieveItCanSort.{0} A |>.Perm A := by - suffices Multiset.ofList (ICan'tBelieveItCanSort.{0} A).toList = A.toList by + theorem perm_ICan'tBelieveItCanSort! [LinearOrder α] (A : Array α) : ICan'tBelieveItCanSort!.{0} A |>.Perm A := by + generalize h : ICan'tBelieveItCanSort! A = x + suffices Multiset.ofList x.toList = A.toList by exact { toList := Multiset.coe_eq_coe.mp 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⌝
  • @@ -39,19 +39,17 @@ theorem perm_ICan'tBelieveItCanSort [LinearOrder α] (A : Array α) : ICan'tBeli
    simp_all only [Multiset.coe_eq_coe] exact h_5.trans <| .symm <| Vector.perm_iff_toList_perm.mp <| Vector.swap_perm (by grind) (by grind) - theorem sorted_ICan'tBelieveItCanSort [LinearOrder α] (A : Array α) : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by - generalize h : ICan'tBelieveItCanSort A = x + theorem sorted_ICan'tBelieveItCanSort! [LinearOrder α] (A : Array α) : ICan'tBelieveItCanSort!.{0} A |>.Pairwise (· ≤ ·) := by + generalize h : ICan'tBelieveItCanSort! A = x apply Id.of_wp_run_eq h - mvcgen + mvcgen <;> expose_names case inv1 => exact ⇓⟨xs, A'⟩ => ⌜A'.take xs.pos |>.toArray.Pairwise (· ≤ ·)⌝ case inv2 => - expose_names 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)⌝ case vc1.step.isTrue => - expose_names simp_all constructor · rw [Array.pairwise_iff_getElem] at h_5 ⊢
  • @@ -62,15 +60,13 @@ theorem sorted_ICan'tBelieveItCanSort [LinearOrder α] (A : Array α) : ICan'tBe
    case vc2.step.isFalse => constructor <;> grind case vc3.step.pre => grind case vc4.step.post.success => - expose_names simp_all rw [Array.pairwise_iff_getElem] at h_3 ⊢ grind case vc5.a.pre => grind case vc6.a.post.success => - expose_names simp_all rwa [show r.toArray = r.toArray.extract 0 N by grind] - theorem ICanActuallyProveItCanSort [LinearOrder α] (A : Array α) : (ICan'tBelieveItCanSort.{0} A |>.Perm A) ∧ (ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·)) := - ⟨perm_ICan'tBelieveItCanSort A, sorted_ICan'tBelieveItCanSort A⟩ + theorem ICan'tBelieveICanProveItCanSort! [LinearOrder α] (A : Array α) : (ICan'tBelieveItCanSort!.{0} A |>.Perm A) ∧ (ICan'tBelieveItCanSort!.{0} A |>.Pairwise (· ≤ ·)) := + ⟨perm_ICan'tBelieveItCanSort! A, sorted_ICan'tBelieveItCanSort! A⟩