Library Tagged_Soundness

Type-safety proofs for Fsub.

Authors: Brian Aydemir and Arthur Charguéraud, with help from Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.

In parentheses are given the label of the corresponding lemma in the appendix (informal proofs) of the POPLmark Challenge.

Require Export Tagged_Infrastructure.

Equalities concerning senvs


Lemma to_tag_subst_tb_ident : forall Z P b,
  to_tag (subst_tb Z P b) = to_tag b.

Hint Rewrite to_tag_subst_tb_ident : rew_env.

Lemma to_senv_map_ident : forall Z P F,
  to_senv (map (subst_tb Z P) F) = to_senv F.

Hint Rewrite to_senv_map_ident : rew_env.

Properties of wf_typ


Lemma type_from_wf_typ : forall E T,
  wf_typ E T -> type T.

Lemma ok_from_wf_typ : forall E T,
  wf_typ E T -> ok E.

Lemma wf_typ_weakening : forall T E F G,
  wf_typ (G ++ E) T ->
  ok (G ++ F ++ E) ->
  wf_typ (G ++ F ++ E) T.

Lemma wf_typ_weaken_head : forall T E F,
  wf_typ E T ->
  ok (F ++ E) ->
  wf_typ (F ++ E) T.

Lemma wf_typ_strengthening : forall E F x T,
 wf_typ (F ++ [(x, Exp)] ++ E) T ->
 wf_typ (F ++ E) T.

Lemma wf_typ_subst_tb : forall F E Z P T,
  wf_typ (F ++ [(Z, Typ)] ++ E) T ->
  wf_typ E P ->
  wf_typ (F ++ E) (subst_tt Z P T).

Lemma wf_typ_open : forall E U T1 T2,
  wf_typ E (typ_all T1 T2) ->
  wf_typ E U ->
  wf_typ E (open_tt T2 U).

Properties of wf_env and wf_typ


Lemma ok_from_wf_env : forall E,
  wf_env E ->
  ok E.

Hint Resolve ok_from_wf_env.

Lemma wf_typ_from_binds_sub : forall x U E,
  wf_env E ->
  binds x (bind_sub U) E ->
  wf_typ (to_senv E) U.

Lemma wf_typ_from_binds_typ : forall x U E,
  wf_env E ->
  binds x (bind_typ U) E ->
  wf_typ (to_senv E) U.

Lemma wf_typ_from_wf_env_typ : forall x T E,
  wf_env ([(x, bind_typ T)] ++ E) ->
  wf_typ (to_senv E) T.

Lemma wf_typ_from_wf_env_sub : forall x T E,
  wf_env ([(x, bind_sub T)] ++ E) ->
  wf_typ (to_senv E) T.

Properties of wf_env


Lemma wf_env_narrowing : forall V E F U X,
  wf_env (F ++ [(X, bind_sub V)] ++ E) ->
  wf_typ (to_senv E) U ->
  wf_env (F ++ [(X, bind_sub U)] ++ E).

Lemma wf_env_strengthening : forall x T E F,
  wf_env (F ++ [(x, bind_typ T)] ++ E) ->
  wf_env (F ++ E).

Lemma wf_env_subst_tb : forall Q Z P E F,
  wf_env (F ++ [(Z, bind_sub Q)] ++ E) ->
  wf_typ (to_senv E) P ->
  wf_env (map (subst_tb Z P) F ++ E).

Environment is unchanged by substitution for a fresh name


Lemma notin_fv_tt_open : forall A B (Y X : atom) (T : syntax A),
  X `notin` fv (open T (@fvar B Y)) ->
  X `notin` fv T.

Lemma notin_fv_wf : forall E (X : atom) T,
  wf_typ (to_senv E) T ->
  X `notin` dom E ->
  X `notin` fv_tt T.

Lemma map_subst_tb_id : forall G Z P,
  wf_env G ->
  Z `notin` dom G ->
  G = map (subst_tb Z P) G.

Other lemmas


Lemma subst_fresh_exp_typ : forall x (u : exp) (V : typ),
  subst x u V = V.

Facts about wf_exp


Lemma expr_from_wf_exp : forall E e,
  wf_exp E e -> expr e.

Lemma wf_exp_weakening : forall e E F G,
  wf_exp (G ++ E) e ->
  ok (G ++ F ++ E) ->
  wf_exp (G ++ F ++ E) e.

Lemma wf_exp_weaken_head : forall e E F,
  wf_exp E e ->
  ok (F ++ E) ->
  wf_exp (F ++ E) e.

