Stream: Coq devs & plugin devs

Topic: Induction induction


view this post on Zulip Matthieu Sozeau (Jun 05 2020 at 21:09):

@Hugo Herbelin @Ali Caglayan I guess we can start discussing here what needs to be done to get recursive-recursive definitions in Coq, along with inductive-inductive types.

view this post on Zulip Ali Caglayan (Jun 05 2020 at 21:18):

Do you know of any literature on recursive-recursive definitions? All I can find are mentions in papers on inductive-inductive types. I am vaguely aware that Agda is able to define things recursive-recursively but I am unsure if anybody has written about this.

view this post on Zulip Ali Caglayan (Jun 05 2020 at 21:39):

In the test-suite in IIind.v you have written Local Inductive but my coq is throwing an error saying that this command does not support this attribute.

view this post on Zulip Ali Caglayan (Jun 05 2020 at 22:05):

I'll have a more detailed look tomorrow. But here is a sorted list II type:

Require Import Coq.Structures.Orders.

(** Sorted lists *)

Module SortedLists (A : OrderedType).

  Include A.

  Inductive SList : Type :=
  | slist_nil  : SList
  | slist_cons : forall (x : t) (ys : SList), slist_lt x ys -> SList
  with slist_lt : t -> SList -> Type :=
  | slist_lt_triv (x : t) : slist_lt x slist_nil
  | slist_lt_cons (x' x : t) (ys : SList) (p : slist_lt x ys)
    : lt x' x -> slist_lt x' ys -> slist_lt x' (slist_cons x ys p)
  .

  Print SList_ind.

End SortedLists.

As I understand it, once we implement recursion-recursion coq will be able to generate the elimination principle of the thing above.

view this post on Zulip Gaëtan Gilbert (Jun 05 2020 at 22:20):

Why Include?

view this post on Zulip Karl Palmskog (Jun 05 2020 at 22:37):

I think you might want instead of the Include:

Module SortedLists (Import A : OrderedType).

(if the goal is to access the stuff in A without qualification)

view this post on Zulip Bas Spitters (Jun 06 2020 at 07:29):

Induction-induction and induction-recursion are well studied. I don't recall having seem recusion-recursion. Is there a paper describing it? Induction-recursion increases the proof theoretic strength. How about recursion-recursion?

view this post on Zulip Bas Spitters (Jun 06 2020 at 07:32):

The sorted list you describe seems to be a variant of non-empty list, a standard example of induction-recursion

view this post on Zulip Matthieu Sozeau (Jun 06 2020 at 11:58):

recursion-recursion is just the idea that mutually recursive definition can have their types depend on each other, and maybe more importantly, the type-correctness of their bodies to depend on the computational content of previous definitions. Typically this is necessary to implement the dependent eliminators of inductive-inductive types. It should also allow to write a mutual [f : nat -> Type with g : forall (n : nat), f n -> B], and indeed I don't think I've ever seen a specific study of these kind of dependent fixpoints written anywhere. My impression is that this does not increase the proof theoretic strength of the system (contrary to induction recursion), as such functions could probably be encoded as [f : nat -> {X : Type & B}]. My proposed PR does implement rec-rec fixpoints to be able to derive the induction principles of ind-ind definitions, I just did not update the automatic scheme declarations yet.

view this post on Zulip Matthieu Sozeau (Jun 06 2020 at 11:59):

Bas Spitters said:

The sorted list you describe seems to be a variant of non-empty list, a standard example of induction-recursion

I imagine a simple inductive definition would do for non-empty lists, what did you have in mind?

view this post on Zulip Matthieu Sozeau (Jun 06 2020 at 12:05):

Ali Caglayan said:

In the test-suite in IIind.v you have written Local Inductive but my coq is throwing an error saying that this command does not support this attribute.

Yep they were old test-suite files, I fixed all that. Now the test-suite only fails because of the checker and one weird bug with alpha-renaming of mutual fixpoints in Ltac I have to investigate.

view this post on Zulip Bas Spitters (Jun 06 2020 at 12:29):

@Matthieu Sozeau I was thinking of fresh lists, not non-empty lists...
The sorted lists are treated in Fredrik's thesis(https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/thesis/thesis.pdf), but I guess you knew that.

view this post on Zulip Jakob Botsch Nielsen (Jun 06 2020 at 12:42):

What branch has experimental support for this? I had a use case where recursion-recursion would have simplified things greatly too.

view this post on Zulip Bas Spitters (Jun 06 2020 at 12:55):

Could be https://github.com/mattam82/coq/commits/IR_fix or https://github.com/mattam82/coq/commits/IR, but I guess it's this:
https://github.com/mattam82/coq/tree/inductive-inductive-types

view this post on Zulip Ali Caglayan (Jun 06 2020 at 12:57):

@Jakob Botsch Nielsen It's the latter one that @Bas Spitters linked.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:03):

@Bas Spitters The recursion-recursion we are talking about essentially states that mutual fixpoints can have the type of later with statements depend on fixpoints that occur earlier in the mutual fixpoint.

view this post on Zulip Bas Spitters (Jun 06 2020 at 13:05):

Are they powerful enough to define the usual inductive-recursive universes, or are they more like small IR definitions?

view this post on Zulip Jakob Botsch Nielsen (Jun 06 2020 at 13:05):

Cool! I will try an earlier example I did with it. I needed it when I was formalizing the interpretation of DPTT into CWF's, but it seems like Matthieu already has a pretty similar example in that branch.

view this post on Zulip Jakob Botsch Nielsen (Jun 06 2020 at 13:08):

Also, I believe @Danil Annenkov needed recursion-recursion too when trying to define semi-simplicial types in Coq.

view this post on Zulip Bas Spitters (Jun 06 2020 at 13:09):

That won't be enough for semi-simplicial types, as we still don;t know how to do it in agda...

view this post on Zulip Bas Spitters (Jun 06 2020 at 13:09):

@Ali Caglayan Is the scheme you are looking at available in agda?

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:10):

Yes Agda supports these definitions. They aren't anything fancy like induction-induction or induction-recursion

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:10):

For example when you define odd and even for nat you can use a mutual fixpoint. But if you don't have mutual fixpoints you can define a function oddeven that does both at the same time into a product.

view this post on Zulip Jakob Botsch Nielsen (Jun 06 2020 at 13:11):

I don't remember exactly what he was trying to do, but it was porting some Agda example to Coq which I think required recursion-recursion.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:11):

So these "recursive-recursive" fixpoints ought to be combined together into some sigma type.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:12):

We can already do this in coq, but it requires have to write these mutual recursive-recursive definitions bundled up together which is inconvenient.

view this post on Zulip Bas Spitters (Jun 06 2020 at 13:14):

Why do you say they are less powerful than induction induction? The example you give is a standard one from Frederiks thesis...

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:17):

For example,

Check (fix A (n : nat) : Type := _
with B (n : nat) : A n -> Type := _
for A : nat -> Type).

currently gets rejected. But is accepted in the in the inductive-inductive-types branch.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:18):

@Bas Spitters I'm just trying to emphasize that it is not a "new feature", but rather a way of writing something we currently can do more conveniently.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:22):

In currently coq we can do my above example as:

Check (fix AB (n : nat) : {A : Type & A -> Type} := _).

and project out of it.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:23):

The point of all of this is that if we want to even state the eliminator for inductive-inductive types we need a recursive-recursive fixpoint.

view this post on Zulip Bas Spitters (Jun 06 2020 at 13:23):

Frederik's analysis shows similarly that one can reduce indind to induction.

view this post on Zulip Jakob Botsch Nielsen (Jun 06 2020 at 13:26):

The trick I used was to have a record defining my function types with the dependencies I needed:

Record interp (n : nat) := {
  interp_ctx Gamma : context;
  interp_ty Gamma sigma : Ty (interp_ctx Gamma);
  interp_tm Gamma sigma M : Tm (interp_ty Gamma sigma);
}.

Then, you can construct this for all n by induction and you get the dependencies you want. I guess this is similar to your way @Ali Caglayan. However, this was also wildly impractical to work with I found.

view this post on Zulip Karl Palmskog (Jun 06 2020 at 13:26):

this one might be relevant as well: https://jashug.github.io/papers/ConstructingII.pdf ("Constructing Inductive-Inductive Types in Cubical Type Theory")

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:26):

I like to think that Frederik's method is a generalisation of reducing an inductive-inductive definition of well-formed contexts, types and terms to a mutually inductive definition of precontext, pretypes and preterms. Thereafter you define various predicates on these to get them to be well-formed. Essentially a pre(whatever) and a well-formed predicate together in a sigma type gives you back the original inductive-inductive type.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:27):

@Jakob Botsch Nielsen Those are exactly the kinds of examples that recursion-recursion would help with.

view this post on Zulip Jakob Botsch Nielsen (Jun 06 2020 at 13:28):

Yes, that's what I am saying :smile:

