Bas Spitters (Jul 11 2022 at 12:33): 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
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.)
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
Karl Palmskog (Jul 13 2022 at 16:33): 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.
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.
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.
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.
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.
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.
Alexander Gryzlov (Jul 14 2022 at 11:18):Looks like your second link is malformed
Bas Spitters (Jul 14 2022 at 12:01):@Alexander Gryzlov sorry, link should be fixed now.
Last updated: Jun 03 2023 at 18:01 UTC