Can I add a topic "Nested inductive scheme"? It should be a plugin rather than Coq itself. MetaCoq already has such a generator. But I talked with them and find the generator is not updated to the latest Coq.

@Qinshi Wang Absolutely, we can discuss it in one of the hacking sessions (morning/evening CET) if you like

@Qinshi Wang On the topic of nested inductive scheme, you might want to have a look at what's been done relatively recently in Coq-elpi (see this paper)

We want to automatically generate induction schemes for data types with nested inductive types, e.g.

Inductive tree A :=

| leaf : A -> tree A

| node : A -> list (tree A) -> tree A.

We are writing some large induction schemes in our project and so does @TJ Barclay 's group. It seems the MetaCoq template https://github.com/MetaCoq/metacoq/tree/master/template-coq handles it. But while MetaCoq is updated to the latest Coq version, this functionality is not updated.

@Kenji Maillard Thanks. Yes, I know it.

Are you interested in updating the MetaCoq plugin to more recent MetaCoq versions? :)

@Yannick Forster Sure. Hopefully I can get some help about MetaCoq.

I will gladly help :) @Matthieu Sozeau (for general MetaCoq things) and @Marcel Ullrich (for the plugin) are usually also very eager yo help

@Yannick Forster As I said in the email, I can compile MetaCoq on Coq 8.13, but not the induction scheme generator.

Yes, I guess that's because the induction scheme generator was implemented on a different version of MetaCoq branch 8.13

https://github.com/uds-psl/metacoq_plugins

This explains which MetaCoq version is assumed

commit 7281139

which is even a commit on the `8.12`

branch it seems

So the natural way to progress would be to install MetaCoq from the tip of the 8.13 branch, compile the plugin there, which will lead to an error message (as you have already noticed :) )

Hopefully the error message is parseable enough s.t. you have an idea where to compare commit 7281139 with the tip of `coq-8.13`

to see what change is necessary

@Kenji Maillard Thanks. Yes, I know it.

It is a bit off topic, but @Qinshi Wang are there reasons why you can't use Coq-Elpi? Is there a Coq-Elpi limitation hitting you? Thanks

As described in the MetaCoq induction paper (https://arxiv.org/abs/2006.15135), it's said Coq-Elpi generates equality function rather than induction scheme. Another problem is not supporting mutually inductive type.

Coq-Elpi generates the induction scheme as well, since it is needed in order to prove that the equality tests are correct.

It is true that it does not handle mutual inductive types, this is a hard limitation that won't be lifted anytime soon... so MetaCoq seems the right choice right now if you need these.

Sorry if the abstract was unclear :) Indeed Enrico's plugin also generates induction schemes, the same way we do using the MetaCoq implementation. (I don't recall 100%, but maybe we even took the idea from Enrico? That should be traceable from Marcel's Bachelor's thesis)

We do use mutual inductive types in our development.

I would expect that lifting to mutual inductives would not be very hard, but as always also not trivial

I think that lifting the algorithm should work. But Coq-Elpi's HOAS of Coq terms does not cover mutual inductive/fixpoints, so you can't really write the extended algorithm in Coq-Elpi :-/

What's the problem with mutuals?

Actually what I'm thinking of (which is also how our hand-written inductive schemes look like now) does not include generating a Forall-like relation.

