Is there a reason why the evaluation relations allow projecting out of any constructor (rather than just the first)? It gives a weird mismatch since `tProj`

contains the inductive and the index of the constructor parameter, but not which constructor it expects (and indeed, this wouldn't really make sense). For example, I would expect something like

```
| eval_proj : forall (i : inductive) (pars arg : nat) (discr : term) (args : list term)
(k : nat) (res : term),
Σ ⊢ discr ▷ mkApps (tConstruct i k) args ->
Σ ⊢ nth (pars + arg) args tDummy ▷ res -> Σ ⊢ tProj (i, pars, arg) discr ▷ res
```

to instead be

```
| eval_proj : forall (i : inductive) (pars arg : nat) (discr : term) (args : list term)
(res : term),
Σ ⊢ discr ▷ mkApps (tConstruct i 0) args ->
Σ ⊢ nth (pars + arg) args tDummy ▷ res -> Σ ⊢ tProj (i, pars, arg) discr ▷ res
```

We are proving some optimization passes correct with respect to erasure's evaluation relation but this mismatch requires us to do carry through some wellformedness conditions that we would not otherwise need.

The semantics of allowing this also seems a bit weird, at least if you're thinking with respect to typing

That's because most of our proofs assume well-typedness of the thing you reduce, where you can prove that k = 0 always, I think your rule is indeed better, and simpler.

I will submit a PR then. The question is if I should stick to wcbv evaluation relations or also try to change this in `red1`

. I'm not sure how breaking the latter would be.

Well, it ended up well :)

Yep :)

Not sure if you saw this, but I also had a question about moving erasure's eval into Type.

Last updated: Jul 24 2024 at 13:02 UTC