Thoughts on turning
normalisation into a typeclass assumption rather than an axiom, for everything but the test-suite? I have most of a PR doing this at https://github.com/MetaCoq/metacoq/pull/792, and justification is there as well.
Isn't slower for no gain? Since we will never instantiate it with a proof.
There are two gains;
And what slowness are you concerned about? It's a
Prop, so there is no impact on extraction. It's a function type, so the impact on native / VM should be negligible. It's true that this adds an extra argument in some places (in others it just removes an argument), but I really don't think this is a concern. If you want, I can include a timing profile / diff?
I was wondering about the proof search. Using type classes just for a monad can lead to exponential blow-up when backtracking because of a type error. But maybe this won't be a problem here.
one imagines you won't ever have two instances in scope for this new class, which is more than strong enough to avoid exponential blowup.
Consider specifying good hint modes for the new classes (the MR lacks any), Coq's default modes are terrible since they allow all parameters to be outputs.
There currently are multiple instances in scope sometimes (already this is the case in the PR). The performance issue is trivial at present, though, because there are no global instances, and no instances that search for other things. I don't think specifying the mode will help much, but I'm fine adding a
Hint Mode +
Another gain: In theory, it would be possible to write a MetaCoq program that automatically manufactures a proof of strong normalization for a given global environment (one piece of the puzzle here: if there are n universes used in the program, then presumably there will be at least n+1 universes used in the proof of strong normalization). Then, for example, the erasure pipeline would not have to depend on an axiom of strong normalization, but could instead manufacture the proof for its particular environment. (I personally think this would be pretty neat!)
PR should be fully ready for review now. Let me know if I should make a timing diff
Last updated: Jan 30 2023 at 18:04 UTC