Stream: MetaCoq

Topic: ✔ generalizing from typing in the empty context


view this post on Zulip Jason Gross (Apr 14 2023 at 22:15):

Neat, thank you!

Lemma weakening_typing_from_empty {cf Σ Γ t T}
  : @typing cf Σ [] t T -> wf Σ -> wf_local Σ Γ -> @typing cf Σ Γ t T.
Proof.
  intros Hty Hwf .
  replace Γ with ([],,, Γ,,, lift_context #|Γ| 0 []);
    [ replace t with (lift #|Γ| 0 t) | .. ];
    [ replace T with (lift #|Γ| 0 T) | .. ].
  { eapply (@weakening_typing cf Σ Hwf [] [] Γ);
      rewrite ?app_context_nil_l; tea. }
  all: rewrite ?app_context_nil_l.
  all: try now generalize (lift_context_length #|Γ| 0 []); destruct lift_context; cbn; congruence.
  all: rewrite lift_closed; try reflexivity.
  all: change 0 with #|[]:context|.
  all: unshelve ((eapply type_closed + eapply subject_closed); eassumption).
  all: assumption.
Qed.

Is it worth adding this to Typing.PCUICClosedTyp or Typing.PCUICWeakeningTyp or something?

view this post on Zulip Yann Leray (Apr 14 2023 at 22:18):

weaken_ctx with Γ := [] ?

view this post on Zulip Jason Gross (Apr 14 2023 at 22:36):

Ah, yes, thank you!

view this post on Zulip Notification Bot (Apr 14 2023 at 22:36):

Jason Gross has marked this topic as resolved.


Last updated: Jul 23 2024 at 21:01 UTC