Théo Zimmermann (Jun 24 2020 at 11:18): 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".
Enrico Tassi (Jul 05 2020 at 12:52):Bump
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
Cyril Cohen (Jul 05 2020 at 13:04):Q: where is the source code?
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?
Michael Soegtrop (Jul 05 2020 at 13:06):Q: Can I use it to prove induction principles I state?
Bas Spitters (Jul 05 2020 at 13:08):Thanks @Yannick Forster that is also my impression.
Marcel Ullrich (Jul 05 2020 at 13:08):https://github.com/uds-psl/metacoq-examples-coqws
here
Cyril Cohen (Jul 05 2020 at 13:10):Marcel Ullrich said:
I am looking for the parametricity translation, can you point me to the corresponding piece of code?
Michael Soegtrop (Jul 05 2020 at 13:10):Similar as you showed, but I want to control it.
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).
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
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
Matthieu Sozeau (Jul 05 2020 at 13:13):And Cyril Cohen :)
Enrico Tassi (Jul 05 2020 at 13:13):Cyril, are you looking for your own code :grinning_face_with_smiling_eyes: ?
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?
Cyril Cohen (Jul 05 2020 at 13:14):Oh I thought there was yet another implementation... ok then I know of this one ;)
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.
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?
Marcel Ullrich (Jul 05 2020 at 13:18):@Samuel Gruetter Yes, this should works.
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
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
Oris 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)?
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.
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?
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
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).
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.
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.
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.
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.
Enrico Tassi (Jul 05 2020 at 13:38):Could be, I'm just saying that "the theory" tells us that the bug is fixable
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.
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?
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)
Cyril Cohen (Jul 05 2020 at 13:39):I could revive it with some help, let's set a meeting?
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.
Matthieu Sozeau (Jul 05 2020 at 13:40):However My bad, it is nested and positiveforall a, exists b, I a b is not strictly positive right?
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.
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?
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
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).
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
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
Yannick Forster (Jul 05 2020 at 13:51):Ah even better, thanks!
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
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).
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
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!
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: May 31 2023 at 02:31 UTC