Stream: Coq workshop 2020

Topic: [S2] Generating induction principles and subterm...


view this post on Zulip Théo Zimmermann (Jun 24 2020 at 11:18):

This is the topic to ask questions on the talk "Generating induction principles and subterm relations for inductive types using MetaCoq".

view this post on Zulip Enrico Tassi (Jul 05 2020 at 12:52):

Bump

view this post on Zulip Bas Spitters (Jul 05 2020 at 13:01):

How does meta-coq compare with agda's reflection to build tactics.
https://github.com/alhassy/gentle-intro-to-reflection

view this post on Zulip Cyril Cohen (Jul 05 2020 at 13:04):

Q: where is the source code?

view this post on Zulip Enrico Tassi (Jul 05 2020 at 13:04):

Q: How do you store previously generated principles in MetaCoq, across multiple runs? Is there a database API?

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 13:06):

Q: Can I use it to prove induction principles I state?

view this post on Zulip Bas Spitters (Jul 05 2020 at 13:08):

Thanks @Yannick Forster that is also my impression.

view this post on Zulip Marcel Ullrich (Jul 05 2020 at 13:08):

https://github.com/uds-psl/metacoq-examples-coqws
here

view this post on Zulip Cyril Cohen (Jul 05 2020 at 13:10):

Marcel Ullrich said:

https://github.com/uds-psl/metacoq-examples-coqws
here

I am looking for the parametricity translation, can you point me to the corresponding piece of code?

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 13:10):

Similar as you showed, but I want to control it.

view this post on Zulip Enrico Tassi (Jul 05 2020 at 13:11):

A: I did not prove it, but others that actually understand category theory did it I believe (I cite them).

view this post on Zulip Marcel Ullrich (Jul 05 2020 at 13:12):

The parametricity translation is in the MetaCoq repository
https://github.com/MetaCoq/metacoq/blob/coq-8.11/translations/param_original.v

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:12):

@Cyril Cohen We're using the parametricity translation from the translations directory of the MetaCoq repo, with some manual postprocessing. I think that was initially implemented by Simon Boulier

view this post on Zulip Matthieu Sozeau (Jul 05 2020 at 13:13):

And Cyril Cohen :)

view this post on Zulip Enrico Tassi (Jul 05 2020 at 13:13):

Cyril, are you looking for your own code :grinning_face_with_smiling_eyes: ?

view this post on Zulip Samuel Gruetter (Jul 05 2020 at 13:14):

If I have an Inductive Prop that invokes itself under a disjunction, can you generate an IH for this?

view this post on Zulip Cyril Cohen (Jul 05 2020 at 13:14):

Oh I thought there was yet another implementation... ok then I know of this one ;)

view this post on Zulip Enrico Tassi (Jul 05 2020 at 13:16):

Samuel Gruetter said:

If I have an Inductive Prop that invokes itself under a disjunction, can you generate an IH for this?

It should work (both the metacoq plugin and the one in Elpi) since Or is just a container with 2 type parameters.

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:17):

@Cyril Cohen The translation is a bit suboptimal for our purposes, that's why we need the postprocessing. We have been thinking to implement one which is more tailored, maybe it would be good to talk to you and Simon about this if we ever get to it?

view this post on Zulip Marcel Ullrich (Jul 05 2020 at 13:18):

@Samuel Gruetter Yes, this should works.

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:19):

@Michael Soegtrop Did we answer your question? I think the proof of a very similar induction principle might even be something like induction 1 using our_metacoq_principle; eauto (plus maybe some manual parts for the differences, but all the structural things should go away for free). And again this should be very similar with Enrico's Elpi plugin

view this post on Zulip Samuel Gruetter (Jul 05 2020 at 13:20):

Enrico Tassi said:

Samuel Gruetter said:

If I have an Inductive Prop that invokes itself under a disjunction, can you generate an IH for this?

It should work (both the metacoq plugin and the one in Elpi) since Or is just a container with 2 type parameters.

Cool! Does it also work if the recursive invocations are under a (forall a: A, exists b: B, recursive_invocation a b)?

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 13:21):

@Yannick Forster : I guess I have to try it. I frequently manually prove induction principles tailored to make my proofs easier to maintain / understand.

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:24):

@Samuel Gruetter in principle there is no reason why it shouldn't work I think. @Marcel Ullrich can you confirm that?

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:24):

@Michael Soegtrop if you have an example we're happy to test it for you, but we're also happy to help if you want to try yourself and get stuck

view this post on Zulip Enrico Tassi (Jul 05 2020 at 13:25):

@Samuel Gruetter Hum, at least in the elpi code the support for the dependent function space is very limited (IIRC it works for vectors, but not much more). The work by Kaposi and Kovács, that happens to follow the sames ideas, supports full CIC, but I did not try to go back and implement it fully (they wrote the paper independently).

view this post on Zulip Marcel Ullrich (Jul 05 2020 at 13:28):

@Yannick Forster @Samuel Gruetter
I am looking into it right now.
One problem is that the parametricity translation for exist or sigT fails.
In theory if one gets the registering right by hand, it should be possible.

