As some of you might already know, I am trying to formalize and publish minimal formalization that is easy to follow for inductive families. I am asking here, because the only other formalization of inductive families exists in metacoq, but the code has many levels of generalizations that makes it hard to follow and understand. I will try to ask all my questions in this thread at different points in time.

The problem I am currently facing is the following: I describe inductive families as follows:

```
Record InductiveDef := mkInductiveDef {
induct_name: string;
(*in Dybjer 3.1.1 (A :: σ) *)
(*induct_params: ClosedContext 0 induct_param_size; (* TODO make this seq?*)*)
induct_params: ScopedContext 0;
(*induct_indices_size: nat;*)
induct_indices: ScopedContext (scoped_context_size induct_params);
(* this is instead of the set part in 3.1.1*)
induct_universe: nat;
(* Dybjer 3.2.1, there are finitely many introduction rules for each set *)
(* former ... here goes the finitely many rules.*)
induct_constrs: seq (InductiveConstructor (scoped_context_size induct_params));
}.
```

Where scoped context is which is used for induct_params, and induct_indices is defined as follows:

```
Inductive ScopedContext (n: nat): Type :=
| Cempty : ScopedContext n
| Ccons (t: Term): Scoped t n -> ScopedContext (S n) -> ScopedContext n.
```

Then I have a term for eliminators:

```
Inductive Term : Type :=
.....
| rec
(* name of the inductive type we are recursing on *)
(n: string)
(params: seq Term)
(* output type of the recursion branch. it is a function that depends on *)
(* params. But params are not argument. so we need to substitute them *)
(* directly *)
(C: Term)
(* what do to for every constructor*)
(branches: seq Term)
(* I₀ ... Iₙ*)
(indices: seq Term)
(* the main argument to provide to the recursor function *)
(arg: Term).
```

I would like to think I figured out everything except one part, the fact that `params ++ indices`

have the type of `induct_params ++ induct_indices`

. The reason I think everything else is figured out because I have confluence proven and stability lemmas proven except for that one part being admitted.

But it is more complex than that because `(induct_params ++ induct_indices)[1]`

depends on `(params ++ indices)[0]`

...etc so it it is not simply a relation on elements of two lists.

I tried coming up with custom relation that is not mutually inductive ... but that was a mistake as in here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/I.20cannot.20find.20provable.20good.20properties.20for.20telescopes

So instead What I did is the following:

defined a function that substitutes elements into from `params ++ indices`

into `induct_params ++ induct_indices`

as follows:

```
Fixpoint subst_params_indices (pi: seq Term) (PI: seq Term): (seq Term) :=
match pi, PI with
| nil, _ => PI
| _, nil => nil
| p::pi', P::PI' => P:: (subst_params_indices pi' (imap (fun i => subst (upn i (p .: ids))) PI'))
end.
```

the intution is we always leave the first element of `induct_params ++ induct_indices`

and then for every element replace `var i`

with the first element of `params ++ indices`

where i is the index in the list recursively.

Then the relation that describes typing for parameters and indices in`rec n p c b i a`

is

`seq_forall_pair (fun pi PI => Σ; Γ ⊢ pi: PI) pis (subst_params_indices pis pi_tys)`

Where seq_forall_pair is defined as follows:

```
Definition seq_forall_pair A B (R: A -> B -> Prop) s1 s2 :=
size s1 = size s2 /\ forall ts, PIn ts (zip s1 s2) -> R (ts.1) (ts.2).
```

That should be good (I also need to make sure to say that the paramters and parameter types have the same size ..).

The problem is unlike most recursive function `subst_params_indices`

is calling another recursive function on the list we are supposed to be recusing on. That makes proving anything about this function, painful. I can give examples later, but my question here, was there a similar problem for typing parameters and indices in metacoq? and is there a way to avoid all that.? Any general advice will be useful.

Something I don’t understand here is that do branches ++ indices mean ? You are concatenating the branches bodies and the actual indices of the term to match ? That sounds strange

indeed it is strange, it was a typo, I wrote branch + indices instead of params + indices once and copy paste everywhere. I fixed it.

it is params + indices as terms when drawn from `rec`

term and they are types when drawn from inductive definition.

An example is this:

```
Definition dsumpi_induct :=
@mkInductiveDef
"dsumpi"
(@Ccons _ (univ 0) (Ui_scoped _ _) (@Cempty _))
(@Ccons _ (pi (var 0) (univ 0)) dsum_pi_scoped (@Cempty _))
5
((@mkInductiveConstructor 1 dpairpi_ctor dpairpi_scoped
)::
nil).
```

