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.
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?
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)
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.
OK, this gives me hopes (just by being a non-negative answer). Thanks Théo!
@Théo Winterhalter don't you have funext for convertibility ? like where the middle conversion is obtained by congruence under + the hypothesis and the two others are for functions
We don't really have η yet…
It's work in progress.
ok, but it holds in Coq, no ?
the part I would expect more difficult is that then ...
Doesn't that only hold in empty contexts?
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.
In empty contexts x
doesn't make sense so I hope not.
Ah, of course, I guess I was conflating it with canonicity
By inversion of typing we should get f x = f x ≡ f x = f y
.
And then it's a question of proving injectivity of (type) constructors, which should follow from confluence.
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.
@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?
Yes, but again we're talking about MetaCoq and not Coq itself.
This kind of stuff is still in progress for η.
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?
I don't think you need η to prove this so it could still work.
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.
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?
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 :-)
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.
Oh, and I need it also for open terms... I guess that's a different story!
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?
no no, I mean that f
and g
might have meta-variables, no that e
is a meta-variable. e
is eq_refl
.
Ah ok, then I agree it should work for open terms.
Is there work/plans on extending MetaCoq with open terms?
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.
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: Dec 07 2023 at 09:01 UTC