view this post on Zulip Enrico Tassi (Jul 05 2020 at 13:30):

@Michael Soegtrop What the plugins give you is a more general induction principle that does not force you write nested fixpoints by hand. The plugins won't prove you own principle automatically, but as @Yannick Forster suggest, you should be able to use the generated principle "as is" and get the induction hypothesis you need.

view this post on Zulip Enrico Tassi (Jul 05 2020 at 13:32):

Marcel Ullrich said:

Yannick Forster Samuel Gruetter
I am looking into it right now.
One problem is that the parametricity translation for exist or sigT fails.
In theory if one gets the registering right by hand, it should be possible.

Unary parametricity is OK for full CIC, you probably discovered a little bug in your plugin that can be surely fixed.

view this post on Zulip Marcel Ullrich (Jul 05 2020 at 13:37):

The problem with the current parametricity implementation in MetaCoq is, that it runs into errors for more complex types like Acc. I think this is also the case here for sigT.

view this post on Zulip Enrico Tassi (Jul 05 2020 at 13:38):

Could be, I'm just saying that "the theory" tells us that the bug is fixable

view this post on Zulip Matthieu Sozeau (Jul 05 2020 at 13:39):

@Marcel Ullrich We certainly want to fix that. I suspect it's the nitty-gritty part of the inductive declarations that are bugguy in some way.

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:39):

But in principle our plugin supports this case? So we don't have a limitation w.r.t. nested dependent types @Marcel Ullrich?

view this post on Zulip Cyril Cohen (Jul 05 2020 at 13:39):

I have a very old pull request that tries to add the fix and cofix cases and fixes some bugs along the way. It was not finished and it is outdated... (I had a hard time keeping up with master)

view this post on Zulip Cyril Cohen (Jul 05 2020 at 13:39):

I could revive it with some help, let's set a meeting?

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 13:40):

@Yannick Forster @Enrico Tassi : a simple example:

forall (T : Type) (P : list T -> Type),  (forall (l1 l2 : list T), P l1 -> P l2 -> p l1 ++ l2) -> forall l : list T, P l

Typically what I have are largish inductive propositions specifying something and typically I want to do a similar transformation as above for lists - to go from the concrete structure of the inductive to something more problem oriented.

view this post on Zulip Matthieu Sozeau (Jul 05 2020 at 13:40):

However forall a, exists b, I a b is not strictly positive right? My bad, it is nested and positive

view this post on Zulip Marcel Ullrich (Jul 05 2020 at 13:40):

@Yannick Forster As far as I know and as I tested it, we support nested dependent types.

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:43):

As a general rule of thumb I would say that if the inductive type is definable in Coq we can generate a strong induction principle (modulo universe bugs in the implementation). It might depend on the I in your example whether the type is strictly positive @Matthieu Sozeau, no?

view this post on Zulip Matthieu Sozeau (Jul 05 2020 at 13:44):

Yes, I meant:

Inductive I : nat  -> nat -> Prop :=
| ci : (forall a, exists b, I a b) -> I 0 0.

which is fine

view this post on Zulip Matthieu Sozeau (Jul 05 2020 at 13:47):

Cyril Cohen said:

I could revive it with some help, let's set a meeting?

That would be nice, I wouldn't expect much changes in the terms, even the inductive declarations are pretty stable now (except for universe-related stuff which stilll moves a bit from version to version).

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:49):

The bug that's bothering us is connected to universes I think, but we can probably sort that our while sorting out other problems. I'll send you an email to set a meeting @Matthieu Sozeau @Cyril Cohen @Marcel Ullrich

view this post on Zulip Matthieu Sozeau (Jul 05 2020 at 13:51):

I've made a specific topic for that here: https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/Parametericity.20translation/near/202922515

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:51):

Ah even better, thanks!

view this post on Zulip Yannick Forster (Jul 05 2020 at 13:53):

@Michael Soegtrop interesting example, but my superficial impression is that the plugins do not help you in such a case. They improve the situation with nested inductive types, but since this is an alternative induction principle for lists (which is not a nested inductive type) I would guess that they can't be of any help

view this post on Zulip Enrico Tassi (Jul 05 2020 at 13:56):

I agree with @Yannick Forster . List alone is not where the derivation helps, it is when you use lists to define another type (like the rose tree mentioned in the talk).

view this post on Zulip Samuel Gruetter (Jul 05 2020 at 13:59):

Matthieu Sozeau said:

Yes, I meant:

Inductive I : nat  -> nat -> Prop :=
| ci : (forall a, exists b, I a b) -> I 0 0.

which is fine

That's the kind of example I'd be interested in, too

view this post on Zulip Yannick Forster (Jul 05 2020 at 14:03):

We're working on making the example work and will hopefully get back to you soon Samuel!

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 14:10):

@Yannick Forster : typically the inductive propositions I am talking about are nested. But also typically I do a similar transformation as for the lists, that is go from structural induction to a "subset of possible cases" type of induction. Typically the proofs of the principles require well founded induction (variants of induction_ltof1).


Last updated: Feb 06 2023 at 05:03 UTC