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

Forgot to mention the efficiency: O(1) cons and O(log n) retrieval.

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: Feb 09 2023 at 01:03 UTC