Skip to content

feat(Algorithms/Lean/MergeSort): relate mergeSort to List.mergeSort #605

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
exekis wants to merge 1 commit into
base: main
Choose a base branch
from
Open

feat(Algorithms/Lean/MergeSort): relate mergeSort to List.mergeSort #605

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ Authors: Sorrachai Yingchareonthawornhcai
module

public import Cslib.Algorithms.Lean.TimeM
public import Mathlib.Data.List.Sort
public import Mathlib.Data.Nat.Cast.Order.Ring
public import Mathlib.Data.Nat.Lattice
public import Mathlib.Data.Nat.Log
Expand Down Expand Up @@ -110,6 +111,16 @@ theorem mergeSort_perm (xs : List α) : ⟪mergeSort xs⟫ ~ xs := by
theorem mergeSort_correct (xs : List α) : IsSorted ⟪mergeSort xs⟫ ∧ ⟪mergeSort xs⟫ ~ xs :=
⟨mergeSort_sorted xs, mergeSort_perm xs⟩

/-- the timed merge sort computes the same sorted list as list merge sort -/
@[simp, grind =]
theorem ret_mergeSort (xs : List α) :
⟪mergeSort xs⟫ = xs.mergeSort (· ≤ ·) := by
have hsorted₁ : (⟪mergeSort xs⟫).SortedLE := by
simpa [List.sortedLE_iff_pairwise] using mergeSort_sorted xs
have hsorted₂ : (xs.mergeSort (· ≤ ·)).SortedLE := List.sortedLE_mergeSort
exact List.Perm.eq_of_sortedLE hsorted₁ hsorted₂
((mergeSort_perm xs).trans (List.mergeSort_perm xs (· ≤ ·)).symm)

end Correctness

section TimeComplexity
Expand Down