Library Flinear

Type safety of System F with linear types

Original authors: Brian Aydemir and Arthur Chargu\'eraud, with help from Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.

Author: Jeongbong Seo

This is a modification of the Coq proof script by Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic, which is described in Lightweight linear types in System F^O, TLDI 2010.

Main modification is to introduce annotated free variables and to drop out typing context.

We use 'Metatheory' library to handle a set of variable.


Definition


We use locally nameless representation, no typing context, cofinite quantification.

Syntax (pre-terms)


Binding variables are represented as natural numbers and free variables are represented as atom type which is defined in Metatheory libaray.
Notation ltvar := nat.
Notation ftvar := atom.
Notation lvar := nat.
Notation fvar := atom.

We use the following notations for types:
  • kinds k, k'
  • types T, U, S
  • type variables A, B, C
  • type parameters X, Y, Z
Similarly, we use the following notations for terms:
  • terms t, u, s
  • term variables a, b, c
  • term parameters x, y, z
We inductively define the kinds, types, and terms of System F^O:
   - kinds k, k'     :=  lin | nonlin
   - types T, U, S   :=  A | X ^^ k | T -(k)-> U | \forall ^^ k. T | T * U
   - terms t, u, s   :=  a | x : T | \lambda : T ^^ k. t | t u | 
                         \Lambda ^^ k. t | t [ T ] | (t, u) | \fst t | \snd t

Inductive kn : Set :=
  | kn_lin
  | kn_nonlin
.

Inductive typ : Set :=
  | typ_bvar : ltvar -> typ
  | typ_fvar : ftvar -> kn -> typ
  | typ_arrow : kn -> typ -> typ -> typ
  | typ_all : kn -> typ -> typ
  | typ_with : typ -> typ -> typ
.

Inductive exp : Set :=
  | exp_bvar : lvar -> exp
  | exp_fvar : fvar -> typ -> exp
  | exp_abs : kn -> typ -> exp -> exp
  | exp_app : exp -> exp -> exp
  | exp_tabs : kn -> exp -> exp
  | exp_tapp : exp -> typ -> exp
  | exp_apair : exp -> exp -> exp
  | exp_fst : exp -> exp
  | exp_snd : exp -> exp
.

Coercion typ_bvar : ltvar >-> typ.
Coercion exp_bvar : lvar >-> exp.

Lemma eq_kn_dec: forall (k1 k2:kn), {k1 = k2} + {~k1 = k2}.

Lemma ftvar_dec : forall (p q : (ftvar * kn)), {p = q} + {p <> q}.

Lemma fvar_dec : forall (p q : (fvar * typ)), {p = q} + {p <> q}.

Lemma eq_typ_dec: forall (t1 t2:typ), {t1 = t2} + {~t1 = t2}.

Notation "alpha ^^ k" := (typ_fvar alpha k) (at level 65).
Notation "A -( k )-> B" := (typ_arrow k A B) (at level 65).
Notation "X ** A" := (exp_fvar X A) (at level 65).

Opening terms


We define opening funtions which substitute type variables and term variables appearing in types, expressions. We are using locally nameless representation, we do not have to worry about variable captures.

Fixpoint open_tt_rec (K : ltvar) (U : typ) (T : typ) {struct T} : typ :=
  match T with
  | typ_bvar J => if eq_nat_dec K J then U else (typ_bvar J)
  | typ_fvar X k => typ_fvar X k
  | typ_arrow k T1 T2 => typ_arrow k (open_tt_rec K U T1) (open_tt_rec K U T2)
  | typ_all k T2 => typ_all k (open_tt_rec (S K) U T2)
  | typ_with T1 T2 => typ_with (open_tt_rec K U T1) (open_tt_rec K U T2)
  end.

Fixpoint open_te_rec (K : ltvar) (U : typ) (e : exp) {struct e} : exp :=
  match e with
  | exp_bvar i => exp_bvar i
  | exp_fvar x t => exp_fvar x t
  | exp_abs k V e1 => exp_abs k (open_tt_rec K U V) (open_te_rec K U e1)
  | exp_app e1 e2 => exp_app (open_te_rec K U e1) (open_te_rec K U e2)
  | exp_tabs k e1 => exp_tabs k (open_te_rec (S K) U e1)
  | exp_tapp e1 V => exp_tapp (open_te_rec K U e1) (open_tt_rec K U V)
  | exp_apair e1 e2 => exp_apair (open_te_rec K U e1) (open_te_rec K U e2)
  | exp_fst e1 => exp_fst (open_te_rec K U e1)
  | exp_snd e1 => exp_snd (open_te_rec K U e1)
  end.

Fixpoint open_ee_rec (k : lvar) (f : exp) (e : exp) {struct e} : exp :=
  match e with
  | exp_bvar i => if eq_nat_dec k i then f else e
  | exp_fvar x t => exp_fvar x t
  | exp_abs K V e1 => exp_abs K V (open_ee_rec (S k) f e1)
  | exp_app e1 e2 => exp_app (open_ee_rec k f e1) (open_ee_rec k f e2)
  | exp_tabs K e1 => exp_tabs K (open_ee_rec k f e1)
  | exp_tapp e1 V => exp_tapp (open_ee_rec k f e1) V
  | exp_apair e1 e2 => exp_apair (open_ee_rec k f e1) (open_ee_rec k f e2)
  | exp_fst e1 => exp_fst (open_ee_rec k f e1)
  | exp_snd e1 => exp_snd (open_ee_rec k f e1)
  end.

Definition open_tt T U := open_tt_rec 0 U T.
Definition open_te e U := open_te_rec 0 U e.
Definition open_ee e1 e2 := open_ee_rec 0 e2 e1.

Notation "{: a ~> C :} A" := (open_tt_rec a C A) (at level 67).
Notation "{: a :~> C :} e" := (open_te_rec a C e) (at level 67).
Notation "{: x ::~> e0 :} e " := (open_ee_rec x e0 e) (at level 67).
Notation "{: ~> C :} A" := (open_tt A C) (at level 67).
Notation "{: :~> C :} e" := (open_te e C) (at level 67).
Notation "{: ::~> e0 :} e " := (open_ee e e0) (at level 67).
Notation " p === q " := (ftvar_dec p q) (at level 70).
Notation " p ==== q " := (fvar_dec p q) (at level 70).

