Stream: MetaCoq

Topic: red_proj, eval_proj and multi-constructor inductives


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Sep 15 2020 at 19:21):

Well, it ended up well :)

view this post on Zulip 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: Aug 11 2022 at 03:02 UTC