view this post on Zulip Ali Caglayan (Jun 06 2020 at 13:30):

The only problem with my rosy idea of the reduction is that I am not sure you can prove the general inductive-inductive eliminator from the pretyped stuff. I usually get very dizzy when trying to read the codes described in Fredrick's thesis, so I am not sure if this is something that can be done.

view this post on Zulip Danil Annenkov (Jun 06 2020 at 13:37):

That won't be enough for semi-simplicial types, as we still don;t know how to do it in agda...

@Bas Spitters Yeah, we need two-level type theory, and we have an encoding of it in Coq. In Agda one at least can write the definition in a natural way and postulate the coherence condition: https://github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/SStypes.agda
There is also this pull request with 2ltt support: https://github.com/agda/agda/pull/4091/commits/555ec43d0ce087a008c7db8f4f9d8a913f023e97
I tried to port some definitions but immediately run into problems.
Although 2ltt is not relevant for the recursion-recursion stuff, being able to write such definitions in a natural way would be nice.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 14:05):

@Karl Palmskog That is a very interesting paper. It's shown that Fredrick's reduction of II-types requires UIP, but Jasper also gives another construction in cubical type theory which supposedly is compatible with Coq + FunExt. But I guess this is just a justification for what we want to add to coq.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 14:11):

@Matthieu Sozeau The Fixpoint keyword doesn't work for recursive-recursive definitions currently. Is this easy to fix?

view this post on Zulip Ali Caglayan (Jun 06 2020 at 16:34):

@Matthieu Sozeau You mention that Scheme is giving the "wrong" elimination rules. I don't think that these are necessarily wrong however, they correspond to the simple elimination rules for II-types described in Forsberg's thesis. The general eliminators are obviously recursive-recursive and their generation using Scheme needs to be added like you say.

Is there a way we can pass an argument to Scheme so that we can choose whether it gives the simple or general eliminators. Similar to Minimiality and Induction. Perhaps a name like Generality might work?

view this post on Zulip Bas Spitters (Jun 06 2020 at 16:40):

I guess currently IndInd will extend the TCB. How difficult would it be to do this reduction in meta-coq? (Just curious.)

view this post on Zulip Gaëtan Gilbert (Jun 06 2020 at 16:41):

What reduction?

view this post on Zulip Ali Caglayan (Jun 06 2020 at 16:45):

Of inductive-inductive types to indexed inductive types.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 16:45):

Forsberg's reduction using K in a crucial way

view this post on Zulip Ali Caglayan (Jun 06 2020 at 16:46):

but Jasper has presented another here https://jashug.github.io/papers/ConstructingII.pdf

view this post on Zulip Ali Caglayan (Jun 06 2020 at 16:46):

That supposedly only needs Intentional ML + Funext

view this post on Zulip Ali Caglayan (Jun 06 2020 at 16:57):

I should note that these reductions only derive the simple eliminators for II-types.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 17:37):

@Matthieu Sozeau This silly example throws an uncaught exception:

Inductive A : Type :=
with B : A -> Type :=
with C : forall (a : A), B a :=.

I would expect an error message telling me that the target sort of C is not valid.

view this post on Zulip Gaëtan Gilbert (Jun 06 2020 at 19:02):

Doesn't seem to be about II, eg Inductive foo : nat := .

view this post on Zulip Gaëtan Gilbert (Jun 06 2020 at 19:03):

https://github.com/coq/coq/issues/12470

view this post on Zulip Matthieu Sozeau (Jun 06 2020 at 19:05):

@Ali Caglayan Adapting Fixpoint should not be too hard in principle, but requires redoing the same things I did in pretyping, where I use evars to typecheck the bodies gradually. I'm wondering if it would not be better to just use pretyping directly to elaborate the mutual fixpoints.

view this post on Zulip Matthieu Sozeau (Jun 06 2020 at 19:23):

I'll have to read Jasper's paper, that sounds interesting.

view this post on Zulip Matthieu Sozeau (Jun 06 2020 at 19:30):

Reductions to inductives will still all be limited to having propositional equalities in lieu of the (most interesting) new definitional equalities you get from the dependent ind-ind eliminators that are implemented in Agda and now Coq. Probably the translations from ETT or ITT to weak type theory apply here as well to show that these definitional equalities do not add logical power though.

view this post on Zulip Ali Caglayan (Jun 06 2020 at 20:28):

@Matthieu Sozeau I sent you a PR with two more examples in the test-suite

view this post on Zulip Ali Caglayan (Jun 06 2020 at 21:26):

@Matthieu Sozeau I'm currently getting these errors when trying to make your branch.

OCAMLOPT  vernac/record.ml
File "vernac/record.ml", line 438, characters 6-286:
Warning 50: unattached documentation comment (ignored)
File "vernac/record.ml", line 1:
Error: Some fatal warnings were triggered (1 occurrences)
Makefile.build:778: recipe for target 'vernac/record.cmx' failed
make[1]: *** [vernac/record.cmx] Error 2
make[1]: Leaving directory '/home/ali/coq'
Makefile.make:178: recipe for target 'submake' failed
make: *** [submake] Error 2

Do you know what might be causing this?

view this post on Zulip Ali Caglayan (Jun 06 2020 at 21:27):

I'm looking around in vernac/record.ml but I am not sure why line 1 is a problem

view this post on Zulip Gaëtan Gilbert (Jun 06 2020 at 21:56):

line 1 is standing in for the whole file

view this post on Zulip Ali Caglayan (Jun 07 2020 at 01:16):

This might be a general issue with mutual fixpoints, but it doesn't seem there is anyway to make arguments implicit in the fixpoint right?

view this post on Zulip Ali Caglayan (Jun 07 2020 at 01:16):

I had an II type where the constructors of the first type had implicit arguments, but I had to specify these when using the constructor further down in the mutual inductive.

view this post on Zulip Matthieu Sozeau (Jun 07 2020 at 09:00):

I think internalization should allow the fixpoints and the constructors have implicits. For that we need to change constrintern.ml I believe. For the error, it's probably be due to the warning about the unattached comment and compiling with warnings as errors

view this post on Zulip Matthieu Sozeau (Jun 07 2020 at 09:09):

Actually, implicits in (fix. ... with ...) work already, e.g. I can use with FTy {Γ : Ctx} (ty : Ty Γ) {struct ty} : TyM Γ (FCtx Γ) ty := in the definitions of eliminators in II_dtt.v

view this post on Zulip Matthieu Sozeau (Jun 07 2020 at 09:44):

I fixed the treatment of implicits of constructors in ind-ind defs now.

view this post on Zulip Matthieu Sozeau (Jun 08 2020 at 10:32):

I also fixed the internalization so one can typecheck fix f (n : nat) := ... g n' bar ... with g (n : nat) (x : f n) {struct n} : ... := ..., but one has to disable guard-checking and add the {struct n} annotation. I think that's the general kind of "recursive-recursive" fixpoints we want, but I'd like to see some more examples of use where we use the previous fixpoints in the types of the arguments of later fixpoints (and not only in their conclusions)

view this post on Zulip Ali Caglayan (Jun 08 2020 at 15:08):

So as others have mentioned, interpretation of well-typed syntax is a common place this comes up. I recall that in Brunerie's thesis (Def 3.2.1), I had to use records to bundle up the definition of the "James construction", since we are mutually defining a family of types (over nat) and various maps between them which are used to construct the next level of the family etc.

Since agda has recursive-recursive definitions, I don't think anybody made note of this when formalizing it.

view this post on Zulip Matthieu Sozeau (Jun 08 2020 at 15:19):

Thanks, I didn't know that one.

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:23):

I've started to write up the example there but I am getting an error.

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:24):

Unset Elimination Schemes.

(** James construction in Homotopy type theory *)

