Library HOAS_Object_Adequacy

Adequacy of the collapsed presentation with only a single binding form with respect to our original locally nameless presentation.

Author: Brian Aydemir (baydemir at cis.upenn.edu)

Require Export Omega.
Require Export Fsub_LetSum_Soundness.
Require Export HOAS_Object_Soundness.
Because both developments use the same names, we use the module system to provide convenient shorthand prefixes that enable us to distinguish symbols. The downside to doing this is that it seems to interfere with Coq's tactic automation, in ways I do not entirely understand.

Module A := Fsub_LetSum_Definitions.
Module A' := Fsub_LetSum_Infrastructure.
Module A'' := Fsub_LetSum_Soundness.
Module B := HOAS_Object_Definitions.
Module B' := HOAS_Object_Infrastructure.
Module B'' := HOAS_Object_Soundness.

Tactics
We redefine some tactics so that they are effective in our current setting.

Ltac gather_atoms :=
  let A := gather_atoms_with (fun x : atoms => x) in
  let B := gather_atoms_with (fun x : atom => singleton x) in
  let C := gather_atoms_with (fun x : A.exp => A.fv_te x) in
  let D := gather_atoms_with (fun x : A.exp => A.fv_ee x) in
  let E := gather_atoms_with (fun x : A.typ => A.fv_tt x) in
  let F := gather_atoms_with (fun x : A.senv => dom x) in
  let G := gather_atoms_with (fun x : A.env => dom x) in
  let H := gather_atoms_with (fun x : B.senv => dom x) in
  let J := gather_atoms_with (fun x : B.env => dom x) in
  let K := gather_atoms_with (fun x : B.syntax => B.fv x) in
  constr:(A `union` B `union` C `union` D `union`
          E `union` F `union` G `union` H `union` J `union` K).

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

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.

Other infrastructure
Opening a term with a variable is an injective operation if the variable is sufficiently fresh.

Lemma open_tt_injective_rec : forall T S k (X : atom),
  X `notin` (A.fv_tt T `union` A.fv_tt S) ->
  A.open_tt_rec k X T = A.open_tt_rec k X S ->
  T = S.

Lemma open_tt_injective : forall T S (X : atom),
  X `notin` (A.fv_tt T `union` A.fv_tt S) ->
  A.open_tt T X = A.open_tt S X ->
  T = S.

Lemma open_te_injective_rec : forall e f k (X : atom),
  X `notin` (A.fv_te e `union` A.fv_te f) ->
  A.open_te_rec k X e = A.open_te_rec k X f ->
  e = f.

Lemma open_te_injective : forall e f (X : atom),
  X `notin` (A.fv_te e `union` A.fv_te f) ->
  A.open_te e X = A.open_te f X ->
  e = f.

Lemma open_ee_injective_rec : forall e f k (X : atom),
  X `notin` (A.fv_ee e `union` A.fv_ee f) ->
  A.open_ee_rec k X e = A.open_ee_rec k X f ->
  e = f.

Lemma open_ee_injective : forall e f (X : atom),
  X `notin` (A.fv_ee e `union` A.fv_ee f) ->
  A.open_ee e X = A.open_ee f X ->
  e = f.

Lemma open_injective_rec : forall T S k (X : atom),
  X `notin` (B.fv T `union` B.fv S) ->
  B.open_rec k X T = B.open_rec k X S ->
  T = S.

Lemma open_injective : forall T S (X : atom),
  X `notin` (B.fv T `union` B.fv S) ->
  B.open T X = B.open S X ->
  T = S.

Level

Definitions
A term is at level n if the greatest index in the term is strictly less than n.

Inductive level_t : nat -> A.typ -> Prop :=
  | level_t_top : forall n,
      level_t n A.typ_top
  | level_t_bvar : forall n i,
      i < n ->
      level_t n (A.typ_bvar i)
  | level_t_fvar : forall n X,
      level_t n (A.typ_fvar X)
  | level_t_arrow : forall n T1 T2,
      level_t n T1 ->
      level_t n T2 ->
      level_t n (A.typ_arrow T1 T2)
  | level_t_all : forall n T1 T2,
      level_t n T1 ->
      level_t (S n) T2 ->
      level_t n (A.typ_all T1 T2)
  | level_t_sum : forall n T1 T2,
      level_t n T1 ->
      level_t n T2 ->
      level_t n (A.typ_sum T1 T2).

Hint Constructors level_t.

