Changing global universes in typing · MetaCoq

Suppose I want to prove wf_ext Σ -> wf_ext (Σ.1, X) -> (Σ.1, X);;; Γ |- t1 : T -> Σ;;; Γ |- t1 : T. Is there a lemma that proves something like this? And what's the relationship I need between X and Σ.2?

Matthieu Sozeau (Dec 06 2022 at 19:58):

If X is monomorphic, then this holds, otherwise you need the universe instantiation lemma

Jason Gross (Dec 06 2022 at 20:03):

Jason Gross (Dec 06 2022 at 20:04):

(What I have is that X is equal to the cst_universes of some ConstantDecl in Σ.2)

Jason Gross (Dec 06 2022 at 22:04):

Hm, it seems that all the lemmas in PCUICWeakeningEnvTyp that are close to what I want have the implication in the wrong direction. I want to show that if normalisation holds in Σ, then normalisation will still hold after replacing the universe context of Σ with the universe context from some declaration in Σ. I guess this is actually a kind-of tricky lemma, because we can't just port the typing judgment.

Matthieu Sozeau (Dec 07 2022 at 16:46):

The theorem's in PCUICUnivSubstitutionTyp. In the case X is a universe polymorphic extension, then Gamma, t1 and T might depend on universes that would become free in Sigma, so you'll need to find an instantiation for those, in the original \Sigma. Maybe you should rather work with an empty_ext \Sigma rather than an arbitrary extension

Jason Gross (Dec 07 2022 at 22:39):

This is unfortunately not a freedom I have. Erasure needs to know that normalisation holds in the context of the universes of every polymorphic definition in the global environment. It would be nice if knowing that normalisation holds in the global environment is enough to know that normalisation holds in the context of every constant defined in that environment. So I need to prove something like

∀ ϕ,
(exists kn cb, lookup_env Σ kn = Some (ConstantDecl cb) /\ cst_universes cb = ϕ)
→ wf_ext (Σ, Monomorphic_ctx)
→ wf_ext (Σ, ϕ)
→ (∀ Γ t T, ((Σ, Monomorphic_ctx) ;;; Γ |- t : T) → Acc (cored Σ Γ) t)
→ (∀ Γ t T, ((Σ, ϕ) ;;; Γ |- t : T) → Acc (cored Σ Γ) t)

So I was hoping that I could just reuse the same term and prove that ((Σ, ϕ) ;;; Γ |- t : T) → ((Σ, Monomorphic_ctx) ;;; Γ |- t : T) , but it seems like this is not the case. Instead I need to find some instantiation of the universes in ϕ that is consistent with the given typing derivation (is there an easy way to find such? is there a lemma already for this?), perform the substitution (importantly it must be a no-op on Σ), and then translate the cored proof across the substitution so that I can recover Acc. Does this sound right?

Stream: MetaCoq