(** The James construction as defined in Brunerie's thesis (https://arxiv.org/abs/1606.05916) has a tricky recursive-recursive definition that we will test here. Without recursive-recursive support in coq, this would have to be defined as a fixpoint into a record type. *)

Inductive Unit : Type := tt : Unit.

Inductive Id {A : Type} (x : A) : A -> Type := refl : Id x x.

Arguments refl {_ _}.

Scheme Id_ind := Induction for Id Sort Type.
Arguments Id_ind [A] x P f y.
Scheme paths_rec := Minimality for Id Sort Type.
Arguments Id [A] x P.

Register refl as core.identity.refl.
Definition Id_rect := Id_ind.
Register Id_rect as core.identity.ind.

Definition transport {A : Type} (P : A -> Type) {x y : A} (p : Id x y) (a : P x)
  : P y := match p with refl => a end.

Definition transport_const {A B : Type} {x y : A} (p : Id x y) (a : B)
  : Id (transport (fun _ => B) p a) a
  := match p with refl => refl end.

Definition apD {A : Type} {B : A -> Type} (f : forall a, B a) {x y : A} (p : Id x y)
  : Id (transport B p (f x)) (f y)
  := match p with refl => refl end.

Definition ap {A B : Type} {x y : A} (f : A -> B) (p : Id x y) : Id (f x) (f y)
  := match p with refl => refl end.

Definition id_concat {A : Type} {x y z : A}
  : Id x y -> Id y z -> Id x z.
Proof.
  intros p q.
  destruct p, q.
  apply refl.
Defined.

Lemma apD_const {A B} {x y : A} (f : A -> B) (p : Id x y)
  : Id (apD f p) (id_concat (transport_const p (f x)) (ap f p)).
Proof.
  destruct p; reflexivity.
Defined.

Definition id_concat_1p {A : Type} {x y : A} (p : Id x y)
  : Id (id_concat refl p) p
  := match p with refl => refl end.

Definition id_inv {A : Type} {x y : A} (p : Id x y) : Id y x
  := match p with refl => refl end.

Lemma id_cancelL {A : Type} {w x y : A} (p q : Id x y) (r : Id w x)
  : Id (id_concat r p) (id_concat r q) -> Id p q.
Proof.
  intro l.
  destruct r.
  refine (id_concat (id_inv _) (id_concat l _)).
  all: apply id_concat_1p.
Defined.

(** Here we need the HIT pushout which we fake using a private inductive type *)
Module Export Pushout.

  Private Inductive Pushout {A B C : Type} (f : A -> B) (g : A -> C) : Type :=
  | pushl : B -> Pushout f g
  | pushr : C -> Pushout f g.

  Axiom pglue : forall {A B C : Type} (f : A -> B) (g : A -> C) (x : A),
    Id (pushl f g (f x)) (pushr f g (g x)).

  (** Induction principle that computes on point constructors *)
  Definition Pushout_ind {A B C : Type} (f : A -> B) (g : A -> C)
    (P : Pushout f g -> Type)
    (l : forall b, P (pushl f g b))
    (r : forall c, P (pushr f g c))
    (h : forall a, Id (transport P (pglue f g a) (l (f a))) (r (g a)))
    (x : Pushout f g) : P x
    := match x with
       | pushl _ _ b => l b
       | pushr _ _ c => r c
       end.

  (** Computation rule for the path constructor *)
  Axiom Pushout_ind_beta_pglue
    : forall {A B C : Type} (f : A -> B) (g : A -> C)
    (P : Pushout f g -> Type)
    (l : forall b, P (pushl f g b))
    (r : forall c, P (pushr f g c))
    (h : forall a, Id (transport P (pglue f g a) (l (f a))) (r (g a)))
    (a : A), Id (apD (Pushout_ind f g P l r h) (pglue f g a)) (h a).

End Pushout.

Arguments pushl {A B C f g}.
Arguments pushr {A B C f g}.

Definition Pushout_rec {A B C : Type} (f : A -> B) (g : A -> C)
  (P : Type) (l : B -> P) (r : C -> P)
  (h : forall a, Id (l (f a)) (r (g a)))
  : Pushout f g -> P.
Proof.
  refine (Pushout_ind f g (fun _ => P) l r _).
  intro a.
  exact (id_concat (transport_const _ _) (h a)).
Defined.

Definition Pushout_rec_beta_pglue {A B C : Type} (f : A -> B) (g : A -> C)
  (P : Type) (l : B -> P) (r : C -> P)
  (h : forall a, Id (l (f a)) (r (g a)))
  : forall a, Id (ap (Pushout_rec f g P l r h) (pglue f g a)) (h a).
Proof.
  intro a.
  refine (id_cancelL _ _ (transport_const (pglue f g a) (l (f a))) _).
  refine (id_concat (id_inv _) _).
  1: apply (apD_const (Pushout_rec f g P l r h) (pglue f g a)).
  exact (Pushout_ind_beta_pglue f g (fun _ => P) l r _ a).
Defined.

Definition JamesConstruction (n : nat) (A : Type) (a : A) : Type.
Proof.
  refine (
  fix J (n : nat) :=
    match n with
    | O => Unit
    | S O => A
    | S (S n) => Pushout (f n) (g n)
    end
  with i (n : nat) : J n -> J (S n) := _
  with α (n : nat) : A -> J n -> J (S n) := _
  with β (n : nat) (x : J n) : Id (α n a x) (i n x) := _
  with f (n : nat) : Pushout (fun x => (a, x)) (i n) -> A * J (S n) := _
  with g (n : nat) : Pushout (fun x => (a, x)) (i n) -> J (S n) := _
  for J : nat -> Type).

It throwsAnomaly "Bad occurrence of recursive call." Please report at http://coq.inria.fr/bugs/. so I don't really know what is going on.

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:25):

@Matthieu Sozeau

view this post on Zulip Matthieu Sozeau (Jun 08 2020 at 16:27):

I fixed this this morning. you have to give {struct n} annotations if you put recursive calls in the "binder" part of the fixpoints. I guess for Beta here

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:50):

Cool I've got a stack overflow

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:50):

This is what caused it:

Definition JamesConstruction (m : nat) (A : Type) (pt : A) : Type.
Proof.
  Check (
  fix J (n : nat) {struct n} :=
    match n with
    | O => Unit
    | S O => A
    | S (S n) => Pushout (f n) (g n)
    end
  with i (n : nat) {struct n} : J n -> J (S n) :=
    match n with
    | O => fun _ => pt
    | S n => pushr (f n) (g n)
    end
  with α (n : nat) {struct n} : A -> J n -> J (S n) :=
    match n with
    | O => fun a _ => a
    | S n => pushl f g
    end
  with β (n : nat) (x : J n) {struct n}  : Id (α n pt x) (i n x) :=
    match n with
    | O => refl
    | S n => fun l => pglue f g (pushr (fun x => (pt, x)) (i n) l)
    end
  with f (n : nat) {struct n} : Pushout (fun x => (pt, x)) (i n) -> A * J (S n) :=
    Pushout_rec _ (fun ax => (fst ax, i n (snd ax))) (fun y => (pt, y)) (fun x => refl)
  with g (n : nat) {Struct n} : Pushout (fun x => (pt, x)) (i n) -> J (S n) :=
    Pushout_rec _ (fun ax => α n (fst ax) (snd ax)) (fun y => y) (fun x => β x)
  for J : nat -> Type).

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:50):

With the same code as before.

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:52):

@Matthieu Sozeau

view this post on Zulip Matthieu Sozeau (Jun 08 2020 at 16:53):

I'll have to debug that. can you get the backtrace (using coqtop -bt)?

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:54):

Stack overflow.
Raised by primitive operation at file "kernel/vars.ml", line 195, characters 5-20
Called from file "kernel/vars.ml", line 206, characters 30-52
Called from file "clib/cList.ml", line 1034, characters 15-18
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1043, characters 6-21
Called from file "kernel/constr.ml", line 786, characters 14-48
Called from file "clib/cArray.ml", line 698, characters 17-24
Called from file "kernel/constr.ml", line 778, characters 14-41
Called from file "clib/cArray.ml", line 713, characters 19-26
Called from file "kernel/constr.ml", line 778, characters 14-41
Called from file "kernel/constr.ml", line 767, characters 13-22
Called from file "clib/cArray.ml", line 698, characters 17-24
Called from file "kernel/constr.ml", line 792, characters 14-41
Called from file "kernel/constr.ml", line 767, characters 13-22
Called from file "clib/cArray.ml", line 698, characters 17-24
Called from file "kernel/constr.ml", line 792, characters 14-41
Called from file "kernel/constr.ml", line 767, characters 13-22
Called from file "engine/evd.ml" (inlined), line 265, characters 9-28
Called from file "engine/evd.ml", line 628, characters 29-65
Called from file "engine/evd.ml", line 631, characters 35-61
Called from file "engine/evd.ml", line 1330, characters 13-41
Called from file "engine/evd.ml", line 1336, characters 18-42
Called from file "engine/evd.ml" (inlined), line 1356, characters 33-51
Called from file "engine/evarutil.ml", line 159, characters 10-30
Called from file "engine/evarutil.ml", line 168, characters 18-45
Called from file "pretyping/evarconv.ml", line 472, characters 14-37
Called from file "pretyping/evarconv.ml", line 347, characters 14-31
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 347, characters 14-31
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 347, characters 14-31
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 347, characters 14-31
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 347, characters 14-31
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 347, characters 14-31
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 347, characters 14-31
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 347, characters 14-31
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 347, characters 14-31
Called from file "pretyping/evarconv.ml", line 332, characters 14-18
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 369, characters 17-47
Called from file "pretyping/evarconv.ml", line 439, characters 21-51
Called from file "pretyping/evarconv.ml", line 371, characters 30-49
Called from

view this post on Zulip Ali Caglayan (Jun 09 2020 at 14:30):

@Matthieu Sozeau Any idea what is causing the overflow?

view this post on Zulip Matthieu Sozeau (Jun 09 2020 at 14:39):