Environments


Although we adopt type-annotated free variables(type parameters and term parameters), we still need to maintain a context of term variables whose types have kn_lin kind, namely a linear context, so as to trace linear-kind term variables and to ensure that they are used exactly once.

Inductive lbinding : Set :=
  | lbind_typ : typ -> lbinding.

Notation lenv := (list (fvar * lbinding)).
Notation lempty := (@nil (fvar * lbinding)).

Lemma eq_lbnd_dec: forall (a b:lbinding), {a = b}+{~a=b}.

Lemma eq_lbinding_dec: forall (x y:(atom * lbinding)%type), {x = y}+{~x = y}.

Well-formedness


A type t with a kind k is well-formed, wf_typ t k, iff all type variables appearing in t are bounded and the kind of t is a subtype of k. Note that a product type must has a kind kn_lin (wf_typ_with) and kn_nonlin is a subtype of kn_lin (wf_typ_sub).

Inductive wf_typ : typ -> kn -> Prop :=
  | wf_typ_var : forall K (X : fvar),
      wf_typ (typ_fvar X K) K
  | wf_typ_arrow : forall K1 K2 K T1 T2,
      wf_typ T1 K1 ->
      wf_typ T2 K2 ->
      wf_typ (typ_arrow K T1 T2) K
  | wf_typ_all : forall L K1 K2 T2,
      (forall A : ftvar, A `notin` L ->
        wf_typ (open_tt T2 (A ^^ K1)) K2) ->
      wf_typ (typ_all K1 T2) K2
  | wf_typ_with : forall K1 K2 T1 T2,
      wf_typ T1 K1 ->
      wf_typ T2 K2 ->
      wf_typ (typ_with T1 T2) kn_lin
  | wf_typ_sub : forall T,
      wf_typ T kn_nonlin ->
      wf_typ T kn_lin
.

A context e is well-formed, wf_lenv e, iff all term variables in e are distinct and all types in e are well-formed with a kind kn_lin.

Inductive wf_lenv : lenv -> Prop :=
  | wf_lenv_empty : wf_lenv lempty
  | wf_lenv_typ : forall (D:lenv) (X:fvar) (T:typ),
      wf_lenv D ->
      X `notin` dom D ->
      wf_typ T kn_lin ->
      wf_lenv ([(X, lbind_typ T)] ++ D).

Local closure



A type t is locally closed, type t, iff t is well-formed.
Definition type T := exists K, wf_typ T K.

An expression e is locally closed, expr e, iff every term variable in e is bounded and every type variable in e is also locally-closed. We are using cofinite quantification for the cases expr_abs and expr_tabs.
Inductive expr : exp -> Prop :=
  | expr_fvar : forall X t,
      type t ->
      expr (exp_fvar X t)
  | expr_abs : forall L K t e1,
      type t ->
      (forall X : fvar, X `notin` L -> expr (open_ee e1 (X ** t))) ->
      expr (exp_abs K t e1)
  | expr_app : forall e1 e2,
      expr e1 ->
      expr e2 ->
      expr (exp_app e1 e2)
  | expr_tabs : forall L K e1,
      (forall A : ftvar, A `notin` L -> expr (open_te e1 (A ^^ K))) ->
      expr (exp_tabs K e1)
  | expr_tapp : forall e1 V,
      expr e1 ->
      type V ->
      expr (exp_tapp e1 V)
  | expr_apair : forall e1 e2,
      expr e1 ->
      expr e2 ->
      expr (exp_apair e1 e2)
  | expr_fst : forall e1,
      expr e1 ->
      expr (exp_fst e1)
  | expr_snd : forall e1,
      expr e1 ->
      expr (exp_snd e1)
.

Linear Context Splitting


levn_split e_1 e_2 e_3 means that e_3 can be divided into e_1 and e_2.

Inductive lenv_split : lenv -> lenv -> lenv -> Prop :=
  | lenv_split_empty:
       lenv_split lempty lempty lempty
  | lenv_split_left: forall D1 D2 D3 X T,
       lenv_split D1 D2 D3 ->
       X `notin` dom D3 ->
       wf_typ T kn_lin ->
       lenv_split ([(X, lbind_typ T)]++D1) D2 ([(X, lbind_typ T)]++D3)
  | lenv_split_right: forall D1 D2 D3 X T,
       lenv_split D1 D2 D3 ->
       X `notin` dom D3 ->
       wf_typ T kn_lin ->
       lenv_split D1 ([(X, lbind_typ T)]++D2) ([(X, lbind_typ T)]++D3).

Values


Inductive value : exp -> Prop :=
  | value_abs : forall K T e1,
      expr (exp_abs K T e1) ->
      value (exp_abs K T e1)
  | value_tabs : forall K e1,
      expr (exp_tabs K e1) ->
      value (exp_tabs K e1)
  | value_apair : forall e1 e2,
      expr e1 ->
      expr e2 ->
      value (exp_apair e1 e2)
.

Typing


Typing relation is defined as follows. For the case of type parameters and lambda abstractions, two rules are defined accroding to a kind of a type. Note the use of the cofinite-quantification style in the rules typing_abs, typing_labs, and typing_tabs

