Stream: MetaCoq

Topic: Dis/proving a meta-theoretical question

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.

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?

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)

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.

Beta Ziliani (Jun 17 2020 at 14:19):

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

Kenji Maillard (Jun 17 2020 at 14:21):

@Théo Winterhalter don't you have funext for convertibility ? like $f \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

Théo Winterhalter (Jun 17 2020 at 14:21):

We don't really have η yet…

Théo Winterhalter (Jun 17 2020 at 14:22):

It's work in progress.

Kenji Maillard (Jun 17 2020 at 14:22):

ok, but it holds in Coq, no ?

Kenji Maillard (Jun 17 2020 at 14:23):

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

Jakob Botsch Nielsen (Jun 17 2020 at 14:25):

Doesn't that only hold in empty contexts?

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.

Théo Winterhalter (Jun 17 2020 at 14:26):

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

Jakob Botsch Nielsen (Jun 17 2020 at 14:26):

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

Théo Winterhalter (Jun 17 2020 at 14:26):

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

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.

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.

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?

Théo Winterhalter (Jun 17 2020 at 15:39):

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

Théo Winterhalter (Jun 17 2020 at 15:40):

This kind of stuff is still in progress for η.

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?

Théo Winterhalter (Jun 18 2020 at 07:17):

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

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.

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?

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

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.

Beta Ziliani (Jun 18 2020 at 15:46):

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

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?

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.

Théo Winterhalter (Jun 19 2020 at 07:13):

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

Beta Ziliani (Jun 19 2020 at 15:01):

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

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.

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: Jun 01 2023 at 11:01 UTC