Stream: MetaCoq

Topic: migrate metacoq to coq-hott


view this post on Zulip Ember Edison (Oct 06 2021 at 18:49):

What problems will I encounter if I try to migrate metacoq to coq-hott?

I have difficulty understanding how many good properties of coq are inherited by coq-hott, and I don't catch the basic properties of coq-hott model.
HITs don't seem to cause problems (really?), but What does flag -indices-matter, Axiom UA mean for metacoq?

view this post on Zulip Ali Caglayan (Oct 06 2021 at 20:38):

So MetaCoq has an internal representation of Coq and they have shown it to be "equivalent" to the coq syntax they are writing it in. The problem with UA is that properties canonicity are lost, thought you have canonicity up to identity type. Point being, almost all the metatheoretic considerations of MetaCoq need to be redone.

The HoTT library doesn't really have HITs but really a close enough approximation of them. We use "private inductive types and axioms hidden in a module". This gives the appearance of HITs in the HoTT library but it isn't a syntactic entity that can be manipulated in metacoq. Not to mention, private inductive types a basically a kernel hack. Speaking outside of coq, there are not any universally agreed upon syntactic definitions of HITs in general, the closest is probably https://arxiv.org/abs/1902.00297

That is not to say, if you postulated say quotients in coq, and somehow represented them in syntax in Metacoq you wouldn't be able to prove things about them. But I would be very sure nice properties like canonicity won't hold (this is already a problem with function extensionality).

In terms of indices-matter, MetaCoq, from what I can see, doesnn't treat this, but that shouldn't be an issue to add to the internal syntax and prove everything normally assuming indices-matter.

I think other properties like subject reduction (terms have the same type when reduced) should hold for all of the above, it's just that it adds more complexity to the metacoq proofs.

view this post on Zulip Gaƫtan Gilbert (Oct 06 2021 at 20:50):

private inductive types a basically a kernel hack

they're a user syntax hack, the kernel doesn't care


Last updated: Aug 11 2022 at 02:03 UTC