Something bad is happening during elaboration, that seems to produce cyclic term through the evar_map. I'm still trying to get to the bottom (sic) of it

view this post on Zulip Matthieu Sozeau (Jun 09 2020 at 14:46):

Oh I see now, the unification used for implicit arguments in your definition produces unrollings of the fixpoints resulting in a cyclic evar_map. I'll have to try and refold them

view this post on Zulip Matthieu Sozeau (Jun 09 2020 at 17:03):

That's not enough to fix it though. The bodies contain calls like (J (S n)) which don't play well with Coq's strategy of reducing fixpoints when applied to constructors. I'm hitting an infinite reduction now.

view this post on Zulip Jakob Botsch Nielsen (Jun 09 2020 at 18:33):

Does that mean SN is broken with inductive-inductive types?

view this post on Zulip Ali Caglayan (Jun 09 2020 at 19:00):

@Jakob Botsch Nielsen This specific example is just about recursive-recursive definitions. We are getting a stack overflow when type checking the James construction (described above). Since this is about type checking I don't think it effects SN.

view this post on Zulip Ali Caglayan (Jun 09 2020 at 19:01):

The question of whether ind-ind types with general elimination rules preserve SN (at least in coq) is a seperate question which I don't know the answer to. I would be surprised if it breaks SN.

view this post on Zulip Ali Caglayan (Jun 09 2020 at 19:02):

(I'm interpreting SN = strong normalization)

view this post on Zulip Ali Caglayan (Jun 09 2020 at 19:12):

@Matthieu Sozeau So changing it to

view this post on Zulip Ali Caglayan (Jun 09 2020 at 19:13):

Definition JamesConstruction (m : nat) (A : Type) (pt : A) : Type.
Proof.
  Check (
  fix J (n : nat) {struct n} :=
    match n with
    | O => Unit
    | S O => A
    | S (S n) => Pushout (f n) (g n)
    end
  with i (n : nat) {struct n} : J n -> J (S n) :=
    match n with
    | O => fun _ => pt
    | S n => pushr (f n) (g n)
    end
  with α (n : nat) {struct n} : A -> J n -> J (S n) :=
    match n with
    | O => fun a _ => a
    | S n => pushl f g
    end
  with β (n : nat) (x : J n) {struct n}  : Id (α n pt x) (i n x) :=
    match n with
    | O => refl
    | S n => fun l => pglue f g (pushr (fun x => (pt, x)) (i n) l)
    end
  with f (n : nat) {struct n} : Pushout (fun x => (pt, x)) (i n) -> A * J (S n) :=
    Pushout_rec (A * J (S n)) (fun ax => (fst ax, i n (snd ax))) (fun y => (pt, y)) (fun x => refl)
  with g (n : nat) {struct n} : Pushout (fun x => (pt, x)) (i n) -> J (S n) :=
    Pushout_rec (J (S n)) (fun ax => α n (fst ax) (snd ax)) (fun y => y) (fun x => β x)
  for J : nat -> Type).

view this post on Zulip Ali Caglayan (Jun 09 2020 at 19:13):

Gives a different loop, this time with the reduction like you said.

view this post on Zulip Ali Caglayan (Jun 09 2020 at 19:13):

Stack overflow.
Raised by primitive operation at file "kernel/vars.ml", line 195, characters 5-20
Called from file "kernel/vars.ml", line 206, characters 30-52
Called from file "clib/cList.ml", line 1034, characters 15-18
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1035, characters 6-21
Called from file "clib/cList.ml", line 1043, characters 6-21
Called from file "kernel/constr.ml", line 786, characters 14-48
Called from file "engine/evd.ml" (inlined), line 265, characters 9-28
Called from file "engine/evd.ml", line 628, characters 29-65
Called from file "engine/evd.ml", line 631, characters 35-61
Called from file "engine/evarutil.ml", line 26, characters 40-70
Called from file "kernel/cClosure.ml", line 1306, characters 13-36
Called from file "kernel/cClosure.ml" (inlined), line 1336, characters 2-19
Called from file "kernel/cClosure.ml", line 1433, characters 10-29
Called from file "kernel/reduction.ml", line 346, characters 27-77
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "kernel/reduction.ml", line 480, characters 20-60
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "kernel/reduction.ml", line 720, characters 20-95
Called from file "kernel/reduction.ml", line 600, characters 22-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "kernel/reduction.ml" (inlined), line 645, characters 34-71
Called from file "kernel/reduction.ml", line 658, characters 26-39
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 245, characters 11-40
Called from file "kernel/reduction.ml", line 338, characters 6-72
Called from file "clib/cArray.ml", line 271, characters 11-52
Called from file "kernel/reduction.ml", line 664, characters 16-70
Called from file "kernel/reduction.ml", line 338, characters 6-72

view this post on Zulip Jakob Botsch Nielsen (Jun 09 2020 at 19:14):

Yes I was talking about strong normalization. Hitting an infinite reduction sounds like normalization is broken, but I guess it could be because Coq checks too much when doing those unfolds or something along those lines.

view this post on Zulip Ali Caglayan (Jun 09 2020 at 19:16):

Yeah, its a problem with this typechecker rather than the language itself.

view this post on Zulip Jakob Botsch Nielsen (Jun 09 2020 at 19:18):

Well, type checking and reduction is not completely orthogonal due to conversion. But I guess conversion has more tricks up its sleeve to make it fast.

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 08:31):

I think induction-induction is fine in general, but this definition seems to demand more than the usual guarded definitions can handle, e.g. that recursive calls on (S n) be allowed (where (S n) is still smaller than the initial argument of shape (S (S n))). I believe in this case you could use the < order on naturals to show the definition is terminating.

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 08:32):

I'm now trying to massage the definition to just require structural recursion

view this post on Zulip Jakob Botsch Nielsen (Jun 10 2020 at 08:58):

Ah, is the termination checker turned off in the types for now? Or why isn't it rejected then?

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 09:24):

It's turned off for the predicates of matches only. However the guard checker doesn't run until the end of the typechecking of the whole fixpoint currently, while the computational content of defs can be used during typechecking

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 09:26):

Hooray, I managed to typecheck it:

Section James.
  Context (A : Type) (pt : A).

  Definition JA J' (n : nat) : Type :=
    match n with
    | 0 => A
    | S n => J' n
    end.

  Definition f (J' : nat -> Type)
   (i : forall (n : nat), JA J' n -> J' n)
   (n : nat) : Pushout (fun x => (pt, x)) (i n) -> A * J' n :=
    Pushout_rec _ _ _ (fun ax => (fst ax, i n (snd ax))) (fun y => (pt, y)) (fun x => refl).

  Definition g (J' : nat -> Type)
    (i : forall (n : nat), JA J' n -> J' n)
    (α : forall (n : nat), A -> JA J' n -> J' n)
    (β : forall (n : nat) (x : JA J' n), Id (α n pt x) (i n x))
    (n : nat) : Pushout (fun x => (pt, x)) (i n) -> J' n :=
    Pushout_rec _ _ _ (fun ax => α n (fst ax) (snd ax)) (fun y => y) (fun x => β n x).

  (* Unset Guard Checking.
    Note we still don't guard-check the return predicates of pattern matchings.
    It does guarantee however that the recursive calls inside the match branches
    are structurally recursive.
  *)

  Definition J' : nat -> Type :=
  fix J' (n : nat) {struct n} : Type :=
  match n with
  | O => A
  | S n1 => Pushout (f J' i n1) (g J' i α β n1)
  end
  with i (n : nat) {struct n} : JA J' n -> J' n :=
    match n return JA J' n -> J' n with
    | O => fun _ => pt
    | S n' => fun jn => @pushr _ _ _ (f J' i n') (g J' i α β n') jn
    end
  with α (n : nat) {struct n} : A -> JA J' n -> J' n :=
    match n return A -> JA J' n -> J' n with
    | O => fun a _ => a
    | S n => fun a jsn => pushl (f:=f J' i n) (g:=g J' i α β n) (a, jsn)
    end
  with β (n : nat) {struct n} : forall (x : JA J' n), Id (α n pt x) (i n x) :=
    match n return forall x : JA J' n, Id (α n pt x) (i n x) with
    | O => fun (x : A) => (@refl A pt)
    | S n => fun l => pglue (f J' i n) (g  J' i α β n)
      (pushr (f:=fun x => (pt, x)) (g:=i n) l)
    end
  for J'.
  Definition J := JA J'.

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 09:36):

I had to freeze the evars corresponding to fixpoint bodies to not run unification into circles and do a bit of fixpoint refolding (that's a bit worrying). Also I was missing a crucial lift in kernel typechecking that resulted in wrong de Bruijn indices when checking a fix under a de Bruijn context. That should fix other issues in the test-suite :)

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 13:14):

The guard checking is run incrementally now so we shouldn't face non-termination anymore

view this post on Zulip Ali Caglayan (Jun 10 2020 at 14:36):

@Matthieu Sozeau There are some unattached documentation comments in pretyping/pretyping.ml

view this post on Zulip Ali Caglayan (Jun 10 2020 at 14:37):

Or rather there is one at 892 and an unused value head at 713

view this post on Zulip Ali Caglayan (Jun 10 2020 at 14:39):

Here is the log since my description is poor:

File "pretyping/pretyping.ml", line 892, characters 12-57:
Warning 50: unattached documentation comment (ignored)
File "pretyping/pretyping.ml", line 713, characters 6-10:
Warning 32: unused value head.

view this post on Zulip Ali Caglayan (Jun 10 2020 at 15:19):

@Matthieu Sozeau typechecking J' takes some time, do you know what is going on here?

view this post on Zulip Ali Caglayan (Jun 10 2020 at 15:27):

Also, what needs to be done in order for the definition of the James construction that I gave to be acceptable?

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 15:28):

I fixed the compilation warnings. J' takes more time because I left some implicit arguments and unification has to work much more. Also I'm applying whnf reduction and refolding fixpoints that are produced by unification so it can take more time because of the additional conversions. These would not be necessary if we had global fixpoint names instead of the block+projection representation.

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 15:30):

As written originally, it's not possible to guard check it. E.g.

Recursive call to J has principal argument equal to
"S n1" instead of "n1".
Recursive definition is:
"fun n : nat =>
 match n return Type with
 | O => A
 | S n1 =>
     @Pushout
       (@Pushout (J n1) (prod A (J n1)) (J (S n1))
          (fun x : J n1 => @pair A (J n1) pt x) (i n1))
       (prod A (J (S n1))) (J (S n1)) (f J i n1) (g J i α β n1)
 end".
Raised at file "pre

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 15:32):

It might be possible if guard-checking also allows some reduction of the previous fixpoints

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 15:33):

