Stream: CUDW 2020

Topic: WG: Induction-induction


view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 09:14):

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

view this post on Zulip Kenji Maillard (Nov 30 2020 at 09:57):

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.

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 10:04):

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

view this post on Zulip Kenji Maillard (Nov 30 2020 at 10:13):

@Matthieu Sozeau should we occupy room 4 ?

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 10:18):

Yep let's go

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 11:30):

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

view this post on Zulip Bas Spitters (Jan 19 2021 at 18:38):

Question at CoqPL21: Is the set theoretic semantics of Coq+IndInd understood.
Some references here:
https://ncatlab.org/nlab/show/inductive-inductive+type

view this post on Zulip Bas Spitters (Jan 19 2021 at 18:39):

I know @Ali Caglayan is interested in this.

view this post on Zulip Ali Caglayan (Jan 20 2021 at 10:51):

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

view this post on Zulip Ali Caglayan (Jan 20 2021 at 10:51):

This reduction is detailed in Forsberg's thesis

view this post on Zulip Ali Caglayan (Jan 20 2021 at 10:52):

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

view this post on Zulip Ali Caglayan (Jan 20 2021 at 10:52):

At least I am not aware of any

view this post on Zulip Ali Caglayan (Jan 20 2021 at 10:53):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 10:55):

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.

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 10:55):

AFAIU, it's a clash of traditions

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 10:56):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 10:56):

because funext is usually taken for granted

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 10:56):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 10:57):

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

view this post on Zulip Kenji Maillard (Jan 20 2021 at 10:57):

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

view this post on Zulip Ali Caglayan (Jan 20 2021 at 10:58):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 10:59):

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

view this post on Zulip Ali Caglayan (Jan 20 2021 at 11:00):

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?

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 11:03):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 11:04):

Due to nested inductive types, you can do funny things

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 11:04):

Here is a minimal example

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

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 11:05):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 11:05):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 11:06):

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

view this post on Zulip Bas Spitters (Jan 20 2021 at 11:41):

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

view this post on Zulip Kenji Maillard (Jan 20 2021 at 11:42):

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

view this post on Zulip Kenji Maillard (Jan 20 2021 at 11:45):

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.

view this post on Zulip Ali Caglayan (Jan 20 2021 at 12:14):

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.

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 12:18):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 12:19):

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

view this post on Zulip Matthieu Sozeau (Jan 20 2021 at 12:23):

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

view this post on Zulip Ali Caglayan (Jan 20 2021 at 12:23):

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.

view this post on Zulip Ali Caglayan (Jan 20 2021 at 12:25):

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

view this post on Zulip Ali Caglayan (Jan 20 2021 at 12:25):

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

view this post on Zulip Ali Caglayan (Jan 20 2021 at 12:26):

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

view this post on Zulip Ali Caglayan (Jan 20 2021 at 12:26):

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

view this post on Zulip Kenji Maillard (Jan 20 2021 at 12:27):

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

view this post on Zulip Matthieu Sozeau (Jan 20 2021 at 12:29):

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.

view this post on Zulip Matthieu Sozeau (Jan 20 2021 at 12:29):

Also, otherwise guard-checking is not clear


Last updated: Oct 16 2021 at 07:02 UTC