Wait no I hallucinated the !, it's not in the original paper

Changes

1 changed files (+8/-8)

• 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,12 +21,12 @@ 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 - generalize h : ICan'tBelieveItCanSort! A = x + 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 } apply Id.of_wp_run_eq h
  • @@ -39,8 +39,8 @@ theorem perm_ICan'tBelieveItCanSort! [LinearOrder α] (A : Array α) : ICan'tBel
    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 <;> expose_names case inv1 => exact ⇓⟨xs, A'⟩ => ⌜A'.take xs.pos |>.toArray.Pairwise (· ≤ ·)⌝
  • @@ -68,5 +68,5 @@ theorem sorted_ICan'tBelieveItCanSort! [LinearOrder α] (A : Array α) : ICan'tB
    simp_all rwa [show r.toArray = r.toArray.extract 0 N by grind] - 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⟩ + 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⟩