Type soundness of Fμ via logical relations

In this chapter we use the theory of complete, 1-bounded ultrametric spaces that we have developed in the previous chapter, to build a unary model of System F with (iso-)recursive types and use it to prove type soundness of the system. This provides an alternative proof technique to the standard progress + preservation approach developed in Software Foundations.
In this chapter we assume the reader is familiar with the proof of normalization of STLC presented in Software Foundations, and the general idea behind the normalization of System F, and concentrate on how we can use the metric space theory to interpret the recursive types. Note that even though we will be using a technique originally developed to prove normalization, we cannot obtain such a property, since recursive types are strong enough to encode general recursion.

Require Import DBLib.DeBruijn DBLib.Environments.
Require Import ModuRes.Constr ModuRes.UPred ModuRes.PCOFE.
Require Import Omega.

Arguments exist [A P]%type _ _ .

Language

We begin by defining our object language: a simple calculus built over functional, polymorphic and recursive types, with an additional ground type of natural numbers.
The syntax is encoded in a standard way, using de Bruijn indices for both type- and term-level variables. We use a slightly modified version of Francois Pottier's library for handling these binders, which givese us generic definitions of weakening and substitution for a small price: we need to provide functions that traverses the structure of our terms and types and identify the place where a substitution should occur. We also need to show that these functions satisfy certain properties, but the library's tactics are sufficiently strong to handle this.
Since we are going to use the call-by-value evaluation strategy, we also need to define values and provide a way to substitute values into expressions. Ultimately, we will need to substitute multiple values at the same time. This functionality is also provided by the library, but we need to show how this substitution behaves with respect to the constructors of our term language. After these lemmas are proved, we can make sure that the library tactics know how to use them. We achieve it by adding the lemmas to the appropriate rewrite database.

Section Language.

  Inductive typ : Set :=
  | tnat : typ
  | tvar : nat → typ
  | tprod : typ → typ → typ
  | tarr : typ → typ → typ
  | tall : typ → typ
  | trec : typ → typ.

  Global Instance Var_typ : Var typ := { var := tvar }.

  Fixpoint traverse_typ (f : nat → nat → typ) l t :=
    match t with
      | tnat ⇒ tnat
      | tvar x ⇒ f l x
      | tprod t1 t2 ⇒ tprod (traverse_typ f l t1) (traverse_typ f l t2)
      | tarr t1 t2 ⇒ tarr (traverse_typ f l t1) (traverse_typ f l t2)
      | tall t ⇒ tall (traverse_typ f (S l) t)
      | trec t ⇒ trec (traverse_typ f (S l) t)
    end.
  Global Instance Traverse_typ : Traverse typ typ :=
    { traverse := traverse_typ }.

  Global Instance TraverseOK_typ : TraverseOK typ typ.
  Proof.
    prove_traverse.
  Qed.

  Inductive exp : Type :=
  | enat : nat → exp
  | evar : nat → exp
  | epair : exp → exp → exp
  | efst : exp → exp
  | esnd : exp → exp
  | elam : exp → exp
  | eapp : exp → exp → exp
  | etlam : exp → exp
  | etapp : exp → exp
  | efold : exp → exp
  | eunfold : exp → exp.

  Global Instance Var_exp : Var exp := {var := evar}.

  Fixpoint traverse_exp (f : nat → nat → exp) l e :=
    match e with
      | enat n ⇒ enat n
      | evar x ⇒ f l x
      | epair e1 e2 ⇒ epair (traverse_exp f l e1) (traverse_exp f l e2)
      | efst e ⇒ efst (traverse_exp f l e)
      | esnd e ⇒ esnd (traverse_exp f l e)
      | elam e ⇒ elam (traverse_exp f (S l) e)
      | eapp e1 e2 ⇒ eapp (traverse_exp f l e1) (traverse_exp f l e2)
      | etlam e ⇒ etlam (traverse_exp f l e)
      | etapp e ⇒ etapp (traverse_exp f l e)
      | efold e ⇒ efold (traverse_exp f l e)
      | eunfold e ⇒ eunfold (traverse_exp f l e)
    end.
  Global Instance Traverse_exp : Traverse exp exp :=
    { traverse := traverse_exp }.

  Global Instance TraverseOK_exp : TraverseOK exp exp.
  Proof.
    prove_traverse.
  Qed.

  Inductive val : Type :=
  | vnat : nat → val
  | vpair : val → val → val
  | vlam : exp → val
  | vtlam : exp → val
  | vfold : exp → val.

  Fixpoint val_to_exp (v : val) :=
    match v with
      | vnat n ⇒ enat n
      | vpair v1 v2 ⇒ epair (val_to_exp v1) (val_to_exp v2)
      | vlam e ⇒ elam e
      | vtlam e ⇒ etlam e
      | vfold e ⇒ efold e
    end.
  Coercion val_to_exp : val >-> exp.

  Fixpoint traverse_val (f : nat → nat → exp) l v :=
    match v with
      | vnat n ⇒ vnat n
      | vpair v1 v2 ⇒ vpair (traverse_val f l v1) (traverse_val f l v2)
      | vlam e ⇒ vlam (traverse f (S l) e)
      | vtlam e ⇒ vtlam (traverse f l e)
      | vfold e ⇒ vfold (traverse f l e)
    end.
  Global Instance Traverse_val : Traverse exp val :=
    { traverse := traverse_val }.

  Global Instance TraverseOK_val : TraverseOK exp val.
  Proof.
    prove_traverse.
  Qed.

  Lemma lift_val_exp (v : val) k n :
    (lift k n v : exp) = lift k n (v : exp).
  Proof.
    revert k n; induction v; intros; do 2 (simpl val_to_exp; simpl_lift_goal); eauto with f_equal.
  Qed.

End Language.

Notation "t1 × t2" := (tprod t1 t2) (at level 40, left associativity) : lang_scope.
Notation "t1 → t2" := (tarr t1 t2) (at level 30, right associativity) : lang_scope.
Notation "∀ t" := (tall t) (at level 60, t at level 30) : lang_scope.
Notation "'μ' t" := (trec t) (at level 20) : lang_scope.
Notation "$ n" := (enat n) (at level 10) : lang_scope.
Notation "# n" := (evar n) (at level 10) : lang_scope.
Notation "〈 e1 , e2 〉" := (epair e1 e2) : lang_scope.
Notation "'π1' e" := (efst e) (at level 30) : lang_scope.
Notation "'π2' e" := (esnd e) (at level 30) : lang_scope.
Notation "'λ' e" := (elam e) (at level 30) : lang_scope.
Notation "e1 @ e2" := (eapp e1 e2) (at level 40, left associativity) : lang_scope.
Notation "'Λ' e" := (etlam e) (at level 30) : lang_scope.
Notation "e •" := (etapp e) (at level 30) : lang_scope.

Ltac commute_env ρ :=
  match type of ρ with
    | env _ ⇒ induction ρ as [| [v |] ρ IHρ]; intros;
                simpl_lift_goal; simpl_subst_goal; [now auto | | now auto];
                rewrite IHρ; simpl_subst_goal; reflexivity
    | _ ⇒ fail "Can only be used on an environment."
  end.

Section EnvSubstsCommute.
  Open Scope lang_scope.

  Lemma subst_nat (γ : env exp) n k : substEnv γ n ($ k) = $ k.
  Proof. revert n; commute_env γ. Qed.

  Lemma subst_pair (γ : env exp) n (e1 e2 : exp) :
    substEnv γ n 〈e1, e2〉 = 〈substEnv γ n e1, substEnv γ n e2〉.
  Proof. revert n; commute_env γ. Qed.

  Lemma subst_fst n (γ : env exp) (e : exp) :
    substEnv γ n (π1 e) = π1 (substEnv γ n e).
  Proof. revert n; commute_env γ. Qed.

  Lemma subst_snd n (γ : env exp) (e : exp) :
    substEnv γ n (π2 e) = π2 (substEnv γ n e).
  Proof. revert n; commute_env γ. Qed.

  Lemma subst_lam n (γ : env exp) (e : exp) :
    substEnv γ n (λ e) = λ substEnv (shift O γ) (S n) e.
  Proof. revert e n; commute_env γ. Qed.

  Lemma subst_app (γ : env exp) n (e1 e2 : exp) :
    substEnv γ n (e1 @ e2) = substEnv γ n e1 @ substEnv γ n e2.
  Proof. revert n; commute_env γ. Qed.

  Lemma subst_tlam (γ : env exp) n e :
    substEnv γ n (Λ e) = Λ substEnv γ n e.
  Proof. revert n; commute_env γ. Qed.

  Lemma subst_tapp (γ : env exp) n (e : exp) :
    substEnv γ n (e •) = (substEnv γ n e) •.
  Proof. revert n; commute_env γ. Qed.

  Lemma subst_fold (γ : env exp) n e :
    substEnv γ n (efold e) = efold (substEnv γ n e).
  Proof. revert n; commute_env γ. Qed.

  Lemma subst_unfold (γ : env exp) n e :
    substEnv γ n (eunfold e) = eunfold (substEnv γ n e).
  Proof. revert n; commute_env γ. Qed.

End EnvSubstsCommute.

Hint Rewrite subst_nat subst_pair subst_fst subst_snd subst_lam subst_app subst_tlam subst_tapp subst_fold subst_unfold : substexp.

Type system and operational semantics

Note that since our term language does not contain explicit types, the typing rule for type application (Ttapp) can apply any well-formed type (note the substitution in the result type). Similarly, the reduction rule SRtla only needs to run the computation susbended by the Λ.

