Library Fequiv

This file presents the equivalence of System Fsub with and without contexts.
  • Authors: Jonghyun Park and Jeongbong Seo


Contents

  • Syntax
    • erased_t and erased_e
  • Variables
  • Parameters
  • Substitution
  • Typing contexts
  • Local closure
  • Well-formed typing contexts
  • Subtyping relation
    • sub: a subtyping relation of System Fsub with contexts
    • ann_sub: a subtyping relation of System Fsub without contexts
  • Typing relation
    • typing: a typing relation of System Fsub with contexts
    • ann_typing: a typing relation of System Fsub without contexts
  • Unrolling
  • Tactical support
  • Properties of System Fsub with contexts
  • Properties of System Fsub without contexts
  • Preliminaries
  • The equivalence proof (Theorem 7)
    • Equivalence of sub and ann_sub
      • Lemma sub_implies_ann_sub
      • Lemma ann_sub_implies_sub
    • Equivalence of typing and ann_typing
      • Lemma typing_implies_ann_typing
      • Lemma ann_typing_implies_typing

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.
Notation ltvar := nat. Notation ftvar := nat. Notation ann_ftvar := nat.
Notation lvar := nat. Notation fvar := nat. Notation ann_fvar := nat.
To prove the equivalence of two systems, we use the following definition of types and terms:
 types T, U, S := \top | A | X | X <: T | T -> U | \forall A <: T. U 
 terms t, u, s := a | x | x : T | \lambda a : T. t | t u | \Lambda A <: T. t | t [ T ] 
Note that the definition allows us to use both parameters with and without annotation. We refer to type parameters without annotation as erased type parameters, and type parameters with annotation as annotated type parameters.

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_ann_ftvar : ann_ftvar -> typ -> typ
| typ_arrow : typ -> typ -> typ
| typ_all : ltvar -> typ -> typ -> typ.

Inductive tm : Set :=
| tm_lvar : lvar -> tm
| tm_fvar : fvar -> tm
| tm_ann_fvar : ann_fvar -> typ -> 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 " X ^^ T " := (typ_ann_ftvar X T) (at level 65).
Notation " T --> U " := (typ_arrow T U) (at level 65).

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

Lemma typ_dec : forall T U : typ,
  {T = U} + {T <> U}.

Lemma ftvar_dec : forall (X Y : ftvar),
  {X = Y} + {X <> Y}.

Lemma ann_ftvar_dec : forall (Xt Yt : (ann_ftvar * typ)),
  {Xt = Yt} + {Xt <> Yt}.

Lemma fvar_dec : forall (x y : fvar),
  {x = y} + {x <> y}.

Lemma ann_fvar_dec : forall (xt yt : (ann_fvar * typ)),
  {xt = yt} + {xt <> yt}.

Notation "p ==_t q" := (fvar_dec p q) (at level 70).
Notation "p ==_T q" := (ftvar_dec p q) (at level 70).
Notation "p ===_t q" := (ann_fvar_dec p q) (at level 70).
Notation "p ===_T q" := (ann_ftvar_dec p q) (at level 70).

erased_t and erased_e

A type T (or a term t) is said to be erased if every parameter in it is erased. We use erased_t and erased_e to denote such erased types and terms.
Inductive erased_t : typ -> Prop :=
| erased_t_top :
  erased_t typ_top
| erased_t_ltvar : forall A,
  erased_t (typ_ltvar A)
| erased_t_ftvar : forall X,
  erased_t (X ^^)
| erased_t_arrow : forall T U,
  erased_t T ->
  erased_t U ->
  erased_t (T --> U)
| erased_t_all : forall A T U,
  erased_t T ->
  erased_t U ->
  erased_t (typ_all A T U).

Inductive erased_e : tm -> Prop :=
| erased_e_lvar : forall a,
  erased_e (tm_lvar a)
| erased_e_fvar : forall x,
  erased_e (x **)
| erased_e_abs : forall a T t,
  erased_t T ->
  erased_e t -> erased_e (tm_abs a T t)
| erased_e_app : forall t t',
  erased_e t ->
  erased_e t' ->
  erased_e (tm_app t t')
| erased_e_tabs : forall A T t,
  erased_t T ->
  erased_e t ->
  erased_e (tm_tabs A T t)
| erased_e_tapp : forall t T,
  erased_e t ->
  erased_t T ->
  erased_e (tm_tapp t T).


Variables

The function LV_all_tt, defined below, calculates the set of type variables that appear in a type T.
Fixpoint LV_all_tt (T: typ) : list ltvar :=
  match T with
    | typ_top => nil
    | typ_ltvar A => A :: nil
    | X ^^ => nil
    | X ^^ T => nil
    | T1 --> T2 => LV_all_tt T1 ++ LV_all_tt T2
    | typ_all A T1 T2 => A :: (LV_all_tt T1 ++ LV_all_tt T2)
  end.

Parameters

Type parameters

The functions FV_tt and FV_te, defined below, calculate the set of erased type parameters in a type and a term, respectively.
Fixpoint FV_tt (T:typ) : list ftvar :=
  match T with
    | typ_top => nil
    | typ_ltvar _ => nil
    | X ^^ => X :: nil
    | X ^^ _ => nil
    | T1 --> T2 => FV_tt T1 ++ FV_tt T2
    | typ_all _ T1 T2 => FV_tt T1 ++ FV_tt T2
  end.

Fixpoint FV_te (t : tm) : list ftvar :=
  match t with
  | tm_lvar _ => nil
  | _ ** => nil
  | _ ** _ => 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.

The functions ann_FV_tt and ann_FV_te, defined below, calculate the set of annotated type parameters in a type and a term, respectively.
Fixpoint ann_FV_tt (T:typ) : list ann_ftvar :=
  match T with
    | typ_top => nil
    | typ_ltvar _ => nil
    | X ^^ => nil
    | X ^^ T => X :: (ann_FV_tt T)
    | T1 --> T2 => ann_FV_tt T1 ++ ann_FV_tt T2
    | typ_all _ T1 T2 => ann_FV_tt T1 ++ ann_FV_tt T2
  end.

Fixpoint ann_FV_te (t:tm) : list ann_ftvar :=
  match t with
    | tm_lvar _ => nil
    | _ ** => nil
    | _ ** T => ann_FV_tt T
    | tm_abs _ T t => ann_FV_tt T ++ ann_FV_te t
    | tm_app t t' => ann_FV_te t ++ ann_FV_te t'
    | tm_tabs _ T t => ann_FV_tt T ++ ann_FV_te t
    | tm_tapp t T => ann_FV_te t ++ ann_FV_tt T
  end.

Term parameters

The function FV_ee, defined below, calculates the set of erased term parameters in a term, and the function ann_FV_ee calculates the set of annotated term parameters in a term.
Fixpoint FV_ee (t : tm) : list fvar :=
  match t with
    | tm_lvar _ => nil
    | x ** => x :: nil
    | _ ** _ => nil
    | tm_abs _ _ 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.

Fixpoint ann_FV_ee (t : tm) : list ann_fvar :=
  match t with
    | tm_lvar _ => nil
    | x ** => nil
    | x ** _ => x :: nil
    | tm_abs _ _ t => ann_FV_ee t
    | tm_app t t' => ann_FV_ee t ++ ann_FV_ee t'
    | tm_tabs _ _ t => ann_FV_ee t
    | tm_tapp t _ => ann_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.
Fixpoint lsubst_tt (B : ltvar) (U : typ) (T : typ) : typ :=
  match T with
    | typ_top => typ_top
    | typ_ltvar A => if A == B then U else typ_ltvar A
    | X ^^ => X ^^
    | X ^^ T => X ^^ T
    | T1 --> T2 => (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) : tm :=
  match t with
    | tm_lvar a => tm_lvar a
    | x ** => x **
    | x ** T => x ** T
    | 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.
Fixpoint lsubst_ee (b : lvar) (u : tm) (t : tm) : tm :=
  match t with
    | tm_lvar a => if a == b then u else tm_lvar a
    | x ** => x **
    | x ** T => x ** T
    | 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 replace an erased type parameter with a type.
Fixpoint fsubst_tt (Y:ftvar) (U : typ) (T : typ) : typ :=
  match T with
    | typ_top => typ_top
    | typ_ltvar A => typ_ltvar A
    | X ^^ => if X == Y then U else X ^^
    | X ^^ T => X ^^ T
    | 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) : tm :=
  match t with
    | tm_lvar a => tm_lvar a
    | X ** => X **
    | X ** T => X ** T
    | 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.

