Lean proofs of graph algorithms

Stream: new members

[Raphael]

I am brand new in the world of proof assistants. Is lean suitable for proving the correctness of simple graph algorithms such as Dijkstra's shortest path algorithm?

[Kevin Buzzard]

Right now I think the answer is "yes in theory, but in practice not many people are working on this kind of question"

[Shreyas Srinivas]

Raphael said:

I am brand new in the world of proof assistants. Is lean suitable for proving the correctness of simple graph algorithms such as Dijkstra's shortest path algorithm?

I am working on this. Some very very basic stuff is already in std or mathlib. Basic data structures are already in std. You will find some useful graph theoretic definitions and results in the combinatorics folder of Mathlib. If you are looking for a guide, see these books for Coq and Isabelle (the second one is still a WIP apparently)

The biggest challenge is to translate textbook graph theory definitions into convenient inductive definitions, especially when you want to identify subgraphs in a graph. So even if you were to ignore the "algorithmic" aspects and just verify the transformation being performed, the definitions get unwieldy very quickly. But this is not a lean specific issue.

[Shreyas Srinivas]

Once you get past this barrier, the next big headache is how sparse algorithms papers can be in details that are very important for you to even check the proof yourself with pen and paper.

[Shreyas Srinivas]

If you are new to this, I would recommend starting with string algorithms. They have a much simpler structure and there has been a lot of interesting work in this area in recent times, in particular on levenshtein distance.

[Raphael]

Thanks so much. String algorithms could be very interesting

[Scott Morrison]

@Shreyas Srinivas, this question was also asked on Stack Exchange at https://proofassistants.stackexchange.com/questions/2437/lean-proofs-for-graph-algorithms --- any chance you'd be interested in answering there as well?

(I think it's helpful for Lean generally if we have answers up in public places. The zulip is great, but needn't be everything!)

[Shreyas Srinivas]

@Scott Morrison : A stackexchange answer would have to be written much better than what I have currently written. I have too much on my plate at the moment to do anything today. But maybe sometime this week I will try to construct a nice stackexchange answer.

Another issue: Termination checking. Lean (and Coq too I believe) termination checks recursive functions which meet a certain positivity criteria which I'd say roughly corresponds to top-down recursion. Most algorithms work bottom up. For example dijkstra's algorithm constructs the shortest path subgraph from a starting node. So now the onus is on the user to prove that this algorithm that is producing a larger and larger subgraph eventually terminates because the input graph is finite (it wouldn't if the input graph was not finite).

[Shreyas Srinivas]

BTW, if you are handling modern string algorithms for edit distance, you might want to formalize some of the math in this paper, in particular the stuff about the so-called seaweed products of permutation matrices: https://link.springer.com/article/10.1007/s00453-013-9830-z

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

The (min, +) matrix products stuff is also useful in other places