Pierre-Marie Pédrot (Dec 08 2020 at 16:43): Pierre-Marie Pédrot (Dec 08 2020 at 16:43):Dear MetaCoq mother brain, I'd like to bring to your attention the following Coq PR: https://github.com/coq/coq/pull/13537. It's an asymptotically efficient implementation of substitutions to be used in the kernel. It's a nifty structure I am quite proud of, which boils down to the infernal hybrid of Okazaki skewed lists with a writer monad tracking shifts. I may probably write a blog post on the topic when I have a bit of time, but in the meantime, I thought that if you were fed up with η-expansion, you might give a try at its implementation (and proof of correctness) in MetaCoq. It's a purely functional data structure that is quite easily implemented in Coq, so the proof shouldn't be too hard. Who knows, it might even be useful for your own development...
Pierre-Marie Pédrot (Dec 08 2020 at 16:43):Forgot to mention the efficiency: O(1) cons and O(log n) retrieval.
Matthieu Sozeau (Dec 08 2020 at 18:19):I looks like it could go into a general "wishes for formalization" list that people interested in learning/developing MetaCoq could tackle, I'll link it from there.
Last updated: May 31 2023 at 09:01 UTC