The functions ann_fsubst_tt and ann_fsubst_te replace an annotated type parameter with a type. Note that ann_fsubst_tt replaces a type parameter only when both a parameter and its annotated type are matched.
Fixpoint ann_fsubst_tt (Y:ann_ftvar) (TY:typ) (U : typ) (T : typ) : typ :=
  match T with
    | typ_top => typ_top
    | typ_ltvar A => typ_ltvar A
    | X ^^ => X ^^
    | X ^^ T =>
      if ann_ftvar_dec (X, T) (Y, TY)
        then U else (X ^^ (ann_fsubst_tt Y TY U T))
    | T1 --> T2 =>
      (ann_fsubst_tt Y TY U T1) --> (ann_fsubst_tt Y TY U T2)
    | typ_all A T1 T2 =>
      typ_all A (ann_fsubst_tt Y TY U T1) (ann_fsubst_tt Y TY U T2)
  end.

Fixpoint ann_fsubst_te (Y : ann_ftvar) (TY:typ) (U:typ) (t:tm) : tm :=
  match t with
    | tm_lvar a => tm_lvar a
    | x ** => x **
    | x ** T => x ** (ann_fsubst_tt Y TY U T)
    | tm_abs A T t =>
      tm_abs A (ann_fsubst_tt Y TY U T) (ann_fsubst_te Y TY U t)
    | tm_app t1 t2 =>
      tm_app (ann_fsubst_te Y TY U t1) (ann_fsubst_te Y TY U t2)
    | tm_tabs A T t =>
      tm_tabs A (ann_fsubst_tt Y TY U T) (ann_fsubst_te Y TY U t)
    | tm_tapp t T =>
      tm_tapp (ann_fsubst_te Y TY U t) (ann_fsubst_tt Y TY U T)
  end.

Term parameters

The function fsubst_ee replaces an erased term parameter with a term.
Fixpoint fsubst_ee (y : fvar) (u t: tm) : tm :=
  match t with
    | tm_lvar a => tm_lvar a
    | x ** => if x == y then u else tm_fvar x
    | x ** T => x ** T
    | 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.

The function ann_fsubst_tt replaces an annotated term parameter with a term. Note that ann_fsubst_ee replaces a term parameter only when both a parameter and its annotated type are matched.
Fixpoint ann_fsubst_ee (y : ann_fvar) (Ty:typ) (u t: tm) : tm :=
  match t with
    | tm_lvar a => tm_lvar a
    | x ** => x **
    | x ** T =>
      if ann_fvar_dec (x, T) (y, Ty) then u else x ** T
    | tm_abs a T t => tm_abs a T (ann_fsubst_ee y Ty u t)
    | tm_app t1 t2 =>
      tm_app (ann_fsubst_ee y Ty u t1) (ann_fsubst_ee y Ty u t2)
    | tm_tabs A T t => tm_tabs A T (ann_fsubst_ee y Ty u t)
    | tm_tapp t T => tm_tapp (ann_fsubst_ee y Ty 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).

Notation "[ ( X , TX ) ~> U ] T" := (ann_fsubst_tt X TX U T) (at level 67).
Notation "[ ( X , TX ) :~> U ] t " := (ann_fsubst_te X TX U t) (at level 67).
Notation "[ ( x , Tx ) ::~> u ] t " := (ann_fsubst_ee x Tx 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_fvar x T) (at level 56).
Notation " X ~<: T " := (ctxt_bind_ftvar 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
    | (_ ~: _) :: Gamma' => dom_tc Gamma'
    | (X ~<: _) :: 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 converse is also true.
Lemma exists_ftvar_bind : forall X Gamma,
  In X (dom_tc Gamma) -> exists T, In (X ~<: T) Gamma.

The function dom_ec, defined below, calculates the set of term parameters bound in a typing context.
Fixpoint dom_ec (Gamma : ctxt) : list fvar :=
  match Gamma with
    | nil => nil
    | (x ~: _) :: Gamma' => x :: dom_ec Gamma'
    | (_ ~<: _ ) :: 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 erased type parameters that appear in a typing context.
Fixpoint FV_tc (Gamma : ctxt) : list ftvar :=
  match Gamma with
    | nil => nil
    | (_ ~: T) :: Gamma' => FV_tt T ++ FV_tc Gamma'
    | (X ~<: T) :: Gamma' => X :: (FV_tt T ++ FV_tc Gamma')
  end.

Thus, FV_tc Gamma includes all the erased 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'.

Local closure

Local closure of types

We bring the definition of lclosed_t from lclosed_t in Fnamedcontext.v, and that of ann_lclosed_t from lclosed_t in Fnamed.v.
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).


Inductive ann_lclosed_t : list ltvar -> typ -> Prop :=
| ann_lclosed_t_top :
  ann_lclosed_t emptyset typ_top
| ann_lclosed_t_ltvar : forall A,
  ann_lclosed_t (A :: emptyset) (typ_ltvar A)
| ann_lclosed_t_ftvar : forall X (T : typ),
  ann_lclosed_t emptyset T ->
  ann_lclosed_t emptyset (X ^^ T)
| ann_lclosed_t_arrow : forall I1 I2 (T U : typ),
  ann_lclosed_t I1 T ->
  ann_lclosed_t I2 U ->
  ann_lclosed_t (I1 ++ I2) (T --> U)
| ann_lclosed_t_all : forall I1 I2 A T U,
  ann_lclosed_t I1 T ->
  ann_lclosed_t I2 U ->
  ann_lclosed_t (I1 ++ (remove eq_nat_dec A I2)) (typ_all A T U).


Local closure of terms

Similarly, we bring the definition of lclosed_e from lclosed_e in Fnamedcontext.v and that of ann_lclosed_e from lclosed_e in Fnamed.v.
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).


Inductive ann_lclosed_e : list ltvar -> list lvar -> tm -> Prop :=
| ann_lclosed_e_lvar : forall a,
  ann_lclosed_e nil (a :: nil) (tm_lvar a)
| ann_lclosed_e_fvar : forall x T,
  ann_lclosed_t emptyset T ->
  ann_lclosed_e emptyset emptyset (x ** T)
| ann_lclosed_e_abs : forall I1 I2 i a T t,
  ann_lclosed_t I1 T ->
  ann_lclosed_e I2 i t ->
  ann_lclosed_e (I1 ++ I2) (remove eq_nat_dec a i) (tm_abs a T t)
| ann_lclosed_e_app : forall I1 I2 i1 i2 t1 t2,
  ann_lclosed_e I1 i1 t1 ->
  ann_lclosed_e I2 i2 t2 ->
  ann_lclosed_e (I1 ++ I2) (i1 ++ i2) (tm_app t1 t2)
| ann_lclosed_e_tabs : forall I1 I2 i A T t,
  ann_lclosed_t I1 T ->
  ann_lclosed_e I2 i t ->
  ann_lclosed_e (I1 ++ (remove eq_nat_dec A I2)) i (tm_tabs A T t)
