Jakob Botsch Nielsen (Sep 12 2020 at 15:32): Jakob Botsch Nielsen (Sep 12 2020 at 15:32):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.
Jakob Botsch Nielsen (Sep 12 2020 at 15:35):The semantics of allowing this also seems a bit weird, at least if you're thinking with respect to typing
Matthieu Sozeau (Sep 14 2020 at 23:20):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.
Jakob Botsch Nielsen (Sep 15 2020 at 08:46):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.
Matthieu Sozeau (Sep 15 2020 at 19:21):Well, it ended up well :)
Jakob Botsch Nielsen (Sep 15 2020 at 19:23):Yep :)
Not sure if you saw this, but I also had a question about moving erasure's eval into Type.
Last updated: Jun 01 2023 at 13:01 UTC