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.

Table of contents:

• Properties of subtyping
• Properties of typing
• Preservation
• Progress

Properties of subtyping

Reflexivity (1)

Weakening (2)

Narrowing and transitivity (3)

Type substitution preserves subtyping (10)

Properties of typing

Weakening (5)

Strengthening (6)

Narrowing for typing (7)

Substitution preserves typing (8)

We provide detailed comments for the following proof, mainly to point out several useful tactics and proof techniques.

Starting a proof with "Proof with <some tactic>" allows us to specify a default tactic that should be used to solve goals. To invoke this default tactic at the end of a proof step, we signal the end of the step with three periods instead of a single one, e.g., "apply typing_weakening...".

The proof proceeds by induction on the given typing derivation for e. We use the remember tactic, along with generalize dependent, to ensure that the goal is properly strengthened before we use induction.

The typing_var case involves a case analysis on whether the variable is the same as the one being substituted for.

In the case where x0=x, we first observe that hypothesis H0 implies that T=U, since x can only be bound once in the environment. The conclusion then follows from hypothesis TypU and weakening. We can use the binds_get tactic, described in the Environment library, with H0 to obtain the fact that T=U.

In order to apply typing_weakening, we need to rewrite the environment so that it has the right shape. (We could also prove a corollary of typing_weakening.) The rewrite_env tactic, described in the Environment library, is one way to perform this rewriting.

In the case where x0<>x, the result follows by an exhaustive case analysis on exactly where x0 is bound in the environment. We perform this case analysis by using the binds_cases tactic, described in the Environment library.

Informally, the typing_abs case is a straightforward application of the induction hypothesis, which is called H0 here.

We use the "pick fresh and apply" tactic to apply the rule typing_abs without having to calculate the appropriate finite set of atoms.

We cannot apply H0 directly here. The first problem is that the induction hypothesis has (subst_ee open_ee), whereas in the goal we have (open_ee subst_ee). The lemma subst_ee_open_ee_var lets us swap the order of these two operations.

The second problem is how the concatenations are associated in the environments. In the goal, we currently have

([(y, bind_typ V)] ++ F ++ E),

where concatenation associates to the right. In order to apply the induction hypothesis, we need

(([(y, bind_typ V)] ++ F) ++ E).

We can use the rewrite_env tactic to perform this rewriting, or we can rewrite directly with an appropriate lemma from the Environment library.

Now we can apply the induction hypothesis.

The remaining cases in this proof are straightforward, given everything that we have pointed out above.

Type substitution preserves typing (11)

Preservation

Inversion of typing (13)

Preservation (20)

Progress

Canonical forms (14)

Progress (16)