| ann_lclosed_e_tapp : forall I1 I2 i t T,
  ann_lclosed_e I1 i t ->
  ann_lclosed_t I2 T ->
  ann_lclosed_e (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. Note the use of lclosed_t in the ctxt_okay_epar and ctxt_okay_tpar cases.
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 nil T ->
  ctxt_okay (x ~: T :: Gamma)
| ctxt_okay_tpar : forall Gamma X T,
  ctxt_okay Gamma ->
  ~ In X (dom_tc Gamma) ->
  lclosed_t Gamma nil T ->
  ctxt_okay (X ~<: T :: Gamma).


Subtyping relation

We bring the definition of sub from sub in Fnamedcontext.v, and that of ann_sub from sub in Fnamed.v. Since out proof necessities induction on the size of ann_sub proofs, we also bring the definition of ann_subLH from subLH in Fnamed.v.
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 X A B,
  sub Gamma U1 T1 ->
  ~ In X (FV_tc Gamma) ->
  ~ In X (FV_tt T2 ++ FV_tt U2) ->
  sub (X ~<: U1 :: Gamma) ({A ~> X ^^} T2) ({B ~> X ^^} U2) ->
  sub Gamma (typ_all A T1 T2) (typ_all B U1 U2).


Inductive ann_sub : typ -> typ -> Prop :=
| ann_sub_top : forall T,
  ann_lclosed_t emptyset T ->
  ann_sub T typ_top
| ann_sub_refl_tvar : forall T X,
  ann_lclosed_t emptyset T ->
  ann_sub (X ^^ T) (X ^^ T)
| ann_sub_trans_tvar : forall T U X,
  ann_sub T U ->
  ann_sub (X ^^ T) U
| ann_sub_arrow : forall T1 T2 U1 U2,
  ann_sub U1 T1 ->
  ann_sub T2 U2 ->
  ann_sub (T1 --> T2) (U1 --> U2)
| ann_sub_all : forall T1 T2 U1 U2 X A B,
  ann_sub U1 T1 ->
  ~ In X (ann_FV_tt T2) ->
  ~ In X (ann_FV_tt U2) ->
  ~ In X (ann_FV_tt T1) ->
  ~ In X (ann_FV_tt U1) ->
  ann_sub ({A ~> X ^^ U1} T2) ({B ~> X ^^ U1} U2) ->
  ann_sub (typ_all A T1 T2) (typ_all B U1 U2).

Inductive ann_subLH : nat -> typ -> typ -> Prop :=
| ann_subLH_top : forall T,
  ann_lclosed_t emptyset T ->
  ann_subLH O T typ_top
| ann_subLH_refl_tvar : forall T X,
  ann_lclosed_t emptyset T ->
  ann_subLH O (X ^^ T) (X ^^ T)
| ann_subLH_trans_tvar : forall T U X n,
  ann_subLH n T U ->
  ann_subLH (S n) (X ^^ T) U
| ann_subLH_arrow : forall T1 T2 U1 U2 n1 n2,
  ann_subLH n1 U1 T1 ->
  ann_subLH n2 T2 U2 ->
  ann_subLH (S (max n1 n2)) (T1 --> T2) (U1 --> U2)
| ann_subLH_all : forall T1 T2 U1 U2 X n1 n2 A B,
  ann_subLH n1 U1 T1 ->
  ~ In X (ann_FV_tt T2) ->
  ~ In X (ann_FV_tt U2) ->
  ~ In X (ann_FV_tt T1) ->
  ~ In X (ann_FV_tt U1) ->
  ann_subLH n2 ({A ~> X ^^ U1} T2) ({B ~> X ^^ U1} U2) ->
  ann_subLH (S (max n1 n2)) (typ_all A T1 T2) (typ_all B U1 U2).


Lemma ann_sub_subLH and ann_subLH_sub formally state the equivalence between ann_sub and ann_subLH.
Lemma ann_sub_subLH : forall annA annB,
  ann_sub annA annB -> exists n, ann_subLH n annA annB.

Lemma ann_subLH_sub : forall n annA annB,
  ann_subLH n annA annB -> ann_sub annA annB.


Typing relation

We bring the definition of typing from typing in Fnamedcontext.v, and that of ann_typing from typing in Fnamed.v. Since our proof uses induction on the size of ann_typing proofs, we introduce the inductive definition ann_typingLH. Note that the definition of ann_typingLH is different from that of typingLH in Fnamed.v. The size of proofs does not increase for the ann_typingLH_sub case.
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 x,
  lclosed_t Gamma emptyset T ->
  ~ In x (dom_ec Gamma) ->
  ~ In x (FV_ee t) ->
  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 X,
  lclosed_t Gamma emptyset T ->
  ~ In X (FV_tc Gamma) ->
  ~ In X (FV_te t ++ FV_tt U) ->
  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.


Inductive ann_typing : tm -> typ -> Prop :=
| ann_typing_fvar : forall x T,
  ann_lclosed_t emptyset T ->
  ann_typing (x ** T) T
| ann_typing_abs : forall a T U t x,
  ann_lclosed_t emptyset T ->
  ~ In x (ann_FV_ee t) ->
  ann_typing ({a ::~> x ** T} t) U ->
  ann_typing (tm_abs a T t) (T --> U)
| ann_typing_app : forall t t' T U,
  ann_typing t (T --> U) ->
  ann_typing t' T ->
  ann_typing (tm_app t t') U
| ann_typing_tabs : forall A T t B U X,
  ann_lclosed_t emptyset T ->
  ~ In X (ann_FV_te t ++ ann_FV_tt U) ->
  ann_typing ({A :~> X ^^ T} t) ({B ~> X ^^ T} U) ->
  ann_typing (tm_tabs A T t) (typ_all B T U)
| ann_typing_tapp : forall t A T U S,
  ann_typing t (typ_all A U S) ->
  ann_sub T U ->
  ann_typing (tm_tapp t T) ({A ~> T} S)
| ann_typing_sub : forall t T U,
  ann_typing t T ->
  ann_sub T U ->
  ann_typing t U.

Inductive ann_typingLH : nat -> tm -> typ -> Prop :=
| ann_typingLH_fvar : forall x T,
  ann_lclosed_t emptyset T ->
  ann_typingLH O (x ** T) T
| ann_typingLH_abs : forall a T U t x k,
  ann_lclosed_t emptyset T ->
  ~ In x (ann_FV_ee t) ->
  ann_typingLH k ({a ::~> x ** T} t) U ->
  ann_typingLH (S k) (tm_abs a T t) (T --> U)
| ann_typingLH_app : forall t t' T U k1 k2,
  ann_typingLH k1 t (T --> U) ->
  ann_typingLH k2 t' T ->
  ann_typingLH (S (max k1 k2)) (tm_app t t') U
| ann_typingLH_tabs : forall A T t B U X k,
  ann_lclosed_t emptyset T ->
  ~ In X (ann_FV_te t ++ ann_FV_tt U) ->
  ann_typingLH k ({A :~> X ^^ T} t) ({B ~> X ^^ T} U) ->
  ann_typingLH (S k) (tm_tabs A T t) (typ_all B T U)
| ann_typingLH_tapp : forall t A T U S k,
  ann_typingLH k t (typ_all A U S) ->
  ann_sub T U ->
  ann_typingLH (Datatypes.S k) (tm_tapp t T) ({A ~> T} S)
| ann_typingLH_sub : forall t T U k,
  ann_typingLH k t T ->
  ann_sub T U ->
  ann_typingLH k t U.

The proof of the equivalence of typing and ann_typing exploits properties of ann_typing proofs whose last case is not the ann_typingLH_sub case. We use ann_pure_typingLH to denote such proofs.
Inductive ann_pure_typingLH : nat -> tm -> typ -> Prop :=
| ann_pure_typingLH_fvar : forall x T,
  ann_lclosed_t emptyset T ->
  ann_pure_typingLH O (x ** T) T
| ann_pure_typingLH_abs : forall a T U t x k,
  ann_lclosed_t emptyset T ->
  ~ In x (ann_FV_ee t) ->
  ann_typingLH k ({a ::~> x ** T} t) U ->
  ann_pure_typingLH (S k) (tm_abs a T t) (T --> U)
| ann_pure_typingLH_app : forall t t' T U k1 k2,
  ann_typingLH k1 t (T --> U) ->
  ann_typingLH k2 t' T ->
  ann_pure_typingLH (S (max k1 k2)) (tm_app t t') U
| ann_pure_typingLH_tabs : forall A T t B U X k,
  ann_lclosed_t emptyset T ->
  ~ In X (ann_FV_te t ++ ann_FV_tt U) ->
  ann_typingLH k ({A :~> X ^^ T} t) ({B ~> X ^^ T} U) ->
  ann_pure_typingLH (S k) (tm_tabs A T t) (typ_all B T U)
| ann_pure_typingLH_tapp : forall t A T U S k,
  ann_typingLH k t (typ_all A U S) ->
  ann_sub T U ->
  ann_pure_typingLH (Datatypes.S k) (tm_tapp t T) ({A ~> T} S).


Lemma ann_typing_implies_ann_typingLH : forall ann_e ann_A,
  ann_typing ann_e ann_A ->
  exists n, ann_typingLH n ann_e ann_A.

Lemma ann_pure_typingLH_implies_ann_typingLH : forall n ann_e ann_A,
  ann_pure_typingLH n ann_e ann_A -> ann_typingLH n ann_e ann_A.


Unrolling

We show the equivalence via two bridge functions: unroll_t and unroll_e. These functions take a typing context Gamma and replace erased parameters with annotated parameters according to the typing context Gamma.

We refer to an operation that replaces erased parameters with annotated ones as "unrolling".

We use unroll_t Gamma T to denote a result of unrolling a type T, and unroll_e Gamma t to denote a result of unrolling a term t.
Fixpoint unroll_t (Gamma : ctxt) (U : typ) : typ :=
  match Gamma with
    | nil => U
    | (x ~: T) :: Gamma' =>
      unroll_t Gamma' U
    | (X ~<: T) :: Gamma' =>
      unroll_t Gamma' ([ X ~> (X ^^ (unroll_t Gamma' T))] U)
  end.

