Finish the proof yayayayayyay

Changes

1 changed files (+29/-21)

• Sort.lean
  • @@ -1,7 +1,7 @@
    import Std.Tactic.Do import Mathlib - def BubbleSort [LT α] [DecidableLT α] (A : Array α) := Id.run do + def BubbleSort [LinearOrder α] (A : Array α) := Id.run do let N := A.size let mut A := A.toVector for i in List.range (N - 1) do
  • @@ -11,7 +11,7 @@ def BubbleSort [LT α] [DecidableLT α] (A : Array α) := Id.run do
    A := A.swap j (j + 1) return A.toArray - def ICan'tBelieveItCanSort [LT α] [DecidableLT α] (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
  • @@ -20,49 +20,57 @@ def ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) := Id.run do
    A := A.swap i j return A.toArray + #guard let A := #[69, 420, 13, 1, 65536] + ICan'tBelieveItCanSort A = A.qsort + open Std.Do - theorem perm_ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) : ICan'tBelieveItCanSort.{0} A |>.Perm A := by + 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 - rw [Multiset.coe_eq_coe] at this - exact { toList := this } + 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⌝ + case inv2 => 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₂ + exact h_5.trans <| .symm <| Vector.perm_iff_toList_perm.mp <| Vector.swap_perm (by grind) (by grind) - theorem sorted_ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) : ICan'tBelieveItCanSort.{0} A |>.Pairwise (¬ · > ·) := by + 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 - case inv1 => exact ⇓⟨xs, A'⟩ => ⌜A'.take xs.prefix.length |>.toArray.Pairwise (¬ · > ·)⌝ - case vc1.step.isTrue => + case inv1 => exact ⇓⟨xs, A'⟩ => ⌜A'.take xs.pos |>.toArray.Pairwise (· ≤ ·)⌝ + case inv2 => expose_names - simp_all - grind - sorry - case vc2.step.isFalse => + 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 - grind - sorry + constructor + · rw [Array.pairwise_iff_getElem] at h_5 ⊢ + intro i j hi hj hij + simp + grind + · grind + 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 - 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] + 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⟩