Nothing special, it is just that I never coded it (it seems that the usefulness/work-needed ratio is not stellar to me, but I may be wrong). @Qinshi Wang can you share some of these types? I always had the impression that many mutual types were written like that because Coq did generate bad induction for the non nested variant (e.g. I've seen the type of lists being made mutual for that reason many times).

Are we talking about mutuals in general or nested inductive mutuals?

Mutual inductive types that use list and so on in their declaration.

@Ali Caglayan I was talking about writing `Inductive rose := Node (l : list rose) | Leaf`

as `Inductive rose := Node (l : my_list) | Leaf with Inductive my_list := MyNil | MyCons (x : rose) (xs : my_list)`

@Enrico Tassi

Inductive ExpressionPreT :=

| ExpBool (b: bool)

...

with Expression :=

| MkExpression (tags: tags_t) (expr: ExpressionPreT) (typ: @P4Type tags_t) (dir: direction).

We use mutual induction to add on additional information. It's unnecessary but makes things easier.

Right, coq doesn't do the "correct" scheme unless its mutual.

Does `ExpressionPreT`

actually mention `Expression`

?

@Enrico Tassi Certainly.

Enrico Tassi said:

I think that lifting the algorithm should work. But Coq-Elpi's HOAS of Coq terms does not cover mutual inductive/fixpoints, so you can't really write the extended algorithm in Coq-Elpi :-/

What I meant is that adapting the MetaCoq plugin implementing the same algorithm would not be very hard

OK, then it is a real mutual, I suggest to follow @Yannick Forster suggestion

I would be interested in discussing whether induction principles with `Forall`

are preferable or not

I think that's orthogonal to supporting mutual inductive types, right? Already the induction principle for `tree`

as above could be written with either a predicate `P`

and using `Forall P`

or with predicates `P : tree -> Prop`

, `P' : list (tree) -> Prop`

@Yannick Forster I did have thought about it. It seems it's indeed the strongest, but maybe not ideal for computation when we are using for recursive function rather than inductive proof.

Are you saying the `Forall`

variant is stronger or the "mutual in spirit" variant?

the strongest variant is using the inductive parametricity predicate, which is a generalization of Forall

Sorry. It seems I misunderstood. You are talking about the existing Forall versus the generated one?

@Pierre-Marie Pédrot I'm not sure about what you mean.

Forall is just the unary parametricity predicate, and the induction principle for nested inductive types is literally the statement of the parametricity lemma

that is, you define the inductive `listε : forall A (P : A -> Type), list A -> Type`

with `nilε : listε A P nil`

and `consε : forall (x : A) (xε : P x) (l : list A) (lε : listε A P l), listε A P (cons x l)`

indeed

with the predicates inlined, I see a major problem which is that the `induction`

tactic must be clever

say you have e.g. P : tree -> Type and Q : list tree -> Type

then induction must invent Q before hand with this variant

I think problems with `induction`

are orthogonal, they would appear already in the hand-written code they currently have, no?

no, it's a design issue that would bubble up

if you pick the predicate lifter variant you don't have to invent a predicate Q so it's easier to use in practice

Are you suggesting a third variant?

There is the unary parametricity variant we have. And there is the variant with two predicates @Qinshi Wang is currently using. Isn't the second what you suggest Pierre-Marie?

no, no, I'm advocating for unary parametricity rather than inlined predicates

(I call inlined predicates the two-predicate variants)

Yes, but are there 3 options on the table and you're advocating for option 1? Or are there 2 and you are advocating for option 1?

there are at least 2, and I am advocating for the first one

I think @Qinshi Wang is already using the other option, so I'd guess that `induction`

already becomes hard to use / unusable

Just from daily experience, I'd also have guessed that the unary parametricity version is always sufficient

it's literally the universal principle, so it's hard to make it any stronger

Pierre-Marie Pédrot said:

that is, you define the inductive

`listε : forall A (P : A -> Type), list A -> Type`

with`nilε : listε A P nil`

and`consε : forall (x : A) (xε : P x) (l : list A) (lε : listε A P l), listε A P (cons x l)`

Is this just different from Forall by Prop versus Type?

I'd also have guessed that the unary parametricity version is always more convenient to use

@Qinshi Wang unfortunately you need all variants for each sort elimination is allowed into

(I think)

I think we cover that already, but even if not that would be a relatively trivial extension

@Qinshi Wang can you explain why you prefer the two predicate version of induction principles in your code?

@Enrico Tassi

I always had the impression that many mutual types were written like that because Coq did generate bad induction for the non nested variant (e.g. I've seen the type of lists being made mutual for that reason many times).

[BedRock hat off] [Scala / DOT hat on] but that leaves out any grammar that's genuinely mutually recursive...

(there's probably mutual inductives in C++ too, but this isn't something that I've run into at the present job)

Mutual inductive types are encodable away with standard indexed inductive types, but AFAIK that's not the case for nested inductive types.

if you're really desperate you can thus get the right principle by bending a bit the definition

but that sounds like encoding something that works with something that doesn't :sweat_smile:

(or "is not well supported")

Pierre-Marie Pédrot said:

Qinshi Wang unfortunately you need all variants for each sort elimination is allowed into

Can we define

Definition list_ind A (P : list A -> Prop) := list_rect P.

Qinshi Wang said:

Pierre-Marie Pédrot said:

Qinshi Wang unfortunately you need all variants for each sort elimination is allowed into

Can we define

Definition list_ind A (P : list A -> Prop) := list_rect P.

This is currently what I do by hand for my nested inductive types

Yannick Forster said:

Qinshi Wang can you explain why you prefer the two predicate version of induction principles in your code?

Because it's easy to write, I guess?

Oh, I guess actually, it's much nicer when handling monads.

I'm not sure that in the case of nested inductive types, relying on the Prop ⊆ Type cumulativity gives rise to an equivalent principle, actually

For example, we want (Q : list A -> Type) to be (m (list A)) instead of (list (m A)).

I don't mean we have carefully justified this design decision. It just happens to be what we're doing.

Yannick Forster said:

Are you saying the

`Forall`

variant is stronger or the "mutual in spirit" variant?

I just understood what you mean by "mutual in spirit". The "mutual in spirit" version easily implies the `Forall`

version by putting `Forall`

as `Q`

in it. But for inductive proofs, it seems the `Forall`

version always works because the strongest induction hypothesis for list A is (Forall P), where P is the induction hypothesis for a single point. So they should be equivalent for the Prop case.

And they are not equivalent for the `Type`

case?

I would be surprised if they are not

For me, the unary parametricity version is easier to write

I didn't expect a fleshed-out answer :) But I guess before spending time on writing a plugin generating induction principles it makes sense to understand how the best induction principles look

Yannick Forster said:

And they are not equivalent for the

`Type`

case?

I think they are not, considering the computation process.

I have written another version of the induction principles:

https://github.com/NeuralCoder3/nested_induction_v2

This code is for MetaCoq 8.13, and thus, very similar to the newest version.

It is also more in line with the previous work of Enrico Tassi in Elpi and the

examples from Qinshi.

But is not fully working right now as the 'functorial' lemmas are missing.

@Qinshi It is true that your scheme does not use an explicit Forall construct but I feel like

that the "PAList : list (tree1 A) -> Type" in one of your examples for rose trees

has the same or less functionality as a Forall but needs to be user-provided.

Please correct me if I am wrong.

in such a simple case as rose trees they're equivalent, but there are weird cases permitted with nested inductive types

As I said, for proof/definition purposes, `Forall`

is the strongest. But for computation purposes, either extraction or proof by computation, we might want to skip some recursive calls?

You can always thunk the subcalls, picking P' := unit -> P.

I don't think it's a good idea anyways to use induction principles when writing programs

they're tailored for cbn

I have convinced myself that you can implement the two predicate version using the parametricity version in the case for rose trees

The proof is straightforward

/ the implementation is straightforward

yeah, it's basically the iso (forall s : A + B, P s) ~ (forall x : A, P (L x)) × (forall y : B, P (R y))

that's a definitional iso

My feeling would be that a "good" plugin would generate the parametricity version, and then there could be a second phase deriving the two predicate version from it

I always have the fancy counter-example `Inductive t := T : forall x y : t, x = y -> t`

if you want an example of a weird nested type.

I never really thought about the 2-predicate inductive principle for that one.

(note the equality between two terms of the type being defined)

more generally, nesting indices is likely a minefield

(add another constructor so it's not empty)

I don't care about inhabitation of my types, the very fact they type-check is suspicious

if you try to translate to mutual inductives I guess you get an inductive-inductive

```
Inductive t := T : forall x y, T_eq x y -> t
with T_eq (a:t) : t -> Prop := T_eq_refl : T_eq a a.
```

indeed, this is one of the reason I suspect we can already get a bit of induction / induction in the current Coq kernel (or maybe prove UIP who knows)

isn't the 2-predicate variant not writable? I think that the second predicate should not be universally quantified over the equality parameter, but you must put something there and I don't see what it might be

what?

give me the intended type of the 2-predicate recursor

something like

```
Fixpoint t_rect (P:T -> Type) (Q:forall x y, P x -> P y -> T_eq x y -> Type) (fT : forall x px y py e, Q x y px py e -> P (T x y e)) : forall t, P t
with T_eq_rect ... : forall x y e, Q x y (t_rect ... x) (t_rect ... y) e
```

(if I remember how the fully general ind-ind recursors work)

hm, I am realizing I don't even know how to implement the parametricity-based induction principle for that one.

I mean I can inhabit the type but I'm not sure it has the right computational behaviour

Can you even have two principles with different behaviour?

Pierre-Marie Pédrot said:

I don't think it's a good idea anyways to use induction principles when writing programs

Sometimes recursive functions do not pass Coq's structural check and we need to use an induction scheme.

That doesn't sound plausible if the function is hand-written: inlining the induction scheme will give you a scheme-free function.

Sorry: it's not plausible that you have to call the principle. It is true that the right way to do the recursion might be surprising with nested types.

You'll need to write some nested fixpoints; I think it's covered in CPDT

One of the points solved by the unary parametricity is that fixpoints do pass the termination check, even when composed

Can you even have two principles with different behaviour?

@Yannick Forster I'm pretty sure that due to intensionality there are infinitely many variants of a given recursor. For instance, for natural numbers you could define a variant where you do a η-expansion through pattern-matching in the recursive case

in general recursors are underspecified, you only care about the situation when they're fully applied to a constructor.

But extensionally there should be just one function with the type of the recursor of natural numbers, no?

yes, but extensionality is but an illusion

the "weird nested type" above is slightly more problematic because I am not even sure of the expected computational behaviour of the recursor, and the one I managed to write is not enjoying the one I would have liked to see.

? is Coq guard not strong enough? Am I not skilled enough in dependent-elimination-fu? So many foundational mysteries.

On a practical note, seizing the opportunity of parametricity experts being gathered here, with the accumulated knowledge and available implementations, isn't it the right time to deprecate the current system for generating induction schemes in Coq and replace it with a compositional parametricity-based system (supporting nested schemes and schemes for arbitrary abbreviations of type)? This was suggested by @ppedrot in a previous discussion I think.

I think it would be great to have more support for this, yes. What I am unclear about is what the right level of implementation for this is. Should these kinds of features be shipped by Coq natively? That would mean they are implemented in OCaml. Maybe such a feature should be an independent plugin, which is however part of the Coq platform? That would give more flexibility with regard to the implementation and any plugin system part of the Coq platform (Ltac2, Coq-Elpi, MetaCoq) could be used

nothing stops us from shipping stuff written in ltac2 with coq

We can swap Ltac2 and Mtac from the list then

I'm a supporter of writing it in OCaml as a program translation (i.e. no tactics, just building terms)

this would give us the more robust implementation

Are you a supporter of *you* writing OCaml program translations, or *anybody*?

anybody, but I can do it if I find a bit of time

Ltac2 doesn't provide any advantage over OCaml for this kind of stuff

and we're sure to have access to all the lowest-level horrors of inductive types and whatnot.

Maybe my point is a bit orthogonal to actual induction principles. Surely it would be good to have more support for nested X (X being induction, subterm relations, equality deciders, etc) already now in OCaml

But is that the right way to go on the long run?

I believe that for thing so critical as induction schemes, yes

look at the amount of trouble when an autogenerated name changes

My feeling always was that the OCaml part of Coq is even more opaque to newcomers than things like MetaCoq - which is a strong statement, because MetaCoq is very opaque

we can strive to make the translation easy to read (it's not currently)

Since we're recapping the previous discussion, long-term deleting as much OCaml code as possible would be desirable (this might be an exception but I'm not so convinced).

and a reason is exactly "I can do it if I find a bit of time" — the Coq core team cannot scale to all the needed metaprogramming, customizations, etc.

If other tools have limitations that hinder doing this task properly, I'd personally vote for the core team to improve those tools.

I'm fine with people developing their libraries outside but mark my words, autogenerating this kind of subtle code is bound to create backwards compat issues and horrendous eisenbugs

the less impedance, the better

I agree with everything Paolo said, including the ambiguity about the point whether this should be an exception

If other tools have limitations that hinder doing this task properly, I'd personally vote for the core team to improve those tools.

I don't think we can say that there is no work involved in the MetaCoq, coq-elpi, and Ltac2 tools. What should be done more?

Here are different implementations I know to build the parametricity translation:

The one in coq-elpi is particularly compact. If we remove from paramcoq all the debug code and the costly treatment of fixpoints which coq-elpi actually improved (using match-expansion rather than generating obligations), I'm pretty sure it reduces to less than 250 lines. Then, it is a question of taste of which language we prefer I guess, even if I agree with @Pierre-Marie Pédrot that relying directly on the internal structures of Coq gives full control over all the tiny details.

This does not mean that functions written in coq-elpi or MetaCoq, or other plugins should not be able to register features usable from Coq (e.g. in tactics). For instance, that would be very useful if `induction`

/`elim`

could automatically take benefit of a scheme written in coq-elpi, MetaCoq or paramcoq. We need for that to make the system of Scheme indeed more flexible and open to extensions by plugins.

I haven't used elpi, but I've seen multiple colleagues pick it up very quickly :-)

I wonder if elpi could also offer the low-level control (as needed) without rewriting the code to another tool, but I don't have an informed opinion on the specifics.

For instance, that would be very useful if induction/elim could automatically take benefit of a scheme written in coq-elpi, MetaCoq or paramcoq.

tactics in Iris Proof Mode (/MoSeL) are extensible via typeclass instances, even if this case seems more challenging (and mixing TCs and CSes will be hard unless unifall lands)

Tactics like `reflexivity`

are extensible by means of type classes. Would this be possible for the dependency in induction schemes (sorry for a naive question but my culture in TC is low)?

Yes, but TC is a sledgehammer for this kind of pin.

When you only want a table, it seems to me that bringing in the kind of sheer horror of proof search that TC provides is really counter-indicated.

It's not ideal indeed. Equations uses TCs to lookup induction principle but it's a pretty blind search, I think you might want an explicitely structured table (do you want the dependent or non dependent eliminator, into which sort etc...)

it seems like we want Register to take a list of strings and refs as keys

```
Register foo_ind as "induction.prop" foo.
```

Paolo Giarrusso said:

I wonder if elpi could also offer the low-level control (as needed) without rewriting the code to another tool, but I don't have an informed opinion on the specifics.

If I knew which kind of control @Pierre-Marie Pédrot is talking about, I would try to answer. IMO it is more about habit, we core devs are all very fluent bin OCaml, not equally fluent in the others languages.

(As a parenthesis, I don't think we should be afraid of writing code in OCaml, whose name precisely derives from being the MetaLanguage of LCF. Isabelle also uses ML as meta-language. The APIs of Coq are probably a bit frightening, because some complexity has been accumulated - and cleanups are necessary -, but such complexity would arise also in MetaCoq, and coq-elpi, as they continue to grow.)

such complexity would arise also in MetaCoq, and coq-elpi, as they continue to grow.)

The main requirement is that this doesn't happen. It'd be good if coq-elpi _allowed_ lower-level control _if needed_...

One of the good points of extension languages is that you can raise the abstraction barriers, and hence simplify the API.

For example declaring an inductive type in OCaml is a horror, just think at the context that you have to provide in which you have to put the parameters but also an entry for the inductive type itself... in Elpi you use a HOAS data type which is much simpler. So you give up some control, and maybe some speed, but the barrier to entry is much lower.

In the same way when you code in Ltac2 (or Elpi) you don't thread sigma (with evars and universe constraints), since the runtime carries them for you. In OCaml you have a monad, which is not a pleasure to work with since the type parameter is `unit`

(for some reasons) so hello CPS...

Moreover, the APIs of all the extension languages we have mentioned here is a fresh start, we have some hope we do a better job than what "history" did in Coq.

In OCaml you have a monad, which is not a pleasure to work with since the type parameter is unit

??

The tactic monad

unit?

Goal.enter

the reason isn't a mystery, it's because you can have multiple or 0 goals

we can add `fold_enter : (goal -> 'a -> 'a tactic) -> 'a -> 'a tactic`

if you want

I know, but as soon as you need the proof context (the goal) you have 2 choices: write all your code outside the monad, or go CPS

no, you can also fail on non-focussed goals

no to what?

no to two choices

there are at least three

and also, proof search != term translation

how are non focussed goals relevant?

I mean that if you have several goals under focus

I was talking about two "coding styles" to split your code into functions. If you write your bricks outside the monad, well, you lose the state carrying/hiding benefit; if you write them in the monad, most combinators make your bind operator void. IMO using the monad type parameter to separate mono-goal-and-context code and multi-goal-not-same-context code was a mistake, since you have the illusion you can share combinators but you actually can't; better to have two types for tactics (with two monads if you like monads).

Last updated: Jan 29 2023 at 15:02 UTC