Inductive typing : lenv -> exp -> typ -> Prop :=
  | typing_unvar : forall X T,
      wf_typ T kn_nonlin ->
      typing lempty (exp_fvar X T) T
  | typing_linvar : forall X T,
      wf_typ T kn_lin ->
      typing [(X, lbind_typ T)] (exp_fvar X T) T
  | typing_abs : forall L K D T1 e1 T2,
      wf_typ T1 kn_nonlin ->
      (forall X : fvar, X `notin` L ->
        typing D (open_ee e1 (X ** T1)) T2) ->
      (K = kn_nonlin -> D = lempty) ->
      typing D (exp_abs K T1 e1) (typ_arrow K T1 T2)
  | typing_labs : forall L K D T1 e1 T2,
      wf_typ T1 kn_lin ->
      (forall X : fvar, X `notin` L ->
        typing ([(X, lbind_typ T1)] ++ D) (open_ee e1 (X ** T1)) T2) ->
      (K = kn_nonlin -> D = lempty) ->
      typing D (exp_abs K T1 e1) (typ_arrow K T1 T2)
  | typing_app : forall T1 K D1 D2 D3 e1 e2 T2,
      typing D1 e1 (typ_arrow K T1 T2) ->
      typing D2 e2 T1 ->
      lenv_split D1 D2 D3 ->
      typing D3 (exp_app e1 e2) T2
  | typing_tabs : forall L D K e1 T1,
      (forall A : ftvar, A `notin` L -> value (open_te e1 (A ^^ K))) ->
      (forall A : ftvar, A `notin` L ->
        typing D (open_te e1 (A ^^ K)) (open_tt T1 (A ^^ K))) ->
      typing D (exp_tabs K e1) (typ_all K T1)
  | typing_tapp : forall K D e1 T T2,
      typing D e1 (typ_all K T2) ->
      wf_typ T K ->
      typing D (exp_tapp e1 T) (open_tt T2 T)
  | typing_apair : forall D e1 e2 T1 T2,
      typing D e1 T1 ->
      typing D e2 T2 ->
      typing D (exp_apair e1 e2) (typ_with T1 T2)
  | typing_fst : forall D e T1 T2,
      typing D e (typ_with T1 T2) ->
      typing D (exp_fst e) T1
  | typing_snd : forall D e T1 T2,
      typing D e (typ_with T1 T2) ->
      typing D (exp_snd e) T2
.

Reduction


