Stream: MetaCoq

Topic: Dis/proving a meta-theoretical question


view this post on Zulip Beta Ziliani (Jun 16 2020 at 20:31):

Hi, I'm not sure if this is the place to put this, but I'm interested in discussing the limits of proving meta-theorems in MetaCoq. If I have f x = g x for x a variable, my intuition says that I should be able to get that f = g. I have a classical proof of it (pen and paper, do not trust it), but I'd like to know if it holds constructively and/or if I can prove it in MetaCoq.

view this post on Zulip Théo Winterhalter (Jun 16 2020 at 21:33):

What lemma exactly do you have in mind?

Goal forall f g n, tApp f [ tRel n ] = tApp g [ tRel n ] -> f = g.

Or do you want to involve conversion or the reifcation of equality?

view this post on Zulip Beta Ziliani (Jun 17 2020 at 14:04):

Good question, probably we need to state that = there is actually eq_refl (sorry, I don't know the terminology of MetaCoq, and let me be loose about contexts and tApp nodes):

typing (tConstructor "eq_refl") (tInd "eq" (tApp f (tRel n)) (tApp g (tRel n)) -> typing (tConstructor "eq_refl") (tInd "eq" f g)

view this post on Zulip Théo Winterhalter (Jun 17 2020 at 14:12):

So what you mean is that if f x and g x are _convertible_ then so are f and g? I believe it should be provable yes, but complicated. From confluence we know that being convertible mean that both terms reduce to the same term (up to universes). Now if there is no β-reduction at top-level we win. If there is one on either side it becomes harder I think.

view this post on Zulip Beta Ziliani (Jun 17 2020 at 14:19):

OK, this gives me hopes (just by being a non-negative answer). Thanks Théo!

view this post on Zulip Kenji Maillard (Jun 17 2020 at 14:21):

@Théo Winterhalter don't you have funext for convertibility ? like fλx.fxλx.gxgf \equiv \lambda x. f\,x \equiv \lambda x. g\,x \equiv g where the middle conversion is obtained by congruence under λ\lambda + the hypothesis and the two others are η\eta for functions

view this post on Zulip Théo Winterhalter (Jun 17 2020 at 14:21):

We don't really have η yet…

view this post on Zulip Théo Winterhalter (Jun 17 2020 at 14:22):

It's work in progress.

view this post on Zulip Kenji Maillard (Jun 17 2020 at 14:22):

ok, but it holds in Coq, no ?

view this post on Zulip Kenji Maillard (Jun 17 2020 at 14:23):

the part I would expect more difficult is that Γeq_refl:fx=gx\Gamma \vdash \texttt{eq\_refl} : f\,x = g\,x then Γfxgx\Gamma \vdash f\,x \equiv g\,x...

view this post on Zulip Jakob Botsch Nielsen (Jun 17 2020 at 14:25):

Doesn't that only hold in empty contexts?

view this post on Zulip Théo Winterhalter (Jun 17 2020 at 14:25):

Right, but we're talking MetaCoq, and specifying η is complicated so I won't speculate just yet. Turning a reflexivity proof into a conversion proof isn't so scary. I think we already have some similar stuff.

view this post on Zulip Théo Winterhalter (Jun 17 2020 at 14:26):

In empty contexts x doesn't make sense so I hope not.

view this post on Zulip Jakob Botsch Nielsen (Jun 17 2020 at 14:26):

Ah, of course, I guess I was conflating it with canonicity

view this post on Zulip Théo Winterhalter (Jun 17 2020 at 14:26):

By inversion of typing we should get f x = f x ≡ f x = f y.

view this post on Zulip Théo Winterhalter (Jun 17 2020 at 14:27):

And then it's a question of proving injectivity of (type) constructors, which should follow from confluence.

view this post on Zulip Matthieu Sozeau (Jun 17 2020 at 15:04):

Théo Winterhalter said:

And then it's a question of proving injectivity of (type) constructors, which should follow from confluence.

It does, inductive types are injective w.r.t. conversion.

view this post on Zulip Paolo Giarrusso (Jun 17 2020 at 15:39):

@Théo Winterhalter @Kenji Maillard

From confluence we know that being convertible mean that both terms reduce to the same term (up to universes).

For Coq, shouldn't that include "up to universes _and eta_", given how convertibility is defined in https://coq.github.io/doc/v8.12/refman/language/core/conversion.html#convertibility — in particular, eta is not part of reduction, so it must be accounted explicitly here?

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

Yes, but again we're talking about MetaCoq and not Coq itself.

view this post on Zulip Théo Winterhalter (Jun 17 2020 at 15:40):

This kind of stuff is still in progress for η.

view this post on Zulip Beta Ziliani (Jun 18 2020 at 01:25):

Ah, but my point in using MetaCoq is to be sure I don't return wrong terms in my meta-programs (Mtac2). What I want to be able is to return eq_refl for f = g, but if that's not true, then I guess we will need to add a typechecking step (booooh) that will most surely always succeed to make sure we don't break things. Am I right?

view this post on Zulip Théo Winterhalter (Jun 18 2020 at 07:17):

I don't think you need η to prove this so it could still work.

view this post on Zulip Paolo Giarrusso (Jun 18 2020 at 13:46):

FWIW: Even if you needn't eta, it seems you'd have to account for it — since the ultimate question for Mtac2 is about Coq? So the proof that Beta wants must use inversion on a Coq convertibility proof, which could be using eta.

view this post on Zulip Paolo Giarrusso (Jun 18 2020 at 13:47):

However, maybe you can prove that if two terms f and g are convertible, then their beta-normal forms are both eta-equivalent (hence convertible) to the same beta-eta-long-normal form, and then follow along the original proof sketch?

view this post on Zulip Beta Ziliani (Jun 18 2020 at 14:52):

sounds reasonable to me, but the real question here is: if I prove something in MetaCoq, to what extent should I worry that it won't be true in Coq? I'm looking for MetaCoq to help me avoid hideous bugs in Mtac2 :-)

view this post on Zulip Théo Winterhalter (Jun 18 2020 at 15:21):

If you take conversion as assumption then indeed you will have the problem that it is for now smaller than that of Coq. I mean, it currently already accounts for η but most properties aren't proven with η so… If you want it I suggest to wait a little bit, people are working on it at the moment.

view this post on Zulip Beta Ziliani (Jun 18 2020 at 15:46):

Oh, and I need it also for open terms... I guess that's a different story!

view this post on Zulip Théo Winterhalter (Jun 18 2020 at 15:54):

For open terms I expect it to be wrong. If you have e : f x = g x in your context, how do you intend to deduce some term of type f = g without funext?

view this post on Zulip Beta Ziliani (Jun 18 2020 at 18:54):

no no, I mean that f and g might have meta-variables, no that e is a meta-variable. e is eq_refl.

view this post on Zulip Théo Winterhalter (Jun 19 2020 at 07:13):

Ah ok, then I agree it should work for open terms.

view this post on Zulip Beta Ziliani (Jun 19 2020 at 15:01):

Is there work/plans on extending MetaCoq with open terms?

view this post on Zulip Théo Winterhalter (Jun 19 2020 at 15:05):

You mean evars right? For me, having free variables is the definition of open term, which we already deal with.
Existential variables are more complicated but I guess it will be handled at some point, I wouldn't expect them in the near future. Maybe @Matthieu Sozeau can comment on this.

view this post on Zulip Matthieu Sozeau (Jun 19 2020 at 15:07):

There is a hope but I don't have deadline for adding them yet. I guess it wouldn't be too hard to do though, it's mainly orthogonal to what is already formalized.


Last updated: Aug 11 2022 at 01:03 UTC