Inductive level_e : nat -> A.exp -> Prop :=
  | level_e_bvar : forall n i,
      i < n ->
      level_e n (A.exp_bvar i)
  | level_e_fvar : forall n X,
      level_e n (A.exp_fvar X)
  | level_e_abs : forall n T e,
      level_t n T ->
      level_e (S n) e ->
      level_e n (A.exp_abs T e)
  | level_e_app : forall n e1 e2,
      level_e n e1 ->
      level_e n e2 ->
      level_e n (A.exp_app e1 e2)
  | level_e_tabs : forall n T e,
      level_t n T ->
      level_e (S n) e ->
      level_e n (A.exp_tabs T e)
  | level_e_tapp : forall n e1 T2,
      level_e n e1 ->
      level_t n T2 ->
      level_e n (A.exp_tapp e1 T2)
  | level_e_let : forall n e1 e2,
      level_e n e1 ->
      level_e (S n) e2 ->
      level_e n (A.exp_let e1 e2)
  | level_e_inl : forall n e1,
      level_e n e1 ->
      level_e n (A.exp_inl e1)
  | level_e_inr : forall n e1,
      level_e n e1 ->
      level_e n (A.exp_inr e1)
  | level_e_case : forall n e1 e2 e3,
      level_e n e1 ->
      level_e (S n) e2 ->
      level_e (S n) e3 ->
      level_e n (A.exp_case e1 e2 e3).

Hint Constructors level_e.

Inductive level : nat -> B.syntax -> Prop :=
  | level_bvar : forall n i,
      i < n ->
      level n (B.bvar i)
  | level_fvar : forall n X,
      level n (B.fvar X)
  | level_habs : forall n e,
      level (S n) e ->
      level n (B.abs e)
  | level_top : forall n,
      level n B.typ_top
  | level_arrow : forall n T1 T2,
      level n T1 ->
      level n T2 ->
      level n (B.typ_arrow T1 T2)
  | level_all : forall n T1 T2,
      level n T1 ->
      level n T2 ->
      level n (B.typ_all T1 T2)
  | level_sum : forall n T1 T2,
      level n T1 ->
      level n T2 ->
      level n (B.typ_sum T1 T2)
  | level_abs : forall n T e,
      level n T ->
      level n e ->
      level n (B.exp_abs T e)
  | level_app : forall n e1 e2,
      level n e1 ->
      level n e2 ->
      level n (B.exp_app e1 e2)
  | level_tabs : forall n T e,
      level n T ->
      level n e ->
      level n (B.exp_tabs T e)
  | level_tapp : forall n e1 T2,
      level n e1 ->
      level n T2 ->
      level n (B.exp_tapp e1 T2)
  | level_let : forall n e1 e2,
      level n e1 ->
      level n e2 ->
      level n (B.exp_let e1 e2)
  | level_inl : forall n e1,
      level n e1 ->
      level n (B.exp_inl e1)
  | level_inr : forall n e1,
      level n e1 ->
      level n (B.exp_inr e1)
  | level_case : forall n e1 e2 e3,
      level n e1 ->
      level n e2 ->
      level n e3 ->
      level n (B.exp_case e1 e2 e3).

Hint Constructors level.

Properties
A term at level n is also a term at level (S n).

Lemma level_t_promote : forall n T,
  level_t n T ->
  level_t (S n) T.

Hint Resolve level_t_promote.

Lemma level_e_promote : forall n e,
  level_e n e ->
  level_e (S n) e.

Hint Resolve level_e_promote.
The following lemmas establish the relationship between the level of a term and opening.

Lemma level_t_open_tt : forall T2 n (X : atom),
  level_t n (A.open_tt_rec n X T2) ->
  level_t (S n) T2.

Lemma level_e_open_te : forall e n (x : atom),
  level_e n (A.open_te_rec n x e) ->
  level_e (S n) e.

Lemma level_e_open_ee : forall e n (x : atom),
  level_e n (A.open_ee_rec n x e) ->
  level_e (S n) e.

Lemma level_open : forall T n (X : atom),
  level n (B.open_rec n X T) ->
  level (S n) T.
Locally closed terms are at level 0.

Lemma level_t_of_type : forall T,
  A.type T -> level_t 0 T.

Hint Resolve level_t_of_type.

Lemma level_e_of_expr : forall e,
  A.expr e -> level_e 0 e.

Hint Resolve level_e_of_expr.

Lemma level_of_lc : forall T,
  B.lc T -> level 0 T.

Hint Resolve level_of_lc.

Closing

Definitions
Closing replaces a free variable with an index. The definition below assumes that K is greater than the greatest index appearing in T.

Fixpoint close_tt_rec (K : nat) (X : atom) (T : A.typ) {struct T} : A.typ :=
  match T with
    | A.typ_top => A.typ_top
    | A.typ_bvar n => A.typ_bvar n
    | A.typ_fvar Y => if X == Y then (A.typ_bvar K) else (A.typ_fvar Y)
    | A.typ_arrow T1 T2 =>
        A.typ_arrow (close_tt_rec K X T1) (close_tt_rec K X T2)
    | A.typ_all T1 T2 =>
        A.typ_all (close_tt_rec K X T1) (close_tt_rec (S K) X T2)
    | A.typ_sum T1 T2 =>
        A.typ_sum (close_tt_rec K X T1) (close_tt_rec K X T2)
  end.

Definition close_tt T X := close_tt_rec 0 X T.

