feat: Adding proofs of correctness and time complexity of insertion sort#280
feat: Adding proofs of correctness and time complexity of insertion sort#280bhargavkulk wants to merge 9 commits intoleanprover:mainfrom
Conversation
|
I think this PR should be put on hold until we reach a decision on #275, specifically this question |
|
Hi Bhargav, thanks for interest in contributing! Just to add context to the above comment, I think this sort of PR will be welcome, but there is some infrastructure flux at the moment. In the meantime could you add the standard copyright header and address the CI failure? Thanks! |
|
I have added the copyright header and fixed the CI error. |
|
@sorrachai Can you review this code? |
sorrachai
left a comment
sorrachai
left a comment
There was a problem hiding this comment.
Please see https://github.com/leanprover/cslib?tab=contributing-ov-file#style-and-documentation for a link to the style documentation. You can follow the style from MergeSort in CSLib, for example.
|
@sorrachai I have added doc comments and edited the code to meet the style guide. Let me know id anything else is missing! |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
Here are some reviews that should help you in merging in changes from main.
| grind | ||
|
|
||
| /-- A list is sorted if it satisfies the `Pairwise (· ≤ ·)` predicate. -/ | ||
| abbrev IsSorted (l : List α) : Prop := List.Pairwise (· ≤ ·) l |
There was a problem hiding this comment.
I think we should use List.SortedLE for this.
At minimum you can't have this duplicated because it will cause a failure in importing this alongside the merge sort module. This declaration Cslib.Algorithms.Lean.TimeM.IsSorted should probably never have been namespaced in this way.
There was a problem hiding this comment.
I think SortedLE is deprecated in favour of Pairwise, so this usage is correct. The abbreviation is not necessary however.
There was a problem hiding this comment.
MergeSort.lean also defines the IsSorted abbrev. So, I am not sure if I should inline it.
There was a problem hiding this comment.
@Shreyas4991 I'm not sure that is correct. The deprecation on List.Sorted does refer to List.Pairwise, but the comment specifically says to consider using SortedLE, which is not deprecated and has sortedLE_iff_pairwise as a grind = lemma. I think it is correct to use SortedLE here. (And in the merge sort file, but let's make a separate PR)
|
I suggest merging main. The simp set for TimeM has changed. In fact depending on when main was merged last time, there might be considerable breakage. |
|
Fwiw this PR duplicates List.orderedInsert. See my Prog version of insertionSort in #275. |
|
@chenson2018 I have made the requested changes. See my comment on the |
|
Just as a heads up, #275 contains insertionSort already. Also the PR does not seem to pass CI at the moment. |
5 participants
I have added the file
InsertionSort.leanin this PR. I am aware thatList.insertionSortexists, but it is not instrumented withtick, which does not make it possible to write the complexity proof. I have chosen the worst case time bound asn^2but the same proof discharges forn(n+1)/2. I know I have not added the required documentation in this PR, but I first want to get an OK for the actual proofs implemented.I think insertion sort, while a very simple algorithm, merits its inclusion because more complicated sorts implemented in the standard libraries of programming languages (like "TimSort" in Python) use insertion sort to quickly sort smaller sub-arrays as insertion sort is faster than divide-and-conquer based comparison sorts like merge and quick sort for very small arrays. I believe that the proofs in this file would aid future proofs about these hybrid in-actual-use sorts.