Stream: MetaCoq

Topic: de Bruijn indices while declaring inductive

Pierre Vial (Sep 22 2020 at 12:05):

Hi,
I'm looking for some input concerning the way de Bruijn indices are introduced in the reified declaration of an iinductive. Let us consider the classic odd and odd declaration:

Inductive odd : nat -> Prop := oddS : forall n:nat, even n -> odd (S n)
with even : nat -> Prop :=
  | evenO : even 0
  | evenS : forall n:nat, odd n -> even (S n).

If I quote the environement used to define evenS, I obtain:

MetaCoq Quote Recursively  Definition evenS_env_reif := evenS.

If I print evenS_env_reif, Il will obtain this inside the environment:

("oddS",
      tProd (nNamed "n")
       (tInd {|  inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");  inductive_ind := 0 |} [])
                                   (tProd nAnon (tApp (tRel 1) [tRel 0])  (tApp (tRel 3)
                                         [tApp  (tConstruct
                                               {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"],  "nat");  inductive_ind := 0 |} 1 []) [tRel 1]])), 2)

This corresponds to how oddS has been declared. If I want to make the above code more readable, let nat_reif and S_reif be the reification of nat and S and the above output tells me that oddSis declared this way:

tProd "n" nat_reif.
       tProd nAnon  App (Rel 1) (Rel 0)).
             App   (Rel 3) (App S_reif (Rel 1) )

In the above ouput, the first occurrence of Rel 1 denotes even and the occurrence of Rel 3 denotes odd.
This means that evenS is the last variable in the environment and that oddS is the second-to-last.
This is understandable, because odd is the first inductive block and even the second one, but how come the constructor even0 is not in the environment? (if it were, it should come between oddS and evenS and we should have Rel 4 instead of Rel 3 if I am correct)

Gaëtan Gilbert (Sep 22 2020 at 12:15):

constructors don't go in the environment
the surrounding environment is just odd then even
App (Rel 1) (Rel 0) is in the surrounding env extended with n : nat so Rel 0 is n and Rel 1 is even
App (Rel 3) (App S_reif (Rel 1)) is in the surrounding env extended with n : nat and _ : even n so Rel 3 is odd and Rel 1 is n

Pierre Vial (Sep 22 2020 at 12:33):

So basically, when a mutual inductive block I is declared (defining inductive types I(0), I(1),..., I(n)), the surrounding environment are the inductive in the order that they appear?

Matthieu Sozeau (Sep 22 2020 at 12:44):

Yes, followed by the parameters (if any). The typing rules in EnvironmentTyping are the definitive source :)

Pierre Vial (Sep 22 2020 at 13:03):

thanks @Gaëtan Gilbert and @Matthieu Sozeau !

Last updated: Jun 01 2023 at 11:01 UTC