feat: add List.mergeSort_append and List.mergeSort_pair - #14995
Merged
Conversation
kim-em
added a commit
to kim-em/cslib
that referenced
this pull request
Sep 2, 2026
State countQueries_mergeSort_cons_cons with List.mergeSort arguments (the form eval_mergeSort rewrites to), isolate the List.mergeSort.eq_3 use in a private helper linking leanprover/lean4#14995, and derive mergeSort_upperBound through UpperBound.of_pointwise. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Pxy48TaP92UgEq28KGm8BG
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
kim-em
force-pushed
the
mergeSort_cons_cons
branch
from
September 2, 2026 02:27
fcae755 to
1aed0ac
Compare
kim-em
changed the title
kim-em
added a commit
to kim-em/cslib
that referenced
this pull request
Sep 2, 2026
Replace the private cons-cons unfolding with a mirror of the mergeSort_append lemma proposed in leanprover/lean4#14995 (merging the sorted halves of any balanced split gives mergeSort), deriving the split form from it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Pxy48TaP92UgEq28KGm8BG
mergeSort_append states that merging the sorted halves of any balanced split of a list gives mergeSort of the list, exposing the recursion of mergeSort without reference to MergeSort.Internal.splitInTwo or any index arithmetic. mergeSort_pair is the two-element simp lemma completing the mergeSort_nil / mergeSort_singleton progression. Needed by cslib. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Pxy48TaP92UgEq28KGm8BG
kim-em
changed the title
kim-em
force-pushed
the
mergeSort_cons_cons
branch
from
September 2, 2026 02:34
1aed0ac to
dcd3139
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds two lemmas exposing the recursion of
List.mergeSortwithout reference toMergeSort.Internal.splitInTwo:mergeSort_append: merging the sorted halves of any balanced split (l₂.length ≤ l₁.length ≤ l₂.length + 1) gives(l₁ ++ l₂).mergeSort. This is the primary statement: it has no index arithmetic, holds uniformly for every list length, and any specific unfolding (take/drop at the midpoint, cons-cons forms) is a two-line corollary.@[simp] mergeSort_pair:[a, b].mergeSort le = if le a b then [a, b] else [b, a], completing themergeSort_nil/mergeSort_singletonprogression. UnlikemergeSort_appendit genuinely simplifies, so it is marked@[simp].Downstream libraries currently have to use the auto-generated
List.mergeSort.eq_3(whose numbering is unstable, and which is not accessible from files using the module system withoutimport all) or unfoldsplitInTwo's subtype plumbing by hand; this came up in leanprover/cslib#401, where a query-complexity model of merge sort is proved to agree withList.mergeSort.🤖 Prepared with Claude Code