Fixpoint close_te_rec (k : nat) (X : atom) (e : A.exp) {struct e} : A.exp :=
  match e with
    | A.exp_bvar n => A.exp_bvar n
    | A.exp_fvar x => A.exp_fvar x
    | A.exp_abs T e =>
        A.exp_abs (close_tt_rec k X T) (close_te_rec (S k) X e)
    | A.exp_app e1 e2 =>
        A.exp_app (close_te_rec k X e1) (close_te_rec k X e2)
    | A.exp_tabs T e =>
        A.exp_tabs (close_tt_rec k X T) (close_te_rec (S k) X e)
    | A.exp_tapp e1 T2 =>
        A.exp_tapp (close_te_rec k X e1) (close_tt_rec k X T2)
    | A.exp_let e1 e2 =>
        A.exp_let (close_te_rec k X e1) (close_te_rec (S k) X e2)
    | A.exp_inl e1 => A.exp_inl (close_te_rec k X e1)
    | A.exp_inr e1 => A.exp_inr (close_te_rec k X e1)
    | A.exp_case e1 e2 e3 =>
        A.exp_case (close_te_rec k X e1)
                   (close_te_rec (S k) X e2)
                   (close_te_rec (S k) X e3)
  end.

Definition close_te e X := close_te_rec 0 X e.

Fixpoint close_ee_rec (k : nat) (y : atom) (e : A.exp) {struct e} : A.exp :=
  match e with
    | A.exp_bvar n => A.exp_bvar n
    | A.exp_fvar x => if y == x then (A.exp_bvar k) else (A.exp_fvar x)
    | A.exp_abs T e =>
        A.exp_abs T (close_ee_rec (S k) y e)
    | A.exp_app e1 e2 =>
        A.exp_app (close_ee_rec k y e1) (close_ee_rec k y e2)
    | A.exp_tabs T e =>
        A.exp_tabs T (close_ee_rec (S k) y e)
    | A.exp_tapp e1 T2 =>
        A.exp_tapp (close_ee_rec k y e1) T2
    | A.exp_let e1 e2 =>
        A.exp_let (close_ee_rec k y e1) (close_ee_rec (S k) y e2)
    | A.exp_inl e1 => A.exp_inl (close_ee_rec k y e1)
    | A.exp_inr e1 => A.exp_inr (close_ee_rec k y e1)
    | A.exp_case e1 e2 e3 =>
        A.exp_case (close_ee_rec k y e1)
                   (close_ee_rec (S k) y e2)
                   (close_ee_rec (S k) y e3)
  end.

Definition close_ee e y := close_ee_rec 0 y e.

Fixpoint close_rec (K : nat) (X : atom) (t : B.syntax) {struct t} : B.syntax :=
  match t with
    | B.bvar n => B.bvar n
    | B.fvar Y => if X == Y then (B.bvar K) else (B.fvar Y)
    | B.abs e => B.abs (close_rec (S K) X e)
    | B.typ_top => B.typ_top
    | B.typ_arrow T1 T2 => B.typ_arrow (close_rec K X T1) (close_rec K X T2)
    | B.typ_all T1 T2 => B.typ_all (close_rec K X T1) (close_rec K X T2)
    | B.typ_sum T1 T2 => B.typ_sum (close_rec K X T1) (close_rec K X T2)
    | B.exp_abs T e => B.exp_abs (close_rec K X T) (close_rec K X e)
    | B.exp_app e1 e2 => B.exp_app (close_rec K X e1) (close_rec K X e2)
    | B.exp_tabs T e => B.exp_tabs (close_rec K X T) (close_rec K X e)
    | B.exp_tapp e T => B.exp_tapp (close_rec K X e) (close_rec K X T)
    | B.exp_let e1 e2 => B.exp_let (close_rec K X e1) (close_rec K X e2)
    | B.exp_inl e1 => B.exp_inl (close_rec K X e1)
    | B.exp_inr e1 => B.exp_inr (close_rec K X e1)
    | B.exp_case e1 e2 e3 =>
        B.exp_case (close_rec K X e1)
                   (close_rec K X e2)
                   (close_rec K X e3)
  end.

Definition close T X := close_rec 0 X T.

Properties
Opening and closing are inverses of each other under certain conditions.

Lemma open_tt_close_tt_inv_rec : forall (T : A.typ) (K : nat) (X : atom),
  level_t K T ->
  A.open_tt_rec K (A.typ_fvar X) (close_tt_rec K X T) = T.

Lemma open_tt_close_tt_inv : forall (T : A.typ) (X : atom),
  A.type T ->
  A.open_tt (close_tt T X) X = T.

Lemma open_te_close_te_inv_rec : forall (e : A.exp) (K : nat) (X : atom),
  level_e K e ->
  A.open_te_rec K (A.typ_fvar X) (close_te_rec K X e) = e.

Lemma open_te_close_te_inv : forall (e : A.exp) (X : atom),
  A.expr e ->
  A.open_te (close_te e X) X = e.

Lemma open_ee_close_ee_inv_rec : forall (e : A.exp) (k : nat) (x : atom),
  level_e k e ->
  A.open_ee_rec k (A.exp_fvar x) (close_ee_rec k x e) = e.

Lemma open_ee_close_ee_inv : forall (e : A.exp) (x : atom),
  A.expr e ->
  A.open_ee (close_ee e x) x = e.

