Library Fnamedcontextcofinite

This file presents a cofinite-quantification style mechanization of System Fsub with contexts using locally named representation.
  • Authors: Jonghyun Park, Sungwoo Park, and Gyesik Lee


We import a number of definitions from libraries

Contents

  • Syntax
  • Parameters
  • Substitution
  • Typing contexts
  • Local closure
  • Well-formed typing contexts
  • Subtyping relation
  • Typing relation
  • Values and evaluation
  • Tactical support
  • Challenge 1A: Transitivity of Subtyping
  • Challenge 2A: Type Safety

Syntax

Both variables and parameters are represented as natural numbers. Since we use locally named representation, they are treated as distinct atoms.
Notation ltvar := nat. Notation ftvar := nat.
Notation lvar := nat. Notation fvar := nat.
We use the following definition of types and terms:
 types T, U, S := \top | A | X <: T | T -> U | \forall A <: T. U 
 terms t, u, s := a | x : T | \lambda a : T. t | t u | \Lambda A <: T. t | t [ T ] 
We use the following notations for variables and parameters:
  • type variables A, B, C
  • type parameters X, Y, Z
  • term variables a, b, c
  • term parameters x, y, z
Inductive typ : Set :=
| typ_top : typ
| typ_ltvar : ltvar -> typ
| typ_ftvar : ftvar -> typ
| typ_arrow : typ -> typ -> typ
| typ_all : ltvar -> typ -> typ -> typ.

Inductive tm : Set :=
| tm_lvar : lvar -> tm
| tm_fvar : fvar -> tm
| tm_abs : lvar -> typ -> tm -> tm
| tm_app : tm -> tm -> tm
| tm_tabs : ltvar -> typ -> tm -> tm
| tm_tapp : tm -> typ -> tm.

Notation " X ^^ " := (typ_ftvar X) (at level 65).
Notation " T --> U " := (typ_arrow T U) (at level 65).

Notation " x ** " := (tm_fvar x) (at level 55).

Parameters

Type parameters

The functions FV_tt and FV_te, defined below, calculate the set of type parameters in a type and a term, respectively. Locally named representation makes the typ_all case for FV_tt and the tm_tabs case for FV_te simple because variables and parameters are syntactically distinct.
Fixpoint FV_tt (T:typ) : list ftvar :=
  match T with
    | typ_top => nil
    | typ_ltvar _ => nil
    | X ^^ => X :: nil
    | T --> U => FV_tt T ++ FV_tt U
    | typ_all _ T U => FV_tt T ++ FV_tt U
  end.

Fixpoint FV_te (t : tm) : list ftvar :=
  match t with
    | tm_lvar _ => nil
    | tm_fvar _ => nil
    | tm_abs _ T t => FV_tt T ++ FV_te t
    | tm_app t t' => FV_te t ++ FV_te t'
    | tm_tabs _ T t => FV_tt T ++ FV_te t
    | tm_tapp t T => FV_te t ++ FV_tt T
  end.

Term parameters

The function FV_ee, defined below, calculates the set of term parameters in a term. Locally named representation also makes the tm_abs case simple for the same reason.
Fixpoint FV_ee (t : tm) : list fvar :=
  match t with
    | tm_lvar _ => nil
    | tm_fvar X => X :: nil
    | tm_abs _ T t => FV_ee t
    | tm_app t t' => FV_ee t ++ FV_ee t'
    | tm_tabs _ _ t => FV_ee t
    | tm_tapp t _ => FV_ee t
  end.

Substitution

Type variables

The functions lsubst_tt and lsubst_te, defined below, replace a type variable with a type for types and terms, respectively. Since we use names to represent a type variables, these functions check the equality between variables for the typ_all case (for lsubst_tt) and the tm_tabs case (for lsubst_te).
Fixpoint lsubst_tt (B : ltvar) (U : typ) (T : typ) {struct T} : typ :=
  match T with
    | typ_top => typ_top
    | typ_ltvar A => if A == B then U else typ_ltvar A
    | X ^^ => X ^^
    | T1 --> T2 => typ_arrow (lsubst_tt B U T1) (lsubst_tt B U T2)
    | typ_all A T1 T2 =>
      if A == B then typ_all A (lsubst_tt B U T1) T2
        else typ_all A (lsubst_tt B U T1) (lsubst_tt B U T2)
  end.

Fixpoint lsubst_te (B : ltvar) (U : typ) (t : tm) {struct t} : tm :=
  match t with
    | tm_lvar a => tm_lvar a
    | tm_fvar X => tm_fvar X
    | tm_abs a T t => tm_abs a (lsubst_tt B U T) (lsubst_te B U t)
    | tm_app t1 t2 => tm_app (lsubst_te B U t1) (lsubst_te B U t2)
    | tm_tabs A T t =>
      if A == B then tm_tabs A (lsubst_tt B U T) t
        else tm_tabs A (lsubst_tt B U T) (lsubst_te B U t)
    | tm_tapp t T => tm_tapp (lsubst_te B U t) (lsubst_tt B U T)
  end.

Term variables

The function lsubst_ee, defined below, replaces a term variable with a term. Note that the tm_abs case also checks the equality between variables.
Fixpoint lsubst_ee (b : lvar) (u : tm) (t : tm) {struct t} : tm :=
  match t with
    | tm_lvar a => if a == b then u else tm_lvar a
    | tm_fvar X => tm_fvar X
    | tm_abs a T t =>
      if a == b then tm_abs a T t else tm_abs a T (lsubst_ee b u t)
    | tm_app t1 t2 => tm_app (lsubst_ee b u t1) (lsubst_ee b u t2)
    | tm_tabs A T t => tm_tabs A T (lsubst_ee b u t)
    | tm_tapp t T => tm_tapp (lsubst_ee b u t) T
  end.

Type parameters

