Stream: MetaCoq

Topic: Global environment extension modulo ordering


view this post on Zulip Jason Gross (Nov 03 2022 at 17:05):

Is there a notion of extension of global environments which doesn't care about ordering of declarations?

view this post on Zulip Théo Winterhalter (Nov 03 2022 at 17:13):

We don't have that, and in the most naive interpretation order does matter. I guess you mean that it should be a dependence DAG rather than a list?

view this post on Zulip Jason Gross (Nov 03 2022 at 17:48):

Is it possible to have two wf environments that differ only in order of declarations which are semantically different?

view this post on Zulip Jason Gross (Nov 03 2022 at 17:49):

(It seems to me that requiring wf should enforce dagness)

view this post on Zulip Gaëtan Gilbert (Nov 03 2022 at 17:53):

sounds lke you want a proof of something like wf Γ -> wf Δ -> Permutation Γ Δ -> forall t T, Γ ⊢ t : T -> Δ ⊢ t : T

view this post on Zulip Jason Gross (Nov 03 2022 at 17:53):

Yes

view this post on Zulip Jason Gross (Nov 03 2022 at 17:54):

Wait, not quite that

view this post on Zulip Jason Gross (Nov 03 2022 at 17:56):

wf_local Σ Γ -> wf_local Δ Γ -> Permutation Σ Δ -> forall t T, Σ ;;; Γ ⊢ t : T -> Δ ;;; Γ ⊢ t : T

view this post on Zulip Meven Lennon-Bertrand (Nov 07 2022 at 14:20):

If I remember correctly, @Kenji Maillard hit a difficulty like this at some point (trying to stitch together two different environments), not sure how he got out of this but he may have something to say

view this post on Zulip Yannick Forster (Nov 07 2022 at 14:21):

(he's on holidays this week though)

view this post on Zulip Meven Lennon-Bertrand (Nov 07 2022 at 14:26):

Let's see what he has to say when he returns :)

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:54):

If both Sigma and Delta are well-formed then it's an easy theorem to prve

view this post on Zulip Jason Gross (Nov 23 2022 at 13:44):

Yes, I'm interested in proving this when Sigma and Delta are well-formed. The context for this is that I want to run the safe checker on a concrete env and with concrete checker flags, and then apply a weakening theorem to the resulting typing derivation to get that my term is well-typed in any Env with enough stuff and with any checker flags that don't matter for that typing derivation.

What's the proof sketch?

view this post on Zulip Matthieu Sozeau (Nov 24 2022 at 11:36):

I think you just need to apply typing_ind_env, like in most of the toplevel theorems like weakening and substitution. Maybe start from the proof of PCUICWeakiningEnv as it's going to be similar. Or even better, generalize that one to the minimal assumption that the new environment gives the same results on lookup's than the initial one, then both theorems will follow

view this post on Zulip Jason Gross (Dec 14 2022 at 16:29):

Created a PR at https://github.com/MetaCoq/metacoq/pull/816


Last updated: Jan 30 2023 at 18:04 UTC