Module TypeContexts

Set Implicit Arguments.
Require Import DeBruijn.
Require Import Types.
Require Import TypeEquality.

A type context is represented as a type, where the variable 0 represents the hole. In general, there can be multiple occurrences of the hole in a context.

Definition ty_ctx :=
ty.

Definition hole : ty_ctx :=
TyVar 0.

A type is turned into a context (without a hole) as follows.

Definition constant : ty -> ty_ctx :=
lift_ty 0.

The hole is filled by substituting for the variable 0.

Definition fill TC T :=
subst_ty T 0 TC.

A type context is lifted by lifting every variable other than 0.

Definition lift_ty_ctx k TC :=
lift_ty (1 + k) TC.

Substituting a type into a type context requires adjusting the type U that is being grafted as well as the type variable k that is being substituted away.

Definition subst_ty_ctx U k TC :=
subst_ty (lift_ty 0 U) (S k) TC.

Lifting commutes with itself.

Lemma lift_lift_ty_ctx:
lift_lift lift_ty_ctx.

Proof.

repeat intro; unfold lift_ty_ctx. apply lift_lift_ty; eauto.
Qed.

Lifting and substitution commute.

Lemma lift_subst_1_ty_ctx:
lift_subst_1 lift_ty lift_ty_ctx subst_ty_ctx.

Proof.

  repeat intro. unfold lift_ty_ctx, subst_ty_ctx. simpl.
  rewrite lift_subst_1_ty; eauto.
  rewrite <- lift_lift_ty; eauto.
Qed.

Substituting into the application of a lifted context amounts to substituting through the context into the type in the hole.

Lemma subst_fill_lift:
forall U TC T,
subst_ty U 0 (fill (lift_ty_ctx 0 TC) T) = fill TC (subst_ty U 0 T).

Proof.

  unfold fill, lift_ty_ctx. simpl. intros.
  rewrite subst_subst_ty; eauto.
  rewrite subst_lift_ty. auto.
Qed.

Lifting the hole has no effect.

Lemma lift_hole:
forall k,
lift_ty_ctx k hole = hole.

Proof.

unfold lift_ty_ctx, hole. intros; simpl; auto.
Qed.

Filling and lifting commute.

Lemma lift_fill:
forall k TC T,
lift_ty k (fill TC T) = fill (lift_ty_ctx k TC) (lift_ty k T).

Proof.

intros. unfold fill, lift_ty_ctx. apply lift_subst_2_ty. eauto.
Qed.

Filling and substitution commute.

Lemma subst_fill:
forall U k TC T,
subst_ty U k (fill TC T) = fill (subst_ty_ctx U k TC) (subst_ty U k T).

Proof.

intros. unfold fill, subst_ty_ctx. apply subst_subst_ty. eauto.
Qed.

Filling a constant context has no effect.

Lemma fill_constant:
forall T1 T2,
fill (constant T1) T2 = T1.

Proof.

unfold fill, constant. intros. apply subst_lift_ty.
Qed.

Tensor commutes with constant.

Lemma tensor_constant:
forall T U,
TyTensor (constant T) (constant U) = constant (TyTensor T U).

Proof.

reflexivity.
Qed.

Filling the hole is the identity.

Lemma fill_hole:
forall T,
fill hole T = T.

Proof.

unfold fill, hole. intros; simpl. apply subst_var_identity.
Qed.

Well-formedness.

Lemma wf_constant:
  forall T,
  wf T ->
  wf (constant T).

Proof.

unfold constant. eauto.
Qed.

Lemma wf_fill:
  forall TC T,
  wf TC ->
  wf T ->
  wf (fill TC T).

Proof.

unfold fill. eauto.
Qed.

Lemma wf_fill_inverse:
  forall TC T,
  wf (fill TC T) ->
  wf TC.

Proof.

unfold fill. eauto using wf_subst_inverse.
Qed.

Lemma wf_lift_ty_ctx:
  forall TC k,
  wf TC ->
  wf (lift_ty_ctx k TC).

Proof.

unfold lift_ty_ctx. eauto.
Qed.

Hint Resolve wf_constant wf_fill wf_lift_ty_ctx.

These lemmas help reduce applications of fill as if it was primitively defined.

Ltac prove_fill :=
  unfold fill, constant; intros; simpl; try rewrite subst_lift_ty; auto.

Lemma fill_pair_1:
  forall layer1 layer2 TC T2 T,
  fill (TyPair layer1 layer2 TC (constant T2)) T = TyPair layer1 layer2 (fill TC T) T2.

Proof.

prove_fill.
Qed.

Lemma fill_pair_2:
forall layer1 layer2 TC T1 T,
fill (TyPair layer1 layer2 (constant T1) TC) T = TyPair layer1 layer2 T1 (fill TC T).

Proof.

prove_fill.
Qed.

Lemma fill_ref:
forall TC T,
fill (TyRef TC) T = TyRef (fill TC T).

Proof.

prove_fill.
Qed.

Lemma fill_tyregioncap_2:
forall TC T1 T rk,
fill (TyRegionCap rk (constant T1) TC) T = TyRegionCap rk T1 (fill TC T).

Proof.

prove_fill.
Qed.

Hint Rewrite fill_hole fill_pair_1 fill_pair_2 fill_ref fill_tyregioncap_2 : fill.

Ltac fill :=
autorewrite with fill in *.