I'll have to think carefully if this should be allowed though and if guard-checking would still ensure SN

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 16:53):

Now this goes through:

Section James.
  Context (A : Type) (pt : A).
  Notation f J i n :=
  (@Pushout_rec (J n%nat) (prod A (J n%nat)) (J (S n)) (fun x => (pt, x)) (i%function n%nat) (A * J (S n))
    (fun ax => (fst ax, i%function n%nat (snd ax))) (fun y => (pt, y)) (fun x => refl)).

  Notation g J i α β n :=
   (Pushout_rec (fun x => (pt, x)) (i%function n%nat) (J (S n%nat))
      (fun ax => α n%nat (fst ax) (snd ax)) (fun y => y) (fun x => β%function n%nat x)).
(*
  Definition f (J : nat -> Type)
   (i : forall (n : nat), J n -> J (S n))
   (n : nat) : Pushout (fun x => (pt, x)) (i n) -> A * J (S n) :=
    Pushout_rec _ _ _ (fun ax => (fst ax, i n (snd ax))) (fun y => (pt, y)) (fun x => refl). *)

  (*Definition g (J : nat -> Type)
    (i : forall (n : nat), J n -> J (S n))
    (α : forall (n : nat), A -> J n -> J (S n))
    (β : forall (n : nat) (x : J n), Id (α n pt x) (i n x))
    (n : nat) : Pushout (fun x => (pt, x)) (i n) -> J (S n) :=
    Pushout_rec _ _ _ (fun ax => α n (fst ax) (snd ax)) (fun y => y) (fun x => β n x).*)

  (* Guard checking bails because it cannot unfold [J (S n)] in the definition of f above s*)

  Definition J : nat -> Type :=
  fix J (n : nat) {struct n} : Type :=
  match n with
  | O => Unit
  | S n0 => J' n0
  end
  with J' (n : nat) : Type :=
  match n with
  | 0 => A
  | S n1 => Pushout (f J i n1) (g J i α β n1)
  end
  with i (n : nat) {struct n} : J n -> J (S n) :=
    match n return J n -> J (S n) with
    | O => fun _ => pt
    | S n' => fun jn => @pushr _ _ _ (f J i n') (g J i α β n') jn
    end
  with α (n : nat) {struct n} : A -> J n -> J (S n) :=
    match n return A -> J n -> J (S n) with
    | O => fun a _ => a
    | S n => fun a jsn => @pushl _ _ _ (f J i n) (g J i α β n) (a, jsn)
    end
  with β (n : nat) {struct n} : forall (x : J n), Id (α n pt x) (i n x) :=
    match n return forall x : J n, Id (α n pt x) (i n x) with
    | O => fun x => refl
    | S n => fun l => pglue (f J i n) (g J i α β n) (pushr l)
    end
  for J.
  End James.

If I switch from Notations to Definitions it fails though, even if the guard checker clearly unfolds definitions..

view this post on Zulip Ali Caglayan (Jun 10 2020 at 17:19):

Where exactly does the guard checker unfold definitions?

view this post on Zulip Jakob Botsch Nielsen (Jun 10 2020 at 17:29):

I guess it has to unfold f/g to realize that J/i/alpha/beta are only used on subterms of n

view this post on Zulip Ali Caglayan (Jun 10 2020 at 17:35):

I meant to say where in the code is it unfolding things :)

view this post on Zulip Ali Caglayan (Jun 10 2020 at 17:35):

I don't know which ml file the guardcheker is in

view this post on Zulip Jakob Botsch Nielsen (Jun 10 2020 at 17:37):

I looked at it a while ago because I was amazed Nat.gcd was structurally recursive, sec

view this post on Zulip Jakob Botsch Nielsen (Jun 10 2020 at 17:39):

https://github.com/coq/coq/blob/c077db40a204132eda8a5d5979022f4961503cab/kernel/inductive.ml#L919
I think this is the one

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 19:52):

Yep that's the one. The Const case unfold if guard checking fails without unfolding

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 21:10):

... But strangely that's not enough for the James example.

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 21:12):

Ok, today I implemented a first version of guard checking for ind-ind, and both the DTT and James construction pass it. It's probably too permissive though, it allows more recursive calls in types than in terms. I'll write a summary tomorrow.

view this post on Zulip Ali Caglayan (Jun 11 2020 at 01:34):

Ah J' is much faster now.

view this post on Zulip Ali Caglayan (Jun 16 2020 at 10:21):

@Matthieu Sozeau Any progress with this?

view this post on Zulip Matthieu Sozeau (Jun 16 2020 at 10:37):

Hmm not really. I'm not happy with the way we have to typecheck fixpoints in the kernel. To handle inductive-inductive types where constructors might depend on constructors in the same inductive type, we have to allow typechecking the body of f under a context where this body appears and can be unfolded. That's another instance where we would need "partial" fixpoints", and maybe even cleaner, being able to gradually define a recursive definition by adding clauses for each constructor, to ensure a nice and safe typechecking procedure.

view this post on Zulip Ali Caglayan (Jun 16 2020 at 17:39):

How difficult would it be to add partial fixpoints?

view this post on Zulip Ali Caglayan (Jun 17 2020 at 12:38):

Or here's a better question: What are partial fixpoints exactly?

view this post on Zulip Matthieu Sozeau (Jun 18 2020 at 15:38):

Let's take an example from II_dtt.v, we have:

with Ty : Ctx -> Type :=
| subst_ty : forall {Γ Δ}, Ty Δ -> Sub Γ Δ -> Ty Γ
| U : forall {Γ}, Ty Γ
| El : forall {Γ : Ctx}, Tm Γ U -> Ty Γ
| Pi : forall {Γ} (A : Ty Γ) (B : Ty (ctx_ext Γ A)), Ty Γ

So here El depends on U. To implement the recursor, we must do:

with FTy {Γ : Ctx} (ty : Ty Γ) {struct ty} : TyM Γ (FCtx Γ) ty :=
      match ty in Ty g return TyM g (FCtx g) ty with
      | @U g => fU g (FCtx g)
      | @El g t => fEl g (FCtx g) t (FTm g (@U g) t)
      | @Pi g a b => ...
      | @subst_ty Γ Δ t s => ...
      end
with FTm (Γ : Ctx) (ty : Ty Γ) (t : Tm Γ ty) {struct t} :
           TmM Γ (FCtx Γ) ty (FTy ty) t := ...

where     (fU : forall x (x0 : CtxM x), TyM x x0 U)
    (fEl : forall Γ  t, TmM Γ  U (fU _ ) t -> TyM Γ  (El t))

