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 `oddS`

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

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`

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?

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

thanks @Gaëtan Gilbert and @Matthieu Sozeau !

Last updated: Apr 21 2024 at 01:02 UTC