What is the problem with proving some form of completeness for
reduce_term (i.e. that it gives something in head normal form, for example)? It seems some work is being put into working around having to do this proof (https://github.com/MetaCoq/metacoq/pull/351)
Are you talking about the one that is proven correct (in the sense that it produces a reduct) or the other one?
Is there one that has a proof that it produces a reduced form?
Regarding the one proven correct, I intend to show it provides a weak head normal form at some point yes. I had started doing that proof but I had some problems in that the term produced by Equations was not reducing well, making it annoying to work with.
Ah, yes, I am talking about the one that is proven sound (if that's what you mean by correct). The one in
Yes that's what I meant.
As you can see there is an attempt that was really time consuming and it was incomplete for several reasons: some optimisations need strong properties on the theory (they might be proven now, I'll have to give it a look sometime), the current definition of whnf is wrong, there is a patch for it waiting inside a PR by Yannick.
The main reason it is not done is that we had other priorities I would say. :)
Ok, that's fair :) We are doing type erasure and also need to have some form of completeness to get rid of some admits.
It might be related to https://github.com/MetaCoq/metacoq/pull/351 which is the PR fixing
whnf (and I think even then it is missing a few cases).
Is getting this lemma urgent?
Right, that's the PR I was looking at. However, this makes safe erasure check after hnf that something is in whnf with a decider, instead of proving that that is the case. A slight detour, which is why I was curious.
No, we have plenty of other things to unadmit and work on, so no pressure :)
Sorry, that was the wrong line, I meant this one: https://github.com/MetaCoq/metacoq/pull/351/files#diff-770b1bdcda5334e5f22431195a95ea32R127
Your second link doesn't highlight anything for me.
I think GitHub does not load
SafeErasureFunction.v, but it's that file line 127
I see, indeed I think it's meant as a temporary solution.
I think I recall that some cases are impossible so we just return something that is not necessarily a whnf. Showing it is impossible is hard though and relies on typing. Furthermore, since it's hard we can't just return garbage that is whnf because then it's no longer a reduct.
Ok, that makes sense. Without having looked much into it, doesn't conversion also need a property like this?
Conversion will need it for completeness yes. This is very much on our todo list. It's just that we ended up choosing to add η before proving type-checking complete, so that we can check real stuff like the HoTT library.
Ok, cool! Thank you :)
Last updated: Aug 11 2022 at 02:03 UTC