Lemma open_close_inv_rec : forall (T : B.syntax) (K : nat) (X : atom),
  level K T ->
  B.open_rec K (B.fvar X) (close_rec K X T) = T.

Lemma open_close_inv : forall (T : B.syntax) (X : atom),
  B.lc T ->
  B.open (close T X) X = T.
If we close a term with a particular name, that name will be fresh for the result.

Lemma close_tt_fresh_rec : forall (T : A.typ) (K : nat) (X : atom),
  X `notin` A.fv_tt (close_tt_rec K X T).

Hint Resolve close_tt_fresh_rec.

Lemma close_tt_fresh : forall (T : A.typ) (X : atom),
  X `notin` A.fv_tt (close_tt T X).

Hint Resolve close_tt_fresh.

Lemma close_te_fresh_te_rec : forall e1 (X : atom) (k : nat),
  X `notin` A.fv_te (close_te_rec k X e1).

Lemma close_te_fresh_te : forall e1 (X : atom),
  X `notin` A.fv_te (close_te e1 X).

Hint Resolve close_te_fresh_te.

Lemma close_ee_fresh_ee_rec : forall e1 (x : atom) (k : nat),
  x `notin` A.fv_ee (close_ee_rec k x e1).

Lemma close_ee_fresh_ee : forall e1 (x : atom),
  x `notin` A.fv_ee (close_ee e1 x).

Hint Resolve close_ee_fresh_ee.

Lemma close_fresh_rec : forall (T : B.syntax) (K : nat) (X : atom),
  X `notin` B.fv (close_rec K X T).

Hint Resolve close_fresh_rec.

Lemma close_fresh : forall (T : B.syntax) (X : atom),
  X `notin` B.fv (close T X).

Hint Resolve close_fresh.

Bijection on senvs
In general, two developments may use different environments (given by the type senv in each development, according to our naming convention) for checking the well-formedness of Fsub types and expressions. In order to define the bijection between Fsub terms, we need a bijection on senvs.

Definition
The definition here is trivial because A.senv and B.senv are the same type. The definition specifically does not check that the environments are ok; that must be done elsewhere.

Inductive senv_bijection : A.senv -> B.senv -> Prop :=
  | senv_bijection_refl : forall E,
      senv_bijection E E.

Hint Constructors senv_bijection.

Properties
We define a tactic for simplifying senv_bijection propositions in the hypothesis list.

Ltac simplify_senv_bijection :=
  match goal with
    | H : senv_bijection ?E ?F |- _ =>
      inversion H; try subst F; try subst; clear H; simplify_senv_bijection
    | _ =>
      idtac
  end.
The bijection respects environment concatentation.

Lemma senv_bijection_app : forall E E' F F',
  senv_bijection E E' ->
  senv_bijection F F' ->
  senv_bijection (E ++ F) (E' ++ F').

Hint Resolve senv_bijection_app.

Lemma senv_bijection_length : forall E E',
  senv_bijection E E' ->
  length E = length E'.

Lemma senv_bijection_head : forall E E' F F',
  senv_bijection (F ++ E) (F' ++ E') ->
  senv_bijection E E' ->
  senv_bijection F F'.

Bijection on types
We first define a relation on well-formed Fsub types and then show that the relation defines a bijection on such terms.

Definition


