Syntactic properties of top-level defs

[jiangsy]

No description provided.

[jiangsy]

I still think we need to add explicit [Wk] in typing rules including but not limited to wf_gvlookup, otherwise it's really difficult to prove the following thm

Lemma gctx_presup_weakening_ctx_nil : forall {Δ Γ A M},
    {{ Δ ;; ⋅ ⊢ M : A }} ->
    {{ ⊢ Δ ;; Γ }} ->
    {{ Δ ;; Γ ⊢ M : A }}.

This form cannot be proved by induction, what we can is to prove its generalization

Lemma gctx_presup_weakening_ctx : forall {Δ Γ Γ' A M},
    {{ Δ ;; Γ ⊢ M : A }} ->
    {{ ⊢ Δ ;; Γ ,++ Γ' }} ->
    {{ Δ ;; Γ ,++ Γ' ⊢ M : A }}.

but this form is incorrect, because now M and A may contain local vars, so we have to add weakening to this to let it become

Lemma gctx_presup_weakening_ctx' : forall {Δ Γ Γ' A M},
    {{ Δ ;; Γ ⊢ M : A }} ->
    {{ ⊢ Δ ;; Γ ,++ Γ' }} ->
    {{ Δ ;; Γ ,++ Γ' ⊢ ^(iter (S (length Γ')) (fun N => {{{ N[Wk] }}}) M) : ^(iter (S (length Γ')) (fun B => {{{ B[Wk] }}}) A) }}.

[HuStmpHrrr]

the direction of the generalization is wrong. it should be to the left, i.e. Γ' ,++ Γ instead.

[jiangsy]

but to prove weakening, we have to let the context grow on the right, because some rules adds a new entry on the right (e.g. Pi formation rule)

and you also agree with @Ailrun that we don't need to change the typing rule to add explicit weakenings?

[HuStmpHrrr]

yes, the context grows on the right, so what adds to the local context needs no change. the extension is to the left of what exists.

[HuStmpHrrr]

this lemma is provable without any modification to the theory if generalization is done in this way.

[jiangsy]

it works

[jiangsy]

just to make point clear that the current syntax don't introduce let yet, so the global context remains unchanged during the derivation

what I am unsure of is, when we add let into the theory, is it built on top of the current formalization or it's also need embedding into the rules directly?

[jiangsy]

and I cannot prove presup for

| wf_exp_eq_gvar_sub :
  `( {{ Δ ;; Γ ⊢s σ : Γ' }} ->
     {{ `#x := [ M ] :: A ∈ Δ }} ->
     {{ Δ ;; Γ ⊢ `#x[σ] ≈ `#x : A }} )

specifially the LHS {{ Δ;; Γ ⊢ #x[σ] : A }}.

though we know A does not refer to any vars in local context, it's hard to argue A[σ] and A are equivalent and apply the wf_conv rule

[jiangsy]

@Antoine-something Can you post the form of thm/proof you mentioned yesterday?

[Antoine-something]

Actually, I took a closer look at the issue and I now understand better why it is not so easy. My intuition was that we should be able to prove that applying substitutions to closed terms does not actually affect them. Something like this:

{{ Δ ;; ⋅ ⊢ M : A }} ->
{{ Δ ;; Γ ⊢s σ : Γ' }} ->
{{ Δ ;; Γ ⊢ M ≈ M[σ] : A }} /\ ∃ i, {{ Δ ;; Γ ⊢ A ≈ A[σ] : Type@i }}

I played around trying to prove this and I managed to solve several cases, but it becomes difficult whenever a subterm of M requires extending the local context. I still think it could work if we have a few helper lemmas for those cases.

[jiangsy]

yeah, the key difficulty is to find a generalization of the property to handle the cases where contexts are extended, I was thinking of some q^n σ thing, where n is the length of Γ

[Ailrun]

The theorem should be something like

{{ Δ ;; Γ ⊢ M : A }} ->
{{ Δ ;; Γ' ⊢s σ : Γ'' }} ->
{{ Δ ;; Γ' ,++ Γ ⊢ M[ q^(length Γ) Id ] ≈ M[ q^(length Γ) σ ] : A }} /\ ∃ i, {{ Δ ;; Γ' ,++ Γ ⊢ A[ q^(length Γ) Id ] ≈ A[ q^(length Γ) σ ] : Type@i }}

instead of using the empty context. Then, the proof for M ≈ M [ q^(length Γ) Id ] should be done separately.

Actually, maybe I will try a proof of the main property today (for a global-context-less version).

[jiangsy]

separately.

Yes, I am thinking of a similar form.

[Ailrun]

Oh damn I am outdated lol

[Ailrun]

I thought that

{{ Δ ;; Γ ⊢ M : A }} ->
{{ Δ ;; Γ' ⊢s σ : Γ'' }} ->
{{ Δ ;; Γ' ,++ Γ ⊢ M[ q^(length Γ) Id ] ≈ M[ q^(length Γ) σ ] : A }} /\ ∃ i, {{ Δ ;; Γ' ,++ Γ ⊢ A[ q^(length Γ) Id ] ≈ A[ q^(length Γ) σ ] : Type@i }}

was somehow related to the weakening lemma, but it is not the case haha. Anyway, I think this general version should work (at most with some minor adjustments).

[Ailrun]

BTW, if M ≈ M [ q^(length Γ) Id ] part can be proved first, I don't think we need ∃ i, {{ Δ ;; Γ' ,++ Γ ⊢ A[ q^(length Γ) Id ] ≈ A[ q^(length Γ) σ ] : Type@i }} part for the theorem

[jiangsy]

I thought that

{{ Δ ;; Γ ⊢ M : A }} ->
{{ Δ ;; Γ' ⊢s σ : Γ'' }} ->
{{ Δ ;; Γ' ,++ Γ ⊢ M[ q^(length Γ) Id ] ≈ M[ q^(length Γ) σ ] : A }} /\ ∃ i, {{ Δ ;; Γ' ,++ Γ ⊢ A[ q^(length Γ) Id ] ≈ A[ q^(length Γ) σ ] : Type@i }}

was somehow related to the weakening lemma, but it is not the case haha. Anyway, I think this general version should work (at most with some minor adjustments).

yes, it's needed only for the presup of the following equivalent case

| wf_exp_eq_gvar_sub :
  `( {{ Δ ;; Γ ⊢s σ : Γ' }} ->
     {{ `#x := [ M ] :: A ∈ Δ }} ->
     {{ Δ ;; Γ ⊢ `#x[σ] ≈ `#x : A }} )

[jiangsy]

the wf_exp_sub case in subst_wk_wf_exp_eq does not seem to work,

specifically, given

1. forall σ : sub,
{{ Δ;; Γ'  ⊢s σ : Γ'' }} ->
{{ Δ;; Γ' ,++ Γ ⊢ M[q^(len Γ) Id] ≈ M[q^(len Γ) σ] : A }}
2. {{ Δ;; Γ''' ⊢s τ : Γ }}
3. {{ Δ;; Γ' ⊢s σ : Γ'' }}

we need to show

{{ Δ;; Γ' ,++ Γ''' ⊢ M[τ][q^(len Γ) Id] ≈ M[τ][q^(len Γ) σ] : A[τ] }}

I don't come up with ideas to further gen the prop to make this case work. I feel like it's a bit fundamental (i.e. the prop could be wrong?) and and wonder shall we rely on extra facts that M and A are NFs and do not contain subst to make it work?

On the other hand, the good news is that if subst_wk_wf_exp_eq worked, then presup would also be good

[jiangsy]

maybe a mutual statement on subst would work

[jiangsy]

I drafted a version subst_wk_wf_exp_subst_eq that includes the subst part, but I don't think it's correct.

[HuStmpHrrr]

There are a couple of things to highlight here. The problem here indicates a missing component in the current formulation of explicit substitutions. Notice that explicit substitutions can be understood as a categorical formulation. From this aspect, it appears that the current definition misses a terminal object, say empfor the empty substitution. Of course there should be a rule to characterize it's a terminal,

G |- emp : .

G |- sigma : .
----------------
G |- sigma ~ emp : .

Saying that there is only one terminal object.

The effect of applying it to a term is noop.

G |- t [ emp ] ~ t : T

That said, it's unclear that what a terminal object should be evaluated to.