To typecheck the El branch, we must have that (FTm g (@U g) t : TmM Γ (FCtx Γ) ty (FTy (@U g)) t = TmM (FCtx Γ) ty U (fU _ (FCtx g)) t, so this requires to have the reduction FTy (U @g) t -> fU _ (FCtx g). We know this to be true only because we typechecked the first branch | @U g.
The way we currently typecheck FTy is to push the complete definition of its body (and actually all the recursive definitions) in the context and then typecheck the same body. This is circular. A more "well-founded" methodology would allow to typecheck each branch in FTy assuming only the previous branches are well-typed and can participate in reduction.

view this post on Zulip Matthieu Sozeau (Jun 18 2020 at 15:43):

My idea of partial fixpoints is just that. We would be allowed to put in the context a partial version of the whole mutual block to ensure that we are not relying on a circular definition at any point. I believe this would also mimick the (perhaps naive) model I have in mind for inductive inductive types where, when you construct a mutual fixpoint on an inductive-inductive you actually follow the same discipline of gradually applying the fixpoint to larger and larger inductive objects that would naturally follow the type dependency order.

view this post on Zulip Ali Caglayan (Jun 23 2020 at 20:52):

I've been thinking about this a bit. At the moment in coq we have the following rule:

(E[Γ]Ai:si)i=1n(E[Γ;(fk:Ak)k=1n]ti:Ai)i=1nE[Γ]Fixfi{fk:Ak:=tk}k=1n:Ai\frac{\left ( E [\Gamma ] \vdash A_i : s_i \right)_{i=1\dots n} \qquad \left( E [ \Gamma ; (f_k : A_k)_{k=1\dots n}] \vdash t_i : A_i \right )_{i=1\dots n}}{E[\Gamma] \vdash \mathsf{Fix} f_i \{ f_k : A_k := t_k \}_{k=1\dots n} : A_i}

With side conditions checking for guardedness. What if we replaced this rule with a slightly more elaborate system. First we add a new judgement E[Γ]PFix{fk:Ak:=tk}k=1nE [\Gamma ]\vdash \mathsf{PFix} \{ f_k : A_k := t_k \}_{k=1 \dots n} which says that this is a "well-formed partial fixpoint" in the environment/context.

We generate this judgement with the following two rules:

E[Γ]A:sE[Γ;f:A]t:AE[Γ]PFix{f:A:=t}(PFixbase)\frac{E [\Gamma] \vdash A : s \qquad E [\Gamma ; f : A] \vdash t : A}{E [\Gamma] \vdash \mathsf{PFix} \{ f : A := t \}} \qquad (\mathsf{PFix}\mathrm{-base})

for the base case and

E[Γ]PFix{fk:Ak:=tk}k=1nE[Γ;(Ak:sk,fk:Ak)k=1n]An+1:sn+1E[Γ;(Ak:sk,fk:Ak)k=1n;An+1:sn+1]tn+1:An+1E[Γ]PFix{fk:Ak:=tk}k=1n+1(PFixexten)\frac{ \begin{aligned} E [\Gamma ] &\vdash \mathsf{PFix} \{ f_k : A_k := t_k \}_{k=1 \dots n} \\ E [\Gamma ; (A_k : s_k , f_k : A_k)_{k=1 \dots n} ] &\vdash A_{n+1} : s_{n+1} \\ E [\Gamma ; (A_k : s_k , f_k : A_k)_{k=1 \dots n}; A_{n+1} : s_{n+1}] &\vdash t_{n+1} : A_{n+1} \end{aligned} }{ E [\Gamma ] \vdash \mathsf{PFix} \{ f_k : A_k := t_k \}_{k=1 \dots n+1} } \qquad (\mathsf{PFix}\mathrm{-exten})

for extending a partial fixpoint by appropriate terms. Finally this would mean we would have a "cap off" rule for forming fixpoints as follows:

E[Γ]PFix{fk:Ak:=tk}k=1nE[Γ]Fixfi{fk:Ak:=tk}k=1n:Ai\frac {E [\Gamma ] \vdash \mathsf{PFix} \{ f_k : A_k := t_k \}_{k=1\dots n} } {E [\Gamma ] \vdash \mathsf{Fix} f_i \{ f_k : A_k := t_k \}_{k=1\dots n} : A_i }

I am however not exactly sure where the guardedness checking needs to be done.

view this post on Zulip Ali Caglayan (Jun 29 2020 at 16:07):

@Matthieu Sozeau Any progress with this?

view this post on Zulip Matthieu Sozeau (Jun 29 2020 at 16:18):

Nope, I was busy elsewhere. Something like the typing rules you propose should work indeed. Except: in PFix-extend, you need to bind each f_k to a projection of the PFix (using a let I presume) when checking the bodies. I think a PFix should actuallly always contain all types of the fixpoints and only a subset (from 0 to some k) of the bodies. And you shouldn't need to check the Aks or bind them (in PFix-extend).

view this post on Zulip Matthieu Sozeau (Jun 29 2020 at 16:28):

In other words, a partial fixpoint could be represented as a fixpoint where the last bodies would be optional. Then you'd have PFix fixes k can reduce to a given fixpoint body only if is present, and is otherwise stuck. We want to ensure that the different ways that an undefined body can appear through reduction are convertible. Naturally we can refer too f_k+1 in t_k directly as a variable declared in the context or through some recursive call to some f_i (i < k) that reduces to a term mentioning f_k+1. That reference will actually become PFix fixes (k+1) after unfolding of the body of f_i.

view this post on Zulip Matthieu Sozeau (Sep 16 2020 at 08:02):

We discussed a bit the introduction of partial fixpoints. People pointed out that a partial fixpoint introduces an axiom (for the undefined parts of the fixpoint) and that it might be more principled to use a general "daimon"/axiom term constructor, such that:

Γdaimon τ:τ\Gamma \vdash \text{daimon}~\tau : \tau

for constructing these partial proofs. I.e. The daimon would be considered guarded in that case. That's a non-trivial change though :)

view this post on Zulip Matthieu Sozeau (Sep 16 2020 at 08:09):

I'm not sure this would play well with unfolding of the recursive definitions during typechecking though, if you get to two daimon by different paths, you shouldn't consider them equal. If however with have partial fixpoints where if f_i is not defined then all calls are stuck, we can ensure that all calls ending in f_i u will be equal even after the definition of f_i.

view this post on Zulip Jason Gross (Sep 16 2020 at 19:10):

Couldn't you just insert an arrow type for tau, taking a dummy nat which is the sort-of goal number? (Also, is "diamon" French for "daemon" or "demon"? I've never seen that word before)

view this post on Zulip Karl Palmskog (Sep 16 2020 at 19:18):

"daemon" is Latin, "daimon"/δαίμων is (ancient) Greek for the same concept. In ancient Latin pronounciation, they sound the same.

view this post on Zulip Karl Palmskog (Sep 16 2020 at 19:22):

one might say that the French got this right and the rest of us using "demon" are saying it wrong. (Compare "Caesar", where the Germans have it right while English is wrong again, at least if Romans are any guide.)

view this post on Zulip Théo Winterhalter (Sep 16 2020 at 20:28):

The French also use "démon".

view this post on Zulip Karl Palmskog (Sep 16 2020 at 20:31):

I think you at least have "daïmôn" as a word, no?

view this post on Zulip Théo Winterhalter (Sep 16 2020 at 20:46):

Ok, we do, but I wasn't aware of this, and it seems to refer to the ancient greek concept. :)

view this post on Zulip Karl Palmskog (Sep 16 2020 at 20:49):

on the Germanic language side, we seem to have mixed up our demons with daimons almost completely, and pop culture doesn't help either. Daemons in operating systems like Unix at least refer to the original concept.

view this post on Zulip Kenji Maillard (Sep 16 2020 at 20:53):

I would have thought that this use of the word "daimon" comes from the paper locus solum where Girard introduces ludics (p.8, 1.2.3).

view this post on Zulip Karl Palmskog (Sep 16 2020 at 21:04):

the one etymology doesn't seem to preclude the other

view this post on Zulip Ali Caglayan (Sep 18 2020 at 11:29):

What is a daimon?

view this post on Zulip Karl Palmskog (Sep 18 2020 at 12:05):

https://en.wikipedia.org/wiki/Daemon_(classical_mythology) -- or the one in the locus solum link above

view this post on Zulip Matthieu Sozeau (Oct 06 2020 at 21:36):

Finally got some time to rebase inductive-inductive types, as I hear some more people are interested.

view this post on Zulip Matthieu Sozeau (Oct 06 2020 at 21:38):

We still need to figure out this partial fixpoint representation. I don't think the "daimon" way is going to work. I'm also a bit sad having to represent partial fixpoints by introducing an option type in the bodies and doing surgery in the type checker.

view this post on Zulip Matthieu Sozeau (Oct 06 2020 at 21:44):

We could also hack by having a kind of -1 struct annotation to tell that a fixpoint body cannot be unfolded, and do the surgery only on these annotations. Not nice either.

view this post on Zulip Matthieu Sozeau (Oct 06 2020 at 21:48):

If we introduce fixpoints where some bodies might be absent that means changing all the reduction machinery in the kernel though.

view this post on Zulip Ali Caglayan (Oct 07 2020 at 08:06):

@Matthieu Sozeau Are the errors in the test suite anything to be worried about?

view this post on Zulip Ali Caglayan (Oct 07 2020 at 08:06):

Also anybody know how Agda type checks mutual inductive bodies?

