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

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

@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

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.

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.

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.

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.

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.

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.

Looks like your second link is malformed

@Alexander Gryzlov sorry, link should be fixed now.

Last updated: Feb 04 2023 at 02:03 UTC