Jakob Botsch Nielsen (Jun 04 2020 at 09:27): Jakob Botsch Nielsen (Jun 04 2020 at 09:27):What is the problem with proving some form of completeness for hnf/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)
Théo Winterhalter (Jun 04 2020 at 09:28):Are you talking about the one that is proven correct (in the sense that it produces a reduct) or the other one?
Jakob Botsch Nielsen (Jun 04 2020 at 09:29):Is there one that has a proof that it produces a reduced form?
Théo Winterhalter (Jun 04 2020 at 09:29):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.
Jakob Botsch Nielsen (Jun 04 2020 at 09:30):Ah, yes, I am talking about the one that is proven sound (if that's what you mean by correct). The one in PCUICSafeReduce.
Théo Winterhalter (Jun 04 2020 at 09:31):Yes https://github.com/MetaCoq/metacoq/blob/coq-8.11/safechecker/theories/PCUICSafeReduce.v#L1099
Théo Winterhalter (Jun 04 2020 at 09:31):Yes that's what I meant.
Théo Winterhalter (Jun 04 2020 at 09:32):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.
Théo Winterhalter (Jun 04 2020 at 09:33):The main reason it is not done is that we had other priorities I would say. :)
Jakob Botsch Nielsen (Jun 04 2020 at 09:34):Ok, that's fair :) We are doing type erasure and also need to have some form of completeness to get rid of some admits.
Théo Winterhalter (Jun 04 2020 at 09:37):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).
Théo Winterhalter (Jun 04 2020 at 09:39):Is getting this lemma urgent?
Jakob Botsch Nielsen (Jun 04 2020 at 09:39):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.
Here: https://github.com/MetaCoq/metacoq/pull/351/files#diff-167f00d53053c34c7df0405319371d66R157
Jakob Botsch Nielsen (Jun 04 2020 at 09:40):No, we have plenty of other things to unadmit and work on, so no pressure :)
Jakob Botsch Nielsen (Jun 04 2020 at 09:40):Sorry, that was the wrong line, I meant this one: https://github.com/MetaCoq/metacoq/pull/351/files#diff-770b1bdcda5334e5f22431195a95ea32R127
Théo Winterhalter (Jun 04 2020 at 09:43):Your second link doesn't highlight anything for me.
Jakob Botsch Nielsen (Jun 04 2020 at 09:44):I think GitHub does not load SafeErasureFunction.v, but it's that file line 127
Théo Winterhalter (Jun 04 2020 at 09:45):I see, indeed I think it's meant as a temporary solution.
Théo Winterhalter (Jun 04 2020 at 09:47):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.
Jakob Botsch Nielsen (Jun 04 2020 at 09:48):Ok, that makes sense. Without having looked much into it, doesn't conversion also need a property like this?
Théo Winterhalter (Jun 04 2020 at 09:54):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.
Jakob Botsch Nielsen (Jun 04 2020 at 09:56):Ok, cool! Thank you :)
Last updated: Jun 01 2023 at 11:01 UTC