Lemma wf_exp_subst_ee : forall F E z g e,
  wf_exp (F ++ [(z, Exp)] ++ E) e ->
  wf_exp E g ->
  wf_exp (F ++ E) (subst_ee z g e).

Lemma wf_exp_subst_te : forall F E Z T e,
  wf_exp (F ++ [(Z, Typ)] ++ E) e ->
  wf_typ E T ->
  wf_exp (F ++ E) (subst_te Z T e).

Lemma wf_exp_open_ee : forall L E e v,
  (forall x : atom, x `notin` L -> wf_exp ([(x,Exp)] ++ E) (open_ee e (@fvar Exp x))) ->
  wf_exp E v ->
  wf_exp E (open_ee e v).

Lemma wf_exp_open_te : forall L E e V,
  (forall X : atom, X `notin` L -> wf_exp ([(X,Typ)] ++ E) (open_te e (@fvar Typ X))) ->
  wf_typ E V ->
  wf_exp E (open_te e V).

Regularity of relations


Lemma sub_regular : forall E S T,
  sub E S T ->
  wf_env E /\ wf_typ (to_senv E) S /\ wf_typ (to_senv E) T.

Lemma typing_regular : forall E e T,
  typing E e T ->
  wf_env E /\ wf_exp (to_senv E) e /\ wf_typ (to_senv E) T.

Lemma value_regular : forall e,
  value e ->
  exists E, wf_exp E e.

Lemma red_regular_l : forall e e',
  red e e' ->
  exists E, wf_exp E e.

Lemma red_regular_r : forall E e e',
  red e e' ->
  wf_exp E e ->
  wf_exp E e'.

Lemma red_regular : forall e e',
  red e e' ->
  exists E, wf_exp E e /\ wf_exp E e'.

Automation


Hint Extern 1 (wf_env ?E) =>
  match goal with
  | H: sub _ _ _ |- _ => apply (proj1 (sub_regular _ _ _ H))
  | H: typing _ _ _ |- _ => apply (proj1 (typing_regular _ _ _ H))
  end.

Hint Extern 1 (wf_typ (to_senv ?E) ?T) =>
  match goal with
  | H: typing E _ T |- _ => apply (proj2 (proj2 (typing_regular _ _ _ H)))
  | H: sub E T _ |- _ => apply (proj1 (proj2 (sub_regular _ _ _ H)))
  | H: sub E _ T |- _ => apply (proj2 (proj2 (sub_regular _ _ _ H)))
  end.

Hint Extern 1 (type ?T) =>
  let go E := (apply (type_from_wf_typ (to_senv E))) in
  match goal with
  | H: typing ?E _ T |- _ => go E
  | H: sub ?E T _ |- _ => go E
  | H: sub ?E _ T |- _ => go E
  end.

Hint Extern 1 (expr ?e) =>
  match goal with
  | H: typing _ ?e _ |- _ =>
      apply (expr_from_wf_exp _ _ (proj1 (proj2 (typing_regular _ _ _ H))))
  end.

Hint Extern 1 (wf_exp _ ?e) =>
  match goal with
    | H : typing _ e _ |- _ =>
      apply (proj1 (proj2 (typing_regular _ _ _ H)))
  end.

Properties of subtyping


Reflexivity (1)


Lemma sub_reflexivity : forall E T,
  wf_env E ->
  wf_typ (to_senv E) T ->
  sub E T T.

Weakening (2)


Section Weakening.

Hint Extern 1 (wf_typ _ _) =>
  repeat rewrite <- map_concat.

Hint Extern 1 (ok _) =>
  repeat rewrite <- map_concat.

Lemma sub_weakening : forall E F G S T,
  sub (G ++ E) S T ->
  wf_env (G ++ F ++ E) ->
  sub (G ++ F ++ E) S T.

End Weakening.

Narrowing and transitivity (3)


Section Narrowing_and_transitivity.

Hint Extern 1 (wf_typ _ ?S) =>
  match goal with
    | H : wf_typ _ S |- _ =>
      simpl_env in H; simpl in H; simpl_env in H
  end.

Lemma sub_narrowing_aux : forall Q F E Z P S T,
  (forall E S T, sub E S Q -> sub E Q T -> sub E S T) ->
  sub (F ++ [(Z, bind_sub Q)] ++ E) S T ->
  sub E P Q ->
  sub (F ++ [(Z, bind_sub P)] ++ E) S T.

Lemma sub_transitivity_aux : forall E' Q E S T,
  wf_typ E' Q ->
  sub E S Q ->
  sub E Q T ->
  sub E S T.

