Use `variable` to clean up Sort.lean

Changes

1 changed files (+11/-9)

• Sort.lean
  • @@ -1,7 +1,9 @@
    import Std.Tactic.Do import Mathlib - def BubbleSort [LinearOrder α] (A : Array α) := Id.run do + 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
  • @@ -11,7 +13,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 := Id.run do let N := A.size let mut A := A.toVector for hi : i in [:N] do
  • @@ -20,26 +22,25 @@ def ICan'tBelieveItCanSort [LinearOrder α] (A : Array α) := Id.run do
    A := A.swap i j return A.toArray - #guard let A := #[69, 420, 13, 1, 65536] + #guard let A := #[69, 420, 1, 1, 13, 1, 65536] ICan'tBelieveItCanSort A = A.qsort open Std.Do - theorem perm_ICan'tBelieveItCanSort [LinearOrder α] (A : Array α) : ICan'tBelieveItCanSort.{0} A |>.Perm A := by + theorem perm : 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 mvcgen - case inv1 => exact ⇓⟨_, A'⟩ => ⌜Multiset.ofList A.toList = A'.toList⌝ - case inv2 => exact ⇓⟨_, A'⟩ => ⌜Multiset.ofList A.toList = A'.toList⌝ + case inv1 | inv2 => exact ⇓⟨_, A'⟩ => ⌜Multiset.ofList A.toList = A'.toList⌝ all_goals try grind case vc1.step.isTrue => expose_names 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 + theorem sorted : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by generalize h : ICan'tBelieveItCanSort A = x apply Id.of_wp_run_eq h mvcgen <;> expose_names
  • @@ -68,5 +69,6 @@ theorem sorted_ICan'tBelieveItCanSort [LinearOrder α] (A : Array α) : ICan'tBe
    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 : (ICan'tBelieveItCanSort.{0} A |>.Perm A) + ∧ (ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·)) := + ⟨perm A, sorted A⟩