view this post on Zulip Matthieu Sozeau (Oct 07 2020 at 08:09):

Agda has a general notion of typechecking w.r.t global environments, so "partial"/yet-to-be-defined fixpoints are naturally represented as axioms in the global context in the course of elaboration. At least that's my understanding

view this post on Zulip Matthieu Sozeau (Oct 07 2020 at 08:11):

I'll look at the test-suite issues

view this post on Zulip Kenji Maillard (Oct 07 2020 at 09:16):

Would it be possible/interesting to extend this notion of partial fixpoint to some local environment ? I'm thinking of a possible extension to Induction-Recursion, and my naive understanding would think that it amounts to typechecking a telescope where definitions can come after their declarations, e.g.

U : Type,El : UType,U :=[ nat : U  π : (A:U)(B:ElAU)U],El:=λ(u:U)match u with natN  pi \texttt{U}~:~\texttt{Type}, \texttt{El}~:~\texttt{U} \to \texttt{Type}, \texttt{U}~:=\,[|~\texttt{nat}~:~\texttt{U}~|~\pi~:~ \forall (A : \texttt{U}) ( B : \texttt{El}\,A \to \texttt{U}) \to U], \texttt{El} := \lambda (u : \texttt{U}) \Rightarrow \texttt{match}~ u ~\texttt{with}~|\texttt{nat} \Rightarrow \mathbb{N}~|~\texttt{pi} \ldots

where U and El can be understood first as axioms in the context that are defined after the fact.

view this post on Zulip Matthieu Sozeau (Oct 07 2020 at 09:21):

It might be the right "general" idea yes. But having context with multiple entries for the same name seems strange

view this post on Zulip Kenji Maillard (Oct 07 2020 at 09:23):

Isn't it just a backpointer ? I mean the second name/definition.

view this post on Zulip Kenji Maillard (Oct 07 2020 at 09:26):

Currently entries in the context are either variable declarations x : A or definitions x := t : A, no ? Here the definitions x:= t : A would be split into x : A, ..., x := t

view this post on Zulip Gaëtan Gilbert (Oct 07 2020 at 09:28):

In terms you don't get x, you just have a debruijn index
how do you make that work with this split context?

view this post on Zulip Kenji Maillard (Oct 07 2020 at 09:33):

Well, here you do want to access x so that you can do the fixpoint, no ? But that's a good point that you cannot just forget the x := t : A construction.

view this post on Zulip Matthieu Sozeau (Oct 07 2020 at 12:11):

As Gaëtan points out, it would be non-trivial to implement with de Bruijn indices. And we can't use named contexts "under" a de Bruijn context currently. So the contexts you describe should be at the global level, where this would be possible: it amounts to the "add global fixpoints first" idea.

view this post on Zulip Kenji Maillard (Oct 07 2020 at 14:00):

A bit of a side-track, but here is an example of an elimination principle for an inductive-inductive type that I'm not able to define in @Matthieu Sozeau 's branch (but I would expect it to be possible)

Axiom todo : forall {A}, A.

Inductive ctx : Type :=
| nil : ctx
| snoc (Γ : ctx) (A : ty Γ) : ctx
with ty : ctx -> Type :=
| Nat Γ : ty Γ.

Section ElimCtx.
  Context (P : ctx -> Type) (Q : forall Γ, P Γ -> ty Γ -> Type).
  Context (hnil : P nil)
          (hsnoc : forall Γ A ( : P Γ) (hA : Q Γ  A), P (snoc Γ A))
          (hNat : forall Γ ( : P Γ), Q Γ  (Nat Γ)).

  Fail
    Fixpoint elim_ctx (c : ctx) {struct c} : P c := todo
    with elim_ty (c : ctx) (A : ty c) {struct A} : Q c (elim_ctx c) A := todo.
  (* The error message highlight ` Q c (elim_ctx c) A ` *)
  (* Error: The reference elim_ctx was not found in the current environment.*)


  (* Expected *)
  Axiom elim_ctx : forall c, P c.
  Axiom elim_ty : forall c A, Q c (elim_ctx c) A.

  Axiom elim_ctx_nil : elim_ctx nil = hnil.
  Axiom elim_ctx_snoc : forall Γ A,
      elim_ctx (snoc Γ A) = hsnoc Γ A (elim_ctx Γ) (elim_ty Γ A).
  Axiom elim_ty_nat : forall Γ,
      elim_ty Γ (Nat Γ) = hNat Γ (elim_ctx Γ).

  Definition elim_ctx_ty : { e : (forall c, P c) & forall c A, Q c (e c) A } :=
    (* to mimick the dependency *)
    let x := hnil in
    let y := hsnoc in
    let z := hNat in
    existT _ elim_ctx elim_ty.
End ElimCtx.

(* Use case *)
Definition interp_ctx_ty : { interp_ctx : ctx -> Type & forall Γ (A : ty Γ), interp_ctx Γ -> Type }.
Proof.
  apply (elim_ctx_ty (fun _ => Type) (fun _ X _ => X -> Type)).
  - exact unit.
  - intros ? ? X F; exact ({x : X & F x}).
  - intros; exact nat.
Defined.

Is there a trick to define this eliminator ? Or am I just too greedy ?

view this post on Zulip Gaëtan Gilbert (Oct 07 2020 at 14:03):

You have to use fix instead of Fixpoint, and repeat the contents
eg https://github.com/SkySkimmer/HoTTClasses/blob/f9affefaa088d02ca7e6e901580ae6f9ff13ca40/theories/cauchy_completion.v#L133-L205

view this post on Zulip Kenji Maillard (Oct 07 2020 at 14:13):

Funny I also tried variations with fix, without success for now, I'll try again with your example

view this post on Zulip Kenji Maillard (Oct 07 2020 at 14:27):

Ok, partial definitions are rejected with a strange error (at least to me), but the full definition is accepted:

  Fail
  Definition elim_ctx : forall (c : ctx),  P c :=
    fix elim_ctx (c : ctx) {struct c} : P c := todo
    with elim_ty (c : ctx) (A : ty c) {struct A} : Q c (elim_ctx c) A := todo
    for elim_ctx.

  (* Recursive call to elim_ctx has principal argument equal to  *)
  (* "c0" instead of a subterm of "A". *)
  (* Recursive definition is: "fun (c : ctx) (A : ty c) => todo". *)

  Definition elim_ctx : forall c, P c :=
    fix elim_ctx (c : ctx) {struct c} : P c :=
      match c return P c with
      | nil => hnil
      | snoc G A => hsnoc G A (elim_ctx G) (elim_ty G A)
      end
    with elim_ty (c : ctx) (A : ty c) {struct A} : Q c (elim_ctx c) A :=
        match A as A0 in ty c0 return Q c0 (elim_ctx c0) A0 with
        | Nat G => hNat G (elim_ctx G)
        end
    for elim_ctx.

Thanks for the help @Gaëtan Gilbert

view this post on Zulip Gaëtan Gilbert (Oct 07 2020 at 14:33):

(* Recursive definition is: "fun (c : ctx) (A : ty c) => todo". *)

with implicit arguments that's @todo (Q c (elim_ctx c))
it might work if instead of being an axiom you define todo as an empty match, ie

Axiom todo_ax : False.
Definition todo {T:Type} : T := match todo_ax with end.

view this post on Zulip Kenji Maillard (Oct 07 2020 at 14:38):

Surprisingly it does not work with the match trick either...

Recursive call to elim_ctx has principal argument equal to
"c" instead of a subterm of "A".
Recursive definition is:
"fun (c : ctx) (A : ty c) => match todoF return (Q c (elim_ctx c) A) with
                             end".

view this post on Zulip Matthieu Sozeau (Oct 07 2020 at 14:40):

Well you see the recursive call here :)

view this post on Zulip Matthieu Sozeau (Oct 07 2020 at 14:41):

I think it would work if you put todos in the branches instead

view this post on Zulip Kenji Maillard (Oct 07 2020 at 14:42):

Yes, fair enough. But the "same" recursive occurence appear in the accepted definition, no ? I will try the trick in the branches.

view this post on Zulip Gaëtan Gilbert (Oct 07 2020 at 14:42):

I thought it didn't check the return?

view this post on Zulip Kenji Maillard (Oct 07 2020 at 14:44):

Indeed, once the main argument is matched upon it is accepted. Good to know but a bit surprising...

view this post on Zulip Matthieu Sozeau (Oct 07 2020 at 15:22):

@Gaëtan Gilbert that's the good thing, guard checking is no longer hacked now. It considers all indices (here c) smaller than the recursive argument (here A). So in the return clause c has to be smaller than A and that only happens when you actually match on A.

view this post on Zulip Kenji Maillard (Oct 07 2020 at 15:29):

Matthieu Sozeau said:

So in the return clause c has to be smaller than A and that only happens when you actually match on A.

How does that happen ??

view this post on Zulip Gaëtan Gilbert (Oct 07 2020 at 15:32):