Dependent sum with one parameter and one index (mainly for testing). Then this funtion calculates the first projection:

```
Definition fst_rec := (* A (A->B) (A, B)*)
lam (lam (lam (rec
(* n *) "dsumpi"
(* p *) ((var 2)::nil)
(* c *) (lam (lam (var 4)))
(* b *) ((lam (lam (lam (var 1))))::nil)
(* i *) ((var 1)::nil)
(* a *) (var 0)
))).
```

In the process of type checking I need to type check that:

```
seq_forall_pair
(*Terms here come from lambda expressions going to context*)
(fun pi : Term => [eta SynType Σ [:: appl (appl (induct "dsumpi") (var 1)) (var 0), term.pi (var 0) (univ 0), univ 0 & Γ] pi])
(* this is taken from p and i *)
[:: var 2; var 1]
(* this is taken from (@Ccons _ (univ 0) (Ui_scoped _ _) (@Cempty _)) and (@Ccons _ (pi (var 0) (univ 0)) dsum_pi_scoped (@Cempty _))
*)
(subst_params_indices [:: var 2; var 1] [:: univ 0; pi (var 0) (univ 0)])
```

The equivalent relation in MetaCoq is `ctx_inst`

, defined in `common/EnvironmentTyping.v`

and mostly used in `pcuic/PCUICTyping.v`

.

Since it is parametric in the typing relation, the way proofs go is that you have `ctx_inst typing (params + indices) (params_typ + indices_typ)`

and `ctx_inst P (params + indices) (params_typ + indices_typ)`

where P is the property you're trying to prove, and from there you go by induction on both. See for example `pcuic/Typing/PCUICRenameTyp.v#L913-L928`

.

This very interesting, it is almost the same as the relation I was struggling with at :https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/I.20cannot.20find.20provable.20good.20properties.20for.20telescopes

I thought it was useless because I couldn't prove a single thing about it. I see one difference, I assumed the function to be mapped to be arbitrary, but you fixed it to substitution. given that this is the only difference I can see, It almost feels like this is all its takes to meke good properties appear.

Wanted to do a bit of update here, I think I found a nice generalization!

The idea of `ctx_inst`

is similar to `ListRel`

but it was hard for me to work with ( at least with listRel)

What I did is come up with a funcion equivalent to `subst_params_indices`

where stuff can be proven by induction as the there is no nested inducton!

this was the copy I came up with:

```
Fixpoint subst_params_indices (pi: seq Term) (PI: seq Term) (σ: nat -> Term): (seq Term) :=
match pi, PI with
| nil, _ => PI
| _, nil => nil
| p::pi', P::PI' => P.[σ]:: (subst_params_indices pi' PI' (p .: σ))
end.
```

With that being said I now have all proofs of stabilities as well as confluence done! I was pain staggering process

I think it was a recurring theme in my implementation to have this pattern of keeping an aditional substition on the side which keeps changing every recurive call

I am not sure if there a simple primitive function for lists that does that, I think, what I am doing informally is map+ keep history of what is being mapped before.

Would it make sense that preservation is not provable directly for single step reduction?

The situation that lead to that is the following:

in my system preservation looks like:

```
Σ; Γ ⊢ t: T ->
⊢ Σ; Γ ->
Σ ⊢ t ⟶ t' ->
Σ; Γ ⊢ t' : T.
```

But there is always that case of inductive types, and one of the cases you need to prove is something that is on the form of:

```
Σ; Γ ⊢ t .[something containing s'] : T
```

But What we have is:

```
H1: Σ; Γ ⊢ t .[something containing s ] : T
H2: Σ ⊢ s ⟶ s'
```

and the induction principle we have allows us to reduce the goal to:

```
Σ ⊢ t .[something containing s ] ⟶ t .[something containing s']
```

but that is not true, it would have been true for multi step Redution. which makes me think that maybe the property I should have been proving is the general reduction that is:

```
Σ; Γ ⊢ t: T ->
⊢ Σ; Γ ->
Σ ⊢ t ⟶* t' -> (* note multi step *)
Σ; Γ ⊢ t' : T.
```

and from there, prove the case for single step. Is that known problem that appear when proving preservtion, or maybe my typing rule would need modification to make this work, or perhaps the cause is that I took wrong turn when doing the proof (I am just following my nose here) ?. I ca provide more information, but I don't want to provide more information than necessary to avoid making the question much longer.

apparently doing multi step is very very painful, at some point I had to maintain custom inversion principle for things like:

`Σ ⊢ rec n p c b i a ⟶ t`

