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

Bump

How does meta-coq compare with agda's reflection to build tactics.

https://github.com/alhassy/gentle-intro-to-reflection

Q: where is the source code?

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

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

Thanks @Yannick Forster that is also my impression.

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

here

Marcel Ullrich said:

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

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

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

The parametricity translation is in the MetaCoq repository

https://github.com/MetaCoq/metacoq/blob/coq-8.11/translations/param_original.v

@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

And Cyril Cohen :)

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

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

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

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.

@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?

@Samuel Gruetter Yes, this should works.

@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

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

?

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

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

@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

@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).

@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.

@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.

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.

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.

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

@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.

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

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)

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

@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.

~~However ~~ My bad, it is nested and positive`forall a, exists b, I a b`

is not strictly positive right?

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

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?

Yes, I meant:

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

which is fine

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

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

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

Ah even better, thanks!

@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

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

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

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

@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