This file presents an exist-fresh style mechanization of System Fsub without contexts using locally nameless representation.

• Authors: Jonghyun Park, Sungwoo Park, and Gyesik Lee

We import a number of definitions from libraries

Contents

• Syntax
• Parameters
• Substitution
• Local closure
• 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 nameless representation, variables are treated as indices, while parameters are treated as distinct atoms.

We use the following definition of types and terms:

 types T, U, S := \top | A | X <: T | T -> U | \forall <: T. U 
 terms t, u, s := a | x : T | \lambda : T. t | t u | \Lambda <: 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

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 nameless 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.

Term parameters

The function FV_ee, defined below, calculates the set of term parameters in a term. Locally nameless representation also makes the tm_abs case simple for the same reason.

Substitution

Type variables

The functions lsubst_tt and lsubst_te, defined below, replace a type variable with a type for types and terms, respectively. Note that the use of locally nameless representation eliminates the equality checking between variables for the typ_all case (for lsubst_tt) and the tm_tabs case (for lsubst_te).

Term variables

The function lsubst_ee, defined below, replaces a term variable with a term. Note that the tm_abs case also does not check the equality between variables.

Type parameters

The functions fsubst_tt and fsubst_te, defined below, replace a type parameter with a type. Note that fsubst_tt replaces a type parameter with a type only when both a parameter and its annotated type are matched. Locally nameless representation makes the typ_all case (for fsubst_tt) and the tm_tabs case (for fsubst_te) simple.

Term parameters

The function fsubst_ee, defined below, replaces a type parameter with a term. Note that fsubst_tt replaces a term parameter with a term only when both a parameter and its annotated type are matched. Locally nameless representation makes the tm_abs case simple.

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.

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 type variable set I, lclosed_t I T holds if I is a set of all the unbounded type variable in T. Thus, a type T is locally closed if lclosed_t emptyset T holds. map_pred_remove_zero I first remove all the occurrence of O in I, and then reduce all the indices in I by 1.

Local closure of terms

For a type variable set I, a term variable set i, lclosed_e I i t holds if I and i are sets of all the unbound type and term variable in t, respectively. Thus, a term t is locally closed if lclosed_e emptyset emptyset t holds.

Subtyping relation

It is straightforward to define the subtyping relation. The sub_top and sub_refl_tvar cases require types to be locally closed. This implies that the subtyping relation holds only for locally closed types. The sub_refl_tvar case requires the annotated type to be well-formed, which corresponds the well-formed context requirement for the System Fsub with typing contexts. Note the use of the exist-fresh style in the sub_all case.

Subtyping relation with sizes

We formally define the size of proofs using the inductive definition subLH. If subLH n T U holds, it means that there is a proof of sub T U whose size is n. Note that the definition of subLH is the same as sub except the annotated size.

Lemma sub_subLH and subLH_sub formally state the equivalence between sub and subLH.

Typing relation

It is also straightforward to define the typing relation. The typing_fvar case requires the annotate type T to be locally closed, which implies the typing relation holds only for locally closed types (We will formally prove this later). Note the use of the exist-fresh style in the typing_abs and typing_tabs cases.

Typing relation with sizes

We formally define the size of proofs using the inductive definition typingLH. If typingLH n t T holds, it means that there is a proof of typing t T whose size is n. Note that the definition of typingLH is the same as typing except the annotated size.

Lemma typing_typingLH and typingLH_typing formally state the equivalence between typing and typingLH.

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.

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.

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.

lclosed_t is invertible.

lclosed_t is stable under type variable substitution.

lclosed_t is also stable under type parameter substitution.

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.

Type parameter substitution over types also has no effect if they do not include such a type parameter.

We may swap variable and parameter substitution.

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.

Basic properties of sub

sub deals with locally closed types only.

Renaming property of sub

As is well-known in the literature, the exists-fresh style necessitates various renaming properties. This section presents the proof of Lemma sub_rename_ftvar which formally states the renaming property of sub.

We first prove Lemma lclosed_t_rename_ftvar, and the prove Lemma sub_rename_ftvar using it.

The proof proceeds by induction on the size of sub T U proofs.

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.

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.

Lemma sub_trans_ftvar_aux deals with the typ_ftvar case.

Lemma sub_trans_fun_aux deals with the typ_arrow case.

Lemma sub_trans_forall_aux deals with the typ_all case.

Using these lemmas, we may complete the proof of the transitivity.

Reflexivity of sub

Reflexivity of sub is straightforward to prove. The proof proceeds by induction on the size of types.

Challenge 2A: Type Safety

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

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.

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.

Parameter substitution over terms also has no effect on terms if they do not include such a parameter.

We may swap variable and parameter substitution.

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).

FV_te and FV_ee are stable under substitutions.

Basic properties of typing

typing deals with locally closed types and terms only.

Renaming property of Typing

As is well-known in the literature, the exists-fresh style necessitates various renaming properties. This section proves two lemmas which states the renaming property of typing for term and type parameters, respectively.

Term parameter renaming

This section presents the proof of Lemma typingLH_subst_lvar_rename_fvar which states the term parameter renaming property of typing. The proof proceeds by induction on the sum of the size of typing proofs and the size of terms whose definition is given as follows:

Type parameter renaming

This section presents the proof of Lemma typingLH_subst_ltvar_rename_ftvar which states the type parameter renaming property of typing. The proof proceeds by induction on the size of typing proofs.

Substitution lemma

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

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 size of typing proofs. Note the use of the renaming lemmas in the typing_abs and typing_tabs cases.

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 size of typing proofs. Note the use of the renaming lemmas in the typing_abs and typing_tabs cases.

Preservation

Preservation is straightforward to prove once we prove the substitution lemmas. Lemma app_red_preservation deals with the red_abs case, and Lemma tapp_red_preservation deals with the red_tabs case.

To guarantee the soundness, we additionally show that reduction does not introduce new parameters.

Progress

Progress is also straightforward to prove.

We first show that there are canonical types for type and term abstraction.

We then show that there are canonical values for arrow and all types

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.