Inductive typ_bijection : A.senv -> A.typ ->
                          B.senv -> B.syntax -> Prop :=
  | typ_bijection_var : forall E E' X,
      ok E ->
      ok E' ->
      binds X Typ E ->
      binds X Typ E' ->
      senv_bijection E E' ->
      typ_bijection E (A.typ_fvar X) E' (B.fvar X)
  | typ_bijection_top : forall E E',
      ok E ->
      ok E' ->
      senv_bijection E E' ->
      typ_bijection E (A.typ_top) E' (B.typ_top)
  | typ_bijection_arrow : forall E E' T1 T1' T2 T2',
      typ_bijection E T1 E' T1' ->
      typ_bijection E T2 E' T2' ->
      typ_bijection E (A.typ_arrow T1 T2) E' (B.typ_arrow T1' T2')
  | typ_bijection_all : forall L E E' T1 T1' T2 T2',
      typ_bijection E T1 E' T1' ->
      (forall X : atom, X `notin` L ->
        typ_bijection ([(X,Typ)] ++ E) (A.open_tt T2 X)
                      ([(X,Typ)] ++ E') (B.open T2' X)) ->
      typ_bijection E (A.typ_all T1 T2) E' (B.typ_all T1' (B.abs T2'))
  | typ_bijection_sum : forall E E' T1 T1' T2 T2',
      typ_bijection E T1 E' T1' ->
      typ_bijection E T2 E' T2' ->
      typ_bijection E (A.typ_sum T1 T2) E' (B.typ_sum T1' T2').

Hint Constructors typ_bijection.

Properties
The relation contains only related environments.

Lemma typ_bijection_senv : forall E E' T1 T2,
  typ_bijection E T1 E' T2 ->
  senv_bijection E E'.

Hint Resolve typ_bijection_senv.
The relation contains only well-formed types.

Lemma typ_bijection_regular_1 : forall E E' T1 T2,
  typ_bijection E T1 E' T2 ->
  A.wf_typ E T1.

Hint Resolve typ_bijection_regular_1.

Lemma typ_bijection_regular_2 : forall E E' T1 T2,
  typ_bijection E T1 E' T2 ->
  B.wf_typ E' T2.

Hint Resolve typ_bijection_regular_2.
The bijection only holds for ok environments.

Lemma typ_bijection_ok_1 : forall E T1 E' T2,
  typ_bijection E T1 E' T2 ->
  ok E.

Hint Resolve typ_bijection_ok_1.

Lemma typ_bijection_ok_2 : forall E E' T1 T2,
  typ_bijection E T1 E' T2 ->
  ok E'.

Hint Resolve typ_bijection_ok_2.
Define a tactic to simplify proving well-formedness goals.

Ltac solve_lc_1 := try first [
    solve [apply lc_var]
  | solve [apply type_var]
  | solve [eapply B''.type_from_wf_typ; eapply typ_bijection_regular_2; eauto]
  | solve [eapply A''.type_from_wf_typ; eapply typ_bijection_regular_1; eauto]
  ].
Weakening holds for the bijection.

Lemma typ_bijection_weakening : forall E E' F F' G G' T1 T2,
  typ_bijection (F ++ E) T1 (F' ++ E') T2 ->
  senv_bijection E E' ->
  senv_bijection F F' ->
  senv_bijection G G' ->
  ok (F ++ G ++ E) ->
  ok (F' ++ G' ++ E') ->
  typ_bijection (F ++ G ++ E) T1 (F' ++ G' ++ E') T2.

Lemma typ_bijection_weakening_head : forall E E' F F' T1 T2,
  typ_bijection E T1 E' T2 ->
  senv_bijection E E' ->
  senv_bijection F F' ->
  ok (F ++ E) ->
  ok (F' ++ E') ->
  typ_bijection (F ++ E) T1 (F' ++ E') T2.

Hint Resolve typ_bijection_weakening_head.
Substitution commutes with the bijection.

Lemma typ_bijection_subst : forall E E' F F' T1 T2 U1 U2 X,
  typ_bijection (F ++ [(X,Typ)] ++ E) T1 (F' ++ [(X,Typ)] ++ E') T2 ->
  typ_bijection E U1 E' U2 ->
  typ_bijection (F ++ E) (A.subst_tt X U1 T1) (F' ++ E') (B.subst X U2 T2).

Lemma typ_bijection_rename : forall E E' T1 T2 (X Y : atom),
  X <> Y ->
  X `notin` (A.fv_tt T1 `union` B.fv T2) ->
  ok ([(Y,Typ)] ++ E) ->
  ok ([(Y,Typ)] ++ E') ->
  senv_bijection E E' ->
  typ_bijection ([(X,Typ)]++E) (A.open_tt T1 X) ([(X,Typ)]++E') (B.open T2 X) ->
  typ_bijection ([(Y,Typ)]++E) (A.open_tt T1 Y) ([(Y,Typ)]++E') (B.open T2 Y).
Now prove that the bijection actually is a bijection.

Lemma typ_bijection_total : forall E T1,
  A.wf_typ E T1 ->
  exists E', exists T2, senv_bijection E E' /\ typ_bijection E T1 E' T2.

Lemma typ_bijection_unique : forall E E' T1 T2 T3,
  typ_bijection E T1 E' T2 ->
  typ_bijection E T1 E' T3 ->
  T2 = T3.

Lemma typ_bijection_injective : forall E E' T1 T2 T3,
  typ_bijection E T1 E' T3 ->
  typ_bijection E T2 E' T3 -> T1 = T2.

Lemma typ_bijection_surjective : forall E' T2,
  B.wf_typ E' T2 ->
  exists E, exists T1, senv_bijection E E' /\ typ_bijection E T1 E' T2.

Bijection on expressions
We first define a relation on well-formed Fsub expressions and then show that the relation defines a bijection on such terms.

Definition


Inductive exp_bijection : A.senv -> A.exp ->
                          B.senv -> B.syntax -> Prop :=
  | exp_bijection_var : forall E E' x,
      ok E ->
      ok E' ->
      senv_bijection E E' ->
      binds x Exp E ->
      binds x Exp E' ->
      exp_bijection E (A.exp_fvar x) E' (B.exp_fvar x)
  | exp_bijection_abs : forall L E E' T T' e e',
      typ_bijection E T E' T' ->
      (forall x : atom, x `notin` L ->
        exp_bijection ([(x,Exp)]++E) (A.open_ee e x) ([(x,Exp)]++E') (B.open e' x)) ->
      exp_bijection E (A.exp_abs T e) E' (B.exp_abs T' (B.abs e'))
  | exp_bijection_app : forall E E' e1 e1' e2 e2',
      exp_bijection E e1 E' e1' ->
      exp_bijection E e2 E' e2' ->
      exp_bijection E (A.exp_app e1 e2) E' (B.exp_app e1' e2')
  | exp_bijection_tabs : forall L E E' T T' e e',
      typ_bijection E T E' T' ->
      (forall X : atom, X `notin` L ->
        exp_bijection ([(X,Typ)]++E) (A.open_te e X) ([(X,Typ)]++E') (B.open e' X)) ->
      exp_bijection E (A.exp_tabs T e) E' (B.exp_tabs T' (B.abs e'))
  | exp_bijection_tapp : forall E E' e e' T T',
      exp_bijection E e E' e' ->
      typ_bijection E T E' T' ->
      exp_bijection E (A.exp_tapp e T) E' (B.exp_tapp e' T')
  | exp_bijection_let : forall L E E' e1 e1' e2 e2',
      exp_bijection E e1 E' e1' ->
      (forall x : atom, x `notin` L ->
        exp_bijection ([(x,Exp)]++E) (A.open_ee e2 x) ([(x,Exp)]++E') (B.open e2' x)) ->
      exp_bijection E (A.exp_let e1 e2) E' (B.exp_let e1' (B.abs e2'))
  | exp_bijection_inl : forall E E' e e',
      exp_bijection E e E' e' ->
      exp_bijection E (A.exp_inl e) E' (B.exp_inl e')
  | exp_bijection_inr : forall E E' e e',
      exp_bijection E e E' e' ->
      exp_bijection E (A.exp_inr e) E' (B.exp_inr e')
  | exp_bijection_case : forall L E E' e1 e1' e2 e2' e3 e3',
      exp_bijection E e1 E' e1' ->
      (forall x : atom, x `notin` L ->
        exp_bijection ([(x,Exp)]++E) (A.open_ee e2 x) ([(x,Exp)]++E') (B.open e2' x)) ->
      (forall x : atom, x `notin` L ->
        exp_bijection ([(x,Exp)]++E) (A.open_ee e3 x) ([(x,Exp)]++E') (B.open e3' x)) ->
      exp_bijection E (A.exp_case e1 e2 e3) E' (B.exp_case e1' (B.abs e2') (B.abs e3')).

Hint Constructors exp_bijection.

Properties
The relation contains only related environments.

Lemma exp_bijection_senv : forall E E' T1 T2,
  exp_bijection E T1 E' T2 ->
  senv_bijection E E'.

Hint Resolve exp_bijection_senv.
The relation contains only well-formed expressions.

Lemma exp_bijection_regular_1 : forall E E' e1 e2,
  exp_bijection E e1 E' e2 ->
  A.wf_exp E e1.

Hint Resolve exp_bijection_regular_1.

Lemma exp_bijection_regular_2 : forall E E' e1 e2,
  exp_bijection E e1 E' e2 ->
  B.wf_exp E' e2.

Hint Resolve exp_bijection_regular_2.
The bijection only holds for ok environments.

Lemma exp_bijection_ok_1 : forall E E' e1 e2,
  exp_bijection E e1 E' e2 ->
  ok E.

Hint Resolve exp_bijection_ok_1.

Lemma exp_bijection_ok_2 : forall E E' e1 e2,
  exp_bijection E e1 E' e2 ->
  ok E'.

Hint Resolve exp_bijection_ok_2.
Define a tactic to simplify proving well-formedness goals.

Ltac solve_lc_2 := try first [
    solve [solve_lc_1]
  | solve [apply expr_var]
  | solve [eapply B''.expr_from_wf_exp; eapply exp_bijection_regular_2; eauto]
  | solve [eapply A''.expr_from_wf_exp; eapply exp_bijection_regular_1; eauto]
  ].
Weakening holds for the bijection.

Lemma exp_bijection_weakening : forall E E' F F' G G' e1 e2,
  exp_bijection (F ++ E) e1 (F' ++ E') e2 ->
  senv_bijection E E' ->
  senv_bijection F F' ->
  senv_bijection G G' ->
  ok (F ++ G ++ E) ->
  ok (F' ++ G' ++ E') ->
  exp_bijection (F ++ G ++ E) e1 (F' ++ G' ++ E') e2.

Lemma exp_bijection_weakening_head : forall E E' F F' e1 e2,
  exp_bijection E e1 E' e2 ->
  senv_bijection E E' ->
  senv_bijection F F' ->
  ok (F ++ E) ->
  ok (F' ++ E') ->
  exp_bijection (F ++ E) e1 (F' ++ E') e2.

Hint Resolve exp_bijection_weakening_head.
Substitution commutes with the bijection.

Lemma typ_bijection_strengthening : forall E E' F F' x T1 T2,
  senv_bijection E E' ->
  senv_bijection F F' ->
  typ_bijection (F ++ [(x,Exp)] ++ E) T1 (F' ++ [(x,Exp)] ++ E') T2 ->
  typ_bijection (F ++ E) T1 (F' ++ E') T2.

Lemma exp_bijection_subst_ee : forall E E' F F' e1 e2 U1 U2 X,
  exp_bijection (F ++ [(X,Exp)] ++ E) e1 (F' ++ [(X,Exp)] ++ E') e2 ->
  exp_bijection E U1 E' U2 ->
  exp_bijection (F ++ E) (A.subst_ee X U1 e1) (F' ++ E') (B.subst X U2 e2).

Lemma exp_bijection_subst_te : forall E E' F F' e1 e2 U1 U2 X,
  exp_bijection (F ++ [(X,Typ)] ++ E) e1 (F' ++ [(X,Typ)] ++ E') e2 ->
  typ_bijection E U1 E' U2 ->
  exp_bijection (F ++ E) (A.subst_te X U1 e1) (F' ++ E') (B.subst X U2 e2).

Lemma exp_bijection_rename_open_ee : forall E E' e1 e2 (x y : atom),
  x <> y ->
  x `notin` (A.fv_ee e1 `union` B.fv e2) ->
  senv_bijection E E' ->
  ok ([(y,Exp)]++E) ->
  ok ([(y,Exp)]++E') ->
  exp_bijection ([(x,Exp)]++E) (A.open_ee e1 x) ([(x,Exp)]++E') (B.open e2 x) ->
  exp_bijection ([(y,Exp)]++E) (A.open_ee e1 y) ([(y,Exp)]++E') (B.open e2 y).

Lemma exp_bijection_rename_open_te : forall E E' e1 e2 (x y : atom),
  x <> y ->
  x `notin` (A.fv_te e1 `union` B.fv e2) ->
  senv_bijection E E' ->
  ok ([(y,Typ)]++E) ->
  ok ([(y,Typ)]++E') ->
  exp_bijection ([(x,Typ)]++E) (A.open_te e1 x) ([(x,Typ)]++E') (B.open e2 x) ->
  exp_bijection ([(y,Typ)]++E) (A.open_te e1 y) ([(y,Typ)]++E') (B.open e2 y).
Now prove that the bijection actually is a bijection.

Lemma exp_bijection_total : forall E e,
  A.wf_exp E e ->
  exists E', exists e', senv_bijection E E' /\ exp_bijection E e E' e'.

Lemma exp_bijection_unique : forall E E' e1 e2 e3,
  exp_bijection E e1 E' e2 ->
  exp_bijection E e1 E' e3 ->
  e2 = e3.

Lemma exp_bijection_injective : forall E E' e1 e2 e3,
  exp_bijection E e1 E' e3 ->
  exp_bijection E e2 E' e3 ->
  e1 = e2.

Lemma exp_bijection_surjective : forall E' e2,
  B.wf_exp E' e2 ->
  exists E, exists e1, senv_bijection E E' /\ exp_bijection E e1 E' e2.

Bijection on environments

Definition


Inductive env_bijection : A.env -> B.env -> Prop :=
  | env_bijection_nil :
      env_bijection nil nil
  | env_bijection_typ : forall E E' x T T',
      x `notin` (dom E `union` dom E') ->
      typ_bijection (A.to_senv E) T (B.to_senv E') T' ->
      env_bijection E E' ->
      env_bijection ([(x, A.bind_typ T)] ++ E) ([(x, B.bind_typ T')] ++ E')
  | env_bijection_sub : forall E E' X T T',
      X `notin` (dom E `union` dom E') ->
      typ_bijection (A.to_senv E) T (B.to_senv E') T' ->
      env_bijection E E' ->
      env_bijection ([(X, A.bind_sub T)] ++ E) ([(X, B.bind_sub T')] ++ E').

Properties


Lemma env_bijection_senv : forall E E',
  env_bijection E E' ->
  senv_bijection (A.to_senv E) (B.to_senv E').

Hint Resolve env_bijection_senv.

Lemma env_bijection_binds_sub_1 : forall E E' X U,
  binds X (A.bind_sub U) E ->
  env_bijection E E' ->
  exists U', typ_bijection (A.to_senv E) U (B.to_senv E') U' /\
             binds X (B.bind_sub U') E'.

Lemma env_bijection_binds_sub_2 : forall E' E X U',
  binds X (B.bind_sub U') E' ->
  env_bijection E E' ->
  exists U, typ_bijection (A.to_senv E) U (B.to_senv E') U' /\
             binds X (A.bind_sub U) E.

Lemma env_bijection_binds_typ_1 : forall E E' X U,
  binds X (A.bind_typ U) E ->
  env_bijection E E' ->
  exists U', typ_bijection (A.to_senv E) U (B.to_senv E') U' /\
             binds X (B.bind_typ U') E'.

Lemma env_bijection_binds_typ_2 : forall E' E X U',
  binds X (B.bind_typ U') E' ->
  env_bijection E E' ->
  exists U, typ_bijection (A.to_senv E) U (B.to_senv E') U' /\
             binds X (A.bind_typ U) E.
The relation holds for only well-formed environments.

Lemma env_bijection_wf_env_1 : forall E E',
  env_bijection E E' ->
  A.wf_env E.

Hint Resolve env_bijection_wf_env_1.

Lemma env_bijection_wf_env_2 : forall E E',
  env_bijection E E' ->
  B.wf_env E'.

Hint Resolve env_bijection_wf_env_2.

Relations derive the same judgements
These first lemmas are trivial, given our definitions.

Lemma wf_typ_bijection : forall E E' T T',
  typ_bijection E T E' T' ->
  (A.wf_typ E T <-> B.wf_typ E' T').

Lemma wf_exp_bijection : forall E E' e e',
  exp_bijection E e E' e' ->
  (A.wf_exp E e <-> B.wf_exp E' e').

Lemma wf_env_bijection : forall E E',
  env_bijection E E' ->
  (A.wf_env E <-> B.wf_env E').
We need a few corollaries of the substitution lemmas for the bijections.

Lemma typ_bijection_subst_head : forall E E' T1 T2 U1 U2 X,
  typ_bijection ([(X,Typ)] ++ E) T1 ([(X,Typ)] ++ E') T2 ->
  typ_bijection E U1 E' U2 ->
  typ_bijection E (A.subst_tt X U1 T1) E' (B.subst X U2 T2).

Lemma typ_bijection_subst_head_open : forall E E' T1 T2 U1 U2 X,
  X `notin` (A.fv_tt T1 `union` B.fv T2) ->
  typ_bijection ([(X,Typ)] ++ E) (A.open_tt T1 X) ([(X,Typ)] ++ E') (B.open T2 X) ->
  typ_bijection E U1 E' U2 ->
  typ_bijection E (A.open_tt T1 U1) E' (B.open T2 U2).

Lemma exp_bijection_subst_ee_head : forall E E' e1 e2 U1 U2 X,
  exp_bijection ([(X,Exp)] ++ E) e1 ([(X,Exp)] ++ E') e2 ->
  exp_bijection E U1 E' U2 ->
  exp_bijection E (A.subst_ee X U1 e1) E' (B.subst X U2 e2).

Lemma exp_bijection_subst_ee_head_open : forall E E' e1 e2 U1 U2 X,
  X `notin` (A.fv_ee e1 `union` B.fv e2) ->
  exp_bijection ([(X,Exp)] ++ E) (A.open_ee e1 X) ([(X,Exp)] ++ E') (B.open e2 X) ->
  exp_bijection E U1 E' U2 ->
  exp_bijection E (A.open_ee e1 U1) E' (B.open e2 U2).

Lemma exp_bijection_subst_te_head : forall E E' e1 e2 U1 U2 X,
  exp_bijection ([(X,Typ)] ++ E) e1 ([(X,Typ)] ++ E') e2 ->
  typ_bijection E U1 E' U2 ->
  exp_bijection E (A.subst_te X U1 e1) E' (B.subst X U2 e2).

Lemma exp_bijection_subst_te_head_open : forall E E' e1 e2 U1 U2 X,
  X `notin` (A.fv_te e1 `union` B.fv e2) ->
  exp_bijection ([(X,Typ)] ++ E) (A.open_te e1 X) ([(X,Typ)] ++ E') (B.open e2 X) ->
  typ_bijection E U1 E' U2 ->
  exp_bijection E (A.open_te e1 U1) E' (B.open e2 U2).
We now prove that the main Fsub relations derive the same sets of judgements.

Lemma sub_bijection_1 : forall E E' T T' S S',
  A.sub E S T ->
  env_bijection E E' ->
  typ_bijection (A.to_senv E) S (B.to_senv E') S' ->
  typ_bijection (A.to_senv E) T (B.to_senv E') T' ->
  B.sub E' S' T'.

Hint Resolve sub_bijection_1.

Lemma sub_bijection_2 : forall E E' T T' S S',
  B.sub E' S' T' ->
  env_bijection E E' ->
  typ_bijection (A.to_senv E) S (B.to_senv E') S' ->
  typ_bijection (A.to_senv E) T (B.to_senv E') T' ->
  A.sub E S T.

Hint Resolve sub_bijection_2.

Lemma typing_bijection_1 : forall E E' e e' T T',
  A.typing E e T ->
  env_bijection E E' ->
  exp_bijection (A.to_senv E) e (B.to_senv E') e' ->
  typ_bijection (A.to_senv E) T (B.to_senv E') T' ->
  B.typing E' e' T'.

Lemma typing_bijection_2 : forall E E' e e' T T',
  B.typing E' e' T' ->
  env_bijection E E' ->
  exp_bijection (A.to_senv E) e (B.to_senv E') e' ->
  typ_bijection (A.to_senv E) T (B.to_senv E') T' ->
  A.typing E e T.

Lemma value_bijection_1 : forall E E' e e',
  A.value e ->
  exp_bijection E e E' e' ->
  B.value e'.

Hint Resolve value_bijection_1.

Lemma value_bijection_2 : forall E E' e e',
  B.value e' ->
  exp_bijection E e E' e' ->
  A.value e.

Hint Resolve value_bijection_2.

Lemma red_bijection_1 : forall E E' e1 e1' e2 e2',
  A.red e1 e2 ->
  exp_bijection E e1 E' e1' ->
  exp_bijection E e2 E' e2' ->
  B.red e1' e2'.

Lemma red_bijection_2 : forall E E' e1 e1' e2 e2',
  B.red e1' e2' ->
  exp_bijection E e1 E' e1' ->
  exp_bijection E e2 E' e2' ->
  A.red e1 e2.