Skip to content

feat(Algorithms): Prove insertion sort is stable#446

Draft
Arleee1 wants to merge 52 commits intoleanprover:mainfrom
Arleee1:insertionstable
Draft

feat(Algorithms): Prove insertion sort is stable#446
Arleee1 wants to merge 52 commits intoleanprover:mainfrom
Arleee1:insertionstable

Conversation

@Arleee1
Copy link
Copy Markdown

@Arleee1 Arleee1 commented Mar 19, 2026

Prove the insertionsort implementation is stable.
Aristotle AI was used for portions of this work.

Depends on #372. My contributions are only in my commits.

Comment thread Cslib/AlgorithmsTheory/Algorithms/ListInsertionSort.lean Outdated
Comment thread Cslib/AlgorithmsTheory/Models/ListComparisonSort.lean Outdated
@Arleee1 Arleee1 requested a review from Shreyas4991 April 15, 2026 20:45
@Arleee1
Copy link
Copy Markdown
Author

Arleee1 commented Apr 15, 2026

Updated based on @Shreyas4991 's PR feedback, also golfed and cleaned up

Made similar updates in the merge sort stable PR #442

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants