Matthieu Sozeau (Nov 30 2020 at 09:14): 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
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.
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.
Kenji Maillard (Nov 30 2020 at 10:13):@Matthieu Sozeau should we occupy room 4 ?
Matthieu Sozeau (Nov 30 2020 at 10:18):Yep let's go
Matthieu Sozeau (Nov 30 2020 at 11:30):Plan: start a draft CEP and explain the current problems of representation of fixpoints.
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
Bas Spitters (Jan 19 2021 at 18:39):I know @Ali Caglayan is interested in this.
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
Ali Caglayan (Jan 20 2021 at 10:51):This reduction is detailed in Forsberg's thesis
Ali Caglayan (Jan 20 2021 at 10:52):AFAIK we don't have such a reduction without axiom K
Ali Caglayan (Jan 20 2021 at 10:52):At least I am not aware of any
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
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.
Pierre-Marie Pédrot (Jan 20 2021 at 10:55):AFAIU, it's a clash of traditions
Pierre-Marie Pédrot (Jan 20 2021 at 10:56):Categoricians call extensional anything that has (a strong form of) K
Pierre-Marie Pédrot (Jan 20 2021 at 10:56):because funext is usually taken for granted
Pierre-Marie Pédrot (Jan 20 2021 at 10:56):but in the type-theoretical world, Extensional Type Theory has a different meaning.
Pierre-Marie Pédrot (Jan 20 2021 at 10:57):To add insult to injury, ETT does prove funext + K
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
Ali Caglayan (Jan 20 2021 at 10:58):Yeah I can clarify, we don't have any equality reflection here,
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)
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?
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
Pierre-Marie Pédrot (Jan 20 2021 at 11:04):Due to nested inductive types, you can do funny things
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.
Here, the type T appears as a parameter of the equality proof, so we can get indices ranging over the type being defined
Pierre-Marie Pédrot (Jan 20 2021 at 11:05):A beer to whomever proves that this feature is enough to encode IndInd
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)
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.
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
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.
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.
Pierre-Marie Pédrot (Jan 20 2021 at 12:18):I'd be very surprised if the Set model wouldn't validate ind-ind
Pierre-Marie Pédrot (Jan 20 2021 at 12:19):Set has extensional equality, so definitional and propositional equality coincide in that model
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 *)
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.
Ali Caglayan (Jan 20 2021 at 12:25):One of the main issues is coq's current inability to handle "recursive-recursive" definitions.
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.
Ali Caglayan (Jan 20 2021 at 12:26):Currently, the type checking of mutual fixpoints can't see things being defined in the body
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
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)
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.
Matthieu Sozeau (Jan 20 2021 at 12:29):Also, otherwise guard-checking is not clear
Last updated: Jun 11 2023 at 00:30 UTC