Stream: MetaCoq

Topic: hnf/reduce_term


view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Jakob Botsch Nielsen (Jun 04 2020 at 09:29):

Is there one that has a proof that it produces a reduced form?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Jun 04 2020 at 09:31):

Yes https://github.com/MetaCoq/metacoq/blob/coq-8.11/safechecker/theories/PCUICSafeReduce.v#L1099

view this post on Zulip Théo Winterhalter (Jun 04 2020 at 09:31):

Yes that's what I meant.

view this post on Zulip 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.

view this post on Zulip 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. :)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Théo Winterhalter (Jun 04 2020 at 09:39):

Is getting this lemma urgent?

view this post on Zulip 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

view this post on Zulip Jakob Botsch Nielsen (Jun 04 2020 at 09:40):

No, we have plenty of other things to unadmit and work on, so no pressure :)

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (Jun 04 2020 at 09:43):

Your second link doesn't highlight anything for me.

view this post on Zulip Jakob Botsch Nielsen (Jun 04 2020 at 09:44):

I think GitHub does not load SafeErasureFunction.v, but it's that file line 127

view this post on Zulip Théo Winterhalter (Jun 04 2020 at 09:45):

I see, indeed I think it's meant as a temporary solution.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Jakob Botsch Nielsen (Jun 04 2020 at 09:56):

Ok, cool! Thank you :)


Last updated: Aug 11 2022 at 02:03 UTC