Adding new algorithms proof in cslib

Stream: CSLib

[Ved Bhatawadekar]

Hey I wanted to contribute to the cslib library. I see someone has added a proof for merge sort in algorithms section.
Which algorithms can I pick up next? any suggestions? I was thinking about doing insertion sort/bubble sort?

[Shreyas Srinivas]

I would recommend waiting until we sort out some model level conundrums (such as cslib#201)

[Shreyas Srinivas]

I recommend checking out the CSLib channel. There seems to be a lot to do in automata theory and logic

[Shreyas Srinivas]

You could try formalising the functional correctness of the McNaughton Yamada algorithm for example

[Chris Henson]

I don't have permission to move messages from here, but yes please ask CSLib-specific questions in the dedicated channel. (I don't work much on algorithms, so I can't really answer your actual question)

[Notification Bot]

This topic was moved here from #computer science > Adding new algorithms proof in cslib by Patrick Massot.

[Wrenna Robson]

I am quite interesting in algorithms stuff too so keen to hear more about this.

[Wrenna Robson]

I can already see stuff I want to improve about the merge sort stuff (having recently worked on Mathlib's version of this, which sadly doesn't track complexity).

[GasStationManager]

For complexity of algorithms yes we'd better wait for the modeling to settle.
Meanwhile, if you're interested in the mathematical properties of algorithms, we can already study them as Lean functions and prove things about them. That's the approach taken in my repo ArtificialAlgorithms. It includes some basic algorithms like insertion sort, but also more exotic ones like Value Iteration and Stochastic Gradient Descent, whose convergence properties are more nontrivial to prove.

[Wrenna Robson]

Just FYI, Sorted is now a deprecated predicate.

[Wrenna Robson]

you probably want SortedLE

[Shreyas Srinivas]

Fwiw, cslib#275 is starting to take shape

[Shreyas Srinivas]

I have some trouble getting one of the coercions working, and I am still preparing serious examples, but you can see some good and bad ones already in the repository