Module Closed

Set Implicit Arguments.
Require Import List.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Programs.
Require Import Environments.
Require Import Typing.

A well-typed value or term is well-scoped.

Lemma well_typed_well_scoped:
  (
    forall R M E v T,
    jv R M E v T ->
    well_scoped_lift lift_value (length E) v
  ) /\ (
    forall R vs T,
    ji R vs T ->
    True
  ) /\ (
    forall R M E t T,
    jt R M E t T ->
    well_scoped_lift lift_term (length E) t
  ).
Local Hint Extern 1 => rewrite lift_ty_env_preserves_length.

Proof.

apply jvit_ind; unfold well_scoped_lift; simpl; intros; try solve [ f_equal; eauto ].

VVar

match goal with h: jenv ?E ?k ?T |- _ => generalize (jenv_well_scoped h); intro end.
unfold lift_var. by_cases. auto.

JVAtRegion

f_equal. closed.
Qed.

A value or term that is well-typed in an empty environment is closed.

Lemma well_typed_closed_value:
  forall R v T,
  jv R nil nil v T ->
  closed_value v.

Proof.

  unfold closed_value, closed. intros.
  eapply well_scoped_lift_monotonic with (k1 := length nil). simpl; auto.
  eapply well_typed_well_scoped. eauto.
Qed.

Substituting for a variable that does not exist in the typing environment has no effect.

Lemma subst_term_overshoot:
  forall R M E t T,
  jt R M E t T ->
  forall k,
  k >= length E ->
  forall v,
  subst_term v k t = t.

Proof.

  intros.
  forwards: (pi3 well_typed_well_scoped). eassumption.
  forwards f: well_scoped_lift_subst. eexact subst_lift_term. eassumption.
  eauto.
Qed.