The functions fsubst_tt and fsubst_te, defined below, replace a type parameter with a type. Note that locally named representation makes the typ_all case (for fsubst_tt) and the tm_tabs case (for fsubst_te) simple.
Fixpoint fsubst_tt (Y:ftvar) (U : typ) (T : typ) {struct T} : typ :=
  match T with
    | typ_top => typ_top
    | typ_ltvar A => typ_ltvar A
    | X ^^ => if X == Y then U else X ^^
    | T1 --> T2 => (fsubst_tt Y U T1) --> (fsubst_tt Y U T2)
    | typ_all A T1 T2 => typ_all A (fsubst_tt Y U T1) (fsubst_tt Y U T2)
  end.

Fixpoint fsubst_te (Y:ftvar) (U:typ) (t:tm) {struct t} : tm :=
  match t with
    | tm_lvar a => tm_lvar a
    | tm_fvar X => tm_fvar X
    | tm_abs a T t => tm_abs a (fsubst_tt Y U T) (fsubst_te Y U t)
    | tm_app t1 t2 => tm_app (fsubst_te Y U t1) (fsubst_te Y U t2)
    | tm_tabs A T t => tm_tabs A (fsubst_tt Y U T) (fsubst_te Y U t)
    | tm_tapp t T => tm_tapp (fsubst_te Y U t) (fsubst_tt Y U T)
  end.

Term parameters

The function fsubst_ee, defined below, replaces a type parameter with a term. Locally named representation makes the tm_abs case simple.
Fixpoint fsubst_ee (y : fvar) (u t: tm) {struct t} : tm :=
  match t with
    | tm_lvar a => tm_lvar a
    | tm_fvar x => if x == y then u else tm_fvar x
    | tm_abs a T t => tm_abs a T (fsubst_ee y u t)
    | tm_app t1 t2 => tm_app (fsubst_ee y u t1) (fsubst_ee y u t2)
    | tm_tabs A T t => tm_tabs A T (fsubst_ee y u t)
    | tm_tapp t T => tm_tapp (fsubst_ee y u t) T
  end.

We introduce several notations to simplify the presentation, which use the following conventions:
  • { ... } denotes variable substitution.
  • ... denotes parameter substitution.
  • ~> denotes type substitution over types.
  • :~> denotes type substitution over terms.
  • ::~> denotes term substitution over terms.
Notation "{ A ~> U } T" := (lsubst_tt A U T) (at level 67).
Notation "{ A :~> U } t" := (lsubst_te A U t) (at level 67).
Notation "{ a ::~> u } t " := (lsubst_ee a u t) (at level 67).

Notation "[ X ~> U ] T" := (fsubst_tt X U T) (at level 67).
Notation "[ X :~> U ] t " := (fsubst_te X U t) (at level 67).
Notation "[ x ::~> u ] t " := (fsubst_ee x u t) (at level 67).

Typing contexts

A typing context records specific properties of parameters which eventually originate from binders. We refer to each record as binding. Since there are two kinds of binders, there are two kinds of bindings.
Inductive ctxt_bind : Set :=
| ctxt_bind_fvar : fvar -> typ -> ctxt_bind
| ctxt_bind_ftvar : ftvar -> typ -> ctxt_bind.

A typing context is a list of these bindings
Notation ctxt := (list ctxt_bind).

X ~<: T denotes a type binding, and x ~: T denotes a term binding.
Notation " X ~<: T " := (ctxt_bind_ftvar X T) (at level 56).
Notation " x ~: T " := (ctxt_bind_fvar x T) (at level 56).

Parameters

The function dom_tc, defined below, calculates the set of type parameters bound in a typing context.
Fixpoint dom_tc (Gamma : ctxt) : list ftvar :=
  match Gamma with
  | nil => nil
  | (ctxt_bind_fvar x T) :: Gamma => dom_tc Gamma
  | (ctxt_bind_ftvar X T) :: Gamma => X :: dom_tc Gamma
end.

In other words, if X ~<: T is in Gamma, X is in dom_tc Gamma.
Lemma ftvar_bind_in_dom_ctxt_t : forall Gamma X T,
  In (X ~<: T) Gamma -> In X (dom_tc Gamma).


The function dom_ec, defined below, calculates the set of term paramertes bound in a typing context.
Fixpoint dom_ec (Gamma : ctxt) : list fvar :=
  match Gamma with
  | nil => nil
  | (ctxt_bind_fvar x T) :: Gamma => x :: dom_ec Gamma
  | (ctxt_bind_ftvar X T) :: Gamma => dom_ec Gamma
end.

In other words, if x ~: T is in Gamma, x is in dom_ec Gamma.
Lemma fvar_bind_in_dom_ctxt_e : forall Gamma x T,
  In (x ~: T) Gamma -> In x (dom_ec Gamma).


The function FV_tc, defined below, calculates the set of all type parameters that appear in a typing context.
Fixpoint FV_tc (Gamma : ctxt) : list ftvar :=
  match Gamma with
  | nil => nil
  | (ctxt_bind_fvar x T) :: Gamma => FV_tt T ++ FV_tc Gamma
  | (ctxt_bind_ftvar X T) :: Gamma => X :: (FV_tt T ++ FV_tc Gamma)
end.

Thus, FV_tc Gamma includes all the type parameters in dom_tc Gamma.
Lemma incl_dom_ftvar_ctxt : forall Gamma X,
  In X (dom_tc Gamma) -> In X (FV_tc Gamma).