now doing it for multi_step reduction is much much harder.

It's a bit difficult to judge from what you are giving us, but my bet is that you should be able to use the induction hypothesis corresponding to `H2`

to "replace" `s`

by `s'`

in `H1`

in a type preserving way. This should be a general lemma, saying roughly that replacing a subterm by another subterm with the same type and convertible to it should preserve typability.

What's clear to me is that not being able to prove preservation for single step reduction directly is strange.

I second this, you should be able to prove it directly by induction on the reduction step and inversion on the typing of the redex. `t.[something containing s]`

makes me think maybe you formalized the congruence rules for one step reduction in some special way?

Matthieu Sozeau said:

makes me think maybe you formalized the congruence rules for one step reduction in some special way?

Actually I think it might be the typing that is formalized in in non-proof friendlly way:

So basically the constructor for recursion principle is `rec n p c b i a: Term`

where `n`

is string which name of the inductive family in question `p: seq Term`

which is list of parameters, `c: Term`

is the motive, `b`

is list of branches, `i`

is list of indices and a is the argument.

For single step reduction there is this this rule:

```
| Reduction_recp: forall Σ n p c b i a p' s t l1 l2,
(*on_one (Reduction Σ) p p'*)
Σ ⊢ s⟶t ->
p = l1 ++ s::l2 ->
p' = l1 ++ t::l2 ->
Σ ⊢ rec n p c b i a ⟶ rec n p' c b i a
```

Now for type checking, we have this substitution:

```
SynType_rec:
....
σ = foldl (fun σ t => t .: σ) ids p ->
.....
```

it is used in two places, but one of them is type checking the motive `c`

:

```
(*first we get the type of parameter, indices *)
p_types = scoped_context_to_pi_order (induct_params body) ->
i_types = scoped_context_to_pi_order (induct_indices body) ->
pi_tys = p_types++i_types ->
....
C = ((make_pi (rcons i_types (foldl (fun a b => appl a b) (induct n) (vars (size (pi_tys))))) (univ l))).[σ] ->
....
Σ; Γ ⊢ C : univ l' -> (* the trouble maker (so far) maybe there are others *)
Σ; Γ ⊢ c : C ->
```

The problem arises when we we single step an element in `p`

, we get stuck on type checking `C`

becaue we substitute `p`

or the resolt of reduction in the term we are type checking rather than the type.

Thinking outloud makes me think, maybe the type relation should be changed to:

```
(*first we get the type of parameter, indices *)
p_types = scoped_context_to_pi_order (induct_params body) ->
i_types = scoped_context_to_pi_order (induct_indices body) ->
pi_tys = p_types++i_types ->
....
C = ((make_pi (rcons i_types (foldl (fun a b => appl a b) (induct n) (vars (size (pi_tys))))) (univ l))) ->
....
Σ;(rev p_types):: Γ ⊢ C : univ l' -> (* the trouble maker (so far) maybe there are others *)
Σ; Γ ⊢ c : C.[σ] ->
```

Then it is no longer problem, typechecking `C`

no longer depends on anything that redues, but this idea just came right now while writing so I might as well leave it here for confirmation :D.

It worked so far, but something tells me there will be more problems: and the correct type checking rule for `C`

(the type f motive) no longer depends on `Γ`

so the rule is much simpler:

```
.... ->
Σ;(rev p_types) ⊢ C : univ l' ->
....
```

the only thing is I am not sure if this is necessary or not, and I don't have the right instincts to tell

That might not be very relevant to your problem, but why do you want to reduce a single parameter a step at a time in the eliminator ?

If you want to describe a normalizing evaluation strategy, then I would follow the standard "cbn" strategy and only evaluate the main argument and not the other arguments. And if you want to show a confluence or standardization theorem (e.g. every possible reduction path in any order can be reduced to a standard reduction path) then I would focus on parallel reduction.

Kenji Maillard said:

That might not be very relevant to your problem, but why do you want to reduce a single parameter a step at a time in the eliminator ?

That is a good question, I dont have good answer unfortuntely aside from saying it felt natural to me to do that since it is single stepping and single is single.

As to what I am doing with the reduction, I am proving type safety ... but also producing algorithm for type checking and conversion checking (weak head normalization or that is what I think I am doing).

For weak-head normalization, I think you should only reduce `a`

and not any of the parameters

It is problematic if one of the terms that is reduced is duplicated in the subject position of any of the typing premises as indeed then induction would fail. The context or type positions should be fine as you can prove context conversion before type preservation or use the conversion rule to reestablish these premises.

Last updated: Jul 23 2024 at 20:01 UTC