Lemma sub_narrowing : forall Q E F Z P S T,
  sub E P Q ->
  sub (F ++ [(Z, bind_sub Q)] ++ E) S T ->
  sub (F ++ [(Z, bind_sub P)] ++ E) S T.

Lemma sub_transitivity : forall Q E S T,
  sub E S Q ->
  sub E Q T ->
  sub E S T.

End Narrowing_and_transitivity.

Type substitution preserves subtyping (10)


Lemma sub_through_subst_tt : forall Q E F Z S T P,
  sub (F ++ [(Z, bind_sub Q)] ++ E) S T ->
  sub E P Q ->
  sub (map (subst_tb Z P) F ++ E) (subst_tt Z P S) (subst_tt Z P T).

Properties of typing


Weakening (5)


Section Typing_weakening.

Hint Extern 4 (wf_typ _ _) =>
  apply wf_typ_weakening; repeat rewrite <- map_concat.

Lemma typing_weakening : forall E F G e T,
  typing (G ++ E) e T ->
  wf_env (G ++ F ++ E) ->
  typing (G ++ F ++ E) e T.

End Typing_weakening.

Strengthening (6)


Lemma sub_strengthening : forall x U E F S T,
  sub (F ++ [(x, bind_typ U)] ++ E) S T ->
  sub (F ++ E) S T.

Narrowing for typing (7)


Lemma typing_narrowing : forall Q E F X P e T,
  sub E P Q ->
  typing (F ++ [(X, bind_sub Q)] ++ E) e T ->
  typing (F ++ [(X, bind_sub P)] ++ E) e T.

Substitution preserves typing (8)


Lemma typing_through_subst_ee : forall U E F x T e u,
  typing (F ++ [(x, bind_typ U)] ++ E) e T ->
  typing E u U ->
  typing (F ++ E) (subst_ee x u e) T.

Type substitution preserves typing (11)


Lemma typing_through_subst_te : forall Q E F Z e T P,
  typing (F ++ [(Z, bind_sub Q)] ++ E) e T ->
  sub E P Q ->
  typing (map (subst_tb Z P) F ++ E) (subst_te Z P e) (subst_tt Z P T).

Preservation


Inversion of typing (13)


Lemma typing_inv_abs : forall E S1 e1 T,
  typing E (exp_abs S1 e1) T ->
  forall U1 U2, sub E T (typ_arrow U1 U2) ->
     sub E U1 S1
  /\ exists S2, exists L, forall x, x `notin` L ->
     typing ([(x, bind_typ S1)] ++ E) (open_ee e1 (@fvar Exp x)) S2 /\ sub E S2 U2.

Lemma typing_inv_tabs : forall E S1 e1 T,
  typing E (exp_tabs S1 e1) T ->
  forall U1 U2, sub E T (typ_all U1 U2) ->
     sub E U1 S1
  /\ exists S2, exists L, forall X, X `notin` L ->
     typing ([(X, bind_sub U1)] ++ E) (open_te e1 (@fvar Typ X)) (open_tt S2 (@fvar Typ X))
     /\ sub ([(X, bind_sub U1)] ++ E) (open_tt S2 (@fvar Typ X)) (open_tt U2 (@fvar Typ X)).

Lemma typing_inv_inl : forall E e1 T,
  typing E (exp_inl e1) T ->
  forall U1 U2, sub E T (typ_sum U1 U2) ->
  exists S1, typing E e1 S1 /\ sub E S1 U1.

Lemma typing_inv_inr : forall E e1 T,
  typing E (exp_inr e1) T ->
  forall U1 U2, sub E T (typ_sum U1 U2) ->
  exists S1, typing E e1 S1 /\ sub E S1 U2.

Preservation (20)


Lemma preservation : forall E e e' T,
  typing E e T ->
  red e e' ->
  typing E e' T.

Progress


Canonical forms (14)


Lemma canonical_form_abs : forall e U1 U2,
  value e ->
  typing empty e (typ_arrow U1 U2) ->
  exists V, exists e1, e = exp_abs V e1.

Lemma canonical_form_tabs : forall e U1 U2,
  value e ->
  typing empty e (typ_all U1 U2) ->
  exists V, exists e1, e = exp_tabs V e1.

Lemma canonical_form_sum : forall e T1 T2,
  value e -> typing empty e (typ_sum T1 T2) ->
  exists e1, e = exp_inl e1 \/ e = exp_inr e1.

Progress (16)


Lemma progress : forall e T,
  typing empty e T ->
  value e \/ exists e', red e e'.