Open Scope lang_scope.
Reserved Notation "[ k | Γ ⊢ e ':::' t ]" (at level 60, arguments at next level, no associativity).
Inductive types : nat → env typ → exp → typ → Prop :=
| Tnat : ∀ k (Γ : env typ) n
                (HC : closed k Γ),
           [ k | Γ ⊢ $ n ::: tnat ]
| Tvar : ∀ k (Γ : env typ) x t
                (HC : closed k Γ)
                (HFnd : lookup x Γ = Some t),
           [ k | Γ ⊢ # x ::: t ]
| Tpair: ∀ k Γ t1 t2 e1 e2
                (HT1 : [ k | Γ ⊢ e1 ::: t1 ])
                (HT2 : [ k | Γ ⊢ e2 ::: t2 ]),
           [ k | Γ ⊢ 〈e1, e2〉 ::: t1 × t2 ]
| Tfst : ∀ k Γ t1 t2 e
                (HT : [ k | Γ ⊢ e ::: t1 × t2 ]),
           [ k | Γ ⊢ π1 e ::: t1 ]
| Tsnd : ∀ k Γ t1 t2 e
                (HT : [ k | Γ ⊢ e ::: t1 × t2 ]),
           [ k | Γ ⊢ π2 e ::: t2 ]
| Tlam : ∀ k Γ t1 t2 e
                (HT : [ k | insert O t1 Γ ⊢ e ::: t2 ]),
           [ k | Γ ⊢ λ e ::: t1 → t2 ]
| Tapp : ∀ k Γ t1 t2 e1 e2
                (HT1 : [ k | Γ ⊢ e1 ::: t1 → t2 ])
                (HT2 : [ k | Γ ⊢ e2 ::: t1 ]),
           [ k | Γ ⊢ e1 @ e2 ::: t2 ]
| Ttlam : ∀ k Γ t e
                 (HT : [ S k | shift O Γ ⊢ e ::: t ]),
            [k | Γ ⊢ Λ e ::: ∀ t ]
| Ttapp : ∀ k Γ (t1 t2 t : typ) e
                 (HT : [ k | Γ ⊢ e ::: ∀ t1 ])
                 (HC : closed k t2)
                 (HS : subst t2 O t1 = t),
            [ k | Γ ⊢ e• ::: t ]
| Tfold : ∀ k Γ t e
                 (HT : [ S k | shift O Γ ⊢ e ::: t ]),
            [ k | Γ ⊢ efold e ::: μ t ]
| Tunfold : ∀ k Γ e t t'
                   (HT : types k Γ e (trec t))
                   (HS : subst (trec t) O t = t'),
              types k Γ (eunfold e) t'
where "[ k | Γ ⊢ e ':::' t ]" := (types k Γ e t).

Reserved Notation "e ↦ e'" (at level 60, no associativity).
Inductive step : exp → exp → Prop :=
| SRfp (v1 v2 : val) :
    π1 〈v1, v2〉 ↦ v1
| SRsp (v1 v2 : val) :
    π2 〈v1, v2〉 ↦ v2
| SRla e er (v : val)
       (HSub : subst (v : exp) O e = er) :
    (λ e) @ v ↦ er
| SRfu e :
    eunfold (efold e) ↦ e
| SRtla e :
    (Λ e) • ↦ e
| SCpairL e1 e1' e2
          (HStep : e1 ↦ e1') :
    〈e1, e2〉 ↦ 〈e1', e2〉
| SCpairR (v : val) e e'
          (HStep : e ↦ e') :
    〈v, e〉 ↦ 〈v, e'〉
| SCfst e e'
        (HStep : e ↦ e') :
    π1 e ↦ π1 e'
| SCsnd e e'
        (HStep : e ↦ e') :
    π2 e ↦ π2 e'
| SCappL e1 e1' e2
         (HStep : e1 ↦ e1') :
    e1 @ e2 ↦ e1' @ e2
| SCappR (v : val) e e'
         (HStep : e ↦ e') :
    v @ e ↦ v @ e'
| SCtapp e e'
         (HStep : e ↦ e') :
    e • ↦ e' •
| SCunfold e e'
           (HStep : e ↦ e') :
    eunfold e ↦ eunfold e'
where "e ↦ e'" := (step e e').

Existing Class closed.

Closedness

Throughout the development we will need certain properties that restrict free variables that can occur in our types and terms. In this section we prove certain useful properties. The less technical among those are the following (expressed in more familiar syntax, but equivalent to the statements below).
  • types_closed_Γ : Δ | Γ ⊢ e : τ ⇒ FTV(Γ) ⊆ dom(Δ)
  • types_closed_t : Δ | Γ ⊢ e : τ ⇒ FTV(τ) ⊆ dom(Δ)
  • types_closed_e : Δ | Γ ⊢ e : τ ⇒ FV(e) ⊆ dom(Γ)
  • closed_step : e ↦ e' ⇒ FV(e') ⊆ FV(e)
Section Closedness.

  Lemma types_closed : ∀ {k Γ e t} (HT : [k | Γ ⊢ e ::: t] ),
                         closed k Γ ∧ closed k t ∧ closed (length Γ) e.
  Proof with intuition (inversion_closed; construction_closed).
    induction 1; try (intuition (inversion_closed; construction_closed)).
    - repeat split; eauto using closed_lookup with typeclass_instances; [].
      unfold closed; simpl_lift_goal; reflexivity.
    - erewrite <- lift_preserves_closed_iff, length_lift in IHHT by apply _...
    - split; [| split; [subst t; apply subst_preserves_closed; [apply _ | |] |]]...
    - erewrite <- lift_preserves_closed_iff, length_lift in IHHT by apply _...
    - subst t'; split; [| split; [apply subst_preserves_closed; [apply _ | |] |]]...
  Qed.

  Definition types_closed_Γ {k Γ t e} (HT : [k | Γ ⊢ e ::: t]) : closed k Γ :=
    proj1 (types_closed HT).
  Definition types_closed_t {k Γ t e} (HT : [k | Γ ⊢ e ::: t]) : closed k t :=
    proj1 (proj2 (types_closed HT)).
  Definition types_closed_e {k Γ t e} (HT : [k | Γ ⊢ e ::: t]) : closed (length Γ) e :=
    proj2 (proj2 (types_closed HT)).

  Lemma val_to_exp_inj (v1 v2 : val) (EQ : (v1 : exp) = (v2 : exp)) : v1 = v2.
  Proof.
    revert v2 EQ; induction v1; destruct v2; intros; inversion EQ; subst; auto with f_equal.
  Qed.

  Lemma closed_val_exp k (v : val) :
    closed k v ↔ closed k (v : exp).
  Proof.
    unfold closed; rewrite <- lift_val_exp.
    split; [congruence | apply val_to_exp_inj].
  Qed.

  Global Instance closed_lift m k (t : typ)
           {HC : closed (m + k) t} :
    closed (S (m + k)) (shift m t).
  Proof.
    unfold closed; rewrite lift_lift_reversed by omega || eauto with typeclass_instances.
    replace (S (m + k) - 1) with (m + k) by auto with arith; congruence.
  Qed.

End Closedness.

Ltac simpl_vals :=
  repeat match goal with
           | [H : val_to_exp ?v1 = val_to_exp ?v2 |- _] ⇒
             apply val_to_exp_inj in H; try (subst v1 || subst v2)
         end.

Definition irred e := ∀ e', ¬ e ↦ e'.
Lemma val_irred (v : val) : irred v.
Proof.
  induction v; intros ? HS; inversion HS; subst; clear HS; [|].
  - apply IHv1 in HStep; contradiction.
  - apply IHv2 in HStep; contradiction.
Qed.

Instance val_pred : preoType val := @disc_preo val discreteType.
Instance exp_pred : preoType exp := @disc_preo exp discreteType.

Lemma ext_step_step : ext_step step.
Proof.
  intros e1 e2 e2' HSub HS; simpl in *; subst e2; eauto.
Qed.

Instance ord_irred : Proper (pord --> impl) (irr step).
Proof.
  intros e e' HS HI; unfold flip in HS; simpl in HS; subst; assumption.
Qed.

Ltac irred_sub HIrr :=
  match goal with
    | |- irred ?e ⇒
      let e' := fresh e in
      let HS := fresh "HS" in
      intros e' HS; (eapply HIrr || fail 2 "Given hyp does not match");
      now eauto using step || fail 2 "Reduction failed"
    | |- _ ⇒ fail 1 "Goal is of a wrong form"
  end.

Ltac valify e :=
  match e with
    | val_to_exp ?v ⇒ constr:v
    | 〈 ?e1, ?e2 〉 ⇒
      let v1 := valify e1 in
      let v2 := valify e2 in
      constr:(vpair v1 v2)
    | $ ?n ⇒ constr:(vnat n)
    | λ ?e ⇒ constr:(vlam e)
    | Λ ?e ⇒ constr:(vtlam e)
    | efold ?e ⇒ constr:(vfold e)
  end.

Ltac irred :=
  match goal with
    | |- irred ?e ⇒
      let v := valify e in apply (val_irred v)
    | HS: ?e ↦ _ |- _ ⇒
      let v := valify e in contradiction (val_irred v _ HS)
    | HI: irred ?e, HS : ?e ↦ _ |- _ ⇒ contradiction (HI _ HS)
    | HI: irred ?e1 |- irred ?e2 ⇒
      match e1 with
          context [e2] ⇒ irred_sub HI
      end
    | HI: irred _ |- _ ⇒ exfalso; eapply HI; now eauto using step
  end.

Ltac isval :=
  match goal with
    | |- ∃ v, ?e = val_to_exp v ⇒
      let v := valify e in (∃ v; reflexivity)
  end.

Ltac try_rew EQ :=
  rewrite EQ || (intros ?v; simpl morph; try_rew EQ).

Ltac simp_rew :=
  let EQt := fresh "EQt" in
  match goal with
    | |- Proper (equiv ==> equiv) ?R ⇒ intros ?t1 ?t2 EQt
    | |- Proper (dist ?n ==> dist ?m) ?R ⇒ intros ?t1 ?t2 EQt
  end; simpl morph; try_rew EQt; reflexivity.

Constructions

We now reach the interesting part of the proof: the definition of the logical relation. As is usual in this type of argument, we will want to give some sort of interpretation to the syntactic types typ. Now we need to consider what the type of this interpretation function should be.
Section Constructions.

The type of the interpretation function

In the simply-typed lambda calculus this was hardly problematic: it was enough to interpret the types as predicates on closed values. The problem is much more tricky when one considers (impredicative) polymorphism, in the form of System F. The canonical solution is to take a universe of "semantic types", T, (in the case of System F those would usually be predicates on terminating, closed expressions). Then, one can interpret an /open/ type τ that is well-formed in the type-level context Δ as a space T^|Δ| → T.
We would want to pursue the same approach here, but we immediately face a question: how should we interpret recursive types? These are supposed to model fixed points of the appropriate type, so we might want to interpret them as fixed points of some operator on semantic types. However, for this to be possible the space of semantic types we use has to admit fixed points. Fortunately, we have already seen a space like that: in the space cbult of complete, 1-bounded ultrametric spaces we have defined Banach's fixed point operator.
This still does not solve the problem fully: after all, Banach's fixpoint theorem only works for contractive maps. This leads us to an abstract account of the "step-indexing" technique — we will take the semantic types to be /uniform/ predicates on expressions. Intuitively, this means that the expression is equipped with a natural number that describes the number of steps for which the expression is "good". Naturally, if the expression is good for k steps, it should also be good for any m ≤ k. Thus, we have the uniform predicates as UPred T := {R : nat * T -> Prop | R is downwards closed}.
This definition gives us almost everything we need. In practice, to prove type soundness, we want our semantic types to only contain closed values. We choose to enforce it by only taking these uniform predicates on expressions that only contain closed values, since it gives us slightly lighter notation.

  Definition closed_vals (R : UPred exp) :=
    ∀ n e (HR : R n e),
      closed 0 e ∧ ∃ v : val, e = v.

The downside of this is that for our subset type to form a /complete/ metric space, it needs to preserve limits of cauchy chains, which we show here.
  Global Instance LP_closed_vals : LimitPreserving closed_vals.
  Proof.
    intros σ σc HCi n e HR; simpl in HR.
    apply (HCi (S n) n e); eassumption.
  Qed.

  Definition T := cofeFromType {R : UPred exp | closed_vals R}.

*Exercise* (2 stars): How would the definitions in this section need to change if we took the semantic types to be UPred (closed values)?
Since we are going to interpret open types, we need to define the interpretations of typing contexts. On paper, we simply wrote T^|Δ| for the interpretation of Δ — or, given that our context is simply a natural number, Tᵏ. We can also achieve this in the Coq setting, by using the finite types. This is a family of inductive types that only have a finite number of elements: Fin.t n has exactly n elements. If with each element of such a type we associate a semantic type, we obtain an object that corresponds to what we wrote on paper as interpretation of contexts — and happens to be a complete metric space, too.
*Note*: FinI is an example of a /dependent/ type, since the type depends on a term (the natural number that indexes FinI). While one of theoretical strengths of Coq's type system, these are notoriously difficult to work with. Luckily, this type is defined in the library, so most of the tricky definitions and lemmas are provided.
Now that we have both the space of the semantic types and the interpretations of the type-level contexts, we can define the type of interpretations of (syntactic) types. We take it to be, for a context of length k, a nonexpansive map from the interpretation of k into semantic types: int k := Tᵏ →ⁿ T.
  Definition TCRel n := FinI T n.
  Definition int k := TCRel k -n> T.
  Definition intE k := TCRel k -n> cofeFromType (UPred exp).

  Notation " e ∈ R @ n " := (proj1_sig R n e) (at level 60, R at level 39, no associativity).
  Local Obligation Tactic := intros; (simp_rew || eauto with typeclass_instances).

Combinators on int k

Now that we have defined the result type of our interpretation of types, we can start to define that function itself. As usual in Coq, we cannot define it simply as an inductive predicate, due to contravariance in the case of arrow types. The other technical restriction is that the types of inductive types and predicates defined in Coq have to end with a sort (Type or Prop), while we would want the interpretation to have the type interpVal : ∀ τ : typ, closed k τ → int k, and int k is not a sort (due to all the extra information we carry about the maps and predicates involved: the underlying map from the interpretation of contexts to predicates on numbers and values *does* end in Prop).
These problems mean that we will need to define the interpretation as a fixpoint over the type — but to build it easily, we first define combinators on int k that define the interpretation of each constructor of the syntactic types. We start with the simple cases of natural numbers and products, and progressively make our way to the more involved constructions.
The definitions of these combinators follow the same pattern: first we define the underlying relation (we choose the presentation as inductive datatypes for those; this is not necessary, but works rather well in practice), and then show that these have all desired properties, thus ending with combinators on the int k type.

Natural numbers

The interpretation of natural numbers is straightforward: the expression belongs to it only if it's of the form $ n for some n. In this case, the step index does not matter, so we can use up_cr to build a relation that just discards it. Likewise, the interpretation of naturals does not depend on the interpretation of the type-level context, so we just use the constant map that returns our pre-built predicate.
  Inductive natR : exp → Prop :=
  | RNat n : natR ($ n).
  Program Definition rel_nat k : int k := umconst (exist (up_cr natR) _).
  Next Obligation.
    intros n e HR; simpl in HR; inversion_clear HR.
    split; [construction_closed | isval].
  Qed.

Products

For the product types we follow the usual approach of the logical relations: the only expressions that belong to the interpretation are pairs — and only if each of the components belongs to the interpretation of the appropriate type. The natural numbers only tag along for the ride: the pair is good for the same number of steps as each of the components.
  Inductive prodR : T → T → nat → exp → Prop :=
  | RPair (RL RR : T) e1 e2 n
          (HL : e1 ∈ RL @ n)
          (HR : e2 ∈ RR @ n) :
      prodR RL RR n 〈e1, e2〉.

The first thing we have to prove about our interpretation of products is that they are monotone in the step-index and only contain closed values. These properties follow easily, since both of the components only contain closed values.
  Program Definition prodR_up (RL RR : T) : T :=
    exist (mkUPred (prodR RL RR) _) _.
  Next Obligation.
    intros n m e e' HLe HSub HProd; simpl in HSub; subst e'.
    inversion_clear HProd; apply RPair; rewrite HLe; assumption.
  Qed.
  Next Obligation.
    intros n e HR; simpl in HR; inversion_clear HR.
    destruct (proj2_sig RL _ _ HL) as [HC1 [v1 EQ1]]; subst.
    destruct (proj2_sig RR _ _ HR0) as [HC2 [v2 EQ2]]; subst.
    split; [construction_closed | isval].
  Qed.

Now we know that our interpretation indeed is a semantic type, but we need slightly more: a nonexpansive combinator on the interpretations (including the interpretation of contexts). To this end, it suffices to show that the product construction preserves equality and n-equality — which for products is rather simple. Then finally we can define the combinator, by ensuring all the morphisms involved are nonexpansive.
  Global Instance prodR_up_equiv : Proper (equiv ==> equiv ==> equiv) prodR_up.
  Proof.
    intros RA1 RA2 EQRA RR1 RR2 EQRR n e; split; intros HProd;
    inversion_clear HProd; apply RPair; intros;
    first [apply EQRA | apply EQRR]; assumption.
  Qed.

  Global Instance prodR_up_dist n : Proper (dist n ==> dist n ==> dist n) prodR_up.
  Proof.
    intros RA1 RA2 EQRA RR1 RR2 EQRR m e HLt; split; intros HProd;
    inversion_clear HProd; apply RPair; intros;
    first [apply EQRA | apply EQRR]; assumption.
  Qed.

  Program Definition rel_prod i : int i -n> int i -n> int i :=
    n[(fun RA ⇒ n[(fun RR ⇒ n[(fun η ⇒ prodR_up (RA η) (RR η))])])].

Functions

Note that in the case of products the interpretations of typing contexts were just passed along: since the product type does not involve type variables, the interpretation also only depended on the final semantic types of the components. The same will be the case for the arrow types — although other parts of the definition will get more involved.
First, since the lambda abstractions suspend computations, we will need an evaluation closure of a semantic type. To this end, we use a generic evaluation closure defined in Constr.v, and instantiate it with our small-step operational semantics, first dropping the extra information we strap on the semantic types, since we only really need the predicate on expressions.

  Definition rel_eval' : T -n> UPred exp :=
    precomp_ne inclM (rel_evalCl step ext_step_step _).

Once this is done, we can define a relation that will be the cornerstone of the interpretation of arrow types. Again, the general principle follows the usual approach of the logical relations technique: the predicate is inhabited only by closed (note the HC hypothesis•) lambda abstractions, such that if we take any expression in the interpretation of the argument type and substitute it for the bound variable, the resulting expression will be in the evaluation closure of the result type. However, to ensure that the resulting predicate is downwards closed, we need to explicitly allow the step-index to decrease before taking the argument in RA (the HLt hypothesis in HFun). This is due to the contravariance, similar to the usual quantification over future worlds in the Kripke semantics of implication.
  Inductive arrR : T → T → nat → exp → Prop :=
  | RLam (RA RR : T) e n
         (HC : closed 1 e)
         (HFun : ∀ (ea : exp) m
                        (HLt : m ≤ n)
                        (HArg : ea ∈ RA @ m),
                   rel_eval' RR m (subst ea O e)) :
      arrR RA RR n (λ e).

After building this definition, everything proceeds the same way as for products: we show that our predicate forms a semantic type, and that it preserves equality and n-equality, and finally we can build an appropriate combinator.
  Program Definition arrR_up RA RR : T :=
    exist (mkUPred (arrR RA RR) _) _.
  Next Obligation.
    intros n m e e' HLe HSub HArr; simpl in HSub; subst e'.
    inversion_clear HArr; apply RLam; eauto with arith; reflexivity.
  Qed.
  Next Obligation.
    intros n e HR; simpl in HR; inversion HR; subst; clear HR.
    split; [construction_closed | isval].
  Qed.

  Global Instance arrR_up_equiv : Proper (equiv ==> equiv ==> equiv) arrR_up.
  Proof.
    intros RA1 RA2 EQRA RR1 RR2 EQRR n e; split; intros HArr;
    inversion_clear HArr; apply RLam; intros; try assumption; [|].
    - rewrite <- EQRR; apply HFun; [| apply EQRA]; assumption.
    - rewrite EQRR; apply HFun; [| apply EQRA]; assumption.
  Qed.

  Global Instance arrR_up_dist n : Proper (dist n ==> dist n ==> dist n) arrR_up.
  Proof.
    intros RA1 RA2 EQRA RR1 RR2 EQRR m e HLt; split; intros HArr;
    inversion_clear HArr; apply RLam; intros; try assumption; [|].
    - eapply rel_eval'; [symmetry; apply EQRR | now eauto with arith
                        | apply HFun; [assumption |] ].
      apply EQRA; eauto with arith.
    - eapply rel_eval'; [apply EQRR | now eauto with arith | apply HFun; [assumption |] ].
      apply EQRA; eauto with arith.
  Qed.

  Program Definition rel_arr i : int i -n> int i -n> int i :=
    n[(fun RA ⇒ n[(fun RR ⇒ n[(fun η ⇒ arrR_up (RA η) (RR η))])])].

Type variables

Now we finally reach the part where we have to take into account the type-level contexts that we have been threading along in the previous constructions. The first thing we have to do is interpret the type variables. This is relatively simple, if we treat a type variable as just an index into the typing context of size k. Given our definition of the interpretation of typing contexts, this is simple: our semantic version of a type variable will be an object of the type Fin.t k, the finite type of size k — and the interpretation is just the appropriate projection of the typing contexts (which, as it happens we know always to be nonexpansive, hence the use of MprojI). The final difficulty will be to get our hands on such an index, but this we will handle when we define the interpretation function.
  Program Definition rel_tvar k (x : Fin.t k) : int k := MprojI x.

Universal types

Universal types are one of the two constructions we consider that actually take into account the type contexts. Thus, the type of the resulting combinator will be int (S k) → int k, both here and for the recursive types.
The definition follows the usual treatment of System F: we allow for any /good/ semantic type to be taken for the one the big lambda introduces, and extend the interpretation context with it. Any expression that is in the evaluation closure of such a semantic type can now be suspended by a big lambda, and the resulting value belongs to the universally quantified type.
  Inductive allR i : int (S i) → TCRel i → nat → exp → Prop :=
  | RTLam (RE : int (S i)) (η : TCRel i) e n
          (HC : closed 0 e)
          (HEv : ∀ (R : T),
                   rel_eval' (RE (extFinI η R)) n e) :
      allR i RE η n (Λ e).

After defining the relation we proceed in the standard way: show that it indeed forms a semantic type and preserves the equality and n-equality, and finally build the appropriate combinator.
  Program Definition allR_up i RE η : T :=
    exist (mkUPred (allR i RE η) _) _.
  Next Obligation.
    intros n m e e' HLe HSub HAll; simpl in HSub; subst e'.
    inversion_clear HAll; apply RTLam; [assumption | intros].
    rewrite HLe; apply HEv.
  Qed.
  Next Obligation.
    intros n e HR; simpl in HR; inversion HR; subst; clear HR.
    split; [construction_closed | isval].
  Qed.

  Global Instance allR_up_equiv i : Proper (equiv ==> equiv ==> equiv) (allR_up i).
  Proof.
    intros RE1 RE2 EQRE η1 η2 EQη n e; split; intros HAll;
    inversion_clear HAll; apply RTLam; intros; try assumption; [|].
    - rewrite <- EQRE, <- EQη; apply HEv; assumption.
    - rewrite EQRE, EQη; apply HEv; assumption.
  Qed.

  Global Instance allR_up_dist i n : Proper (dist n ==> dist n ==> dist n) (allR_up i).
  Proof.
    intros RE1 RE2 EQRE η1 η2 EQη m e HLt; split; intros HAll;
    inversion_clear HAll; apply RTLam; intros; try assumption; [|].
    - eapply rel_eval'; [| eassumption | apply HEv; assumption].
      rewrite <- EQRE, <- EQη; reflexivity.
    - eapply rel_eval'; [| eassumption | apply HEv; assumption].
      rewrite EQRE, EQη; reflexivity.
  Qed.

  Program Definition rel_all i : int (S i) -n> int i :=
    n[(fun RE ⇒ n[(allR_up i RE)])].

Recursive types

The final type constructor we need to handle is the recursive type — and it is the trickiest one. The idea is to build a contractive map on T that would correspond to interpreting "one layer" of folding the recursive type, and then, since the map is contractive, take its fixpoint to be the interpretation. To do this, we proceed by taking the interpretation of the subtype τ of μ τ, the interpretation of the typing context, and the /approximation/ of the interpretation of the recursive type (RA). Then we extend the interpretation of the context with this approximation, to use with the interpretation of the subtype. The final detail we have to take care of is the contractiveness: this is dealt with by the later operator ▹, which decreases the step-index by one, as long as there are steps to decrease. Finally, if all these conditions are fulfilled, we can take efold of our expression to be in the /next approximation/ of the interpretation of the recursive type.
  Inductive recR i (RE : int (S i)) (η : TCRel i) (RA : T) : nat → exp → Prop :=
  | RFold e n
           (HC : closed 0 e)
           (HEv : (▹ rel_eval' (RE (extFinI η RA)))%up n e) :
      recR i RE η RA n (efold e).

  Program Definition recR_up i RE η RA : T :=
    exist (mkUPred (recR i RE η RA) _) _.
  Next Obligation.
    intros n1 n2 e e' HLt HSub HRec; simpl in HSub; subst e'.
    inversion_clear HRec; apply RFold; [assumption |].
    rewrite HLt; assumption.
  Qed.
  Next Obligation.
    intros n e HR; simpl in HR; inversion_clear HR.
    split; [construction_closed | isval].
  Qed.

  Global Instance recR_up_equiv i : Proper (equiv ==> equiv ==> equiv ==> equiv) (recR_up i).
  Proof.
    intros RE1 RE2 EQRE η1 η2 EQη R1 R2 EQR n v; split; intros HRec;
    inversion_clear HRec; apply RFold; intros; try assumption; [|].
    - rewrite <- EQRE, <- EQη, <- EQR; auto.
    - rewrite EQRE, EQη, EQR; auto.
  Qed.

  Global Instance recR_up_dist i n : Proper (dist n ==> dist n ==> dist n ==> dist n) (recR_up i).
  Proof.
    intros RE1 RE2 EQRE η1 η2 EQη R1 R2 EQR m v HLt; split; intros HRec;
    inversion HRec; subst; clear HRec; constructor; intros; try assumption; [|].
    - eapply later_up_dist; [| eassumption | apply HEv].
      rewrite <- EQRE, <- EQη, <- EQR; reflexivity.
    - eapply later_up_dist; [| eassumption | apply HEv].
      rewrite EQRE, EQη, EQR; reflexivity.
  Qed.

  Program Definition rel_foldF i : int (S i) -n> TCRel i -n> T -n> T :=
    n[(fun RE ⇒ n[(fun η ⇒ n[(recR_up i RE η)])])].

Once we prove that our predicate actually forms a semantic type, which is rather standard by now and that it preserves both equality and n-equality to form the functional rel_foldF, we get to the interesting part: we show that for any interpretations of the smaller type and the context, the operator on semantic types we get is actually contractive. This follows in a simple way, since we put the later operator in place precisely so that this lemma would hold. Once this is done, however, we can finally invoke Banach's fixpoint theorem, and prove some side conditions to get the combinator we wanted. Note that we still needed to provide the fixp operator with some "starting" relation; as we recall, the exact relation we put there does not matter, since the fixpoint is unique.
  Instance contr_rel_foldF i RE η : contractive (rel_foldF i RE η).
  Proof.
    intros n R1 R2 EQR m t HLt; split; intros HRec;
    inversion_clear HRec; constructor; intros; try assumption; [|].
    - destruct m as [| m]; [exact I |].
      eapply rel_eval'; [| apply lt_S_n; eassumption | apply HEv].
      rewrite EQR; reflexivity.
    - destruct m as [| m]; [exact I |].
      eapply rel_eval'; [| apply lt_S_n; eassumption | apply HEv].
      rewrite EQR; reflexivity.
  Qed.

  Program Definition rel_fold i : int (S i) -n> int i :=
    n[(fun RE ⇒ n[(fun η ⇒ fixp (rel_foldF i RE η) (exist (up_cr (const False)) _))])].
  Next Obligation.
    intros n e HR; contradiction HR.
  Qed.
  Next Obligation.
    intros η1 η2 EQη; apply fixp_equiv.
    rewrite EQη; reflexivity.
  Qed.
  Next Obligation.
    intros η1 η2 EQη; apply fixp_ne.
    rewrite EQη; reflexivity.
  Qed.
  Next Obligation.
    intros RE1 RE2 EQRE η; apply fixp_equiv.
    rewrite EQRE; reflexivity.
  Qed.
  Next Obligation.
    intros RE1 RE2 EQRE η; apply fixp_ne.
    rewrite EQRE; reflexivity.
  Qed.

End Constructions.

Notation " e ∈ R @ n " := (proj1_sig R n e) (at level 60, R at level 39, no associativity).

Interpretation

Now that we have defined all the important combinators, we can actually tie the knot, and define the interpretation of types. However, it only makes sense to interpret the types that are well-formed (closed) in the context. Thus, we need to carry the closedness proofs with us (the place where this pays off is the type variable, where the closedness allows us to say, informally "and since the type is well-formed, we can just use the appropriate index into the interpretation of the typing context"). Both for this case, and for carrying these proofs around we need the several simple lemmas provided below.
Section Interpretation.

  Lemma closed_tvar {n k : nat} {HC : closed k (tvar n)} : n < k.
  Proof.
    inversion_closed.
    destruct (le_lt_dec k n); [| assumption].
    rewrite lift_idx_old in H by assumption.
    symmetry in H; contradiction (n_Sn _ H).
  Qed.
  Lemma closed_prod {k t1 t2} {HC : closed k (t1 × t2)} : closed k t1 ∧ closed k t2.
  Proof.
    inversion_closed; auto.
  Qed.
  Definition closed_prod1 {k t1 t2} {HC : closed k (t1 × t2)} : closed k t1 :=
    proj1 closed_prod.
  Definition closed_prod2 {k t1 t2} {HC : closed k (t1 × t2)} : closed k t2 :=
    proj2 closed_prod.
  Lemma closed_arr {k t1 t2} {HC : closed k (t1 → t2)} : closed k t1 ∧ closed k t2.
  Proof.
    inversion_closed; auto.
  Qed.
  Definition closed_arr1 {k t1 t2} {HC : closed k (t1 → t2)} : closed k t1 :=
    proj1 closed_arr.
  Definition closed_arr2 {k t1 t2} {HC : closed k (t1 → t2)} : closed k t2 :=
    proj2 closed_arr.
  Lemma closed_all {k t} {HC : closed k (∀ t)} : closed (S k) t.
  Proof.
    inversion_closed; assumption.
  Qed.
  Lemma closed_rec {k t} {HC : closed k (μ t)} : closed (S k) t.
  Proof.
    inversion_closed; assumption.
  Qed.

With the lemmas we are set: we define the interpretation of types recursively on the type, using the appropriate combinators defined earlier. Note how in the type variable case — the only one that is not completely trivial, we produce an element of the finite type Fin.t by using the proof that the type variable is smaller than the size of the context.
  Fixpoint interpVal {k} (t : typ) (HC : closed k t) : int k :=
    match t return closed k t → int k with
      | tnat ⇒ fun _ ⇒ rel_nat k
      | tvar n ⇒ fun HC ⇒ rel_tvar k (Fin.of_nat_lt (p := n) closed_tvar)
      | t1 × t2 ⇒ fun HC ⇒ rel_prod k (interpVal t1 closed_prod1) (interpVal t2 closed_prod2)
      | t1 → t2 ⇒ fun HC ⇒ rel_arr k (interpVal t1 closed_arr1) (interpVal t2 closed_arr2)
      | ∀ t ⇒ fun HC ⇒ rel_all k (interpVal t closed_all)
      | μ t ⇒ fun HC ⇒ rel_fold k (interpVal t closed_rec)
    end HC.

In addition to the interpretation of types, we need two derived forms: the interpretation that is closed under evaluation — which we build by simple postcomposition with the evaluation closure used earlier — and the interpretation of (term-level) contexts. This second construct is a simple extension of the interpretation of types to sequences thereof. The assumption about closedness of types in Γ is included for proof engineering purposes: since the interpretation of types requires one to even be defined, we would have to thread this information through anyway, and it is simpler to require it in the place where it is needed.

  Definition interpExp {k} (t : typ) {HC : closed k t} : intE k :=
    postcomp_ne rel_eval' (interpVal t HC).

  Inductive relEnvs k : env typ → TCRel k → nat → env exp → Prop :=
  | rel_nil η n :
      relEnvs k nil η n nil
  | rel_cons :
      ∀ η n t Γ e γ
             (HC : closed k t)
             (HR : e ∈ interpVal t HC η @ n)
             (HRE : relEnvs k Γ η n γ),
        relEnvs k (Some t :: Γ)%list η n (Some e :: γ)%list.
  Instance preoEnvVal : preoType (env exp) := @disc_preo _ discreteType.
  Program Definition interpEnv {k} Γ : TCRel k -n> UPred (env exp) :=
    n[(fun η ⇒ mkUPred (relEnvs k Γ η) _)].
  Next Obligation.
    intros m n γ γ' HLe HEq HRE; simpl in HEq; subst γ'.
    induction HRE; econstructor; [| now auto].
    rewrite HLe; assumption.
  Qed.
  Next Obligation.
    intros η1 η2 EQη n γ; simpl; change (η1 == η2) in EQη.
    split; intros HRE; (induction HRE; econstructor; [| now eauto]).
    - eapply (morph_resp (interpVal t HC)); [symmetry |]; eassumption.
    - eapply (morph_resp (interpVal t HC)); eassumption.
  Qed.
  Next Obligation.
    intros η1 η2 EQη m γ HLt; simpl.
    split; intros HRE; (induction HRE; econstructor; [| now eauto]).
    - symmetry in EQη; eapply (interpVal t HC); eassumption.
    - eapply (interpVal t HC); eassumption.
  Qed.

Once we have the interpretation of contexts defined, we can finally give interpretation to open expressions, i.e., the logical relation. This is done in a standard way, by closing off all the variables of Γ with a related substitution γ.
As before, there is some choice of where to put the closedness conditions. We could require that Γ and t are closed in k, and that e is closed in Γ to even /state/ that e is in the logical relation. However, this would prove cumbersome in the proof. Thus, we choose to state these as the assumptions in the definition of the logical relation, so that we can say that, for example, e is in the relation even if it is not closed in Γ — such a statement would just be false (as opposed to ill-formed or impossible to make).
  Definition logrel k (Γ : env typ) (e : exp) (t : typ) :=
    ∀ (n : nat) e' (γ : env exp) (η : TCRel k)
           (HCe : closed 0 e')
           (HCt : closed k t)
           (HRE : interpEnv Γ η n γ)
           (HEq : e' = substEnv γ O e),
      interpExp t η n e'.

End Interpretation.

Notation "'E[[' t ']]'" := (interpExp t).
Notation "'V[[' t ']]'" := (interpVal t _).
Notation "'C[[' Γ ']]'" := (interpEnv Γ).

Properties of the Interpretation

First we need some immediate properties that follow from our definition of semantic types, as well as lemmas that help unfold equalities on universal and recursive types, which we don't explore in detail.
Section Properties.

  Lemma interp_values {k n e} {t : typ} {η} {HC : closed k t} (HR : e ∈ V[[ t ]] η @ n) :
    ∃ v : val, e = v.
  Proof.
    assert (HT := proj2_sig (V[[ t ]] η) _ _ HR); simpl in HT; tauto.
  Qed.

  Lemma interp_closed {k n e} {t : typ} {η}
        {HC : closed k t} (HR : e ∈ V[[ t ]] η @ n) :
    closed 0 e.
  Proof.
    assert (HT := proj2_sig (V[[ t ]] η) _ _ HR); simpl in HT; tauto.
  Qed.

End Properties.

Section AllRec.

  Lemma unfold_rec k (η : TCRel k) (t : typ) (HC : closed k (μ t)) :
    V[[μ t]] η == rel_foldF k (interpVal t closed_rec) η (V[[μ t]] η).
  Proof.
    apply fixp_eq.
  Qed.

  Lemma ext_all m k (η : TCRel m) (ρ : TCRel k) (t1 t2 : typ) (HC1 : closed m (∀ t1)) (HC2 : closed k (∀ t2))
        (HR : ∀ R, interpVal t1 closed_all (extFinI η R) == interpVal t2 closed_all (extFinI ρ R)) :
    V[[∀ t1]] η == V[[∀ t2]] ρ.
  Proof.
    simpl; intros i v; split; intros HAll; inversion_clear HAll; apply RTLam; intros; try assumption; [|].
    - rewrite <- HR; apply HEv.
    - rewrite HR; apply HEv.
  Qed.

  Lemma ext_rec m k (η : TCRel m) (ρ : TCRel k) (t1 t2 : typ) (HC1 : closed m (μ t1)) (HC2 : closed k (μ t2))
        (HR : ∀ R, interpVal t1 closed_rec (extFinI η R) == interpVal t2 closed_rec (extFinI ρ R)) :
    V[[μ t1]] η == V[[μ t2]] ρ.
  Proof.
    unfold interpVal; fold (@interpVal (S m)); fold (@interpVal (S k)); apply fixp_equiv.
    intros R i v; split; intros HRec; inversion_clear HRec;
    apply RFold; intros; try assumption; [|].
    - rewrite <- HR; apply HEv.
    - rewrite HR; apply HEv.
  Qed.

End AllRec.

Weakening and substitution

Finally, we get down to some crucial proerties. The point of this section is proving two important lemmas: invariance of the interpretation under weakening and substitution in /types/. These properties will be proved by induction on the type (that is weakened or substituted in), and this poses a problem: since on the way we may pass /type-level/ binders, we will need an appropriately general statements. (One needs to come up with a similar generalization when proving preservation of type under substitution required in the standard preservation proof.) The statements of the lemmas we are trying to prove are as follows: V[[ t ]] η == V[[ shift 0 t ]] (η · R) V[[ subst t2 0 t1 ]] η == V[[ t1 ]] ((V[[ t2 ]] η) · η).
For some represesentations of type variables these statements might be general enough. However, this is where one of the costs of deBruijn representations shows: for an appropriately general lemma we have to imagine that we have already passed some binders. This means that our interpretations of contexts have been extended with that number of relations. This gives us the appropriate form of the substitution lemma: V[[ subst (lift m 0 t2) m t1 ]] (ρ · η) == V[[ t1 ]] (ρ · ((V[[ t2 ]] η) · η)).
Note that since t2 might itself be open, we need to appropriately weaken it before substituting on the left; on the right the interpretation is already applied to the interpretation of the context, and so is a simple relation itself. Similarly, for weakening we get: V[[ t ]] (ρ · η) == V[[ shift m t ]] (ρ · (R · η)). Note that in fact this requires a particular shape of the natural number in the closedness condition to match the order in which the context is extended, due to the strong, dependently typed interpretations of contexts we use. Also, in the above the dot is used to denote both the extension of the context by one relation and by the whole context, which are different operations in the implementation.
Once the lemmas are stated correctly, the proofs are relatively straightforward, barring some rewriting in the proofs when the actual indexing into the interpretations of the contexts happens, i.e., in the type-variable case.
Section InterpretationProperties.

  Lemma interp_val_closed_ext k (t : typ) (HC1 HC2 : closed k t) :
    interpVal t HC1 == interpVal t HC2.
  Proof.
    revert k HC1 HC2; induction t; intros.
    - reflexivity.
    - unfold interpVal; erewrite of_nat_lt_ext; reflexivity.
    - intros η; simpl morph.
      apply prodR_up_equiv; [apply IHt1 | apply IHt2].
    - intros η; simpl morph.
      apply arrR_up_equiv; [apply IHt1 | apply IHt2].
    - intros η; apply ext_all.
      intros R; apply IHt.
    - intros η; apply ext_rec.
      intros R; apply IHt.
  Qed.

  Lemma interp_weakenG {t : typ} {k m} η ρ R
        (HC : closed (m + k) t)
        (HCR : closed (m + S k) (shift m t))
  :
    V[[ t ]] (extFinEnv η ρ) == V[[ shift m t ]] (extFinEnv (extFinI η R) ρ).
  Proof.
    revert m ρ HC HCR; induction t; intros m; simpl_lift_goal; intros.
    - intros n v; simpl; reflexivity.
    - unfold interpVal; simpl morph.
      generalize closed_tvar; clear HCR.
      generalize closed_tvar; clear HC.
      intros HLt; destruct (le_lt_dec m n).
      + rewrite lift_idx_old by assumption; simpl plus; intros HLt'.
        rewrite !(extFinEnv_lookup_right _ _ _).
        generalize (minus_le_lt _ HLt') as HLt''; replace (S n - m) with (S (n - m)) by auto with arith; intros.
        simpl; change (η (Fin.of_nat_lt (minus_le_lt l HLt)) == η (Fin.of_nat_lt (lt_S_n _ _ HLt''))).
        erewrite of_nat_lt_ext; reflexivity.
      + rewrite lift_idx_recent by assumption; intros HLt2; simpl morph.
        rewrite !(extFinEnv_lookup_left _ _ l); reflexivity.
    - simpl morph; apply prodR_up_equiv; [apply IHt1 | apply IHt2].
    - simpl morph; apply arrR_up_equiv; [apply IHt1 | apply IHt2].
    - apply ext_all; intros R0.
      rewrite !extFin_env_one; apply (IHt (S m)).
    - apply ext_rec; intros R0.
      rewrite !extFin_env_one; apply (IHt (S m)).
  Qed.

  Lemma interp_weaken k (t : typ) η R
        (HC : closed k t)
        (HCR : closed (S k) (shift 0 t)) :
    V[[ t ]] η == V[[ shift 0 t ]] (extFinI η R).
  Proof.
    assert (HT := interp_weakenG η empFinI R HC HCR); simpl morph in HT.
    rewrite !extFinEnv_empR in HT; assumption.
  Qed.

  Lemma interp_weaken_many m k (t : typ) (ρ : TCRel m) (η : TCRel k)
        (HC1 : closed k t)
        (HC2 : closed (m + k) (lift m 0 t)) :
    V[[lift m 0 t]] (extFinEnv η ρ) == V[[t]] η.
  Proof.
    revert HC2; induction m; simpl morph.
    - rewrite lift_zero; intros.
      rewrite (FinI_invert_O ρ), extFinEnv_empR.
      apply interp_val_closed_ext.
    - simpl plus; pattern (S m) at 1 2; replace (S m) with (1 + m) by reflexivity.
      rewrite <- (lift_lift_fuse _ 0) by auto with arith; intros.
      assert (HT : closed (m + k) (lift m 0 t)).
      { unfold closed in ×.
        rewrite lift_lift_reversed in HC2 by eauto with typeclass_instances || omega.
        lift_injective.
        replace (S (m + k) - 1) with (m + k) in HC2 by auto with arith; assumption.
      }
      rewrite (FinI_invert_S ρ), <- extFin_env_one.
      rewrite <- interp_weaken.
      apply IHm.
  Qed.

  Lemma interp_substG {t1 t2 : typ} {m k} (η : TCRel k) (ρ : TCRel m)
        (HC1 : closed (m + S k) t1)
        (HC2 : closed k t2)
        (HCS : closed (m + k) (subst (lift m 0 t2) m t1)) :
    V[[subst (lift m 0 t2) m t1]] (extFinEnv η ρ) == V[[t1]] (extFinEnv (extFinI η (V[[t2]] η)) ρ).
  Proof.
    revert m ρ HC1 HCS; induction t1; intros m ρ HC1; simpl_subst_goal; intros.
    - split; intros; simpl in *; assumption.
    - unfold subst_idx in ×.
      destruct (lt_eq_lt_dec n m) as [[HLt | HEq] | HLt]; intros; simpl morph.
      + rewrite !(extFinEnv_lookup_left _ _ HLt); reflexivity.
      + subst n; rewrite (extFinEnv_lookup_right _ _ (le_n m)).
        generalize (minus_le_lt _ closed_tvar) as HLt.
        rewrite minus_diag; intros; simpl.
        apply interp_weaken_many.
      + destruct n as [| n]; [inversion HLt |].
        revert HCS; simpl minus; rewrite <- minus_n_O; intros.
        apply le_S_n in HLt; assert (HT : m ≤ S n) by auto with arith.
        rewrite !(extFinEnv_lookup_right _ _ _).
        generalize (minus_le_lt HT closed_tvar) as HLtR.
        replace (S n - m) with (S (n - m)) by auto with arith; intros.
        simpl; change (η (Fin.of_nat_lt (minus_le_lt HLt closed_tvar)) == η (Fin.of_nat_lt (lt_S_n _ _ HLtR))).
        erewrite of_nat_lt_ext; reflexivity.
    - simpl morph; apply prodR_up_equiv; [apply IHt1_1 | apply IHt1_2].
    - simpl morph; apply arrR_up_equiv; [apply IHt1_1 | apply IHt1_2].
    - apply ext_all; intros R.
      revert HCS; rewrite lift_lift_fuse by auto with arith; intros.
      rewrite !extFin_env_one; apply (IHt1 (S m)).
    - apply ext_rec; intros R.
      revert HCS; rewrite lift_lift_fuse by auto with arith; simpl morph; intros.
      rewrite !extFin_env_one; apply (IHt1 (S m)).
  Qed.

  Lemma interp_subst k (η : TCRel k) (t1 t2 : typ)
        (HC1 : closed (S k) t1)
        (HC2 : closed k t2)
        (HCS : closed k (subst t2 0 t1)) :
    V[[subst t2 0 t1]] η == V[[t1]] (extFinI η (V[[t2]] η)).
  Proof.
    assert (HT := interp_substG η empFinI HC1 HC2).
    rewrite lift_zero in HT; simpl morph in HT; specialize (HT _).
    rewrite !extFinEnv_empR in HT; assumption.
  Qed.

End InterpretationProperties.

Properties of the Environments

We also need some properties of the interpretations of environments. Most of these are simple consequences of the lemmas we have proved before. The important ones are preservation under type-level weakening and the lookup property that allows us to prove the compatibility of the variable typing rule.
Section EnvironmentsProperties.

  Lemma relEnvs_lookup {n k η x} {Γ : env typ} {t : typ} {γ}
        (HCt : closed k t)
        (HFnd : lookup x Γ = Some t)
        (HRE : C[[ Γ ]] η n γ) :
    ∃ v, lookup x γ = Some v ∧ (v : exp) ∈ V[[t]] η @ n.
  Proof.
    revert x HFnd; induction HRE; intros;
    [apply lookup_empty_Some in HFnd; contradiction |].
    destruct x as [| x].
    - rewrite <- raw_insert_zero, lookup_insert_bingo in HFnd by reflexivity.
      inversion HFnd; subst; clear HFnd.
      ∃ e; split; [rewrite <- raw_insert_zero, lookup_insert_bingo; reflexivity |].
      eapply interp_val_closed_ext, HR.
    - rewrite lookup_successor in *; simpl in *; clear dependent e.
      destruct (IHHRE _ HFnd) as [v [HFnd' HR] ]; clear IHHRE HFnd.
      ∃ v; split; assumption.
  Qed.

  Lemma relEnvs_weaken m n k η R Γ γ
        (HLt : m ≤ n)
        (HRE : C[[ Γ ]] η n γ) :
    interpEnv (k := S k) (shift 0 Γ) (extFinI η R) n γ.
  Proof.
    induction HRE; simpl_lift_goal; [apply rel_nil |].
    assert (HT := closed_lift 0 _ _); simpl in HT.
    eapply rel_cons; [| apply IHHRE; assumption].
    assert (IW := interp_weaken); symmetry in IW; eapply IW; assumption.
  Qed.

  Lemma relEnvs_closed {n k η Γ γ}
        (HRE : interpEnv (k := k) Γ η n γ) :
    closed 0 γ.
  Proof.
    induction HRE; [construction_closed |].
    apply interp_closed in HR; construction_closed.
  Qed.

  Lemma relEnvs_subst_closed {n k η Γ γ} {e : exp}
        (HC : closed (length Γ) e)
        (HRE : interpEnv (k := k) Γ η n γ) :
    closed 0 (substEnv γ 0 e).
  Proof.
    revert HC; change (length Γ) with (0 + length Γ); generalize 0 as m.
    induction HRE; intros; simpl_subst_goal.
    - replace (m + length (nil : env typ)) with m in HC by apply plus_n_O.
      assumption.
    - replace (m + length (Some t :: Γ)) with (S m + (length Γ))
        in HC0 by apply plus_n_Sm.
      apply IHHRE in HC0; unfold closed.
      rewrite lift_subst_2 by apply le_n; simpl.
      f_equal; [| assumption].
      apply interp_closed in HR.
      apply closed_monotonic with 0; [apply _ | assumption | auto with arith].
  Qed.

End EnvironmentsProperties.

Lemma eval_simpl {k} (t : typ) {HC : closed k t} η n e :
  E[[ t ]] η n e ==
  ((irred e → e ∈ V[[ t ]] η @ n) ∧
   ∀ e' (HS : e ↦ e'), (▹ E[[ t ]] η)%up n e').
Proof. apply evalCl_eq. Qed.
Opaque interpExp.

Lemma eval_val {k} (t : typ) {HC : closed k t} η n e
      (HIrr : irred e)
      (HVal : e ∈ V[[ t ]] η @ n) :
  E[[ t ]] η n e.
Proof.
  rewrite eval_simpl; split; [now auto | intros; irred].
Qed.

Definition wf_ind_lt := well_founded_induction Wf_nat.lt_wf.

Compatibility Lemmas

Now we are finally able to prove compatibility lemmas — our key building blocks for proving the fundamental lemma. Each of these shows that the logical relation follows the appropriate rule of the type system. Since these are the key proofs in the development, we provide some annotations.
Section CompatibilityLemmas.

Natural numbers.
  Lemma compat_nat k Γ n : logrel k Γ ($ n) tnat.
  Proof.
    unfold logrel; intros; simpl_subst_all; subst e'.
    apply eval_val; [irred |].
    apply RNat.
  Qed.

Variables
  Lemma compat_var k Γ x t
        (HFnd : lookup x Γ = Some t) :
    logrel k Γ (#x) t.
  Proof.
    unfold logrel; intros; simpl_subst_all; subst.
    destruct (relEnvs_lookup _ HFnd HRE) as [e [HFnd' HR] ].
    assert (HCγ := relEnvs_closed HRE).
    assert (HT := substEnv_lookup (k := 0) x HFnd' HCγ); simpl in HT; rewrite HT; clear HT.
    destruct (interp_values HR) as [v EQv]; subst e.
    apply eval_val; [apply val_irred | assumption].
  Qed.

Intro forms
  Lemma compat_pair k t1 t2 Γ e1 e2
        (HLL : logrel k Γ e1 t1)
        (HLR : logrel k Γ e2 t2) :
    logrel k Γ 〈e1, e2〉 (t1 × t2).
  Proof.
    unfold logrel; intros; simpl_subst_all.
    subst e'; inversion_closed_in HCe.
    specialize (HLL _ _ _ _ H0 closed_prod1 HRE eq_refl).
    specialize (HLR _ _ _ _ H closed_prod2 HRE eq_refl).
    revert HLL; generalize (substEnv γ 0 e1); clear e1 H0; intros e1 HL1.
    revert HLR; generalize (substEnv γ 0 e2); clear e2 H ; intros e2 HL2.
    clear HRE; revert e1 e2 HL1 HL2; induction n using wf_ind_lt; rename H into HInd; intros.
    rewrite eval_simpl; split; [intros HIrr; clear HInd |
      intros; destruct n as [| n]; [exact I |]; inversion HS; subst; clear HS].
    - rewrite eval_simpl in HL1, HL2; apply proj1 in HL1; apply proj1 in HL2.
      assert (HI1 : irred e1) by irred; specialize (HL1 HI1); clear HI1.
      destruct (interp_values HL1) as [v1 HEq]; subst.
      simpl; apply RPair; [apply HL1 | apply HL2; irred].
    - apply HInd; [now auto with arith | | rewrite (le_n_Sn n); assumption].
      apply HL1, HStep.
    - apply HInd; [now auto with arith | rewrite (le_n_Sn n); assumption |].
      apply HL2, HStep.
  Qed.

  Lemma compat_lam k t1 t2 Γ e
        (HL : logrel k (insert 0 t1 Γ) e t2) :
    logrel k Γ (λ e) (t1 → t2).
  Proof.
    unfold logrel; intros; simpl_subst_all; subst.
    apply eval_val; [irred |].
    assert (HCγ := relEnvs_closed HRE).
    unfold closed in HCγ; rewrite HCγ in *; clear HCγ.
    inversion_closed_in HCe; apply fold_closed in H.
    simpl; apply RLam; intros; [assumption |].
    destruct (interp_values HArg) as [va HEq]; subst ea.
    apply HL with (γ := insert 0 (va : exp) γ); [| | reflexivity].
    -
      apply subst_preserves_closed; [apply _ | | assumption].
      apply interp_closed in HArg; assumption.
    -
      rewrite !raw_insert_zero.
      eapply rel_cons; [eassumption |].
      rewrite <- HLt in HRE; assumption.
  Qed.

  Lemma compat_tlam k Γ e t
        (HL : logrel (S k) (shift 0 Γ) e t) :
    logrel k Γ (Λ e) (∀ t).
  Proof.
    unfold logrel; intros; simpl_subst_all; subst.
    apply eval_val; [irred | simpl].
    inversion_closed_in HCe; apply fold_closed in H.
    apply RTLam; [assumption | intros].
    apply HL with (γ := γ); [eassumption | | reflexivity].
    apply relEnvs_weaken with n; auto with arith.
  Qed.

  Lemma compat_fold k Γ e t
        (HL : logrel (S k) (shift 0 Γ) e t) :
    logrel k Γ (efold e) (μ t).
  Proof.
    unfold logrel; intros; simpl_subst_all; subst.
    apply eval_val, unfold_rec; [irred |].
    inversion_closed_in HCe; apply fold_closed in H.
    apply RFold; intros; [assumption |].
    destruct n as [| n]; [exact I |].
    apply HL with (γ := γ); [assumption | | reflexivity].
    eapply relEnvs_weaken; [reflexivity | rewrite (le_n_Sn n); assumption].
  Qed.

Elim forms
  Lemma compat_fst k Γ (t1 t2 : typ) e
        (HC1 : closed k (t1 × t2))
        (HL : logrel k Γ e (t1 × t2)) :
    logrel k Γ (π1 e) t1.
  Proof.
    unfold logrel; intros; simpl_subst_all; subst.
    inversion_closed_in HCe; apply fold_closed in H.
    specialize (HL _ _ _ _ _ _ HRE eq_refl).
    revert HL; generalize (substEnv γ 0 e); clear.
    induction n using wf_ind_lt; rename H into HInd; intros.
    rewrite eval_simpl; split; [intros HIrr; clear HInd |
      intros; destruct n as [| n]; [exact I |]; inversion HS; subst; clear HS].
    - assert (HIe : irred e) by irred.
      rewrite eval_simpl in HL; apply proj1 in HL; specialize (HL HIe); clear HIe.
      simpl in HL; inversion HL; subst; clear HL.
      destruct (interp_values HL0) as [v1 EQ1]; destruct (interp_values HR) as [v2 EQ2].
      subst; irred.
    - clear HInd; rewrite eval_simpl in HL; apply proj1 in HL; simpl in ×.
      assert (HI : irred 〈v1, v2〉) by irred; specialize (HL HI); clear HI; inversion_clear HL.
      apply eval_val; [irred | erewrite (le_n_Sn n) ].
      revert HL0; apply interp_val_closed_ext.
    - apply HInd, HL, HStep; now auto with arith.
  Qed.

  Lemma compat_snd k Γ (t1 t2 : typ) e
        (HC1 : closed k (t1 × t2))
        (HL : logrel k Γ e (t1 × t2)) :
    logrel k Γ (π2 e) t2.
  Proof.
    unfold logrel; intros; simpl_subst_all; subst.
    inversion_closed_in HCe; apply fold_closed in H.
    specialize (HL _ _ _ _ _ _ HRE eq_refl).
    revert HL; generalize (substEnv γ 0 e); clear.
    induction n using wf_ind_lt; rename H into HInd; intros.
    rewrite eval_simpl; split; [intros HIrr; clear HInd |
      intros; destruct n as [| n]; [exact I |]; inversion HS; subst; clear HS].
    - assert (HIe : irred e) by irred.
      rewrite eval_simpl in HL; apply proj1 in HL; specialize (HL HIe); clear HIe.
      simpl in HL; inversion HL; subst; clear HL.
      destruct (interp_values HL0) as [v1 EQ1]; destruct (interp_values HR) as [v2 EQ2].
      subst; irred.
    - clear HInd; rewrite eval_simpl in HL; apply proj1 in HL; simpl in ×.
      assert (HI : irred 〈v1, v2〉) by irred; specialize (HL HI); clear HI; inversion_clear HL.
      apply eval_val; [irred | erewrite (le_n_Sn n) ].
      revert HR; apply interp_val_closed_ext.
    - apply HInd, HL, HStep; now auto with arith.
  Qed.

  Lemma compat_app k Γ (t1 t2 : typ) e1 e2
        (HC1 : closed k (t1 → t2))
        (HL1 : logrel k Γ e1 (t1 → t2))
        (HL2 : logrel k Γ e2 t1) :
    logrel k Γ (e1 @ e2) t2.
  Proof.
    unfold logrel; intros; simpl_subst_all; subst e'; inversion_closed_in HCe.
    apply fold_closed in H0; apply fold_closed in H.
    specialize (HL1 _ _ _ _ _ _ HRE eq_refl).
    specialize (HL2 _ _ _ _ _ closed_arr1 HRE eq_refl).
    revert HL1 HL2; generalize (substEnv γ 0 e2); generalize (substEnv γ 0 e1); clear.
    induction n using wf_ind_lt; rename H into HInd; intros e1 e2 HL1 HL2.
    rewrite eval_simpl; split; [intros HIrr; clear HInd |
      intros; destruct n as [| n]; [exact I |]; inversion HS; subst; clear HS].
    - assert (HI1 : irred e1) by irred; rewrite eval_simpl in HL1; apply proj1 in HL1.
      specialize (HL1 HI1); inversion HL1; subst; clear HI1 HL1 HFun HC.
      change (λ e) with (vlam e : exp) in HIrr; assert (HI2 : irred e2) by irred.
      rewrite eval_simpl in HL2; apply proj1 in HL2; specialize (HL2 HI2).
      destruct (interp_values HL2) as [v EQ]; subst; irred.
    - simpl; rewrite eval_simpl in HL1; apply proj1 in HL1; specialize (HL1 (val_irred (vlam _))).
      rewrite eval_simpl in HL2; apply proj1 in HL2; specialize (HL2 (val_irred _)).
      inversion_clear HL1; clear HC HInd.
      specialize (HFun _ _ (le_n _) HL2).
      erewrite interp_val_closed_ext, <- le_n_Sn in HFun; apply HFun.
    - apply HInd; [now auto with arith | | rewrite (le_n_Sn n); assumption].
      apply HL1, HStep.
    - apply HInd; [now auto with arith | rewrite (le_n_Sn n); assumption |].
      apply HL2, HStep.
  Qed.

  Lemma compat_tapp k Γ (t1 t2 : typ) e
        (HC1 : closed k (∀ t1))
        (HC2 : closed k t2)
        (HL : logrel k Γ e (∀t1)) :
    logrel k Γ (e •) (subst t2 0 t1).
  Proof.
    unfold logrel; intros; simpl_subst_all; subst; inversion_closed_in HCe.
    apply fold_closed in H; specialize (HL _ _ _ _ _ _ HRE eq_refl).
    revert HL; generalize (substEnv γ 0 e); clear - HC2.
    induction n using wf_ind_lt; rename H into HInd; intros.
    rewrite eval_simpl; split; [intros HIrr; clear HInd |
      intros; destruct n as [| n]; [exact I |]; inversion HS; subst; clear HS].
    - assert (HIe : irred e) by irred; rewrite eval_simpl in HL; apply proj1 in HL.
      specialize (HL HIe); inversion HL; subst; clear HL HIe; irred.
    - rewrite eval_simpl in HL; apply proj1 in HL; specialize (HL (val_irred (vtlam _))).
      inversion HL; subst; clear HInd HL; simpl.
      specialize (HEv (V[[t2]] η)); rewrite <- interp_subst, <- le_n_Sn in HEv; apply HEv.
    - apply HInd, HL, HStep; now auto with arith.
  Qed.

  Lemma compat_unfold k Γ e t
        (HC : closed k (μ t))
        (HL : logrel k Γ e (μ t)) :
    logrel k Γ (eunfold e) (subst (μ t) 0 t).
  Proof.
    unfold logrel; intros; simpl_subst_all; subst; inversion_closed_in HCe.
    apply fold_closed in H; specialize (HL _ _ _ _ _ _ HRE eq_refl).
    revert HL; generalize (substEnv γ 0 e); clear.
    induction n using wf_ind_lt; rename H into HInd; intros.
    rewrite eval_simpl; split; [intros HIrr; clear HInd |
      intros; destruct n as [| n]; [exact I |]; inversion HS; subst; clear HS].
    - assert (HIe : irred e) by irred; rewrite eval_simpl in HL; apply proj1 in HL.
      specialize (HL HIe); inversion HL; subst; clear HL HIe; irred.
    - simpl; rewrite eval_simpl in HL; apply proj1 in HL; specialize (HL (val_irred (vfold _))).
      apply unfold_rec in HL; inversion_clear HL.
      rewrite <- interp_subst in HEv; apply HEv.
    - apply HInd, HL, HStep; now auto with arith.
  Qed.

End CompatibilityLemmas.

Fundamental Lemma

Now we can finally prove the Fundamental Lemma: any well-typed program is in the logical relation at that type. The proof will follow by induction on the typing derivation, and use the appropriate compatibility lemma at each case. Since there will be plenty of cases, we will use some simple automation, and add all the compatibility lemmas to a hint database first.
Hint Resolve compat_nat compat_var compat_pair compat_lam compat_tlam compat_fold
     compat_fst compat_snd compat_app compat_tapp compat_unfold : compat.

Lemma Fundamental : ∀ k Γ e t,
                      [k | Γ ⊢ e ::: t] → logrel k Γ e t.
Proof.
  induction 1; subst; eauto using types_closed_t with compat.
Qed.

Towards Soundness

With the Fundamental lemma proved, we are almost done. Still, we need some more syntactic definitions to even state the soundness property. This is relatively straightforward, though. In the end, soundness turns out to be a simple corollary of the Fundamental Lemma, much as it usually is.

Inductive stepn : nat → exp → exp → Prop :=
| stepO e : stepn O e e
| stepS n e e1 e2
        (HS : e ↦ e1)
        (HN : stepn n e1 e2) :
    stepn (S n) e e2.

Corollary Soundness n e e' t
        
        (HT : [0 | nil ⊢ e ::: t] )
        
        (HSN : stepn n e e')
        (HIrr : irred e') :
  ∃ v : val, e' = v.
Proof.
  assert (HL := Fundamental _ _ _ _ HT).
  apply types_closed in HT; destruct HT as [_ [HCt HCe] ].
  assert (HR := rel_nil _ empFinI n).
  assert (HC := relEnvs_subst_closed HCe HR); clear HCe.
  specialize (HL n _ _ _ _ _ HR eq_refl).
  clear HR HC; simpl in HL; induction HSN.
  - rewrite eval_simpl in HL; apply proj1 in HL; specialize (HL HIrr).
    apply (interp_values HL).
  - apply IHHSN, HL, HS; assumption.
Qed.

Exercises

Since this is a relatively advanced tutorial, we did not feel the need to include many exercises and unfinished proofs in the text. However, to achieve a good feeling for the way the kind of definitions we use here works, it is beneficial to actually do some extra proofs. Thus, we propose the following set of exercises.

*Exercise* Sum and unit types (2 stars).

While it does not change the complexity of the model, recursive types are not particularly useful without also having sum types in the language. Extend the language with the type of sums t1 + t2, and the unit type (), the appropriate expressions and values. Define their interpretations, and make sure the Fundamental lemma still holds. Note, the proof of the Fundamental lemma itself should not change.

*Exercise* Existential types (3 stars).

Technically, one can encode existential types using universal types (how?). However, this is cumbersome, and all the machinery needed to implement existential types directly in the language is already in place. Implement the existential types, and make sure the Fundamental lemma still holds.

*Exercise* Relational interpretation (4 stars, involved).

For System Fμ, the unary model does not give us much we couldn't prove using progress and preservation. A binary model, on the other hand, is much more interesting, since we can use it to prove parametricity results for our calculus. Define a binary interpretation of the programming language, and make sure the Fundamental lemma still holds. Note, the interpretation of types will have to change from the uniform predicates to /uniform relations/, and the evaluation closure will need to change significantly.

TODO *Exercise* Relational parametricity (3 stars, involved).

Use the relational interpretation to prove a parametricity result. Have to actually come up with a doable property, though.