All of these functions are distributive over ++.
Lemma dom_tc_app_dist : forall Gamma Gamma',
  dom_tc (Gamma ++ Gamma') = dom_tc Gamma ++ dom_tc Gamma'.

Lemma dom_ec_app_dist : forall Gamma Gamma',
  dom_ec (Gamma ++ Gamma') = dom_ec Gamma ++ dom_ec Gamma'.

Lemma FV_tc_app_dist : forall Gamma Gamma',
  FV_tc (Gamma ++ Gamma') = FV_tc Gamma ++ FV_tc Gamma'.

Substitution

We refer to an operation on typing contexts that replaces all the occurrence of a specific parameter in the type of each typing binding with a type as "substitution".

For example, substituting X into Y ^^ on [X ~<: Y ^^; Y ~<: X ^^] results in [X ~<: Y ^^; Y ~<: Y ^^].

ctxt_ftvar_subst_map X T Gamma denotes a substitution of a type parameter X into a type T on a typing context Gamma.
Definition ctxt_ftvar_subst Y U (bind:ctxt_bind) :=
  match bind with
    | ctxt_bind_fvar x T => ctxt_bind_fvar x ([Y ~> U] T)
    | ctxt_bind_ftvar X T => ctxt_bind_ftvar X ([Y ~> U] T)
  end.

Definition ctxt_ftvar_subst_map Gamma X T :=
  map (ctxt_ftvar_subst X T) Gamma.

Notation "[ X ==> T ] Gamma " :=
  (ctxt_ftvar_subst_map Gamma X T) (at level 67).

Local closure

A type (or term) is said to be locally closed if every type (and term) variable has a corresponding binder. To formalize local closure of types and terms, we introduce two inductive definitions lclosed_t and lclosed_e for types and terms, respectively.

Local closure of types

For a typing context Gamma and a type variable set I, lclosed_t Gamma I T holds if I is a set of all the unbounded type variable in T, and every type parameter is bound in Gamma. Thus, a type T is locally closed if it has a typing context Gamma such that lclosed_t Gamma emptyset T holds.
Inductive lclosed_t : ctxt -> list ltvar -> typ -> Prop :=
| lclosed_t_top : forall Gamma,
  lclosed_t Gamma emptyset typ_top
| lclosed_t_ltvar : forall Gamma A,
  lclosed_t Gamma (A :: emptyset) (typ_ltvar A)
| lclosed_t_ftvar : forall Gamma X,
  In X (dom_tc Gamma) ->
  lclosed_t Gamma emptyset (X ^^)
| lclosed_t_arrow : forall Gamma I1 I2 (T U : typ),
  lclosed_t Gamma I1 T ->
  lclosed_t Gamma I2 U ->
  lclosed_t Gamma (I1 ++ I2) (T --> U)
| lclosed_t_all : forall Gamma I1 I2 A T U,
  lclosed_t Gamma I1 T ->
  lclosed_t Gamma I2 U ->
  lclosed_t Gamma (I1 ++ (remove eq_nat_dec A I2)) (typ_all A T U).


Local closure of terms

For a typing context Gamma, a type variable set I, a term variable set i, lclosed_e Gamma I i t holds if I and i are sets of all the unbound type and term variable in t, respectively, and every parameter is bound in Gamma. Thus, a term t is locally closed if it has a typing context Gamma such that lclosed_e Gamma emptyset emptyset t holds.
Inductive lclosed_e : ctxt -> list ltvar -> list lvar -> tm -> Prop :=
| lclosed_e_lvar : forall Gamma a,
  lclosed_e Gamma nil (a :: nil) (tm_lvar a)
| lclosed_e_fvar : forall Gamma x,
  In x (dom_ec Gamma) ->
  lclosed_e Gamma nil nil (x **)
| lclosed_e_abs : forall Gamma I1 I2 i a T t,
  lclosed_t Gamma I1 T ->
  lclosed_e Gamma I2 i t ->
  lclosed_e Gamma (I1 ++ I2) (remove eq_nat_dec a i) (tm_abs a T t)
| lclosed_e_app : forall Gamma I1 I2 i1 i2 t1 t2,
  lclosed_e Gamma I1 i1 t1 ->
  lclosed_e Gamma I2 i2 t2 ->
  lclosed_e Gamma (I1 ++ I2) (i1 ++ i2) (tm_app t1 t2)
| lclosed_e_tabs : forall Gamma I1 I2 i A T t,
  lclosed_t Gamma I1 T ->
  lclosed_e Gamma I2 i t ->
  lclosed_e Gamma (I1 ++ (remove eq_nat_dec A I2)) i (tm_tabs A T t)
| lclosed_e_tapp : forall Gamma I1 I2 i t T,
  lclosed_e Gamma I1 i t ->
  lclosed_t Gamma I2 T ->
  lclosed_e Gamma (I1 ++ I2) i (tm_tapp t T).


Well-formed typing contexts

We say that a typing context is well-formed if every type contained within are well-formed w.r.t its corresponding typing contexts, and every parameter is distinct.
Inductive ctxt_okay : ctxt -> Prop :=
| ctxt_okay_nil : ctxt_okay nil
| ctxt_okay_epar : forall Gamma x T,
  ctxt_okay Gamma ->
  ~ In x (dom_ec Gamma) ->
  lclosed_t Gamma emptyset T ->
  ctxt_okay (x ~: T :: Gamma)
| ctxt_okay_tpar : forall Gamma X T,
  ctxt_okay Gamma ->
  ~ In X (dom_tc Gamma) ->
  lclosed_t Gamma emptyset T ->
  ctxt_okay (X ~<: T :: Gamma).


Subtyping relation

It is straightforward to define the subtyping relation. The sub_top and sub_refl_tvar cases require types to be locally closed, and typing contexts to be well-formed. This implies that the subtyping relation holds only for locally closed types under well-formed typing contexts. Note the use of the cofinite-quantification style in the sub_all case.
Inductive sub : ctxt -> typ -> typ -> Prop :=
| sub_top : forall Gamma T,
  ctxt_okay Gamma ->
  lclosed_t Gamma emptyset T ->
  sub Gamma T typ_top
| sub_refl_tvar : forall Gamma X,
  ctxt_okay Gamma ->
  lclosed_t Gamma emptyset (X ^^) ->
  sub Gamma (X ^^) (X ^^)
| sub_trans_tvar : forall Gamma T U X,
  In (X ~<: T) Gamma ->
  sub Gamma T U ->
  sub Gamma (X ^^) U
| sub_arrow : forall Gamma T1 T2 U1 U2,
  sub Gamma U1 T1 ->
  sub Gamma T2 U2 ->
  sub Gamma (T1 --> T2) (U1 --> U2)
| sub_all : forall Gamma T1 T2 U1 U2 A B L,
  sub Gamma U1 T1 ->
  (forall X, ~ In X L ->
    sub (X ~<: U1 :: Gamma) ({ A ~> X ^^ } T2) ({ B ~> X ^^ } U2)) ->
  sub Gamma (typ_all A T1 T2) (typ_all B U1 U2).


Typing relation

It is also straightforward to define the typing relation. The typing_fvar case requires typing contexts to be well-formed, which implies that the typing relation holds only for well-formed typing contexts. The typing_fvar case also requires term binding x ~: T to be in a well-formed typing context, which implies the typing relation holds only for locally closed types (We will formally prove this later). Note the use of the cofinite-quantification style in the typing_abs and typing_tabs cases.
Inductive typing : ctxt -> tm -> typ -> Prop :=
| typing_fvar : forall Gamma x T,
  ctxt_okay Gamma ->
  In (x ~: T) Gamma ->
  typing Gamma (x **) T
| typing_abs : forall Gamma a T U t L,
  lclosed_t Gamma emptyset T ->
  (forall x, ~ In x L ->
    typing (x ~: T :: Gamma) ({a ::~> x **} t) U) ->
  typing Gamma (tm_abs a T t) (T --> U)
| typing_app : forall Gamma t t' T U,
  typing Gamma t (T --> U) ->
  typing Gamma t' T ->
  typing Gamma (tm_app t t') U
| typing_tabs : forall Gamma A B t T U L,
  lclosed_t Gamma emptyset T ->
  (forall X, ~ In X L ->
    typing (X ~<: T :: Gamma) ({A :~> X ^^} t) ({B ~> X ^^} U)) ->
  typing Gamma (tm_tabs A T t) (typ_all B T U)
| typing_tapp : forall Gamma t A T T' U,
  typing Gamma t (typ_all A T' U) ->
  sub Gamma T T' ->
  typing Gamma (tm_tapp t T) ({A ~> T} U)
| typing_sub : forall Gamma t T U,
  typing Gamma t T ->
  sub Gamma T U ->
  typing Gamma t U.


Values and evaluation

To state the preservation lemma, we first need to define values and the small-step evaluation relation. These inductive relations are straightforward to define.
Inductive value : tm -> Prop :=
| value_abs : forall a T t, value (tm_abs a T t)
| value_tabs : forall A T t, value (tm_tabs A T t).

Inductive red : tm -> tm -> Prop :=
| red_app_1 : forall t1 t1' t2,
  red t1 t1' ->
    red (tm_app t1 t2) (tm_app t1' t2)
| red_app_2 : forall t1 t2 t2',
  value t1 ->
  red t2 t2' ->
    red (tm_app t1 t2) (tm_app t1 t2')
| red_abs : forall a T t u,
  value u ->
  red (tm_app (tm_abs a T t) u) ({a ::~> u} t)
| red_tapp : forall t t' T,
  red t t' ->
    red (tm_tapp t T) (tm_tapp t' T)
| red_tabs : forall A T U t,
  red (tm_tapp (tm_tabs A T t) U) ({A :~> U} t).


Tactical support

We introduce an automation tactic Simplify to simplify the proof. Simplify attempts to evaluate several fixpoint functions, such as FV_tt and lsubst_tt, as much as possible. This simplification is useful for the following case:
 ...
 H : ~ In X (FV_tt (Gamma_1 ++ Gamma_2 ++ Gamma_3 ++ Gamma_4) )
 ...
 --------------------------------------------------------------
 ~ In X (FV_tt Gamma_4)
Simplify by eauto first decomposes the hypothesis H as follows:
 ...
 ? : ~ In X (FV_tt Gamma_1)
 ? : ~ In X (FV_tt Gamma_2)
 ? : ~ In X (FV_tt Gamma_3)
 ? : ~ In X (FV_tt Gamma_4)
 ...
 --------------------------------------------------------------
 ~ In X (FV_tt Gamma_4)
Then it applies eauto to solve the goal.

Tactic Notation "Simplify" "by" tactic(tac) := simplifyTac tac.

Challenge 1A: Transitivity of Subtyping

This section presents our solution to the POPLmark Challenge 1A.

Properties of lclosed_t

Note that sub uses lclosed_t in its definition. To reason about sub, therefore, we need the properties of lclosed_t. Here we present several properties of lclosed_t that we use in our solution.

Lemma lclosed_t_ftvar_dom_ctxt_typ : forall T Gamma I X,
  lclosed_t Gamma I T ->
  In X (FV_tt T) ->
  In X (dom_tc Gamma).


lclosed_t Gamma I T holds as long as Gamma contains all the parameters that appear in T.
Lemma lclosed_t_incl : forall Gamma Gamma' I T,
  incl (dom_tc Gamma) (dom_tc Gamma') ->
  lclosed_t Gamma I T ->
  lclosed_t Gamma' I T.

Lemma lclosed_t_remove_ftvar_bind : forall T U X Gamma I,
  ~ In X (FV_tt T) ->
  lclosed_t (X ~<: U :: Gamma) I T ->
  lclosed_t Gamma I T.

lclosed_t is invertible.
Lemma lclosed_t_ltvar_split : forall T Gamma A X U I0,
  ~ In X (FV_tt T) ->
  lclosed_t (X ~<: U :: Gamma) I0 ({A ~> X ^^} T) ->
  (exists I, (lclosed_t Gamma I T /\ remove eq_nat_dec A I = I0)).

lclosed_t is stable under type variable substitution.
Lemma lclosed_t_subst_ltvar : forall T Gamma U I A,
  lclosed_t Gamma emptyset U ->
  lclosed_t Gamma I T ->
  lclosed_t Gamma (remove eq_nat_dec A I) ({A ~> U} T).

Properties of ctxt_okay

sub and typing uses ctxt_okay in their definition, and thus we need to reason about ctxt_okay in order to reason about sub and typing. This section presents such properties of ctxt_okay.
Lemma ctxt_okay_app : forall Gamma Delta,
  ctxt_okay (Gamma ++ Delta)->
  ctxt_okay Delta.

Lemma ctxt_okay_unique_ftvar : forall Gamma X T,
  ctxt_okay (X ~<: T :: Gamma) ->
  ~ In X (FV_tc Gamma).

Every parameter in Gamma is distinct if ctxt_okay Gamma holds.
Lemma ctxt_okay_unique_fvar_bind : forall Gamma x T U,
  ctxt_okay Gamma ->
  In (x ~: T) Gamma ->
  In (x ~: U) Gamma ->
  T = U.

Lemma ctxt_okay_unique_ftvar_bind : forall Gamma X T U,
  ctxt_okay Gamma ->
  In (X ~<: T) Gamma ->
  In (X ~<: U) Gamma ->
  T = U.

Properties of substitution over types

Our solution exploits several properties of substitution over types.

Type variable substitution over types has no effect if they do not include such a type variable.
Lemma subst_ltvar_nochange_t : forall I T Gamma,
  lclosed_t Gamma I T ->
  forall A U,
    ~ In A I -> {A ~> U} T = T.

Type parameter substitution over types also has no effect if they do not include such a type parameter.
Lemma subst_ftvar_nochange_t : forall T U X,
  ~ In X (FV_tt T) -> [X ~> U] T = T.


We may swap variable and parameter substitutions.
Lemma subst_ftvar_ltvar_t : forall T U S X Gamma,
  lclosed_t Gamma emptyset U ->
  forall A,
    [X ~> U] ({A ~> S} T) = {A ~> [X ~> U] S} ([X ~> U] T).

We may replace a type variable with a fresh type parameter, and then replace the type parameter with a given type instead of directly replacing the type variable with the given type.
Lemma subst_seq_ftvar_ltvar_t : forall T U X,
  ~ In X (FV_tt T) ->
  forall A,
    [X ~> U] ({A ~> X ^^} T) = {A ~> U} T.

Basic properties of sub


sub deals with well-formed contexts only.
Lemma sub_ctxt_okay : forall T U Gamma,
  sub Gamma T U -> ctxt_okay Gamma.

sub deals with locally closed types only.
Lemma sub_lclosed_t : forall T U Gamma,
  sub Gamma T U -> lclosed_t Gamma emptyset T /\ lclosed_t Gamma emptyset U .

Structural properties of sub

Permutation

This section proves Lemma permuting_subLH which states the permutation property of sub.

We first prove Lemma permuting_lclosed_t which is an auxiliary lemma for Lemma permuting_lclosed_t.
Lemma permuting_lclosed_t : forall Gamma0 Gamma Delta bind bind' T I,
  lclosed_t Gamma0 I T ->
  Gamma0 = (Delta ++ (bind :: bind' :: Gamma)) ->
  lclosed_t (Delta ++ (bind' :: bind :: Gamma)) I T.


We then prove Lemma permuting_subLH using Lemma permuting_lclosed_t. Note that Lemma permuting_subLH, unlike Lemma permuting_lclosed_t, requires the typing context to be well-formed after the permutation.
Lemma permuting_sub : forall Gamma0 T U,
  sub Gamma0 T U ->
  forall Gamma Delta bind bind',
  Gamma0 = (Delta ++ (bind :: bind' :: Gamma)) ->
  ctxt_okay (Delta ++ (bind' :: bind :: Gamma)) ->
  sub (Delta ++ (bind' :: bind :: Gamma)) T U.


Weakening

This section proves Lemma weakening_sub_cons and weakening_sub_concat which state the weakening property of sub.

We first prove Lemma weakening_sub_cons by induction on the structure of sub proofs.
Lemma weakening_sub_cons : forall Gamma T U,
  sub Gamma T U ->
  forall bind,
    ctxt_okay (bind :: Gamma) ->
    sub (bind :: Gamma) T U.

We then prove Lemma weakening_sub_concat using Lemma weakening_sub_cons by induction on the structure of typing contexts.
Lemma weakening_sub_concat : forall Gamma T U,
  sub Gamma T U ->
  forall Gamma',
    ctxt_okay (Gamma' ++ Gamma) ->
    sub (Gamma' ++ Gamma) T U.


Transitivity of sub

Finally, we present the major result of this section: the transitivity of sub. The proof is challenging because we need to prove the transitivity and the narrowing property simultaneously.

Narrowing property of subtyping

To simplify the proof, we first prove the narrowing property under the assumption that the transitivity of sub holds for a specific type.

We use sub_transitivity_on T to state the assumption that the transitivity of sub holds for a specific type T.
Definition sub_transitivity_on T := forall Gamma U S,
  sub Gamma U T -> sub Gamma T S -> sub Gamma U S.

Lemma ctxt_okay_subst_cons : forall Gamma0,
  ctxt_okay Gamma0 ->
  forall Gamma X T U,
    Gamma0 = X ~<: T :: Gamma ->
    lclosed_t Gamma emptyset U ->
    ctxt_okay (X ~<: U :: Gamma).

Lemma ctxt_okay_subst_concat : forall Gamma' Gamma X T U,
  ctxt_okay (Gamma' ++ X ~<: T :: Gamma) ->
  lclosed_t Gamma emptyset U ->
  ctxt_okay (Gamma' ++ X ~<: U :: Gamma).


Lemma sub_narrowing_aux : forall Gamma0 T U,
  sub Gamma0 T U ->
  forall Gamma Gamma' X S S',
    Gamma0 = Gamma' ++ X ~<: S :: Gamma ->
    sub_transitivity_on S ->
    sub Gamma S' S ->
    sub (Gamma' ++ X ~<: S' :: Gamma) T U.

Lemma sub_narrowing : forall T U X S Gamma Gamma' ,
  sub (Gamma' ++ X ~<: S :: Gamma) T U ->
  forall S',
    sub_transitivity_on S ->
    sub Gamma S' S ->
      sub (Gamma' ++ X ~<: S' :: Gamma) T U.

Transitivity

We then prove the transitivity of sub by induction on the size of types. The size of types is defined by function size_t.
Fixpoint size_t (T : typ) : nat :=
  match T with
  | typ_top => 0
  | typ_ltvar _ => 0
  | typ_ftvar _ => 0
  | typ_arrow T1 T2 => S (size_t T1 + size_t T2)
  | typ_all _ T1 T2 => S (size_t T1 + size_t T2)
  end.

Lemma size_t_nochange_ltvar : forall T A X,
  size_t ({A ~> X ^^} T) = size_t T.

Lemma sub_trans_ftvar_aux deals with the typ_ftvar case.
Lemma sub_trans_ftvar_aux : forall T U X Gamma,
  sub Gamma T U ->
  U = (X ^^) ->
  forall S, sub Gamma U S -> sub Gamma T S.

Lemma sub_trans_fun_aux deals with the typ_arrow case.
Lemma sub_trans_fun_aux : forall T U U1 U2 S Gamma,
  sub_transitivity_on U1 ->
  sub_transitivity_on U2 ->
  sub Gamma T U ->
  sub Gamma U S ->
  U = U1 --> U2 ->
  sub Gamma T S.

Lemma sub_trans_forall_aux deals with the typ_all case.
Lemma sub_trans_forall_aux : forall T U U1 U2 S A,
  (forall S', size_t S' < size_t U -> sub_transitivity_on S') ->
  forall Gamma,
    sub Gamma T U ->
    U = typ_all A U1 U2 ->
    sub Gamma U S ->
    sub Gamma T S.

Using these lemmas, we may complete the proof of the transitivity.
Lemma sub_transitivity_aux : forall n T,
  size_t T < n -> sub_transitivity_on T.

Lemma sub_transitivity : forall T T' U Gamma,
  sub Gamma T U ->
  sub Gamma U T' ->
  sub Gamma T T'.

Reflexivity of sub

Reflexivity of sub is straightforward to prove. The proof proceeds by induction on the size of types.
Lemma sub_reflexivity_aux : forall n T Gamma,
  size_t T < n ->
  ctxt_okay Gamma ->
  lclosed_t Gamma emptyset T ->
  sub Gamma T T.

Challenge 2A: Type Safety

This section presents our solution to the POPLmark Challenge 2A.

Strengthening properties

For any relation based on typing contexts, if the relation is stable under the removal of irrelevant bindings, we say that the relation has the strengthening property. This section presents the strengthening property of various relations, such as lclosed_t.
Lemma strengthen_lclosed_t_fvar_app_aux : forall Gamma0 x T Gamma Delta I U,
  lclosed_t Gamma0 I U ->
  Gamma0 = Gamma ++ (x ~: T) :: Delta ->
  lclosed_t (Gamma ++ Delta) I U.

Lemma strengthen_lclosed_t_ftvar_aux : forall Gamma0 Gamma X T I U,
  ~ In X (FV_tt U) ->
  lclosed_t Gamma0 I U ->
  Gamma0 = ((X ~<: T) :: Gamma) ->
  lclosed_t Gamma I U.


Lemma strengthen_lclosed_e_fvar_aux : forall Gamma0 Gamma x T I i t,
  ~ In x (FV_ee t) ->
  lclosed_e Gamma0 I i t ->
  Gamma0 = ((x ~: T) :: Gamma) ->
  lclosed_e Gamma I i t.

Lemma strengthen_lclosed_e_ftvar_aux : forall Gamma0 Gamma X T I i t,
  ~ In X (FV_te t) ->
  lclosed_e Gamma0 I i t ->
  Gamma0 = ((X ~<: T) :: Gamma) ->
  lclosed_e Gamma I i t.


Lemma strengthen_ctxt_okay : forall Gamma Delta Gamma0 x T ,
  ctxt_okay Gamma0 ->
  Gamma0 = Gamma ++ (x ~: T) :: Delta ->
  ctxt_okay (Gamma ++ Delta).


Lemma strengthen_sub : forall Gamma0 U U',
  sub Gamma0 U U' ->
  forall Gamma x T Delta,
    Gamma0 = Gamma ++ x ~: T :: Delta ->
    sub (Gamma ++ Delta) U U'.


Properties of lclosed_e

Unlike sub which uses lclosed_t only, typing uses both lclosed_t and lclosed_e. This section presents properties of lclosed_e that we will use in the rest.

lclosed_e is also invertible.
Lemma lclosed_e_lvar_split : forall Gamma t I i' a x T,
  ~ In x (FV_ee t) ->
  lclosed_e ((x ~: T) :: Gamma) I i' ({a ::~> x **} t) ->
    (exists i, lclosed_e Gamma I i t /\ remove eq_nat_dec a i = i').

Lemma lclosed_e_ltvar_split : forall Gamma t I' i A X T,
  ~ In X (FV_te t) ->
  lclosed_e (X ~<: T :: Gamma) I' i ({A :~> X ^^} t) ->
    (exists I, lclosed_e Gamma I i t /\ remove eq_nat_dec A I = I').

Properties of substitution over terms.

For the proof of type safety, we deal with not only substitution over types but also substitution over terms, and thus we will present its properties in this section.

Variable substitution over terms has no effect if they do not include such a variable.
Lemma subst_lvar_nochange_e : forall t Gamma I i x t',
  lclosed_e Gamma I i t ->
  ~ In x i ->
  {x ::~> t'} t = t.

Lemma subst_ltvar_nochange_e : forall t Gamma I i A S,
  lclosed_e Gamma I i t ->
  ~ In A I ->
  {A :~> S} t = t.

Parameter substitution over terms also has no effect on terms if they do not include such a parameter.
Lemma subst_fvar_nochange_e : forall t t' x,
  ~ In x (FV_ee t) -> [x ::~> t'] t = t.

Lemma subst_ftvar_nochange_e : forall t X S,
  ~ In X (FV_te t) -> ([ X :~> S ] t) = t.


We may swap variable and parameter substitutions.
Lemma subst_fvar_lvar_e : forall Gamma t t' a x y I,
  lclosed_e Gamma I emptyset t' ->
  x <> y ->
  [y ::~> t']({a ::~> x **} t) = {a ::~> x **}([y ::~> t']t).

Lemma subst_ltvar_fvar_e : forall t A X x t' Gamma I,
  lclosed_e Gamma emptyset I t' ->
  {A :~> X ^^}([x ::~> t'] t) = [x ::~> t']({A :~> X ^^} t).

Lemma subst_ftvar_lvar_e : forall t t' X U x,
  [X :~> U]({x ::~> t'} t) = {x ::~> ([X :~> U] t')}([X :~> U] t).

Lemma subst_ftvar_ltvar_e : forall t A X S S' Gamma,
  lclosed_t Gamma emptyset S ->
  [X :~> S] ({A :~> S'} t) = {A :~> [X ~> S] S'} ([X :~> S] t).

We may replace a variable with a fresh parameter, and then replace the parameter with a given type (or term) instead of directly replacing the variable with the given type (or term).
Lemma subst_seq_fvar_lvar_e : forall t t' a x,
  ~ In x (FV_ee t) ->
  [x ::~> t']({a ::~> x **} t) = {a ::~> t'} t.

Lemma subst_seq_ftvar_ltvar_e : forall t S X,
  ~ In X (FV_te t) ->
  forall A,
    [X :~> S] ({A :~> (X ^^)} t) = {A :~> S} t.

Additional properties of ctxt_okay

While presenting our solution to Challenge 1A, we already present some properties of ctxt_okay related with type bindings. This section other properties of ctxt_okay related with term bindings.
Lemma ctxt_okay_fvar_bind_lclosed_t : forall Gamma x T,
  ctxt_okay Gamma ->
  In (x ~: T) Gamma ->
  lclosed_t Gamma emptyset T.

Properties of FV_tt, FV_te, FV_ee, and FV_tc

Lemma ftvar_bind_in_ctxt_preserve_not_in : forall Gamma T X Y,
  In (X ~<: T) Gamma
  -> ~ In Y (FV_tc Gamma)
  -> ~ In Y (FV_tt T).


Lemma not_in_FV_tt_dist_fsubst_tt : forall T X0 X U,
  ~ In X0 (FV_tt U)
  -> ~ In X0 (FV_tt T)
  -> ~ In X0 (FV_tt ([X ~> U] T)).




Lemma not_in_FV_te_dist_fsubst_te : forall t X0 X T,
  ~ In X0 (FV_tt T)
  -> ~ In X0 (FV_te t)
  -> ~ In X0 (FV_te ([X :~> T] t)).


Lemma FV_ee_subst_ftvar_nochange : forall t X T,
  FV_ee ([X :~> T] t) = FV_ee t.


Lemma not_in_FV_tc_dist_ctxt_subst_ftvar_map : forall Gamma X0 X T,
  ~ In X0 (FV_tc Gamma)
  -> ~ In X0 (FV_tt T)
  -> ~ In X0 (FV_tc ([X ==> T] Gamma)).


Basic properties of typing


typing deals with well-formed contexts.
Lemma typing_ctxt_okay : forall Gamma t T,
  typing Gamma t T ->
  ctxt_okay Gamma.

typing deals with locally closed types only.
Lemma typing_lclosed_t : forall Gamma t T,
  typing Gamma t T ->
  lclosed_t Gamma emptyset T.

typing deals with locally closed terms only.
Lemma typing_lclosed_e : forall Gamma t T,
  typing Gamma t T ->
  lclosed_e Gamma emptyset emptyset t.

Structural properties of typing

Permutation

This section proves Lemma permuting_typingLH which states the permutation property of typing.
Lemma permuting_typing : forall Gamma0 t T ,
  typing Gamma0 t T ->
  forall Gamma bind bind' Delta,
    Gamma0 = Gamma ++ bind :: bind' :: Delta ->
    ctxt_okay (Gamma ++ bind' :: bind :: Delta) ->
    typing (Gamma ++ bind' :: bind :: Delta) t T.


Weakening

This section proves Lemma weakening_typing which states the weakening property of typing. The proof proceeds by induction on the structure of typing proofs. (See Lemma weakening_typingLH for details)
Lemma weakening_typing : forall Gamma t T,
    typing Gamma t T ->
    forall bind,
      ctxt_okay (bind :: Gamma) ->
      typing (bind :: Gamma) t T.


Substitution lemma

This section presents the main result: typing is stable under type and term parameter substitution.

Auxiliary lemmas

This section presents several auxiliary lemmas that we use in the rest of proofs.
Lemma ftvar_subst_ctxt_bind_in : forall Gamma X T bind,
  In bind Gamma ->
  In (ctxt_ftvar_subst X T bind) ([X ==> T]Gamma).

Lemma ftvar_subst_ctxt_dom_tc_nochange : forall X T Gamma,
  dom_tc ([X ==> T] Gamma) = dom_tc Gamma.


Lemma ftvar_subst_ctxt_dom_ec_nochange : forall Gamma X T,
  dom_ec ([X ==> T] Gamma) = dom_ec Gamma.


Lemma ftvar_subst_ctxt_nochange : forall Gamma X T,
  ~ In X (FV_tc Gamma)
  -> Gamma = [X ==> T] Gamma.


Type parameter substitution lemma

We first prove Lemma typing_subst_ftvar which shows that typing is stable under type parameter substitution. The proof proceeds by induction on the structure of typing proofs.
Lemma lclosed_t_subst_ftvar_remove : forall T U X S I Gamma Delta Gamma0,
  lclosed_t Gamma0 I U ->
  Gamma0 = (Gamma ++ (X~<: T) :: Delta) ->
  lclosed_t Delta emptyset S ->
  lclosed_t (([X ==> S] Gamma) ++ Delta) I ([X ~> S] U).


Lemma lclosed_t_subst_ftvar : forall Gamma0 I T Gamma X U Delta,
  lclosed_t Gamma0 I T ->
  Gamma0 = Gamma ++ (X ~<: U :: Delta) ->
  forall U',
    sub Delta U' U ->
    lclosed_t (([X ==> U'] Gamma) ++ Delta) I ([X ~> U'] T).


Lemma ctxt_okay_subst_ftvar : forall Gamma X T Delta,
  ctxt_okay (Gamma ++ (X ~<: T :: Delta))
  -> forall U,
    sub Delta U T
    -> ctxt_okay (([X ==> U] Gamma) ++ Delta).


Lemma sub_subst_ftvar : forall Gamma0 U' U,
  sub Gamma0 U' U ->
  forall Gamma X T Delta R,
    Gamma0 = Gamma ++ (X ~<: T :: Delta) ->
    sub Delta R T ->
    sub (([X ==> R] Gamma) ++ Delta) ([X ~> R] U') ([X ~> R] U).


Lemma typing_subst_ftvar_aux : forall Gamma0 t T,
  typing Gamma0 t T ->
  forall Gamma X U U' Delta,
    Gamma0 = Gamma ++ X ~<: U :: Delta ->
    sub Delta U' U ->
    typing (([X ==> U']Gamma) ++ Delta) ([X :~> U'] t) ([X ~> U'] T).


Lemma typing_subst_ftvar : forall Gamma0 t T,
  typing Gamma0 t T ->
  forall X U U' Gamma,
    Gamma0 = X ~<: U :: Gamma ->
    sub Gamma U' U ->
    typing Gamma ([X :~> U'] t) ([X ~> U'] T).

Lemma typing_subst_ltvar : forall X U Gamma A B t T U',
  typing (X ~<: U :: Gamma) ({A :~> X ^^} t) ({B ~> X ^^} T)
  -> sub Gamma U' U
  -> ~ In X (FV_te t)
  -> ~ In X (FV_tt T)
  -> typing Gamma ({A :~> U'} t) ({B ~> U'} T).

Term parameter substitution lemma

We then prove Lemma typing_subst_fvar which shows that typing is stable under term parameter substitution. The proof also proceeds by induction on the structure of typing proofs.
Lemma typing_subst_fvar_aux : forall Gamma0 t T,
  typing Gamma0 t T ->
  forall Gamma x U u Delta,
    Gamma0 = Gamma ++ x ~: U :: Delta ->
    typing (Gamma ++ Delta) u U ->
    typing (Gamma ++ Delta) ([ x ::~> u ] t) T.

Lemma typing_subst_fvar : forall Gamma x U t u T,
  typing (x ~: U :: Gamma) t T ->
  typing Gamma u U ->
  typing Gamma ([ x ::~> u ] t) T.

Lemma typing_subst_lvar : forall x U Gamma a t u T,
  typing (x ~: U :: Gamma) ({a ::~> x **} t) T->
  typing Gamma u U ->
  ~ In x (FV_ee t) ->
  typing Gamma ({a ::~> u} t) T.

Preservation

Preservation is straightforward to prove once we prove the substitution leamms. Lemma app_red_preservation deals with the red_abs case, and Lemma tapp_red_preservation deals with the red_tabs case.
Lemma app_red_preservation : forall Gamma t0 T a T0 t U1 U2 u,
  typing Gamma t0 T
  -> t0 = tm_abs a T0 t
  -> sub Gamma T (U1 --> U2)
  -> typing Gamma u U1
  -> typing Gamma ({a ::~> u} t) U2.

Lemma tapp_red_preservation : forall Gamma t0 A T B T0 t U1 U2 R,
  typing Gamma t0 T0
  -> t0 = tm_tabs A T t
  -> sub Gamma T0 (typ_all B U1 U2)
  -> sub Gamma R U1
  -> typing Gamma ({A :~> R} t) ({B ~> R} U2).

Lemma preservation : forall t T Gamma,
  typing Gamma t T ->
  forall t', red t t' -> typing Gamma t' T.

Progress

Progress is also straightforward to prove.

We first show that there are canonical types for type and term abstraction.
Lemma abs_subtype_form : forall T1 T2 T Gamma,
  sub Gamma (T1 --> T2) T
  -> T = typ_top \/ exists T1' T2', T = T1' --> T2'.

Lemma abs_typing_form : forall t a t0 T T0 Gamma,
  typing Gamma t T
  -> t = tm_abs a T0 t0
  -> T = typ_top \/ exists T1 T2, T = T1 --> T2.

Lemma tabs_subtype_form : forall A T1 T2 T Gamma,
  sub Gamma (typ_all A T1 T2) T
  -> T = typ_top \/ exists B T1' T2', T = typ_all B T1' T2'.

Lemma tabs_typing_form : forall t A T0 t0 T Gamma,
  typing Gamma t T
  -> t = tm_tabs A T0 t0
  -> T = typ_top \/ exists B T0' T1', T = typ_all B T0' T1'.

We then show that there are canonical values for arrow and all types
Lemma canonical_form_abs : forall t T U Gamma,
  value t
  -> typing Gamma t (T --> U)
  -> exists a T0 t0, t = tm_abs a T0 t0.

Lemma canonical_form_tabs : forall t A T U Gamma,
  value t
  -> typing Gamma t (typ_all A T U)
  -> exists A0 T0 t0, t = tm_tabs A0 T0 t0.

Finally, we show that a well-typed term is never stuck: either it is a value, or it can reduce. The proof proceeds by simple induction on the typing relation, and exploits the canonical forms of values for arrow and all types.
Lemma progress : forall t T Gamma,
  typing Gamma t T
  -> Gamma = emptyset
  -> value t \/ exists t', red t t'.

This page has been generated by coqdoc