Library Fsub_Soundness
Require Import Metatheory Fsub_Definitions Fsub_Infrastructure.
In parentheses are given the label of the corresponding
lemma in the description of the POPLMark Challenge.
Reflexivity (1)
Lemma sub_reflexivity : forall E T,
okt E ->
wft E T ->
sub E T T .
Weakening (2)
Lemma sub_weakening : forall E F G S T,
sub (E & G) S T ->
okt (E & F & G) ->
sub (E & F & G) S T.
Narrowing and transitivity (3)
Section NarrowTrans.
Definition transitivity_on Q := forall E S T,
sub E S Q -> sub E Q T -> sub E S T.
Hint Unfold transitivity_on.
Hint Resolve wft_narrow.
Lemma sub_narrowing_aux : forall Q F E Z P S T,
transitivity_on Q ->
sub (E & Z ~<: Q & F) S T ->
sub E P Q ->
sub (E & Z ~<: P & F) S T.
Lemma sub_transitivity : forall Q,
transitivity_on Q.
Lemma sub_narrowing : forall Q E F Z P S T,
sub E P Q ->
sub (E & Z ~<: Q & F) S T ->
sub (E & Z ~<: P & F) S T.
End NarrowTrans.
Type substitution preserves subtyping (10)
Lemma sub_through_subst_tt : forall Q E F Z S T P,
sub (E & Z ~<: Q & F) S T ->
sub E P Q ->
sub (E & map (subst_tb Z P) F) (subst_tt Z P S) (subst_tt Z P T).
Weakening (5)
Lemma typing_weakening : forall E F G e T,
typing (E & G) e T ->
okt (E & F & G) ->
typing (E & F & G) e T.
Strengthening (6)
Lemma sub_strengthening : forall x U E F S T,
sub (E & x ~: U & F) S T ->
sub (E & F) S T.
Preservation by Type Narrowing (7)
Lemma typing_narrowing : forall Q E F X P e T,
sub E P Q ->
typing (E & X ~<: Q & F) e T ->
typing (E & X ~<: P & F) e T.
Preservation by Term Substitution (8)
Lemma typing_through_subst_ee : forall U E F x T e u,
typing (E & x ~: U & F) e T ->
typing E u U ->
typing (E & F) (subst_ee x u e) T.
Preservation by Type Substitution (11)
Lemma typing_through_subst_te : forall Q E F Z e T P,
typing (E & Z ~<: Q & F) e T ->
sub E P Q ->
typing (E & map (subst_tb Z P) F) (subst_te Z P e) (subst_tt Z P T).
Inversions for Typing (13)
Lemma typing_inv_abs : forall E S1 e1 T,
typing E (trm_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 (E & x ~: S1) (e1 open_ee_var x) S2 /\ sub E S2 U2.
Lemma typing_inv_tabs : forall E S1 e1 T,
typing E (trm_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 (E & X ~<: U1) (e1 open_te_var X) (S2 open_tt_var X)
/\ sub (E & X ~<: U1) (S2 open_tt_var X) (U2 open_tt_var X).
Preservation Result (20)
Lemma preservation_result : preservation.
Canonical Forms (14)
Lemma canonical_form_abs : forall t U1 U2,
value t -> typing empty t (typ_arrow U1 U2) ->
exists V, exists e1, t = trm_abs V e1.
Lemma canonical_form_tabs : forall t U1 U2,
value t -> typing empty t (typ_all U1 U2) ->
exists V, exists e1, t = trm_tabs V e1.
Progress Result (16)
Lemma progress_result : progress.