Fixpoint unroll_e (Gamma : ctxt) (u : tm) : tm :=
  match Gamma with
    | nil => u
    | (x ~: T) :: Gamma' =>
      unroll_e Gamma' ([x ::~> (x ** (unroll_t Gamma' T))] u)
    | (X ~<: T) :: Gamma' =>
      unroll_e Gamma' ([ X :~> (X ^^ (unroll_t Gamma' T))] u)
  end.

Tactical support

We introduce an automation tactic Simplify to simplify the proof. Simplify attempts to evaluate several fixpoint functions, such as FV_tt, ann_FV_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.

Properties of System Fsub with contexts

This section presents properties of System Fsub with contexts that we use in the equivalence proof. Each lemma has the same name as the corresponding lemma in Fnamedcontext.v.

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


Lemma ctxt_okay_app : forall Gamma Delta,
  ctxt_okay (Gamma ++ Delta)->
  ctxt_okay Delta.

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.

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


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


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.


Lemma sub_ctxt_okay : forall T U Gamma,
  sub Gamma T U ->
  ctxt_okay Gamma.

Lemma sub_lclosed_t : forall T U Gamma,
  sub Gamma T U ->
  lclosed_t Gamma emptyset T /\ lclosed_t Gamma emptyset U .

Lemma typing_ctxt_okay : forall Gamma t T,
  typing Gamma t T ->
  ctxt_okay Gamma.

Properties of System Fsub without contexts

This section presents properties of System Fsub without contexts that we use in the equivalence proof. Almost every lemma has a different name from the corresponding lemma in Fnamed.v. We annotate the name of the corresponding lemma as a comment for such lemmas. If there is no comment, it means that the lemma has the same name as the corresponding lemma.

lclosed_t_ltvar_split from Fnamed.v
Lemma ann_lclosed_t_ltvar_split : forall T A X U I0,
  ann_lclosed_t I0 ({A ~> X ^^ U} T) ->
  (exists I, (ann_lclosed_t I T /\ remove eq_nat_dec A I = I0)).

lclosed_t_subst_ltvar from Fnamed.v
Lemma ann_lclosed_t_subst_ltvar : forall T U I A,
  ann_lclosed_t emptyset U ->
  ann_lclosed_t I T ->
  ann_lclosed_t (remove eq_nat_dec A I) ({A ~> U} T).

