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`

?

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 `ConstantDecl`

in `Σ.2`

)

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: Jun 22 2024 at 23:01 UTC