Library HOAS_Untyped_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 HOAS_Untyped_Definitions.

Equalities concerning `senv`s





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 in 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 (Y X : atom) T,

  X `notin` fv_tt (open_tt T Y) ->

  X `notin` fv_tt 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 bind_typ_fresh : forall E F x V,

  wf_typ (F ++ [(x, Exp)] ++ E) V ->

  x `notin` fv V.




Lemma subst_fresh_exp_typ : forall E F x u V,

  wf_typ (F ++ [(x, Exp)] ++ E) V ->

  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 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 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 in 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 x) S2 /\ sub E S2 U2.




Lemma typing_inv_tabs : forall E S1 e1 T,

  typing E (exp_tabs S1 in e1) T ->

  forall U1 U2, sub E T (typ_all U1 in U2) ->

     sub E U1 S1

  /\ exists S2, exists L, forall X, X `notin` L ->

     typing ([(X, bind_sub U1)] ++ E) (open_te e1 X) (open_tt S2 X)

     /\ sub ([(X, bind_sub U1)] ++ E) (open_tt S2 X) (open_tt U2 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 in e1.




Lemma canonical_form_tabs : forall e U1 U2,

  value e ->

  typing empty e (typ_all U1 in U2) ->

  exists V, exists e1, e = exp_tabs V in 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'.