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

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?

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

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

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

Yes

Wait, not quite that

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

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

(he's on holidays this week though)

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

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

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?

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

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

Last updated: Nov 29 2023 at 06:01 UTC