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
If X is monomorphic, then this holds, otherwise you need the universe instantiation lemma
What's the universe instantiation lemma? / where is it?
(What I have is that
X is equal to the
cst_universes of some
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.
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
Maybe you should rather work with an empty_ext \Sigma rather than an arbitrary extension
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?
Last updated: May 31 2023 at 02:31 UTC