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 :)
Not sure if you saw this, but I also had a question about moving erasure's eval into Type.
Last updated: Feb 09 2023 at 03:06 UTC