Stream: MetaCoq

Topic: Axioms vs (typeclass) hypotheses

Jason Gross (Nov 24 2022 at 02:19):

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.

Théo Winterhalter (Nov 24 2022 at 08:33):

Isn't slower for no gain? Since we will never instantiate it with a proof.

Jason Gross (Nov 24 2022 at 12:12):

There are two gains;

1. In theory it's possible to prove normalization of a weaker environment using a stronger one. I've taken care to parameterize over normalization that fixes Sigma, so that this is possible.
2. This is instrumentally useful to factoring the code so that the checker can be fueled in a way that makes opaque proofs not depend on this axiom. I would really like to be able to avoid assuming the axiom of strong normalization when proving Löb's theorem (and in fact I think there's a chance it is required, because I need the axioms used in my outer environment to reflect the ones in my inner environment. Btw, how worried should I be about the proofs that require axiom-free-ness? It seems a shame that they can't be used with the set of axioms they depend on, such as the primitive float axioms + funext + UIP.)

Jason Gross (Nov 24 2022 at 12:14):

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?

Théo Winterhalter (Nov 24 2022 at 13:23):

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.

Paolo Giarrusso (Nov 24 2022 at 15:54):

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.

Jason Gross (Nov 24 2022 at 18:52):

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 +

Jason Gross (Nov 24 2022 at 22:27):

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

Jason Gross (Nov 25 2022 at 00:44):

PR should be fully ready for review now. Let me know if I should make a timing diff

Last updated: Jun 04 2023 at 23:30 UTC