Zulip Chat Archive

Stream: new members

Topic: Graphs, trees, binary search trees, array, algorithms


Huỳnh Trần Khanh (Feb 06 2021 at 10:54):

I want to formalize competitive programming problems in Lean. Think of it as a competitive programming analog of the IMO Grand Challenge, LOL. But I don't really know how to formalize commonly used algorithms and data structures such as BFS, Dijkstra, Floyd–Warshall, sparse tables, segment trees and stuff. Can anyone point me in the right direction?

Huỳnh Trần Khanh (Feb 06 2021 at 11:05):

For example, could you point me to a GitHub repository of formalized algorithms in Lean?

Alena Gusakov (Feb 06 2021 at 11:46):

Personally idk about any repositiories with all of that, but I do know that mathlib currently contains a little bit of material on binary trees

Alena Gusakov (Feb 06 2021 at 11:46):

Don't remember how much material there is though

Kevin Buzzard (Feb 06 2021 at 11:58):

Can you not just follow the kind of thing done in Haskell?

Huỳnh Trần Khanh (Feb 06 2021 at 12:49):

Of course I can't, that's why I'm asking! Sure I can crib techniques from Haskell when I formalize the implementation but I think proving is more complicated, and I'm pretty sure Haskell is not a verification language by any stretch of the imagination.

Huỳnh Trần Khanh (Feb 06 2021 at 12:55):

By now I've skimmed through every thread in the Program verification stream and I couldn't find anything I'm looking for.

Kevin Buzzard (Feb 06 2021 at 13:38):

I had misunderstood, I thought you were just asking about implementing the algorithms and data structures you listed

Kevin Buzzard (Feb 06 2021 at 13:40):

Maybe you should ask a more precise question

Mario Carneiro (Feb 06 2021 at 19:47):

Generally speaking, you can just write a program like you would in haskell and as long as it's non-meta you can prove properties about it after the fact in lean

Mario Carneiro (Feb 06 2021 at 19:49):

the only thing you have to be careful about while writing the definition is that it is structured such that it "manifestly" terminates

Andrew Ashworth (Feb 07 2021 at 00:47):

as always, software foundations has you covered:

Andrew Ashworth (Feb 07 2021 at 00:47):

https://softwarefoundations.cis.upenn.edu/vfa-current/index.html

Huỳnh Trần Khanh (Feb 07 2021 at 02:34):

@Andrew Ashworth Oh neat! From what I've gathered, it looks like no one has attempted to formalize and prove properties about the algorithms and data structures I mentioned in Lean right? So I could consider myself a pioneer, haha. And I don't expect segment trees, sparse tables or even tries to be covered by software foundations as these data structures are specific to competitive programming, which is a pretty niche field.


Last updated: Dec 20 2023 at 11:08 UTC