I am reading the paper: Decidability of Conversion for Type Theory in Type Theory

and they mention they require somegthing called "induction-recursion"

and then there is this gist https://gist.github.com/jcmckeown/07d844a9724745cedd61 which implies that this feature is not in coq, and based on the explanation, it sounds like mutual inductive types, can someone help me get un-lost in this area ?

"Feature request: induction-recursion" https://github.com/coq/coq/issues/4259

so it is not there, but what are alternative options/workarounds ? (given that I don't even know what induction-recursion is to start with)

Not sure on the alternative (other than "use dependent types less"), but it *is* a form of mutual recursion: it just involves datatypes (inductive) and functions (recursive).

Induction-recursion is a scheme to define inductively a type mutually with a function on this type given recursively. The typical example of an Inductive-recursive type is that of a universe of code `U : Type`

together with a decoding function `El : U -> Type`

. In pseudo Coq code for instance you might hope to be able to write (if Coq supported induction-recursion which it does not)

```
Inductive U : Type :=
| codeBool : U
| codePi : forall (domain : U) (codomain : El domain -> U), U
with El (A : U) : Type :=
match A with
| codeBool => Bool
| codePi A B => forall (a : El A), El (B a).
```

Note that `El`

is required in the constructor `codePi`

and conversely the two constructors of `U`

are required to be able to define `El`

Thanks Kanji, that's a nicer explanation...

For references, I guess one of the original point to go is Induction recursion and initial algebras, and the phd thesis of Fredrik Nordvall Forsberg

IIRC a common use case is that the indexes of your inductive mention the recursive function, and sometimes that can disappear with less precise types; for instance, switching from intrinsically typed terms (Exp T) back to intrinsically typed (Exp). OTOH, for the paper you mention it would probably be a major change. I'm not sure how well what they do would even work.

And then there are encodings of some form of induction recursion in Coq, usually by first passing through an inductive-inductive definition where you replace the function `El`

by its graph `ElGraph : U -> Type -> Type`

and then using an encoding of induction-induction such as that one (For finitary induction-induction, induction is enough ) (Edit: That encoding probably does not work for the case of a universe of codes, but there is another one presented in partial univalence in n-truncated type theory that I use quite often)

For the paper you mention, Loic Pujet managed to do an encoding using only indexed inductive types in Agda last year, and a few people are trying to port this encoding to Coq but it is largely a work in progress

I'm sorry, but the link on "that one" isn't working for me... Could somebody please post the URL?

thanks for the clarifications from everyone

Before we can support induction-induction or induction-recursion, we need to generalize fix points so that the types of later clauses can depend on the bodies of previous clauses. This has been called "recursion-recursion" by some. @Matthieu Sozeau had a ind-rec patch which we diluted to a rec-rec patch at some point, but there is a lot going on so we never made progress on it.

The general idea of the patch is to replace List.map in the fixpoint datastructure with List.foldl or something. Once we have rec-rec then implementing ind-ind or ind-rec will become clearer, and will essentially require internalising the codes for such definitions. ind-rec at least has a clear compilation but ind-ind always has some extra incompatability which needs thinking about. (Basically ind-ind also changes the proof strength of Coq only in the absense of axiom K.

Agda has had both for a while, so maybe the main issue is lack of developer time and attention.

@Ali Caglayan May I ask how hard is that (given my non-existant knowledge of ocaml), maybe you have estimation of how long it will take working full time on it (1 month, one year)?

If I am ever going to work on this feature, my goal will not just have a POC but instead have it upstream so the time to upstream is what I am mostly interested in ?

I mean the feature was already basically implemented by @Matthieu Sozeau. Most of the work is rebasing on top of a newer Coq, trying to understand how the PR was meant to work and trying to understand how Coq works. Once you get something that runs, then you spend time fixing the test-suite and any developments in the CI.

Technically, it shouldn't take a long time to do. But it ultimately requires a few weeks total of dev time from a few devs which isn't something I think is available at the moment.

Depending on your situation that you need it for, there are ways to encode the types you need directly in Coq today.

Most ind-ind types for instance can be done as a mutual inductive type together with extra checks. Think syntax of type theory with an IsWellTyped predicate. For induction recurison the situation is similar also, as long as you aren't doing something crazy like adding a universe of types.

Noted, I will have to first understand the paper I am trying to implement thoroughly and then see what is the best approach.

To be honest,I am still fairly noob

hopefully I will get back with a plan on Monday

thanks a lot for the insights

There is a dev working group coming up soon, I'll make a note to ask if we might spend some time getting RR, II and IR in Coq.

Also note that there are two levels of "having a feature in Coq": one is having it added to the kernel, another is to have all the upper layers know about it and be able to use it properly. Having a feature in the kernel is already nice because you can experiment with it, but if it is not well integrated in the upper layers, you quickly get into trouble if you want to use it in a "real" development… AFAICT this is for instance the current status of `SProp`

: it is in the kernel, but close to nobody uses it yet, because it has poor interaction with eg tactics

isn't there going to be a rule or recommendation to formalize stuff like induction-induction and induction-recursion and recursion-recursion in MetaCoq first, and then get it into the ML kernel?

(Depending on the kernel feature, it might take a while before the upper layers handle it properly. See e.g. universe polymorphism / primitive projections, introduced in 2014 and which is still quirky)

I think there is already some rule/recommendation about peer-reviewed paper, but peer reviewing is a bit more hit and miss

@Karl Palmskog While it'd be very nice to have it in MetaCoq before having it in the kernel (which may actually happen) I think that the current difficulties are more about design trade-offs than foundational issues.

well I am not sure if I will be able to work on that direction for the time being

Last updated: Jun 14 2024 at 20:01 UTC