This follows https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Induction.20induction

When do you plan to do this WG ? And what's the current status (design? implementation ?) ?

I think it would be really useful to have in general that indices of an inductive inductive definition are smaller than the witness of the predicate (like `t : P c`

is structurally bigger than `c`

) otherwise I stumbled on annoying issues where I had to be careful about normalizing some terms in my proof script so that the indices disappear before giving them to Coq through refine.

We could start now, given it will likely be just the two of us unless @Ali Caglayan joins at some point.

@Matthieu Sozeau should we occupy room 4 ?

Yep let's go

Plan: start a draft CEP and explain the current problems of representation of fixpoints.

Question at CoqPL21: Is the set theoretic semantics of Coq+IndInd understood.

Some references here:

https://ncatlab.org/nlab/show/inductive-inductive+type

I know @Ali Caglayan is interested in this.

IIRC if we stick to extensional type theory, so coq with axiom K we get a reduction of IndInd types to Indexed inductive types

This reduction is detailed in Forsberg's thesis

AFAIK we don't have such a reduction without axiom K

At least I am not aware of any

Since coq has indexed inductive types, it can probably be shown that Coq+IndInd=Coq in some suitable way

FTR, the qualification of MLTT + K as an "extensional type theory" is extremely confusing to me, and I am probably not the only one out there.

AFAIU, it's a clash of traditions

Categoricians call extensional anything that has (a strong form of) K

because funext is usually taken for granted

but in the type-theoretical world, Extensional Type Theory has a different meaning.

To add insult to injury, ETT does prove funext + K

Ali Caglayan said:

AFAIK we don't have such a reduction without axiom K

I think @Jasper Hugunin 's paper shows that the reduction of IndInd to Indexed inductives in Forsberg's thesis implies K

Yeah I can clarify, we don't have any equality reflection here,

(To continue my rant, the nlab page on extensionality is a marvel of confusion. Even as an expert in type theory I am very puzzled by what it states)

Kenji Maillard said:

Ali Caglayan said:

AFAIK we don't have such a reduction without axiom K

I think Jasper Hugunin 's paper shows that the reduction of IndInd to Indexed inductives in Forsberg's thesis implies K

Yeah, but AFAIK that's an issue with that specific reduction, not that it is impossible to do in general right?

Fun fact: I suspect that vanilla Coq has a tiny bit of Ind-Ind already built-in

Due to nested inductive types, you can do funny things

Here is a minimal example

```
Inductive T := t : forall x y : T, x = y -> T.
```

Here, the type T appears as a parameter of the equality proof, so we can get indices ranging over the type being defined

A beer to whomever proves that this *feature* is enough to encode IndInd

(Note: without nested inductive types this doesn't go through. I am not even sure of the interpretation of that inductive type in fancy models)

@Kenji Maillard Jasper's paper is about cubical type theory, isn't it?

@Ali Caglayan it would be interesting to detail that. I.e. that the set theoretical model of Coq already models IndInd. It's expected, but I don't think there is a theorem yet.

Bas Spitters said:

Kenji Maillard Jasper's paper is about cubical type theory, isn't it?

Ali Caglayan it would be interesting to detail that. I.e. that the set theoretical model of Coq already models IndInd. It's expected, but I don't think there is a theorem yet.

IIRC the first part is an analysis of IndInd outside cubical type theory

Pierre-Marie Pédrot said:

Here is a minimal example

`Inductive T := t : forall x y : T, x = y -> T.`

I got puzzled by that type but one constraint is that you cannot refer to constructors of the type being defined (at least I do not see how).

You can still define funny types, such as the following that collapses to Nat in presence of UIP/K, but looks non-trivial otherwise:

```
Inductive AlmostNat : Type := Z : AlmostNat | AlmostS : forall x : AlmostNat, x = x -> AlmostNat.
```

Bas Spitters said:

Ali Caglayan it would be interesting to detail that. I.e. that the set theoretical model of Coq already models IndInd. It's expected, but I don't think there is a theorem yet.

I am not super sure if it models IndInd, at least with definitional computation rules. I am not even sure it's expected to.

I'd be very surprised if the Set model wouldn't validate ind-ind

Set has extensional equality, so definitional and propositional equality coincide in that model

@Kenji Maillard it is still trivial though, although it looks funny:

```
From Equations Require Import Equations.
Inductive AlmostNat : Type := Z : AlmostNat | AlmostS : forall x : AlmostNat, x = x -> AlmostNat.
Derive NoConfusion for AlmostNat.
Derive Subterm for AlmostNat.
Derive EqDec for AlmostNat.
Require Import Equations.Prop.EqDec.
Instance almost_nat_dec x : EqDecPoint AlmostNat x.
Proof.
induction x.
intros y. destruct y.
left; reflexivity.
right; intros z; noconf z.
pose proof (eq_proofs_unicity_point e).
intros []. right; intros z; noconf z.
red in IHx. destruct (IHx x0). destruct e1.
destruct (H e0). left; reflexivity.
right; intros z; noconf z. now apply n.
Qed.
Instance almost_nat_uip : UIP AlmostNat :=
fun x y p => eq_proofs_unicity_point p.
Print Assumptions almost_nat_uip.
(* closed *)
```

Ah Ok, I got confused with terminology. I am pretty sure IndInd holds in the set theoretic model, however I am doubtful that the current syntax of coq can capture that.

One of the main issues is coq's current inability to handle "recursive-recursive" definitions.

This is when a mutual fixpoint can have later bodies be of types that are defined earlier in the fixpoint.

Currently, the type checking of mutual fixpoints can't see things being defined in the body

I know @Matthieu Sozeau had some ideas on how to fix this but I am unsure what is now known

@Matthieu Sozeau Thanks for the proof, I was half expecting that, but couldn't convince myself (and I didn't expect Equations to be able to prove that equality is decidable, that's what I was missing)

Yep. The big issue was that the current implementation allows "internal" unfolding of previous case branches in later ones *for the same inductive*, we should restrict it to only have the computational behavior of previous fixpoints available, not the current one, to make type-checking nicer.

Also, otherwise guard-checking is not clear

Last updated: Jun 11 2023 at 00:30 UTC