Stream: coq-community devs & users

Topic: Functional algorithms verified


view this post on Zulip Bas Spitters (Jul 11 2022 at 12:33):

Nice book about algorithms in isabelle. I wonder how much of this is readily available in Coq.
https://functional-algorithms-verified.org/functional_algorithms_verified.pdf

view this post on Zulip Kazuhiko Sakaguchi (Jul 11 2022 at 13:15):

I might be nitpicking here, but I found it unfortunate that Chapter 2 does not cover tail-recursive mergesort. I wouldn't be surprised if many of their implementations trigger a stack overflow in practice. (So there is room for improvements.)

view this post on Zulip Karl Palmskog (Jul 13 2022 at 16:32):

@Bas Spitters just to ensure that you didn't miss this, which was discussed in another mathcomp Coq users topic: https://github.com/clayrat/fav-ssr

view this post on Zulip Karl Palmskog (Jul 13 2022 at 16:33):

crossref: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/ordered.20data.20structure.3F/near/289447680

view this post on Zulip Bas Spitters (Jul 14 2022 at 07:42):

Very cool. @Alexander Gryzlov Can you compare your coq proofs with the isabelle ones? Perhaps, mostly in term of automation, which seems to be isabelle's main bragging right.

view this post on Zulip Alexander Gryzlov (Jul 14 2022 at 09:19):

Hey, glad you're interested in the port! I was planning to write a blog post or two with a comparison after I finish the project, but basically the main differences are in the use of sets/multisets (I'm using predicates and list equivalences instead, so the reasoning becomes more "intuitionistic") and the fact that Coq code has to be total, which means the code has to be rearranged in some places and/or extra well-foundedness proofs are needed.

view this post on Zulip Alexander Gryzlov (Jul 14 2022 at 09:22):

Re automation, I actually don't use any beyond relying on SSreflect's computational ideology, so the proofs are quite "low-level" and typically 2-3x larger than Isabelle counterparts, following the same structure. I suspect it can be made much closer to Isabelle by using something like itauto, not sure how well it plays with SSR.

view this post on Zulip Alexander Gryzlov (Jul 14 2022 at 09:26):

My initial idea was to do a second pass over the proofs at some point in the future and try to extract some generic sequence/tree theories out of them instead of "sweeping things under the rug" with automation, so currently it's all very explicit.

view this post on Zulip Bas Spitters (Jul 14 2022 at 10:40):

That's interesting about Sets. Would it be possible to use mc's finset, or a similar quotient?
https://math-comp.github.io/htmldoc/mathcomp.ssreflect.finset.html

We're having some discussion here on how to combine automation with math-comp.

view this post on Zulip Alexander Gryzlov (Jul 14 2022 at 11:12):

I thought about using finsets at first, but actually using predicates with their proofs is pretty straightforward and you get more generality. I think the only place you could profit from finiteness is the Huffman's algorithm.

view this post on Zulip Alexander Gryzlov (Jul 14 2022 at 11:18):

Looks like your second link is malformed

view this post on Zulip Bas Spitters (Jul 14 2022 at 12:01):

@Alexander Gryzlov sorry, link should be fixed now.


Last updated: Feb 04 2023 at 02:03 UTC