Inductive red : exp -> exp -> Prop :=
  | red_app_1 : forall e1 e1' e2,
      expr e2 ->
      red e1 e1' ->
      red (exp_app e1 e2) (exp_app e1' e2)
  | red_app_2 : forall e1 e2 e2',
      value e1 ->
      red e2 e2' ->
      red (exp_app e1 e2) (exp_app e1 e2')
  | red_tapp : forall e1 e1' V,
      type V ->
      red e1 e1' ->
      red (exp_tapp e1 V) (exp_tapp e1' V)
  | red_abs : forall K T e1 v2,
      expr (exp_abs K T e1) ->
      value v2 ->
      red (exp_app (exp_abs K T e1) v2) (open_ee e1 v2)
  | red_tabs : forall K e1 T,
      expr (exp_tabs K e1) ->
      type T ->
      red (exp_tapp (exp_tabs K e1) T) (open_te e1 T)
  | red_fst_cong : forall e e',
      red e e' ->
      red (exp_fst e) (exp_fst e')
  | red_fst_beta : forall e1 e2,
      expr e1 ->
      expr e2 ->
      red (exp_fst (exp_apair e1 e2)) e1
  | red_snd_cong : forall e e',
      red e e' ->
      red (exp_snd e) (exp_snd e')
  | red_snd_beta : forall e1 e2,
      expr e1 ->
      expr e2 ->
      red (exp_snd (exp_apair e1 e2)) e2
.

Automation


We declare most constructors as Hints to be used by the auto and eauto tactics. We exclude constructors from the subtyping and typing relations that use cofinite quantification. It is unlikely that eauto will find an instantiation for the finite set L, and in those cases, eauto can take some time to fail. (A priori, this is not obvious. In practice, one adds as hints all constructors and then later removes some constructors when they cause proof search to take too long.)


Cases Tactic

Following tactics help to insert case markers in a proof.

Tactic Notation "typ_cases" tactic(first) tactic(c) :=
  first;
  [ c "typ_bvar" | c "typ_fvar" |
    c "typ_arrow" | c "typ_all" | c "typ_with" ].

Tactic Notation "exp_cases" tactic(first) tactic(c) :=
  first;
  [ c "exp_bvar" | c "exp_fvar" |
    c "exp_abs" | c "exp_app" |
    c "exp_tabs" | c "exp_tapp" |
    c "exp_apair" | c "exp_fst" | c "exp_snd" ].

Tactic Notation "expr_cases" tactic(first) tactic(c) :=
  first;
  [ c "expr_fvar"
    c "expr_abs" | c "expr_app" |
    c "expr_tabs" | c "expr_tapp" |
    c "expr_apair" | c "expr_fst" | c "expr_snd" ].

Tactic Notation "wf_typ_cases" tactic(first) tactic(c) :=
  first;
  [ c "wf_typ_var" | c "wf_typ_arrow" | c "wf_typ_all" | c "wf_typ_with" | c "wf_typ_sub" ].

Tactic Notation "wf_lenv_cases" tactic(first) tactic(c) :=
  first;
  [ c "wf_lenv_empty" | c "wf_lenv_typ" ].

Tactic Notation "lenv_split_cases" tactic(first) tactic(c) :=
  first;
  [ c "lenv_split_empty" | c "lenv_split_left" | c "lenv_split_right" ].

Tactic Notation "value_cases" tactic(first) tactic(c) :=
  first;
  [ c "value_abs" | c "value_tabs" | c "value_apair" ].

Tactic Notation "red_cases" tactic(first) tactic(c) :=
  first;
  [ c "red_app_1" | c "red_app_2" |
    c "red_tapp" | c "red_abs" | c "red_tabs" |
    c "red_fst_cong" | c "red_fst_beta" |
    c "red_snd_cong" | c "red_snd_beta" ].

Tactic Notation "typing_cases" tactic(first) tactic(c) :=
  first;
  [ c "typing_unvar" | c "typing_linvar" |
    c "typing_abs" | c "typing_labs" | c "typing_app" |
    c "typing_tabs" | c "typing_tapp" |
    c "typing_apair" | c "typing_fst" | c "typing_snd" ].

Infrastructure lemmas and tactic definitions for F^O


This section contains a number of definitions, tactics, and lemmas that are based only on the syntax of the language at hand. While the exact statements of everything here would change for a different language, the general structure of this file (i.e., the sequence of definitions, tactics, and lemmas) would remain the same.

Table of contents:

Free variables


In this section, we define free variable functions. The functions fv_tt and fv_te calculate the set of atoms used as free type variables in a type or expression, respectively. The function fv_ee calculates the set of atoms used as free expression variables in an expression. Cases involving binders are straightforward since bound variables are indices, not names, in locally nameless representation.

Fixpoint fv_tt (T : typ) {struct T} : atoms :=
  match T with
  | typ_bvar J => {}
  | typ_fvar X k => singleton X
  | typ_arrow K T1 T2 => (fv_tt T1) `union` (fv_tt T2)
  | typ_all K T2 => (fv_tt T2)
  | typ_with T1 T2 => (fv_tt T1) `union` (fv_tt T2)
  end.

Fixpoint fv_te (e : exp) {struct e} : atoms :=
  match e with
  | exp_bvar i => {}
  | exp_fvar x t => fv_tt t
  | exp_abs K V e1 => (fv_tt V) `union` (fv_te e1)
  | exp_app e1 e2 => (fv_te e1) `union` (fv_te e2)
  | exp_tabs K e1 => (fv_te e1)
  | exp_tapp e1 V => (fv_tt V) `union` (fv_te e1)
  | exp_apair e1 e2 => (fv_te e1) `union` (fv_te e2)
  | exp_fst e1 => (fv_te e1)
  | exp_snd e1 => (fv_te e1)
  end.

Fixpoint fv_ee (e : exp) {struct e} : atoms :=
  match e with
  | exp_bvar i => {}
  | exp_fvar x t => singleton x
  | exp_abs K V e1 => (fv_ee e1)
  | exp_app e1 e2 => (fv_ee e1) `union` (fv_ee e2)
  | exp_tabs K e1 => (fv_ee e1)
  | exp_tapp e1 V => (fv_ee e1)
  | exp_apair e1 e2 => (fv_ee e1) `union` (fv_ee e2)
  | exp_fst e1 => (fv_ee e1)
  | exp_snd e1 => (fv_ee e1)
  end.

Fixpoint fv_lenv (D : lenv) {struct D} : atoms :=
  match D with
  | nil => {}
  | cons (X, lbind_typ T) l =>
      singleton X `union` fv_tt T `union` fv_lenv l
  end.

Substitution


In this section, we define substitution for expression and type variables appearing in types, expressions, and environments. Substitution differs from opening because opening replaces type variables whereas substitution replaces type parameters. The definitions below are relatively simple for two reasons.
  • We are using locally nameless representation, where bound variables (type variables) are represented using indices. Thus, there is no need to rename variables to avoid capture.
  • The definitions below assume that the term being substituted in, i.e., the second argument to each function, is locally closed. Thus, there is no need to shift indices when passing under a binder.

Fixpoint subst_tt (alpha : ftvar) (ka : kn) (U : typ) (T : typ) {struct T} : typ :=
  match T with
  | typ_bvar J => typ_bvar J
  | typ_fvar beta kb => if (alpha,ka) === (beta,kb) then U else T
  | typ_arrow K T1 T2 => typ_arrow K (subst_tt alpha ka U T1) (subst_tt alpha ka U T2)
  | typ_all K T2 => typ_all K (subst_tt alpha ka U T2)
  | typ_with T1 T2 => typ_with (subst_tt alpha ka U T1) (subst_tt alpha ka U T2)
  end.

Fixpoint subst_te (alpha : ftvar) (ka : kn) (U : typ) (e : exp) {struct e} : exp :=
  match e with
  | exp_bvar i => exp_bvar i
  | exp_fvar x t => exp_fvar x (subst_tt alpha ka U t)
  | exp_abs K V e1 => exp_abs K (subst_tt alpha ka U V) (subst_te alpha ka U e1)
  | exp_app e1 e2 => exp_app (subst_te alpha ka U e1) (subst_te alpha ka U e2)
  | exp_tabs K e1 => exp_tabs K (subst_te alpha ka U e1)
  | exp_tapp e1 V => exp_tapp (subst_te alpha ka U e1) (subst_tt alpha ka U V)
  | exp_apair e1 e2 => exp_apair (subst_te alpha ka U e1) (subst_te alpha ka U e2)
  | exp_fst e1 => exp_fst (subst_te alpha ka U e1)
  | exp_snd e1 => exp_snd (subst_te alpha ka U e1)
  end.

Fixpoint subst_ee (x : fvar) (tx : typ) (u : exp) (e : exp) {struct e} : exp :=
  match e with
  | exp_bvar i => exp_bvar i
  | exp_fvar y ty => if (x, tx) ==== (y, ty) then u else e
  | exp_abs K V e1 => exp_abs K V (subst_ee x tx u e1)
  | exp_app e1 e2 => exp_app (subst_ee x tx u e1) (subst_ee x tx u e2)
  | exp_tabs K e1 => exp_tabs K (subst_ee x tx u e1)
  | exp_tapp e1 V => exp_tapp (subst_ee x tx u e1) V
  | exp_apair e1 e2 => exp_apair (subst_ee x tx u e1) (subst_ee x tx u e2)
  | exp_fst e1 => exp_fst (subst_ee x tx u e1)
  | exp_snd e1 => exp_snd (subst_ee x tx u e1)
  end.

Definition subst_tlb (alpha : ftvar) (ka : kn) (P : typ) (b : lbinding) : lbinding :=
  match b with
  | lbind_typ T => lbind_typ (subst_tt alpha ka P T)
  end.

Notation "[: ( alpha , k ) ~> C :] B" := (subst_tt alpha k C B) (at level 67).
Notation "[: ( alpha , k ) :~> C :] e " := (subst_te alpha k C e) (at level 67).
Notation "[: ( X , A ) ::~> e :] e0 " := (subst_ee X A e e0) (at level 67).

The "pick fresh" tactic


The "pick fresh" tactic introduces a fresh atom into the context. We define it in two steps.

The first step is to define an auxiliary tactic gather_atoms, meant to be used in the definition of other tactics, which returns a set of atoms in the current context. The definition of gather_atoms follows a pattern based on repeated calls to gather_atoms_with. The one argument to this tactic is a function that takes an object of some particular type and returns a set of atoms that appear in that argument. It is not necessary to understand exactly how gather_atoms_with works. If we add a new inductive datatype, say for kinds, to our language, then we would need to modify gather_atoms. On the other hand, if we merely add a new type, say products, then there is no need to modify gather_atoms; the required changes would be made in fv_tt.


The second step in defining "pick fresh" is to define the tactic itself. It is based on the (pick fresh ... for ...) tactic defined in the Atom library. Here, we use gather_atoms to construct the set L rather than leaving it to the user to provide. Thus, invoking (pick fresh x) introduces a new atom x into the current context that is fresh for "everything" in the context.

Tactic Notation "pick" "fresh" ident(x) :=
  let L := gather_atoms in (pick fresh x for L).

The "pick fresh and apply" tactic


This tactic is implementation specific only because of its reliance on gather_atoms, which is itself implementation specific. The definition below may be copied between developments without any changes, assuming that the other other developments define an appropriate gather_atoms tactic. For documentation on the tactic on which the one below is based, see the Metatheory library.

Tactic Notation
      "pick" "fresh" ident(atom_name) "and" "apply" constr(lemma) :=
  let L := gather_atoms in
  pick fresh atom_name excluding L and apply lemma.

Properties of opening and substitution


The following lemmas provide useful structural properties of substitution and opening. While the exact statements are language specific, we have found that similar properties are needed in a wide range of languages.

Below, we indicate which lemmas depend on which other lemmas. Since te functions depend on their tt counterparts, a similar dependency can be found in the lemmas.

The lemmas are split into three sections, one each for the tt, te, and ee functions. The most important lemmas are the following:
  • Substitution and opening commute with each other, e.g., subst_tt_open_tt_var.
  • Opening a term is equivalent to opening the term with a fresh name and then substituting for that name, e.g., subst_tt_intro.
We keep the sections as uniform in structure as possible. In particular, we state explicitly strengthened induction hypotheses even when there are more concise ways of proving the lemmas of interest.

Properties of type substitution in types


The next lemma is the strengthened induction hypothesis for the lemma that follows, which states that opening a locally closed term is the identity. This lemma is not otherwise independently useful.

Lemma open_tt_rec_type_aux : forall T j V i U,
  i <> j ->
  open_tt_rec j V T = open_tt_rec i U (open_tt_rec j V T) ->
  T = open_tt_rec i U T.

Opening a locally closed term is the identity. This lemma depends on the immediately preceding lemma.

Lemma open_tt_rec_type : forall P U k,
  type P ->
  P = open_tt_rec k U P.

If a name is fresh for a term, then substituting for it is the identity.

Lemma subst_tt_fresh : forall alpha ka U T,
   alpha `notin` fv_tt T ->
   T = subst_tt alpha ka U T.

Substitution commutes with opening under certain conditions. This lemma depends on the fact that opening a locally closed term is the identity.

Lemma subst_tt_open_tt_rec : forall T1 T2 alpha ka P k,
  type P ->
  subst_tt alpha ka P (open_tt_rec k T2 T1) =
    open_tt_rec k (subst_tt alpha ka P T2) (subst_tt alpha ka P T1).

The next lemma is a direct corollary of the immediately preceding lemma---the index is specialized to zero.

Lemma subst_tt_open_tt : forall T1 T2 (alpha:ftvar) ka P,
  type P ->
  subst_tt alpha ka P (open_tt T1 T2) = open_tt (subst_tt alpha ka P T1) (subst_tt alpha ka P T2).

The next lemma is a direct corollary of the immediately preceding lemma---here, we're opening the term with a variable. In practice, this lemma seems to be needed as a left-to-right rewrite rule, when stated in its current form.

Lemma subst_tt_open_tt_var : forall (alpha beta:ftvar) ka kb P T,
  beta <> alpha ->
  type P ->
  open_tt (subst_tt alpha ka P T) (beta ^^ kb) = subst_tt alpha ka P (open_tt T (beta ^^ kb)).

The next lemma states that opening a term is equivalent to first opening the term with a fresh name and then substituting for the name. This is actually the strengthened induction hypothesis for the version we use in practice.

Lemma subst_tt_intro_rec : forall alpha ka T2 U k,
  alpha `notin` fv_tt T2 ->
  open_tt_rec k U T2 = subst_tt alpha ka U (open_tt_rec k (typ_fvar alpha ka) T2).

The next lemma is a direct corollary of the immediately preceding lemma---the index is specialized to zero.

Lemma subst_tt_intro : forall (alpha : ftvar) ka T2 U,
  alpha `notin` fv_tt T2 ->
  open_tt T2 U = subst_tt alpha ka U (open_tt T2 (alpha ^^ ka)).

Properties of type substitution in expressions


This section follows the structure of the previous section. The one notable difference is that we require two auxiliary lemmas to show that substituting a type in a locally-closed expression is the identity.

Lemma open_te_rec_expr_aux : forall e j u i P ,
  open_ee_rec j u e = open_te_rec i P (open_ee_rec j u e) ->
  e = open_te_rec i P e.

Lemma open_te_rec_type_aux : forall e j Q i P,
  i <> j ->
  open_te_rec j Q e = open_te_rec i P (open_te_rec j Q e) ->
  e = open_te_rec i P e.

Lemma open_te_rec_expr : forall e U k,
  expr e ->
  e = open_te_rec k U e.

Lemma subst_te_open_te_rec : forall e T alpha ka P k,
  type P ->
  subst_te alpha ka P (open_te_rec k T e) =
    open_te_rec k (subst_tt alpha ka P T) (subst_te alpha ka P e).

Lemma subst_te_open_te : forall e T alpha ka P,
  type P ->
  subst_te alpha ka P (open_te e T) = open_te (subst_te alpha ka P e) (subst_tt alpha ka P T).

Lemma subst_te_open_te_var : forall (alpha beta:ftvar) ka kb P e,
  beta <> alpha ->
  type P ->
  open_te (subst_te alpha ka P e) (beta ^^ kb) = subst_te alpha ka P (open_te e (beta ^^ kb)).

Lemma subst_te_intro_rec : forall alpha ka e U k,
  alpha `notin` fv_te e ->
  open_te_rec k U e = subst_te alpha ka U (open_te_rec k (typ_fvar alpha ka) e).

Lemma subst_te_intro : forall (alpha : ftvar) ka e U,
  alpha `notin` fv_te e ->
  open_te e U = subst_te alpha ka U (open_te e (alpha ^^ ka)).

Properties of expression substitution in expressions


This section follows the structure of the previous two sections.

Lemma open_ee_rec_expr_aux : forall e j v u i,
  i <> j ->
  open_ee_rec j v e = open_ee_rec i u (open_ee_rec j v e) ->
  e = open_ee_rec i u e.

Lemma open_ee_rec_type_aux : forall e j V u i,
  open_te_rec j V e = open_ee_rec i u (open_te_rec j V e) ->
  e = open_ee_rec i u e.

Lemma open_ee_subst_ee_rec: forall e X tx Y T U n,
  Y <> X ->
  {: n ::~> Y ** T :}e = [: (X, tx) ::~> U :]({: n ::~> Y ** T :}e) ->
  e = [: (X, tx) ::~> U :]e.

Lemma open_te_subst_ee_rec: forall e X tx alpha ka U n,
  {: n :~> alpha ^^ ka :}e = [: (X, tx) ::~> U :]({: n :~> alpha ^^ ka :}e) ->
  e = [: (X, tx) ::~> U :]e.

Lemma open_ee_rec_expr : forall u e k,
  expr e ->
  e = open_ee_rec k u e.

Lemma subst_ee_open_ee_rec : forall e1 e2 x tx u k,
  expr u ->
  subst_ee x tx u (open_ee_rec k e2 e1) =
    open_ee_rec k (subst_ee x tx u e2) (subst_ee x tx u e1).

Lemma subst_ee_open_ee : forall e1 e2 x tx u,
  expr u ->
  subst_ee x tx u (open_ee e1 e2) =
    open_ee (subst_ee x tx u e1) (subst_ee x tx u e2).

Lemma subst_ee_open_ee_var : forall (x y:fvar) tx ty u e,
  y <> x ->
  expr u ->
  open_ee (subst_ee x tx u e) (exp_fvar y ty) = subst_ee x tx u (open_ee e (exp_fvar y ty)).

Lemma subst_te_open_ee_rec : forall e1 e2 alpha ka P k,
  subst_te alpha ka P (open_ee_rec k e2 e1) =
    open_ee_rec k (subst_te alpha ka P e2) (subst_te alpha ka P e1).

Lemma subst_te_open_ee : forall e1 e2 alpha ka P,
  subst_te alpha ka P (open_ee e1 e2) = open_ee (subst_te alpha ka P e1) (subst_te alpha ka P e2).

Lemma subst_te_open_ee_var : forall alpha ka (x:fvar) tx P e,
  open_ee (subst_te alpha ka P e) (exp_fvar x (subst_tt alpha ka P tx)) = subst_te alpha ka P (open_ee e (exp_fvar x tx)).

Lemma subst_ee_open_te_rec : forall e P x tx u k,
  expr u ->
  subst_ee x tx u (open_te_rec k P e) = open_te_rec k P (subst_ee x tx u e).

Lemma subst_ee_open_te : forall e P x tx u,
  expr u ->
  subst_ee x tx u (open_te e P) = open_te (subst_ee x tx u e) P.

Lemma subst_ee_open_te_var : forall x tx (alpha:ftvar) ka u e,
  expr u ->
  open_te (subst_ee x tx u e) (alpha ^^ ka) = subst_ee x tx u (open_te e (alpha ^^ ka)).

Lemma subst_ee_intro_rec : forall X tx e u k,
  X `notin` fv_ee e ->
  open_ee_rec k u e = subst_ee X tx u (open_ee_rec k (X ** tx) e).

Lemma subst_ee_intro : forall (X : fvar) tx e u,
  X `notin` fv_ee e ->
  open_ee e u = subst_ee X tx u (open_ee e (exp_fvar X tx)).

Properites of the lenv_split relation


Basic properties of the env_split relation.

Lemma dom_lenv_split: forall E1 E2 E3,
  lenv_split E1 E2 E3 ->
  dom E3 [=] dom E1 `union` dom E2.

Lemma lenv_split_commute: forall E1 E2 E3,
  lenv_split E1 E2 E3 ->
  lenv_split E2 E1 E3.

Lemma lenv_split_empty_left: forall E F,
  lenv_split lempty E F ->
  E = F.

Lemma lenv_split_empty_right: forall E F,
  lenv_split E lempty F ->
  E = F.

wf_lenv_split D_1 D_2 D_3 implies that all contexts D_1, D_2, and D_3 are well-formed.
Lemma wf_lenv_split: forall D1 D2 D3,
  lenv_split D1 D2 D3 ->
  wf_lenv D3.

Lemma wf_lenv_split_left: forall D1 D2 D3,
  lenv_split D1 D2 D3 ->
  wf_lenv D1.

Lemma wf_lenv_split_right: forall D1 D2 D3,
  lenv_split D1 D2 D3 ->
  wf_lenv D2.


If lenv_split D_1 D_2 D_3 then an element in D_3 is found in either D_1 or D_2.
Lemma lenv_split_cases_mid: forall D1 D2 DL x T DR,
  lenv_split D1 D2 (DL ++ [(x, lbind_typ T)] ++ DR) ->
  (exists D1L, exists D1R, exists D2L, exists D2R,
    D1 = D1L ++ [(x, lbind_typ T)] ++ D1R /\
    D2 = D2L ++ D2R /\
    lenv_split D1L D2L DL /\
    lenv_split D1R D2R DR) \/
  (exists D1L, exists D1R, exists D2L, exists D2R,
    D1 = D1L ++ D1R /\
    D2 = D2L ++ [(x, lbind_typ T)] ++ D2R /\
    lenv_split D1L D2L DL /\
    lenv_split D1R D2R DR).

If lenv_split D_1 D_2 D_3 then D_1 and D_2 are distinct.
Lemma lenv_split_not_in_left: forall D1 D2 D3 x,
  lenv_split D1 D2 D3 ->
  x `in` dom D1 ->
  x `notin` dom D2.

Lemma lenv_split_not_in_right: forall D1 D2 D3 x,
  lenv_split D1 D2 D3 ->
  x `in` dom D2 ->
  x `notin` dom D1.

If lenv_split D_1 D_2 D_3 then we can append another context F to in front of both D_1 and D_3.
Lemma lenv_split_lin_weakening_left: forall F D1 D2 D3,
  lenv_split D1 D2 D3 ->
  wf_lenv (F ++ D3) ->
  lenv_split (F ++ D1) D2 (F ++ D3).

If lenv_split D_1 D_2 D_3 then we can eliminate an element from both D_1 and D_3.
Lemma lenv_split_sub_left: forall D1L D1R D2 DL DR x U F,
   lenv_split
        (D1L ++ [(x, lbind_typ U)] ++ D1R)
        D2
        (DL ++ [(x, lbind_typ U)] ++ DR) ->
   wf_lenv (DL ++ F ++ DR) ->
   lenv_split
        (D1L ++ F ++ D1R)
        D2
        (DL ++ F ++ DR).

If lenv_split D_1 D_2 D_3 then we can eliminate an element from both D_2 and D_3.
Lemma lenv_split_sub_right: forall D1 D2L D2R DL DR x U F,
   lenv_split
        D1
        (D2L ++ [(x, lbind_typ U)] ++ D2R)
        (DL ++ [(x, lbind_typ U)] ++ DR) ->
   wf_lenv (DL ++ F ++ DR) ->
   lenv_split
        D1
        (D2L ++ F ++ D2R)
        (DL ++ F ++ DR).

If lenv_split D_1 D_2 D_3 then we can add an element to an arbitrary position of both D_1 and D_3.
Lemma lenv_split_weakening_left: forall D1L D1R D2L D2R D3L D3R x T,
  lenv_split (D1L ++ D1R) (D2L ++ D2R) (D3L ++ D3R) ->
  lenv_split D1L D2L D3L ->
  lenv_split D1R D2R D3R ->
  wf_lenv (D3L ++ [(x, lbind_typ T)] ++ D3R) ->
  lenv_split (D1L ++ [(x, lbind_typ T)] ++ D1R) (D2L ++ D2R) (D3L ++ [(x, lbind_typ T)]++ D3R).

If lenv_split D_1 D_2 D_3 then we can add an element to an arbitrary position of both D_2 and D_3.
Lemma lenv_split_weakening_right: forall D1L D1R D2L D2R D3L D3R x T,
  lenv_split (D1L ++ D1R) (D2L ++ D2R) (D3L ++ D3R) ->
  lenv_split D1L D2L D3L ->
  lenv_split D1R D2R D3R ->
  wf_lenv (D3L ++ [(x, lbind_typ T)] ++ D3R) ->
  lenv_split (D1L ++ D1R) (D2L ++ [(x, lbind_typ T)] ++ D2R) (D3L ++ [(x, lbind_typ T)]++ D3R).

Lemma lenv_split_cases_app: forall DL D1 D2 DR,
  lenv_split D1 D2 (DL ++ DR) ->
  exists D1L, exists D1R, exists D2L, exists D2R,
    lenv_split D1L D2L DL /\
    lenv_split D1R D2R DR /\
    D1L ++ D1R = D1 /\
    D2L ++ D2R = D2.

Lemma lenv_split_permute: forall D1 D2 D3,
  lenv_split D1 D2 D3 ->
  permute D3 (D1 ++ D2).

When reasoning about the binds relation and map, we occasionally encounter situations where the binding is over-simplified. The following hint undoes that simplification, thus enabling Hints from the Environment library.


Administrative lemmas for F^O



Properties of wf_typ, wf_lenv, and lenv_split


A well-formed type T is locally closed.
Lemma type_from_wf_typ : forall T K,
  wf_typ T K -> type T.

Well-formedness is preserved under type substitution.
Lemma wf_typ_subst_tb : forall alpha ka P T K,
  wf_typ T K ->
  wf_typ P ka->
  wf_typ (subst_tt alpha ka P T) K.

Well-formedness is preserved under renaming.
Lemma wf_typ_rename : forall T (x y:ftvar) K1 K2,
  y `notin` (fv_tt T) ->
  x `notin` (fv_tt T) ->
  wf_typ (open_tt T (x ^^ K1)) K2 ->
  wf_typ (open_tt T (y ^^ K1)) K2.

Lemma wf_all_exists : forall T (alpha:ftvar) K1 K2,
  alpha `notin` (fv_tt T) ->
  wf_typ (open_tt T (alpha ^^ K1)) K2 ->
  wf_typ (typ_all K1 T) K2.

This is an auxiliary lemma for case analysis of a kind K. destruct K is not enough because wf_typ t kn_lin does not ensure that the kind of t is genuinely kn_lin, as it can be derived from wf_typ t kn_nonlin by the rule wf_typ_sub. Using this lemma, we can handle that case.
Lemma kn_cases : forall t K,
  wf_typ t K ->
  wf_typ t kn_nonlin \/ ~ wf_typ t kn_nonlin.

A well-formed environment D consists of distinct elements.
Lemma uniq_from_wf_lenv: forall D,
  wf_lenv D ->
  uniq D.

We add uniq_from_wf_env as a hint here since it helps blur the distinction between wf_env and uniq in proofs. The lemmas in the Environment library use uniq, whereas here we naturally have (or can easily show) the stronger wf_env. Thus, uniq_from_wf_env serves as a bridge that allows us to use the environments library.


Lemma wf_lenv_lin_weakening: forall D1 D2 x TX,
  wf_typ TX kn_lin ->
  wf_lenv (D1 ++ D2) ->
  x `notin` dom (D1 ++ D2) ->
  wf_lenv (D1 ++ [(x, lbind_typ TX)] ++ D2).

Lemma wf_lenv_split_both: forall D1 D2 D3,
  lenv_split D1 D2 D3 ->
  wf_lenv (D1 ++ D2).

lenv_split relation is preserved under type substitution.
Lemma lenv_split_subst_tb : forall D1 D2 D3 alpha ka P,
  lenv_split D1 D2 D3 ->
  wf_typ P ka ->
  lenv_split (map (subst_tlb alpha ka P) D1)
             (map (subst_tlb alpha ka P) D2)
             (map (subst_tlb alpha ka P) D3).

lenv_split relation is preserved under permutation.
Lemma lenv_split_exists_permute: forall D1 D2 D3 DX,
  lenv_split D1 D2 D3 ->
  permute D3 DX ->
  exists D1P, exists D2P,
    permute D1 D1P /\
    permute D2 D2P /\
    lenv_split D1P D2P DX.

Properties of substitution


Local closure is preserved under substitution


While these lemmas may be considered properties of substitution, we separate them out due to the lemmas that they depend on.

The following lemma depends on subst_tt_open_tt_var.

Lemma subst_tt_type : forall alpha ka P T,
  type T ->
  type P ->
  type (subst_tt alpha ka P T).

The following lemma depends on subst_tt_type and subst_te_open_ee_var.

Lemma subst_te_expr : forall alpha ka P e,
  expr e ->
  type P ->
  expr (subst_te alpha ka P e).

The following lemma depends on subst_ee_open_ee_var and subst_ee_open_te_var.

Lemma subst_ee_expr : forall x tx e1 e2,
  expr e1 ->
  expr e2 ->
  expr (subst_ee x tx e2 e1).

We add as hints the fact that local closure is preserved under substitution. This is part of our strategy foexprr automatically discharging local-closure proof obligations.


Valueness is preserved under substitution with locally closed types or expressions


Lemma value_through_subst_te : forall e Z P k,
  type P ->
  value e ->
  value (subst_te Z k P e).

Lemma value_through_subst_ee: forall e1 x xt u,
  expr u ->
  value e1 ->
  value (subst_ee x xt u e1).

Substitution makes no effect for some cases


Assume typing D e T. A substitution for a term parameter which is not found in the linear context D and has a genuine linear kind, kn_lin, does not affect e.
Lemma non_subst : forall X tx D e T U,
  typing D e T ->
  X `notin` dom D ->
  wf_typ tx kn_lin /\ ~ wf_typ tx kn_nonlin->
  e = [: (X, tx) ::~> U :]e.

Lemma subst_tlb_identity: forall D alpha ka T,
  alpha `notin` fv_lenv D ->
  D = (map (subst_tlb alpha ka T) D).

Regularity lemmas


typing D e T implies that
  • the linear context D is well-formed,
  • e is locally closed, and
  • T is well-formed (with kn_lin).
Note that we use kn_lin for the well-formedness of type T since it is the most general case in result of the subtype relation.
Lemma typing_regular : forall D e T,
  typing D e T ->
  wf_lenv D /\ expr e /\ wf_typ T kn_lin.

Every value is locally closed.
Lemma value_regular : forall e,
  value e ->
  expr e.

Reduction relation red handles only locally closed expressions.
Lemma red_regular : forall e e',
  red e e' ->
  expr e /\ expr e'.

Automation


The lemma uniq_from_wf_env was already added above as a hint since it helps blur the distinction between wf_env and uniq in proofs.

As currently stated, the regularity lemmas are ill-suited to be used with auto and eauto since they end in conjunctions. Even if we were, for example, to split sub_regularity into three separate lemmas, the resulting lemmas would be usable only by eauto and there is no guarantee that eauto would be able to find proofs effectively. Thus, the hints below apply the regularity lemmas and type_from_wf_typ to discharge goals about local closure and well-formedness, but in such a way as to minimize proof search.

The first hint introduces an wf_env fact into the context. It works well when combined with the lemmas relating wf_env and wf_typ. We choose to use those lemmas explicitly via auto( using ...) tactics rather than add them as hints. When used this way, the explicitness makes the proof more informative rather than more cluttered (with useless details).

The other three hints try outright to solve their respective goals.





Type-safety proofs for F^O


In parentheses are given the label of the corresponding lemma in the appendix (informal proofs) of the POPLmark Challenge.

Properties of typing


The linear context is unordered.

Lemma typing_permute: forall D1 D2 e t,
  typing D1 e t ->
  permute D1 D2 ->
  typing D2 e t.

The linear context is unordered.
Lemma typing_split: forall D3 e T D1 D2,
  typing (D1 ++ D2) e T ->
  lenv_split D1 D2 D3 ->
  typing D3 e T.

The linear context is empty for non-linear kind term.
Lemma value_nonlin_inversion: forall D e T,
  typing D e T ->
  value e ->
  wf_typ T kn_nonlin ->
  D = lempty.

Type substitution preserves typing (11)


Lemma typing_through_subst_te : forall D alpha ka e T P,
  typing D e T ->
  wf_typ P ka ->
  typing (map (subst_tlb alpha ka P) D) (subst_te alpha ka P e) (subst_tt alpha ka P T).

Substitution preserves typing (8)


Lemma typing_through_subst_ee_nonlin: forall D e T x xt u,
  typing D e T ->
  typing lempty u xt ->
  x `notin` dom D ->
  typing D (subst_ee x xt u e) T.

Lemma typing_through_subst_ee_lin: forall D2 x U D1 e T F u,
  value u ->
  typing (D2 ++ [(x, lbind_typ U)] ++ D1) e T ->
  typing F u U ->
  wf_lenv (D2 ++ F ++ D1) ->
  typing (D2 ++ F ++ D1) (subst_ee x U u e) T.

Preservation (20)


Lemma preservation : forall D e e' T,
  typing D e T ->
  red e e' ->
  typing D e' T.

Progress


Canonical forms (14)


Lemma canonical_form_abs : forall e K U1 U2,
  value e ->
  typing nil e (typ_arrow K U1 U2) ->
  exists K1, exists V, exists e1, (e = exp_abs K1 V e1) /\ (K = kn_nonlin -> K1 = kn_nonlin).

Lemma canonical_form_tabs : forall e Q U1,
  value e ->
  typing lempty e (typ_all Q U1) ->
  exists V, exists e1, e = exp_tabs V e1.

Lemma canonical_form_with : forall e U1 U2,
  value e ->
  typing lempty e (typ_with U1 U2) ->
  exists e1, exists e2, e = exp_apair e1 e2.

Progress (16)


Lemma progress : forall e T,
  (forall X, X `notin` fv_ee e) ->
  typing lempty e T ->
  value e \/ exists e', red e e'.

This page has been generated by coqdoc