Slightly simplify sort proof

Changes

1 changed files (+13/-15)

• Sort.lean
  • @@ -1,8 +1,10 @@
    import Std.Tactic.Do import Batteries.Data.Array.Pairwise - import Mathlib.Data.Multiset.Defs + import Mathlib.Data.Nat.Basic - variable [LinearOrder α] (A : Array α) + -- Specify universe for α to avoid + -- https://github.com/leanprover/lean4/pull/10865 + variable {α : Type} [LinearOrder α] (A : Array α) def BubbleSort := Id.run do let N := A.size
  • @@ -28,20 +30,16 @@ def ICan'tBelieveItCanSort := Id.run do
    open Std.Do - theorem perm : ICan'tBelieveItCanSort.{0} A |>.Perm A := by + -- https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/mvcgen.20doesn't.20produce.20any.20invariant.20goals/near/557949517 + theorem perm : ICan'tBelieveItCanSort 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 | 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.toList <| Vector.swap_perm (by grind) (by grind) + mvcgen invariants + · ⇓⟨_, A'⟩ => ⌜Array.Perm A A'.toArray⌝ + · ⇓⟨_, A'⟩ => ⌜Array.Perm A A'.toArray⌝ + with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm] - theorem sorted : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by + theorem sorted : ICan'tBelieveItCanSort A |>.Pairwise (· ≤ ·) := by generalize h : ICan'tBelieveItCanSort A = x apply Id.of_wp_run_eq h mvcgen <;> expose_names
  • @@ -72,8 +70,8 @@ theorem sorted : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by
    simp_all exact (show r.toArray = r.toArray.extract 0 N by grind) ▸ h_1 - theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort.{0} A).Perm A - ∧ (ICan'tBelieveItCanSort.{0} A).Pairwise (· ≤ ·) := + theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort A).Perm A + ∧ (ICan'tBelieveItCanSort A).Pairwise (· ≤ ·) := ⟨perm A, sorted A⟩ -- Not sure why this needs so much boilerplate