match A as A0 in ty c0 return Q c0 (elim_ctx c0) A0

in ty c0 binds c0 in the return and makes it smaller than A

view this post on Zulip Ali Caglayan (Nov 09 2020 at 13:22):

@Matthieu Sozeau Any progress with this recently?

view this post on Zulip Matthieu Sozeau (Nov 10 2020 at 08:13):

I discussed a restricted design with @Kenji Maillard, I'll get back to it next week I hope.

view this post on Zulip Ali Caglayan (Dec 29 2020 at 01:53):

@Matthieu Sozeau Any progress with this?

view this post on Zulip Jasper Hugunin (Mar 09 2021 at 00:59):

I wrote a Coq pearl that might be of interest to folks in this thread. It turns out that Definitional UIP for SProp makes it straightforward (relatively speaking; it's still pretty complicated) to construct Inductive-Inductive types in Coq, satisfying definitional computation rules for the general eliminator. Definitional UIP gets you close enough to extensional type theory that you can just "do as Forsberg did", and perform a 2-layer construction. You can see the formalization of an example at this repository in the file theories/Example.v; it is easy to generalize to other II types as well. If you want II types in Coq today, and are willing to accept UIP (so no HoTT), this might be the way to go.

view this post on Zulip Matthieu Sozeau (Mar 09 2021 at 08:28):

Wow, that's impressive!

view this post on Zulip Ali Caglayan (Mar 27 2021 at 15:05):

@Matthieu Sozeau Any progress?

view this post on Zulip Ali Caglayan (Mar 27 2021 at 17:14):

@Jasper Hugunin That construction of IndInd types is very cool! I've only had time to look at it now. Are you able to describe in words what is going on in the stage1 and stage2 parts?

I wonder if it possible to write a plugin that turns an inductive inductive definition into one defined like that?

view this post on Zulip Ali Caglayan (Mar 27 2021 at 17:15):

I also don't think the use of SProp is such an issue btw, since we don't even touch SProp in the library, I am not sure if you are able to even draw a contradiction from this.

view this post on Zulip Ali Caglayan (Mar 27 2021 at 17:16):

I imagine it might be possible to mark all the defined parts of the type as opaque allowing it to compute, but not unfold to show the SProp stuff

view this post on Zulip Jasper Hugunin (Mar 27 2021 at 18:15):

@Ali Caglayan Glad you liked it! It would certainly be possible to write a plugin for this, but I do not have plans to do it anytime soon.

You should also be able to perform the general construction internally: define a type of inductive inductive definitions/specifications/codes, and a Gallina function that takes a code and returns a type + constructors + eliminator (+ computation rules as propositional equalities, which compute to eq_refl on concrete cases).

The problem with SProp is that I also need Definitional UIP, which turns out to imply UIP for equalities in Prop or in Type (with -indices-matter, like in HoTT). If you turn that option off after you are done defining an II type, I think that the eliminator stops computing (haven't tested this).

Making things opaque to tactics like simpl is not strong enough to give consistency guarantees; the kernel will happily silently break that abstraction barrier. And if you make them Qed. opaque, they stop computing.

For stage1 we try to compute the eliminator, but we end up with some side conditions saying that a certain passed-in proof of PA for the index is equal to what we can compute the proof of PA for the index should be. This will always be true when we need it to, based on how we are defining stage1, but we don't have access to that fact yet because stage1 is in the middle of being defined, and we had to introduce an abstraction. So instead we throw that side condition into Q, which can be an SProp since we have Definitional UIP. Once we finish all that up, we find that Q turns out to have the same shape that P did: it is another dependent/slice algebra over A and B, but effectively at one hlevel lower (since it is built from conjunctions of paths in P), so now a (strict) proposition rather than a set. So we do the same thing once more, only this time when we run into those side conditions, they are that we need to know equality of two proofs of Q. But Q is an SProp, so this is trivial, so we get a proof that Q always holds where we need it to, and since Q implies P, P also holds where we need it to.

Another way of thinking about stage1 (and I should have made this abstraction in the code) is that we are working in a monad of partial values: F X := Σ (Q : SProp), Q -> X, and proving P under this monad. Then the cases in stage1 look like

| pre_eta x =>  fun ga => return Peta x
| pre_ext pa pb => fun '(conj ga gb) => let a : A := sub_in pa ga in let b : B a := sub_in pb gb in
  let* Pa := stage1A pa ga in
  let* Pb := stage1B pb a gb Pa in
  return Pext a b Pa Pb
...
| pre_inj pa => fun '(sub_in pphi gphi) '(conj ga pe : goodB (pre_inj pa) (sub_in pphi _).(wit)) (Pphi : PA (sub_in pphi gphi)) =>
    match pe in Id _ pphi
    return
       (gphi : goodA pphi) (Pphi : PA (sub_in pphi gphi)),
      F (PB (sub_in pphi gphi) (sub_in (pre_inj pa) (conj ga pe)) Pphi)
    with refl => λ (gphi : goodA pa) Pphi 
      let a : A := sub_in pa ga in
      let* Pa := stage1A pa ga in
      assume (Id Pa Pphi) fun 'refl =>
      return Pinj a Pq
    end gphi Pphi

Where assume has type forall {X : Type} (R : SProp), (R -> F X) -> F X, letting you assume whatever SProps you want. (Morally, this is a bind combined with assume : forall (R : SProp), F R, but you run into the lack of cumulativity if you go that way.)

view this post on Zulip Jasper Hugunin (Mar 27 2021 at 18:20):

Since the stage1 construction takes a slice algebra and returns a slice algebra one hlevel lower, I believe that it should be possible to get the (non-computing) general eliminator from the simple eliminator, which is all that stage1 uses (which I showed how to get in cubical type theory (though again non-computing) in a previous paper, and I believe that it should work with axiomatic function extensionality) by iterating the stage1 construction and taking the limit, which I believe should be a contractible slice algebra, thus provably inhabited.

view this post on Zulip Jasper Hugunin (Mar 27 2021 at 18:26):

Oh yes, and another way of looking at the stage1 construction is that it can be put into the form of the simple eliminator for an inductive-inductive type, that is, with PB b a not indexed by PA. Indeed, that looks like simplePA '(sub_in pa ga) := Σ (Q : SProp), Q → PA (sub_in pa ga), and simplePB '(sub_in pb gb) (phi : A) := forall (Pa : PA phi), Σ (Q : SProp), Q → PB phi (sub_in pb gb) Pa (and there is some variation possible as to whether to have that quantifier in simplePB be forall or exists; both work, and they give similar proofs, just shifting a few parts around).

view this post on Zulip Ali Caglayan (Mar 27 2021 at 18:42):

Thank you for the detailed explanation!

view this post on Zulip Ali Caglayan (Mar 27 2021 at 18:42):

I noticed that your example looks like Types and Contexts with a single unit type btw.

view this post on Zulip Ali Caglayan (Mar 27 2021 at 18:42):

Also Unsetting UIP still allows it to compute from what I am observing.

view this post on Zulip Gaëtan Gilbert (Mar 27 2021 at 19:16):

The problem with SProp is that I also need Definitional UIP, which turns out to imply UIP for equalities in Prop or in Type (with -indices-matter, like in HoTT). If you turn that option off after you are done defining an II type, I think that the eliminator stops computing (haven't tested this).

the option applies at the time of defining an inductive type, so you only need it around the declaration of eq-in-sprop
Also I think -indices-matter is stronger than uip, but didn't check

view this post on Zulip Jasper Hugunin (Mar 28 2021 at 04:39):

OK, so you could turn the option off to prevent defining other inductives in SProp that shouldn't be, and things will still compute, but you will still have an inconsistent system once you assume Univalence, since you will still be able to prove UIP using eq-in-SProp. (which might/should have to be in a file compiled without -indices-matter).

view this post on Zulip Jasper Hugunin (Mar 28 2021 at 04:42):

Yes, the example is almost exactly types and contexts with a single base type defined in every context. We just have X empty contexts rather than 1, to include an arbitrary type. There are plenty of other ways of defining this specific example (particularly, A := X * list unit, B _ := unit works), but it is still complex enough that you can usually tell when you have a natural/generalizable translation (at least for people who have spent a certain amount of time thinking about the problem).

view this post on Zulip Jasper Hugunin (Mar 28 2021 at 04:51):

I previously proved (in the paper Constructing Inductive-Inductive Types in Cubical Type Theory) that the simple eliminator with propositional computation rules for Forsberg's construction of this exact type implies UIP for X; this result is a sort of converse: definitional UIP means the general eliminator for Forsberg's construction is definable and has strict computation rules.

view this post on Zulip Matthieu Sozeau (Mar 29 2021 at 14:48):

Ali Caglayan said:

Matthieu Sozeau Any progress?

Not yet. I'm focused on some long-awaited typeclass stuff at the moment, but ind-ind is next in line


Last updated: Oct 16 2021 at 02:03 UTC