Jason Gross (Nov 03 2022 at 17:05): 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?
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?
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?
Jason Gross (Nov 03 2022 at 17:49):(It seems to me that requiring wf should enforce dagness)
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
Jason Gross (Nov 03 2022 at 17:53):Yes
Jason Gross (Nov 03 2022 at 17:54):Wait, not quite that
Jason Gross (Nov 03 2022 at 17:56):wf_local Σ Γ -> wf_local Δ Γ -> Permutation Σ Δ -> forall t T, Σ ;;; Γ ⊢ t : T -> Δ ;;; Γ ⊢ t : T
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
Yannick Forster (Nov 07 2022 at 14:21):(he's on holidays this week though)
Meven Lennon-Bertrand (Nov 07 2022 at 14:26):Let's see what he has to say when he returns :)
Matthieu Sozeau (Nov 23 2022 at 12:54):If both Sigma and Delta are well-formed then it's an easy theorem to prve
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?
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
Jason Gross (Dec 14 2022 at 16:29):Created a PR at https://github.com/MetaCoq/metacoq/pull/816
Last updated: Oct 13 2024 at 01:02 UTC