feat(Algorithms): Prove insertion sort is stable#446
feat(Algorithms): Prove insertion sort is stable#446Arleee1 wants to merge 50 commits intoleanprover:mainfrom
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…o query-final-squash
Co-authored-by: Shreyas Srinivas <Shreyas4991@users.noreply.github.com> Co-authored-by: Eric Wieser <eric-wieser@users.noreply.github.com> Co-authored-by: Tanner Duve <tannerduve@gmail.com>
…o query-final-squash
Arleee1
force-pushed
the
insertionstable
branch
from
c1bfab5 to
f46ca23
Compare
| /- | ||
| Copyright (c) 2026 Shreyas Srinivas. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Shreyas Srinivas, Eric Wieser |
There was a problem hiding this comment.
you should append your name here to the authors list. You are adding new content to this file.
|
|
||
| section SortStability | ||
|
|
||
| /-- Definition of a stable sorting algorithm. -/ |
There was a problem hiding this comment.
Definition of a stable list sorting algorithm. This definition uses List functions and is of course specific to lists. We should revisit the location of this definition at some point. This is a property of lists independent of Progs on the comparison query model.
There was a problem hiding this comment.
Thank you for the review! I will update to specify that it is for lists. As for the location, I think it could make sense to define classes for list sorting algorithms in a separate file and another class that extends it for stable algorithms, what do you think of that idea?
There was a problem hiding this comment.
That's a bigger change. I would leave it for a later PR. I just think a TODO comment would suffice. It should say that these definitions should be upstreamed or relocated
3 participants
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.