Graphs, trees, binary search trees, array, algorithms

Stream: new members

[Huỳnh Trần Khanh]

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]

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

[Alena Gusakov]

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]

Don't remember how much material there is though

[Kevin Buzzard]

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

[Huỳnh Trần Khanh]

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]

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]

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

[Kevin Buzzard]

Maybe you should ask a more precise question

[Mario Carneiro]

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]

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]

as always, software foundations has you covered:

[Andrew Ashworth]

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

[Huỳnh Trần Khanh]

@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.