lclosed_t_subst_ftvar from Fnamed.v
Lemma ann_lclosed_t_subst_ftvar : forall T U U' X I,
  ann_lclosed_t I T ->
  ann_lclosed_t emptyset U ->
  ann_lclosed_t I ([(X, U') ~> U] T).


Lemma subst_ltvar_nochange_t : forall I T,
  ann_lclosed_t I T -> forall A U, ~ In A I -> {A ~> U} T = T.

subst_ftvar_nochange_t from Fnamed.v
Lemma subst_ann_ftvar_nochange_t : forall T U S X,
  ~ In X (ann_FV_tt T) -> [(X, U) ~> S] T = T.


Fixpoint synsize_t (T:typ) :=
  match T with
    | typ_top => 0
    | typ_ltvar _ => 0
    | X ^^ => 0
    | X ^^ T => S (synsize_t T)
    | T --> U => S (synsize_t T + synsize_t U)
    | typ_all _ T U => S (synsize_t T + synsize_t U)
  end.

lem_subst_ftvar_nochange_t_idemp from Fnamed.v
Lemma lem_subst_ann_ftvar_nochange_t_idemp : forall T S,
  synsize_t S <= synsize_t T ->
  forall X U, [(X, T) ~> U] S = S.

subst_rename_ftvar_ltvar_t from Fnamed.v
Lemma subst_rename_ann_ftvar_ltvar_t : forall T U S X Y,
  forall A,
    [(X,U) ~> Y^^U] ({A ~> S} T) = {A ~> [(X,U) ~> Y^^U] S} ([(X,U) ~> Y^^U] T).

subst_ftvar_ltvar_t from Fnamed.v
Lemma subst_ann_ftvar_ltvar_t : forall T U S S' X,
  ann_lclosed_t emptyset S ->
  forall A,
    [(X,U) ~> S] ({A ~> S'} T) = {A ~> [(X,U) ~> S] S'} ([(X,U) ~> S] T).

subst_seq_ftvar_ltvar_t from Fnamed.v
Lemma subst_seq_ann_ftvar_ltvar_t : forall T U S X,
  ~ In X (ann_FV_tt T) ->
  forall A,
    [(X,U) ~> S] ({A ~> (X^^U)} T) = {A ~> S} T.

sub_lclosed_t from Fnamed.v
Lemma ann_sub_ann_lclosed_t : forall T U,
  ann_sub T U -> ann_lclosed_t emptyset T /\ ann_lclosed_t emptyset U.

lclosed_t_rename_ftvar from Fnamed.v
Lemma ann_lclosed_t_rename_ftvar : forall T U X Y I,
  ann_lclosed_t I T ->
  ann_lclosed_t I ([(X, U) ~> Y ^^ U] T).


sub_rename_ftvar_aux from Fnamed.v
Lemma ann_sub_rename_ftvar_aux : forall m n T U,
  n < m ->
  ann_subLH n T U ->
  forall X Y S,
      ann_subLH n ([(X,S) ~> Y^^S] T)
                  ([(X,S) ~> Y^^S] U).


sub_rename_ftvar from Fnamed.v
Lemma ann_sub_rename_ftvar : forall T U,
  ann_sub T U ->
  forall X Y S,
      ann_sub ([(X,S) ~> Y^^S] T)
              ([(X,S) ~> Y^^S] U).


This lemma does not appear in Fnamed.v, but is easily provable.
Lemma ann_subLH_ltvar_subst_rename_ftvar : forall T U,
  forall X, ~ In X (ann_FV_tt T) -> ~ In X (ann_FV_tt U) ->
  forall S A B Y n,
  ann_subLH n ({A ~> X ^^ S} T) ({B ~> X ^^ S} U) ->
  ann_subLH n ({A ~> Y ^^ S} T) ({B ~> Y ^^ S} U).


sub_ltvar_subst_rename_ftvar from Fnamed.v
Lemma ann_sub_ltvar_subst_rename_ftvar : forall T U,
  forall X, ~ In X (ann_FV_tt T) -> ~ In X (ann_FV_tt U) ->
  forall S A B Y,
  ann_sub ({A ~> X ^^ S} T) ({B ~> X ^^ S} U) ->
  ann_sub ({A ~> Y ^^ S} T) ({B ~> Y ^^ S} U).

sub_transitivity_on from Fnamed.v
Definition ann_sub_transitivity_on T := forall U S,
  ann_sub U T -> ann_sub T S -> ann_sub U S.

Fixpoint size_t (T : typ) : nat :=
  match T with
    | typ_top => 0
    | typ_ltvar _ => 0
    | typ_ftvar _ => 0
    | typ_ann_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 U,
  size_t ({A ~> X ^^ U} T) = size_t T.

sub_narrowing_aux from Fnamed.v
Lemma ann_sub_narrowing_aux : forall m n T U,
  n < m ->
  ann_subLH n T U ->
  forall S S',
    ann_sub_transitivity_on S ->
    ann_sub S' S ->
    forall X,
      ann_sub ([(X, S) ~> X ^^ S'] T) ([(X, S) ~> X ^^ S'] U).

sub_narrowing from Fnamed.v
Lemma ann_sub_narrowing : forall T U,
  ann_sub T U ->
  forall S S',
    ann_sub_transitivity_on S ->
    ann_sub S' S ->
    forall X,
      ann_sub ([(X, S) ~> X ^^ S'] T)
          ([(X, S) ~> X ^^ S'] U).

sub_trans_ftvar_aux from Fnamed.v
Lemma ann_sub_trans_ftvar_aux : forall A S U X,
  ann_sub A S ->
  S = (X ^^ U) ->
  forall S', ann_sub S S' -> ann_sub A S'.

sub_trans_fun_aux from Fnamed.v
Lemma ann_sub_trans_fun_aux : forall T U U1 U2 S,
  ann_sub_transitivity_on U1 ->
  ann_sub_transitivity_on U2 ->
  ann_sub T U ->
  ann_sub U S ->
  U = U1 --> U2 ->
  ann_sub T S.

sub_trans_forall_aux from Fnamed.v
Lemma ann_sub_trans_forall_aux : forall T U U1 U2 S A,
  (forall S, size_t S < size_t U -> ann_sub_transitivity_on S) ->
  ann_sub T U ->
  U = typ_all A U1 U2 ->
  ann_sub U S ->
  ann_sub T S.

sub_transitivity_aux from Fnamed.v
Lemma ann_sub_transitivity_aux : forall n T,
  size_t T < n -> ann_sub_transitivity_on T.

sub_transitivity from Fnamed.v
Lemma ann_sub_transitivity : forall T U S,
  ann_sub T U ->
  ann_sub U S ->
  ann_sub T S.

sub_reflexivity_aux from Fnamed.v
Lemma ann_sub_reflexivity_aux : forall n T,
  size_t T < n -> ann_lclosed_t emptyset T -> ann_sub T T.

This lemma also does not appear in Fnamed.v, but it is easily provable.
Lemma ann_sub_reflexivity : forall T,
  ann_lclosed_t emptyset T ->
  ann_sub T T.


subst_ftvar_nochange_e from Fnamed.v
Lemma subst_ann_ftvar_nochange_e : forall t X T U,
  ~ In X (ann_FV_te t) -> ([ ( X , T ) :~> U ] t) = t.


Lemma subst_lvar_lvar_e : forall t a x T b y U,
  a <> b ->
{b ::~> y ** U}({a ::~> x ** T} t) = {a ::~> x ** T}({b ::~> y ** U} t).

Lemma subst_ltvar_lvar_e : forall t A X a x T U ,
  {A :~> X ^^ T} ({a ::~> x ** U} t) = {a ::~> x ** U} ({A :~> X^^T} t).

subst_ftvar_lvar_e from Fnamed.v
Lemma subst_ann_ftvar_lvar_e : forall t u X T U a,
  [(X, T) :~> U]({a ::~> u} t) = {a ::~> ([(X, T) :~> U] u)}([ (X, T) :~> U] t).

subst_rename_ftvar_ltvar_e from Fnamed.v
Lemma subst_rename_ann_ftvar_ltvar_e : forall t A X Y T U,
  [(X, T) :~> (Y^^T)] ({A :~> U} t) =
    {A :~> [(X, T)~>(Y^^T)] U} ([(X, T) :~> (Y^^T)] t).

subst_seq_ftvar_ltvar_e from Fnamed.v
Lemma subst_seq_ann_ftvar_ltvar_e : forall t T U X,
  ~ In X (ann_FV_te t) ->
  forall A,
    [(X,T) :~> U] ({A :~> (X^^T)} t) = {A :~> U} t.

FV_te_nochange_lvar from Fnamed.v
Lemma ann_FV_te_nochange_lvar : forall t a x y T,
  ann_FV_te ({a ::~> x ** T} t) = ann_FV_te ({a ::~> y ** T} t).

FV_ee_nochange_ftvar from Fnamed.v
Lemma ann_FV_ee_nochange_ftvar : forall t X T Y U,
  ann_FV_ee ([(X, T) :~> Y^^U] t) = ann_FV_ee t.


Fixpoint size_e (t : tm) : nat :=
  match t with
    | tm_lvar _ => 0
    | tm_fvar _ => 0
    | tm_ann_fvar _ _ => 0
    | tm_abs _ _ t => S (size_e t)
    | tm_app t1 t2 => S (size_e t1 + size_e t2)
    | tm_tabs _ _ t => S (size_e t)
    | tm_tapp t _ => S (size_e t)
  end.

Lemma size_e_nochange_lvar : forall a x T t,
  size_e ({a ::~> x ** T} t) = size_e t.

Lemma size_e_nochange_ltvar : forall A X T t,
  size_e ({ A :~> X ^^ T} t) = size_e t.


typingLH_subst_lvar_rename_fvar from Fnamed.v
Lemma ann_typingLH_subst_lvar_rename_fvar_aux : forall k t u a x y T U n,
  n + size_e t < k ->
  ann_typingLH n u T ->
  u = {a ::~> x ** U} t ->
  ann_typingLH n ({a ::~> y ** U} t) T.

This lemma does not appear in Fnamed.v. Note that this lemma is a corollary of Lemma ann_typingLH_subst_lvar_rename_fvar_aux.
Lemma ann_typingLH_subst_lvar_rename_fvar : forall n t a x y T U,
  ann_typingLH n ({a ::~> x ** U} t) T ->
  ann_typingLH n ({a ::~> y ** U} t) T.

typing_rename_ftvar_aux from Fnamed.v
Lemma ann_typingLH_rename_ftvar : forall m n t T,
  n < m ->
  ann_typingLH n t T ->
  forall X Y U,
  ann_typingLH n ([(X, U) :~> Y ^^ U] t) ([(X, U) ~> Y ^^ U] T).

typingLH_subst_ltvar_rename_ftvar from Fnamed.v
Lemma ann_typingLH_subst_ltvar_rename_ftvar : forall m t T,
  forall X, ~ In X (ann_FV_te t) -> ~ In X (ann_FV_tt T) ->
  forall U Y A B ,
  ann_typingLH m ({A :~> X ^^ U} t) ({B ~> X ^^ U} T) ->
  ann_typingLH m ({A :~> Y ^^ U} t) ({B ~> Y ^^ U} T).

sub_subst_ftvar_aux from Fnamed.v
Lemma ann_sub_subst_ftvar_aux : forall m n T U,
  n < m ->
  ann_subLH n T U ->
  forall X S S',
    ann_sub S' S ->
    ann_sub ([(X, S) ~> S'] T) ([(X, S) ~> S'] U).

sub_subst_ftvar from Fnamed.v
Lemma ann_sub_subst_ftvar : forall T U,
  ann_sub T U ->
  forall X S S',
    ann_sub S' S ->
    ann_sub ([(X,S) ~> S'] T) ([(X,S) ~> S'] U).

Preliminaries

Properties of substitution

We use unroll_t and unroll_e to show the equivalence, and these functions replace erased parameters with annotated parameters. Note that such substitution does not appear when we deal with either typing or ann_typing.

This section presents properties of such substitution that appears only when we use unroll_t and unroll_e.

We may swap variable and parameter substitution.
Lemma swap_fsubst_tt_lsubst_tt : forall T A X U U',
  [X ~> X ^^ U'] ({A ~> U} T) =
  {A ~> [X ~> X ^^ U'] U} ([X ~> X ^^ U'] T).

Lemma swap_fsubst_te_lsubst_te : forall t X Y A T U,
  [Y :~> Y ^^ U] ({A :~> X ^^ T} t) =
  {A :~> X ^^ T} ([Y :~> Y ^^ U] t).

Lemma swap_fsubst_ee_lsubst_ee : forall t x x' T T' a,
  [x' ::~> x' ** T'] ({a ::~> x ** T} t) =
  {a ::~> x ** T} ([x' ::~> x' ** T'] t).

Lemma swap_fsubst_ee_lsubst_te : forall t x X A T T',
  [x ::~> x ** T'] ({A :~> X ^^ T} t) =
  {A :~> X ^^ T} ([x ::~> x ** T'] t).

Lemma swap_fsubst_te_lsubst_ee : forall t x X T T' a,
  [X :~> X ^^ T'] ({a ::~> x ** T} t) =
  {a ::~> x ** T} ([X :~> X ^^ T'] t).


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

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

Lemma fsubst_ee_lsubst_ee_seq : forall t a x T,
  ~ In x (FV_ee t) ->
  [ x ::~> x ** T ] ({ a ::~> x **} t) = { a ::~> x ** T } t.

Properties of erased_t and erased_e


erased_t and erased_e are stable under substitution.
Lemma erased_t_lsubst_tt_safe : forall T A U,
  erased_t ({A ~> U} T) -> erased_t T.

Lemma erased_t_lsubst_tt_safe_inv : forall T U A,
  erased_t T -> erased_t U -> erased_t ({A ~> U} T).


Lemma erased_e_lsubst_te_safe : forall t A X,
  erased_e ({A :~> X ^^} t) ->
  erased_e t.

Lemma erased_e_lsubst_te_safe_inv : forall t A T,
  erased_e t ->
  erased_t T ->
  erased_e ({A :~> T} t).


Lemma erased_e_lsubst_ee_safe : forall t a u,
  erased_e ({a ::~> u} t) -> erased_e t.

Lemma erased_e_lsubst_ee_safe_inv : forall t a u,
  erased_e t -> erased_e u -> erased_e ({a ::~> u} t).


An erased type (or term) does not include annotated parameters
Lemma erased_t_implies_not_in_ann_FV_tt : forall X T,
  erased_t T -> ~ In X (ann_FV_tt T).

Lemma erased_e_implies_not_in_ann_FV_te : forall X t,
  erased_e t -> ~ In X (ann_FV_te t).

Lemma erased_e_implies_not_in_ann_FV_ee : forall x t,
  erased_e t -> ~ In x (ann_FV_ee t).


Basic properties of lclosed_t, sub, and typing.


lclosed_t deals with erased types only.
Lemma lclosed_t_implies_erased_t : forall Gamma I T,
  lclosed_t Gamma I T -> erased_t T.


sub deals with erased types only.
Lemma sub_implies_erased_t : forall Gamma A B,
  sub Gamma A B -> erased_t A /\ erased_t B.


typing deals with erased types and terms only.
Lemma typing_implies_erased_t : forall T Gamma t,
  typing Gamma t T ->
  erased_t T.

Lemma typing_implies_erased_e : forall Gamma t T,
  typing Gamma t T -> erased_e t.


Basic properties of unroll_t and unroll_e

unroll_t and unroll_e lie at the heart of the equivalence proof. This section presents their basic properties that we will use in the equivalence proof. Most of proofs proceed by induction on the size of typing contexts, which is defined as follows:
Fixpoint size_ctxt (Gamma : ctxt) : nat :=
  match Gamma with
    | nil => 0
    | _ :: Gamma' => 1 + size_ctxt Gamma'
  end.

size_ctxt is distributive over ++
Lemma size_ctxt_app : forall Gamma Delta,
  size_ctxt (Gamma ++ Delta) = (size_ctxt Gamma) + (size_ctxt Delta).

Properties of unroll_t

We first show that if T has a specific form, then unroll_t Gamma T also has a specific form, accordingly.
Lemma unroll_t_top : forall Gamma,
  unroll_t Gamma typ_top = typ_top.

Lemma unroll_t_ltvar : forall Gamma A,
  unroll_t Gamma (typ_ltvar A) = typ_ltvar A.

Lemma unroll_t_ann_ftvar : forall Gamma X T,
  unroll_t Gamma (X ^^ T) = X ^^ T.

Lemma unroll_t_ftvar : forall Gamma Gamma_1 Gamma_2 X T,
  ctxt_okay Gamma ->
  Gamma = Gamma_1 ++ (X ~<: T :: Gamma_2) ->
  unroll_t Gamma (X ^^) = X ^^ (unroll_t Gamma_2 T).

Lemma unroll_t_ftvar_inv : forall Gamma X,
  ctxt_okay Gamma ->
  (unroll_t Gamma (X ^^) = X ^^) \/
  exists T', (unroll_t Gamma (X ^^) = X ^^ T').

Lemma unroll_t_fun : forall Gamma T U,
  unroll_t Gamma (T --> U) = (unroll_t Gamma T) --> (unroll_t Gamma U).

Lemma unroll_t_all : forall Gamma A T U,
  unroll_t Gamma (typ_all A T U) =
  typ_all A (unroll_t Gamma T) (unroll_t Gamma U).

We then show that the converse is also true: if unroll_t Gamma T has a specific form, then T also has a specific form, accordingly.
Lemma inv_unroll_t_top : forall T Gamma,
  ctxt_okay Gamma ->
  erased_t T ->
  typ_top = unroll_t Gamma T ->
  typ_top = T.

Lemma inv_unroll_t_ltvar : forall T Gamma A,
  ctxt_okay Gamma ->
  erased_t T ->
  typ_ltvar A = unroll_t Gamma T ->
  typ_ltvar A = T.

Lemma inv_unroll_t_ftvar : forall T Gamma X ann_U,
  ctxt_okay Gamma ->
  erased_t T ->
  X ^^ ann_U = unroll_t Gamma T ->
  exists Gamma_1 Gamma_2 U,
    (T = X ^^) /\
    (Gamma = Gamma_1 ++ X ~<: U :: Gamma_2) /\
    (ann_U = unroll_t Gamma_2 U).

Lemma inv_unroll_t_ftvar_nochange : forall X T Gamma,
  ctxt_okay Gamma ->
  erased_t T ->
  X ^^ = unroll_t Gamma T ->
  X ^^ = T.

Lemma inv_unroll_t_fun : forall T Gamma ann_U ann_S,
  ctxt_okay Gamma ->
  erased_t T ->
  (ann_U --> ann_S) = unroll_t Gamma T ->
  exists U S,
    (T = U --> S) /\
    (ann_U = (unroll_t Gamma U)) /\
    (ann_S = (unroll_t Gamma S)).

Lemma inv_unroll_t_all : forall T Gamma A ann_U ann_S,
  ctxt_okay Gamma ->
  erased_t T ->
  (typ_all A ann_U ann_S) = unroll_t Gamma T ->
  exists U S,
    (T = typ_all A U S) /\
    (ann_U = (unroll_t Gamma U)) /\
    (ann_S = (unroll_t Gamma S)).

We may swap unroll_t and type variable substitution.
Lemma unroll_t_lsubst_tt : forall Gamma A U T,
  unroll_t Gamma ({A ~> U} T) = {A ~> unroll_t Gamma U} (unroll_t Gamma T).

If T is erased and Gamma2 contains all the parameters of T, then unroll_t (Gamma_1 ++ Gamma_2) T results in the same result as unroll_t Gamma2 T as long as ctxt_okay (Gamma1 ++ Gamma2) holds.
Lemma unroll_t_weakening : forall Gamma1 Gamma2 T,
  ctxt_okay (Gamma1 ++ Gamma2) ->
  lclosed_t Gamma2 emptyset T ->
  unroll_t Gamma2 T = unroll_t (Gamma1 ++ Gamma2) T.

unroll_t is invertible.
Lemma unroll_t_inv : forall T U Gamma,
  erased_t T ->
  erased_t U ->
  ctxt_okay Gamma ->
  unroll_t Gamma T = unroll_t Gamma U ->
  T = U.

Properties of unroll_e

Similarly, this section shows properties of unroll_e.

First of all, as unroll_t, we first show that if t has a specific form, then unroll_e Gamma t also has a specific form, accordingly.
Lemma unroll_e_lvar : forall Gamma a,
  unroll_e Gamma (tm_lvar a) = tm_lvar a.

Lemma unroll_e_ann_fvar : forall Gamma x T,
  unroll_e Gamma (x ** T) = x ** T.

Lemma unroll_e_fvar : forall Gamma Gamma_1 Gamma_2 x T,
  ctxt_okay Gamma ->
  Gamma = Gamma_1 ++ (x ~: T :: Gamma_2) ->
  unroll_e Gamma (x **) = x ** (unroll_t Gamma_2 T).

Lemma unroll_e_fvar_inv : forall Gamma x,
  ctxt_okay Gamma ->
  (unroll_e Gamma ( x ** ) = x ** ) \/
  exists T, (unroll_e Gamma (x ** ) = x ** T).

Lemma unroll_e_abs : forall Gamma a T t,
  unroll_e Gamma (tm_abs a T t) =
  tm_abs a (unroll_t Gamma T) (unroll_e Gamma t).

Lemma unroll_e_app : forall Gamma t t',
  unroll_e Gamma (tm_app t t') = tm_app (unroll_e Gamma t) (unroll_e Gamma t').

Lemma unroll_e_tabs : forall Gamma A T t,
  unroll_e Gamma (tm_tabs A T t) =
  tm_tabs A (unroll_t Gamma T) (unroll_e Gamma t).

Lemma unroll_e_tapp : forall Gamma t T,
  unroll_e Gamma (tm_tapp t T) = tm_tapp (unroll_e Gamma t) (unroll_t Gamma T).

We then show that its converse is also true: if unroll_e Gamma t has a specific form, then t also has a specific form, accordingly.
Lemma inv_unroll_e_fvar : forall t Gamma x ann_T,
  ctxt_okay Gamma ->
  erased_e t ->
  x ** ann_T = unroll_e Gamma t ->
  exists Gamma_1 Gamma_2 T,
    (t = x **) /\
    (Gamma = Gamma_1 ++ x ~: T :: Gamma_2) /\
    (ann_T = unroll_t Gamma_2 T).

Lemma inv_unroll_e_abs : forall Gamma t a ann_T ann_t',
  ctxt_okay Gamma ->
  erased_e t ->
  tm_abs a ann_T ann_t' = unroll_e Gamma t ->
  exists T t',
    (t = tm_abs a T t') /\
    (ann_T = (unroll_t Gamma T)) /\
    (ann_t' = (unroll_e Gamma t')).

Lemma inv_unroll_e_app : forall Gamma t ann_t1 ann_t2,
  ctxt_okay Gamma ->
  erased_e t ->
  tm_app ann_t1 ann_t2 = unroll_e Gamma t ->
  exists t1 t2,
    (t = tm_app t1 t2) /\
    (ann_t1 = unroll_e Gamma t1) /\
    (ann_t2 = unroll_e Gamma t2).

Lemma inv_unroll_e_tabs : forall Gamma t A ann_T ann_t',
  ctxt_okay Gamma ->
  erased_e t ->
  tm_tabs A ann_T ann_t' = unroll_e Gamma t ->
  exists T t',
    (t = tm_tabs A T t') /\
    (ann_T = (unroll_t Gamma T)) /\
    (ann_t' = (unroll_e Gamma t')).

Lemma inv_unroll_e_tapp : forall Gamma t ann_t' ann_T,
  ctxt_okay Gamma ->
  erased_e t ->
  tm_tapp ann_t' ann_T = unroll_e Gamma t ->
  exists t' T,
    (t = tm_tapp t' T) /\
    (ann_t' = unroll_e Gamma t') /\
    (ann_T = unroll_t Gamma T).

We may swap unroll_e and variable substitution.
Lemma swap_unroll_e_lsubst_te : forall Gamma A X T t,
  unroll_e Gamma ({A :~> X ^^ T} t) = {A :~> X ^^ T} (unroll_e Gamma t).

Lemma swap_unroll_e_lsubst_ee : forall Gamma x X A e,
  unroll_e Gamma ({x ::~> X ** A} e) = {x ::~> X ** A} (unroll_e Gamma e).

Properties of ann_FV_tt, ann_FV_te, and ann_FV_ee

Lemma not_in_ann_FV_tt_nochange_fsubst_tt : forall T X Y U,
  ~ In X (ann_FV_tt T) ->
  ~ In X (ann_FV_tt U) ->
  X <> Y ->
  ~ In X (ann_FV_tt ([Y ~> Y ^^ U] T)).


Lemma not_in_ann_FV_te_nochange_fsubst_te : forall t X Y T,
  ~ In X (ann_FV_te t) ->
  ~ In X (ann_FV_tt T) ->
  X <> Y ->
  ~ In X (ann_FV_te ([Y :~> Y ^^ T] t)).


Lemma not_in_ann_FV_te_nochange_fsubst_ee : forall t T x X,
  ~ In X (ann_FV_te t) ->
  ~ In X (ann_FV_tt T) ->
  ~ In X (ann_FV_te ([ x ::~> x ** T] t)).


Lemma not_in_ann_FV_ee_nochange_fsubst_te : forall t x X T,
  ~ In x (ann_FV_ee t) ->
  ~ In x (ann_FV_ee ([X :~> T] t)).


Lemma not_in_ann_FV_ee_nochange_fsubst_ee : forall t x y u,
  ~ In x (ann_FV_ee t) ->
  ~ In x (ann_FV_ee u) ->
  ~ In x (ann_FV_ee ([ y ::~> u ] t)).


Lemma not_in_FV_tc_not_in_FV_tt_not_in_ann_FV_tt : forall Gamma X T,
  ctxt_okay Gamma ->
  erased_t T ->
  ~ In X (FV_tc Gamma) ->
  ~ In X (FV_tt T) ->
  ~ In X (ann_FV_tt (unroll_t Gamma T)).


Lemma not_in_ann_FV_te_not_in_FV_tc_not_in_ann_FV_te : forall Gamma X t,
  ctxt_okay Gamma ->
  ~ In X (ann_FV_te t) ->
  ~ In X (FV_tc Gamma) ->
  ~ In X (ann_FV_te (unroll_e Gamma t)).


Lemma not_in_ann_FV_ee_not_in_dom_ec_not_in_ann_FV_ee : forall Gamma x t,
  ctxt_okay Gamma ->
  ~ In x (ann_FV_ee t) ->
  ~ In x (dom_ec Gamma) ->
  ~ In x (ann_FV_ee (unroll_e Gamma t)).


The equivalence proof

To prove the equivalence of two systems, we first need to show the equivalence of lclosed_t and ann_lclosed_t.

We prove the equivalence of lclosed_t and ann_lclosed_t by showing that lclosed_t Gamma I T holds if and only if ann_lclosed_t I (unroll_t Gamma T) holds.

This equivalence holds only when a typing context Gamma is well-formed. Suppose that Gamma is X ~<: X. Definitely, lclosed_t Gamma emptyset X holds, but unroll_t Gamma X is X, and thus ann_lclosed_t emptyset X does not hold.

We first prove Lemma lclosed_t_implies_ann_lclosed_t which states the only if part of the equivalence. The proof proceeds by two lemmas whose proof proceeds by induction on the structure of lclosed_t proofs, and on the size of typing contexts, respectively.

We first prove Lemma lclosed_t_implies_ann_lclosed_t_size_aux which states that the only if part holds for a given typing context Gamma when we assume that the only if part holds for all typing contexts whose size is less than that of Gamma. Note that we use lclosed_t_size_IH_on for that purpose.

Using Lemma lclosed_t_implies_ann_lclosed_t_size_aux, we then prove Lemma lclosed_t_implies_ann_lclosed_t_aux. The proof proceeds by induction on the size of typing contexts.
Definition lclosed_t_size_IH_on n := forall Gamma T I,
  ctxt_okay Gamma ->
  size_ctxt Gamma < n ->
  lclosed_t Gamma I T ->
  ann_lclosed_t I (unroll_t Gamma T).

Lemma lclosed_t_implies_ann_lclosed_t_size_aux : forall Gamma T I,
  lclosed_t_size_IH_on (size_ctxt Gamma) ->
  ctxt_okay Gamma ->
  lclosed_t Gamma I T ->
  ann_lclosed_t I (unroll_t Gamma T).

Lemma lclosed_t_implies_ann_lclosed_t_aux : forall m Gamma I T,
  size_ctxt Gamma < m ->
  ctxt_okay Gamma ->
  lclosed_t Gamma I T ->
  ann_lclosed_t I (unroll_t Gamma T).

Lemma lclosed_t_implies_ann_lclosed_t : forall Gamma A T,
  ctxt_okay Gamma ->
  lclosed_t Gamma T A ->
  ann_lclosed_t T (unroll_t Gamma A).

We then prove Lemma ann_lclosed_t_implies_lclosed_t which states the if part of the equivalence. The proof proceeds by induction on the structure of ann_lclosed_t proofs.
Lemma ann_lclosed_t_implies_lclosed_t : forall ann_T I,
  ann_lclosed_t I ann_T ->
  forall Gamma T,
    ctxt_okay Gamma ->
    erased_t T ->
    ann_T = unroll_t Gamma T ->
    lclosed_t Gamma I T.


Equivalence of sub and ann_sub

Now, we present the equivalence of sub and ann_sub. We prove the equivalence by showing that sub Gamma T U holds if and only if ann_sub (unroll_t Gamma T) (unroll_t Gamma U) holds.

We first prove Lemma sub_implies_ann_sub which states the only if part of the equivalence. The proof proceeds by induction on the structure of sub proofs.
Lemma sub_implies_ann_sub : forall Gamma T U,
  sub Gamma T U -> ann_sub (unroll_t Gamma T) (unroll_t Gamma U).

We then prove Lemma ann_sub_implies_sub which states the if part of the equivalence. The proof proceeds by induction on the size of ann_sub proofs. Note the use of the renaming lemma for the ann_sub_all case.
Lemma ann_sub_implies_sub_aux : forall m n ann_T ann_U,
  n < m ->
  ann_subLH n ann_T ann_U ->
  forall Gamma T U,
    ctxt_okay Gamma ->
    erased_t T ->
    erased_t U ->
    ann_T = unroll_t Gamma T ->
    ann_U = unroll_t Gamma U ->
    sub Gamma T U.

Lemma ann_sub_implies_sub : forall Gamma T U,
  ctxt_okay Gamma ->
  erased_t T ->
  erased_t U ->
  ann_sub (unroll_t Gamma T) (unroll_t Gamma U) ->
  sub Gamma T U.


Equivalence of typing and ann_typing

This section presents the equivalence of typing and ann_typing. We prove the equivalence by showing that typing Gamma t T holds if and only if ann_typing (unroll_e Gamma t) (unroll_t Gamma T) holds.

It is straightforward to prove the only if part.

Lemma typing_implies_ann_typing states the only if part of the equivalence. Its proof proceeds by simple induction on the structure of typing proofs.
Lemma typing_implies_ann_typing : forall Gamma t T,
  typing Gamma t T ->
  ann_typing (unroll_e Gamma t) (unroll_t Gamma T).

Unlike the only if part, the proof of the if part is challenging. The main technical challenge is to deal with the typing_app, typing_tapp, and typing_sub cases that may introduce incompatible annotated types in their premise. We say that an annotated type T is incompatible under a typing context Gamma when for any erased types T', T = unroll_t Gamma T' does not hold. We similarly define the incompatible annotated term. To complete the proof, we need to deal with these incompatible types and terms.

To deal with incompatible types and terms, we first prove Lemma ann_typingLH_implies_ann_pure_typingLH. It states that if any compatible term has a type T, then there exists a compatible type which is a super type of T.
Lemma typ_decompose : forall T A X,
  ~ In A (LV_all_tt T) ->
  exists T', T = {A ~> X ^^} T' /\ ~ In X (FV_tt T').

Lemma sub_unroll_t_fun : forall ann_T ann_T',
  ann_sub ann_T ann_T' ->
  forall Gamma ann_U ann_U' T,
  ctxt_okay Gamma ->
  erased_t T ->
  ann_T = unroll_t Gamma T ->
  ann_T' = ann_U --> ann_U' ->
  exists U U',
    erased_t U /\
    erased_t U' /\
    ann_sub ann_T ((unroll_t Gamma U) --> (unroll_t Gamma U')) /\
    ann_sub ((unroll_t Gamma U) --> (unroll_t Gamma U')) ann_T'.

Lemma sub_unroll_t_all : forall ann_T ann_T',
  ann_sub ann_T ann_T' ->
  forall Gamma ann_U ann_U' A T,
  ctxt_okay Gamma ->
  erased_t T ->
  ann_T = unroll_t Gamma T ->
  ann_T' = typ_all A ann_U ann_U' ->
  exists B U U',
    erased_t U /\ erased_t U' /\
    ann_sub ann_T (typ_all B (unroll_t Gamma U) (unroll_t Gamma U')) /\
    ann_sub (typ_all B (unroll_t Gamma U) (unroll_t Gamma U')) ann_T'.

Definition ann_typingLH_implies_ann_pure_typing_on n :=
  forall m ann_t ann_T,
    m < n ->
    ann_typingLH m ann_t ann_T ->
    forall Gamma t,
      ctxt_okay Gamma ->
      erased_e t ->
      ann_t = unroll_e Gamma t ->
      exists T,
        erased_t T /\
        ann_pure_typingLH m (unroll_e Gamma t) (unroll_t Gamma T) /\
        ann_sub (unroll_t Gamma T) ann_T.

Lemma ann_pure_typingLH_implies_ann_pure_typingLH : forall m ann_t ann_T,
  ann_typingLH_implies_ann_pure_typing_on m ->
  ann_pure_typingLH m ann_t ann_T ->
  forall Gamma t,
    ctxt_okay Gamma ->
    erased_e t ->
    ann_t = unroll_e Gamma t ->
    exists T,
      erased_t T /\
      ann_pure_typingLH m (unroll_e Gamma t) (unroll_t Gamma T) /\
      ann_sub (unroll_t Gamma T) ann_T.


Lemma ann_typingLH_implies_ann_pure_typingLH_aux : forall m ann_t ann_T,
  ann_typingLH_implies_ann_pure_typing_on m ->
  ann_typingLH m ann_t ann_T ->
  forall Gamma t,
    ctxt_okay Gamma ->
    erased_e t ->
    ann_t = unroll_e Gamma t ->
    exists T,
      erased_t T /\
      ann_pure_typingLH m (unroll_e Gamma t) (unroll_t Gamma T) /\
      ann_sub (unroll_t Gamma T) ann_T.

Lemma ann_typingLH_implies_ann_pure_typingLH_ind : forall n m ann_t ann_T,
  m < n ->
  ann_typingLH m ann_t ann_T ->
  forall Gamma t,
    ctxt_okay Gamma ->
    erased_e t ->
    ann_t = unroll_e Gamma t ->
    exists T,
      erased_t T /\
      ann_pure_typingLH m (unroll_e Gamma t) (unroll_t Gamma T) /\
      ann_sub (unroll_t Gamma T) ann_T.


Lemma ann_typingLH_implies_ann_pure_typingLH : forall m ann_t ann_T,
  ann_typingLH m ann_t ann_T ->
  forall Gamma t,
    ctxt_okay Gamma ->
    erased_e t->
    ann_t = unroll_e Gamma t ->
    exists T,
      erased_t T /\
      ann_pure_typingLH m (unroll_e Gamma t) (unroll_t Gamma T) /\
      ann_sub (unroll_t Gamma T) ann_T.

We then prove Lemma ann_typing_implies_typing which states the if part of the equivalence statement.

Lemma ann_typingLH_implies_ann_pure_typingLH allows us to deal with incompatible types since we can use their compatible super type.
Definition ann_typingLH_implies_typing_on n :=
  forall m ann_t ann_T,
    m < n ->
    ann_typingLH m ann_t ann_T ->
    forall Gamma t T,
      ctxt_okay Gamma ->
      erased_e t ->
      erased_t T ->
      ann_t = unroll_e Gamma t ->
      ann_T = unroll_t Gamma T ->
      typing Gamma t T.

Lemma ann_pure_typingLH_implies_typing : forall n ann_t ann_T,
  ann_typingLH_implies_typing_on n ->
  ann_pure_typingLH n ann_t ann_T ->
  forall Gamma t T,
    ctxt_okay Gamma ->
    erased_e t ->
    erased_t T ->
    ann_t = unroll_e Gamma t ->
    ann_T = unroll_t Gamma T ->
    typing Gamma t T.

Lemma ann_typingLH_implies_typing : forall n m ann_t ann_T,
  m < n ->
  ann_typingLH m ann_t ann_T ->
  forall Gamma t T,
    ctxt_okay Gamma ->
    erased_e t ->
    erased_t T ->
    ann_t = unroll_e Gamma t ->
    ann_T = unroll_t Gamma T ->
    typing Gamma t T.

Lemma ann_typing_implies_typing : forall Gamma t T,
  ctxt_okay Gamma ->
  erased_e t ->
  erased_t T ->
  ann_typing (unroll_e Gamma t) (unroll_t Gamma T) ->
  typing Gamma t T.

This page has been generated by coqdoc