Type soundness of λ-ref via logical relations.

In this chapter we utilize the other aspect of the complete, ultrametric spaces — the general solution of recursive domain equations — to build a unary system of a lambda-calculus with higher-order references and general recursion. Like in the previous chapter, this provides an alternative technique to the progress + preservation formulation.
The crucial development of this chapter will be stating the recursive domain equation that desribes the relationship between semantic types and semantic descriptions of heaps, which we call worlds. Once we state the equation, we can use the general solution to build the spaces of semantic types and worlds, and show how we can interpret the reference types in this setup.

Require Import DBLib.DeBruijn DBLib.Environments.

Arguments exist {A P} _ _.

The Language

We start the chapter by defining the object language: a simple calculus with product, functional and general reference types, as well as a trivial unit type.
We use the now-familiar syntax with de Bruijn indices for variables. Note that the function expression binds two arguments: this is since it encodes a general (call-by-value) fix point operator instead of the usual lambda abstraction. As in the Fμ chapter, we define values and substitution of values into expressions, and proving the lemmas about substituting multiple values at once.
Inductive type :=
| tUnit
| tProd : type → type → type
| tSum : type → type → type
| tRef : type → type
| tFun : type → type → type.

Inductive exp :=
| eUnit
| eVar : nat → exp
| ePair : exp → exp → exp
| eInL : exp → exp
| eInR : exp → exp
| eFun : exp → exp
| eLoc : nat → exp
| eProj1 : exp → exp
| eProj2 : exp → exp
| eCase : exp → exp → exp → exp
| eApply : exp → exp → exp
| eRef : exp → exp
| eDeref : exp → exp
| eAssign : exp → exp → exp.

Inductive val :=
| vUnit
| vPair : val → val → val
| vInL : val → val
| vInR : val → val
| vFun : exp → val
| vLoc : nat → val.

Implicit Types (τ : type) (v : val) (e : exp).

Bind Scope lr_scope with type.
Bind Scope lr_scope with exp.
Notation "'()'" := tUnit : lr_scope.
Notation "τ × σ" := (tProd τ σ) (at level 40, left associativity) : lr_scope.
Notation "τ + σ" := (tSum τ σ) (at level 50, left associativity) : lr_scope.
Notation "τ → σ" := (tFun τ σ) (at level 60, right associativity) : lr_scope.
Notation "'ref' τ" := (tRef τ) (at level 10) : lr_scope.

Notation "e1 @ e2" := (eApply e1 e2) (at level 40, left associativity) : lr_scope.
Notation "'λ' e" := (eFun e) (at level 30) : lr_scope.
Notation "# n" := (eVar n) (at level 10) : lr_scope.
Notation "〈 e1 , e2 〉" := (ePair e1 e2) : lr_scope.
Notation "'π1' e" := (eProj1 e) (at level 10) : lr_scope.
Notation "'π2' e" := (eProj2 e) (at level 10) : lr_scope.
Notation "'ıL' e" := (eInL e) (at level 10) : lr_scope.
Notation "'ıR' e" := (eInR e) (at level 10) : lr_scope.
Notation "! e" := (eDeref e) (at level 35) : lr_scope.
Notation "'new' e" := (eRef e) (at level 10) : lr_scope.
Notation "e1 '::=' e2" := (eAssign e1 e2) (at level 20) : lr_scope.

Delimit Scope lr_scope with lr.
Open Scope lr_scope.

Section Traversal.
  Global Instance Var_exp: Var exp := { var := eVar }.
  Fixpoint traverse_exp (f : nat → nat → exp) l e :=
    match e with
      | eUnit ⇒ eUnit
      | # x ⇒ f l x
      | 〈 e1, e2 〉 ⇒ 〈 traverse_exp f l e1, traverse_exp f l e2 〉
      | π1 e ⇒ π1 (traverse_exp f l e)
      | π2 e ⇒ π2 (traverse_exp f l e)
      | ıL e ⇒ ıL (traverse_exp f l e)
      | ıR e ⇒ ıR (traverse_exp f l e)
      | eCase e eL eR ⇒ eCase (traverse_exp f l e) (traverse_exp f (S l) eL) (traverse_exp f (S l) eR)
      | λ e ⇒ λ (traverse_exp f (S (S l)) e)
      | e1 @ e2 ⇒ traverse_exp f l e1 @ traverse_exp f l e2
      | eLoc n ⇒ eLoc n
      | new e ⇒ new (traverse_exp f l e)
      | ! e ⇒ ! (traverse_exp f l e)
      | e1 ::= e2 ⇒ traverse_exp f l e1 ::= traverse_exp f l e2
    end.

  Global Instance Traverse_exp : Traverse exp exp :=
    { traverse := traverse_exp }.

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

  Fixpoint val_to_exp v :=
    match v with
      | vUnit ⇒ eUnit
      | vPair v1 v2 ⇒ 〈 val_to_exp v1, val_to_exp v2 〉
      | vInL v ⇒ ıL (val_to_exp v)
      | vInR v ⇒ ıR (val_to_exp v)
      | vFun e ⇒ λ e
      | vLoc n ⇒ eLoc n
    end.
  Coercion val_to_exp : val >-> exp.

  Fixpoint traverse_val (f : nat → nat → exp) l v :=
    match v with
      | vUnit ⇒ vUnit
      | vPair v1 v2 ⇒ vPair (traverse_val f l v1) (traverse_val f l v2)
      | vInL v ⇒ vInL (traverse_val f l v)
      | vInR v ⇒ vInR (traverse_val f l v)
      | vFun e ⇒ vFun (traverse f (S (S l)) e)
      | vLoc n ⇒ vLoc n
    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) n k :
    lift n k (v : exp) = (lift n k v : exp).
  Proof.
    induction v; simpl; repeat simpl_lift_goal; simpl; congruence.
  Qed.

End Traversal.

Lemma val_to_exp_inj : ∀ v1 v2 (Heq: (v1 : exp) = v2), v1 = v2.
Proof.
  induction v1; destruct v2; intros; try (discriminate Heq); simpl in *;
  [reflexivity |..]; inversion Heq; clear Heq; f_equal; now auto.
Qed.

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

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; try autorewrite with substexp; reflexivity
    | _ ⇒ fail "Can only be used on an environment."
  end.

Section EnvSubstsCommute.

  Lemma subst_lam : ∀ (ρ : env exp) n (e : exp),
    substEnv ρ n (λ e) = λ substEnv (lift 2 O ρ) (S (S n)) e.
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_app :
    ∀ (ρ : env exp) n (e1 e2 : exp),
      substEnv ρ n (e1 @ e2) = substEnv ρ n e1 @ substEnv ρ n e2.
  Proof. intros ρ; commute_env ρ. Qed.

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

  Lemma subst_proj1:
    ∀ (ρ: env exp) n (e: exp),
      substEnv ρ n (π1 e) = π1 (substEnv ρ n e).
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_proj2:
    ∀ (ρ: env exp) n (e: exp),
      substEnv ρ n (π2 e) = π2 (substEnv ρ n e).
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_inl:
    ∀ (ρ: env exp) n (e: exp),
           substEnv ρ n (ıL e) = ıL (substEnv ρ n e).
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_inr:
    ∀ (ρ: env exp) n e,
           substEnv ρ n (ıR e) = ıR (substEnv ρ n e).
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_case:
    ∀ (ρ : env exp) n e1 e2 e3,
      substEnv ρ n (eCase e1 e2 e3) =
      eCase (substEnv ρ n e1) (substEnv (shift 0 ρ) (S n) e2) (substEnv (shift 0 ρ) (S n) e3).
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_unit:
    ∀ (ρ: env exp) n, substEnv ρ n eUnit = eUnit.
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_loc:
    ∀ (ρ: env exp) n l, substEnv ρ n (eLoc l) = eLoc l.
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_ref:
    ∀ (ρ: env exp) n (e: exp), substEnv ρ n (new e) = new (substEnv ρ n e).
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_deref:
    ∀ (ρ: env exp) n (e: exp), substEnv ρ n (! e) = ! (substEnv ρ n e).
  Proof. intros ρ; commute_env ρ. Qed.

  Lemma subst_assign:
    ∀ (ρ: env exp) n (e1 e2: exp),
      substEnv ρ n (e1 ::= e2) = (substEnv ρ n e1) ::= (substEnv ρ n e2).
  Proof. intros ρ; commute_env ρ. Qed.

End EnvSubstsCommute.

Hint Rewrite subst_lam subst_app subst_pair subst_proj1 subst_proj2 subst_inl subst_inr subst_case subst_unit subst_loc subst_ref subst_deref subst_assign : substexp.

Type system and operational semantics

These are virtually standard systems for the lambda calculus with references. Note that the type system does not include a typing of heaps or a rule for locations, so the usual progress + preservation approach to soundness would not work without extending it. However, it is sufficient for our approach.

Implicit Types (Γ : env type).
Reserved Notation "[ Γ ⊢ e : τ ]" (at level 50, e at next level).

Inductive types : env type → exp → type → Prop :=
| VarT Γ x τ (HLu : lookup x Γ = Some τ) :
    [ Γ ⊢ # x : τ ]
| UnitT Γ :
    [ Γ ⊢ eUnit : () ]
| PairT Γ e1 e2 τ1 τ2
        (HT1 : [Γ ⊢ e1 : τ1]) (HT2 : [Γ ⊢ e2 : τ2]) :
    [Γ ⊢ 〈e1, e2〉 : τ1 × τ2]
| Proj1T Γ e τ1 τ2
         (HT : [Γ ⊢ e : τ1 × τ2]) :
    [Γ ⊢ π1 e : τ1]
| Proj2T Γ e τ1 τ2
         (HT : [Γ ⊢ e : τ1 × τ2]) :
    [Γ ⊢ π2 e : τ2]
| CaseT Γ e e1 e2 τ τ1 τ2
        (HT1 : [insert 0 τ1 Γ ⊢ e1 : τ]) (HT2 : [insert 0 τ2 Γ ⊢ e2 : τ]) (HT3 : [Γ ⊢ e : τ1 + τ2]) :
    [Γ ⊢ eCase e e1 e2 : τ]
| InLT Γ e τ1 τ2
       (HT : [Γ ⊢ e : τ1]) :
    [Γ ⊢ ıL e : τ1 + τ2]
| InRT Γ e τ1 τ2
       (HT : [Γ ⊢ e : τ2]) :
    [Γ ⊢ ıR e : τ1 + τ2]
| FunT Γ e τ1 τ2
       (HT : [insert 0 τ1 (insert 0 (τ1 → τ2) Γ) ⊢ e : τ2]) :
    [Γ ⊢ λ e : τ1 → τ2]
| ApplyT Γ e1 e2 σ τ
         (HT1 : [Γ ⊢ e1 : σ → τ]) (HT2 : [Γ ⊢ e2 : σ]) :
    [Γ ⊢ e1 @ e2 : τ]
| RefT Γ e τ
       (HT : [Γ ⊢ e : τ]) :
    [Γ ⊢ new e : ref τ]
| DerefT Γ e τ
         (HT : [Γ ⊢ e : ref τ]) :
    [Γ ⊢ ! e: τ]
| AssignT Γ e1 e2 τ
          (HT1 : [Γ ⊢ e1 : ref τ]) (HT2 : [Γ ⊢ e2 : τ]) :
    [Γ ⊢ e1 ::= e2 : () ]
where "[ Γ ⊢ e : τ ]" := (types Γ e τ) : lr_scope.

Lemma types_closed Γ e τ (HT : [Γ ⊢ e : τ]) : closed (length Γ) e.
Proof. induction HT; construction_closed. Qed.

Require Import ModuRes.Finmap.
Require Import Arith.

Notation "f '[' k ↦ v ']'" := (fdUpdate k v f) (at level 5) : lr_scope.

Require Import ModuRes.PCOFE ModuRes.RecDom ModuRes.CBUltInst ModuRes.Constr ModuRes.UPred.

Instance val_type : Setoid val := discreteType.
Instance preo_val : preoType val := disc_preo val.
Instance preo_exp : preoType exp := @disc_preo _ discreteType.

We use finite maps from location to values as heaps.
Definition heap := nat -f> val.

Reserved Notation "e || h ↦ e' || h'" (at level 50, h at level 49, e' at level 48).

Implicit Types (h : heap).

Inductive step : exp → heap → exp → heap → Prop :=

| ApplyFunR v e e' h
            (HSub : e' = subst (λ e) 0 (subst (v : exp) 0 e)) :
    (λ e) @ v || h ↦ e' || h
| Proj1PairR v1 v2 h :
    (π1 〈v1, v2〉) || h ↦ v1 || h
| Proj2PairR v1 v2 h :
    (π2 〈v1, v2〉) || h ↦ v2 || h
| CaseInLR v eL eR e' h
           (HSub : e' = subst (v : exp) 0 eL) :
    eCase (ıL v) eL eR || h ↦ e' || h
| CaseInRR v eL eR e' h
           (HSub : e' = subst (v : exp) 0 eR) :
    eCase (ıR v) eL eR || h ↦ e' || h
| RefR v l h h'
       (HFresh : ¬ l ∈ dom h)
       (HUpdate : h' = h [l ↦ v]) :
    new v || h ↦ eLoc l || h'
| DerefR l h v
         (HLookup : h l = Some v) :
    ! (eLoc l) || h ↦ v || h
| AssignR l v h h'
          (HDom : l ∈ dom h)
          (HUpdate : h' = h [ l ↦ v ]) :
    eLoc l ::= v || h ↦ eUnit || h'

| AppLC e1 e1' e2 h h'
        (HS : e1 || h ↦ e1' || h') :
    e1 @ e2 || h ↦ e1' @ e2 || h'
| AppRC e e' v h h'
        (HS : e || h ↦ e' || h') :
    v @ e || h ↦ v @ e' || h'
| PairLC e1 e1' e2 h h'
         (HS : e1 || h ↦ e1' || h') :
    〈e1, e2〉 || h ↦ 〈e1', e2〉 || h'
| PairRC e e' v h h'
         (HS : e || h ↦ e' || h') :
    〈v, e〉 || h ↦ 〈v, e'〉 || h'
| Proj1C e e' h h'
         (HS : e || h ↦ e' || h') :
    (π1 e) || h ↦ (π1 e') || h'
| Proj2C e e' h h'
         (HS : e || h ↦ e' || h') :
    (π2 e) || h ↦ (π2 e') || h'
| InLC e e' h h'
       (HS : e || h ↦ e' || h') :
    (ıL e) || h ↦ (ıL e') || h'
| InRC e e' h h'
       (HS : e || h ↦ e' || h') :
    (ıR e) || h ↦ (ıR e') || h'
| CaseC e e' eL eR h h'
        (HS : e || h ↦ e' || h') :
    eCase e eL eR || h ↦ eCase e' eL eR || h'
| RefC e e' h h'
       (HS : e || h ↦ e' || h') :
    (new e) || h ↦ (new e') || h'
| DerefC e e' h h'
         (HS : e || h ↦ e' || h') :
    (! e) || h ↦ (! e') || h'
| AssignLC e1 e1' e2 h h'
           (HS : e1 || h ↦ e1' || h') :
    e1 ::= e2 || h ↦ e1' ::= e2 || h'
| AssignRC v e e' h h'
           (HS : e || h ↦ e' || h') :
    v ::= e || h ↦ v ::= e' || h'
where "e || h ↦ e' || h'" := (step e h e' h') : lr_scope.

Some additional definitions: n-step reduction and irreducibility.
Inductive step_n : nat → exp → heap → exp → heap → Prop :=
| StepO e h :
    step_n 0 e h e h
| StepS n e1 e2 e3 h1 h2 h3
        (HStep : e1 || h1 ↦ e2 || h2)
        (HStepn : step_n n e2 h2 e3 h3) :
    step_n (S n) e1 h1 e3 h3.

Definition irred e h := ∀ e' h', ¬ e || h ↦ e' || h'.

Values are irreducible.
Lemma irred_val v h : irred v h.
Proof.
  revert h; induction v; intros h exp h' Hred;
  try (inversion Hred; subst; clear Hred; eapply IHv; eassumption).
  inversion Hred; subst; clear Hred; [eapply IHv1 | eapply IHv2]; eassumption.
Qed.

Some handy tactics:
  • valify is a helper tactic, that tries to find a value that would coerce to its argument, e
  • irred is a general tactic that tries to solve a goal by using irreducibility. It tries to use irred_val or an irreducibility assumption, potentially in conjunction with assumptions about reducibility. Furthermore, it tries to solve goal that require us to show irreducibility of a subexpression of something we know is irreducible, and plain contradictions by using the operational semantics.
  • isval is useful when we need to exhibit a value that is equal to some expression. It uses valify to find such a value.
  • simpl_vals makes use of injectivity of the coercion from values to expressions, to try to strip it off and substitute away as many of the values as it can.

Ltac valify e :=
  match e with
    | val_to_exp ?v ⇒ constr:v
    | 〈 ?e1, ?e2 〉%lr ⇒
      let v1 := valify e1 in
      let v2 := valify e2 in
      constr:(vPair v1 v2)
    | ıL ?e ⇒ let v := valify e in constr:(vInL v)
    | ıR ?e ⇒ let v := valify e in constr:(vInR v)
    | λ ?e ⇒ constr:(vFun e)
    | eUnit ⇒ constr:vUnit
    | eLoc ?l ⇒ constr:(vLoc l)
  end.

Ltac irred :=
  match goal with
    | |- irred ?e _ ⇒
      let v := valify e in apply (irred_val v)
    | HS: ?e || _ ↦ _ || _ |- _ ⇒
      let v := valify e in contradiction (irred_val v _ _ _ HS)
    | HI: irred ?e ?h, HS : ?e || ?h ↦ _ || _ |- _ ⇒ contradiction (HI _ _ _ _ HS)
    | HI: irred ?e1 ?h |- irred ?e2 ?h ⇒
      match e1 with
          context [e2] ⇒
          let HS := fresh "HS" in
          intros ? ? HS; (eapply HI || fail 2 "Given hyp does not match");
          now eauto using step || fail 2 "Reduction failed"
      end
    | HI: irred _ _ |- False ⇒ 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 simpl_vals :=
  repeat match goal with
           | [H : val_to_exp ?v = ?e |- _] ⇒
             let v' := valify e in
             apply (val_to_exp_inj v v') in H; try (subst v || subst v')
           | [H : ?e = val_to_exp ?v |- _] ⇒
             let v' := valify e in
             apply (val_to_exp_inj v' v) in H; try subst v
         end.

Recursive Domain Equation

The following section is the crux of this chapter. In the following we will describe our space of semantic types, and use the general solution of the recursive domain equations (found in [MetricRec.v]) to construct the spaces of types and worlds.
Reminiscent of the previous chapter, we want to use uniform predicates on expressions as the target of our interpretation — and much the same as there, we need to require some additional properties of it: namely that the expressions in the interpretations are closed values. We do this by taking UPC to be a subset type of UPred exp that only contains closed values.

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

Instance LP_closedVal : LimitPreserving rel_closedVal.
Proof.
  intros c Cc HC k v HR; simpl in ×.
  apply HC in HR; assumption.
Qed.

Definition UPC := {P : UPred exp | rel_closedVal P}.

Now consider what will we need to interpret the reference type. It should contain locations (which are closed values), but the question which locations are "good" remains. The answer is for the interpretation to take an additional parameter: a semantic description of a heap, or, a world. The world is supposed to map locations into the *semantic* types of values that should be stored in that part of the heap. Note, however, that the space of semantic types is precisely what we are trying to define. This means that our would-be definition of semantic types is circular.
We solve this circularity by using the [MetricRec] library, which implements a solution of the recursive domain equations developed in [???]. As we will see, the precise knowledge of how the solution is constructed is not necessary; we will explain the parts that are needed as we go through the definitions here.

Section TypeFunctorDefs.
  Existing Instances pt_disc pcm_disc.

First, we need to state the equation we want to solve. To this end, we define a map TFun that for each complete metric space T builds a space of the same shape we need of our semantic types — but with the recursive occurrence substituted with T, T ↦ (nat ⇀ T) →ₘ UPC.
  Definition TFun T `{cT : cofe T} :=
    (nat -f> T) -m> UPC.

  Context {T1 T2} `{cT1 : cofe T1, cT2 : cofe T2}.

One of the few constraints that the solution places on the input equations is that they need to be functors, i.e., we need to define a corresponding action on the nonexpansive maps. Since the recursive occurrence of T in TFun is in a negative position, this action should be contravariant: its type should be TFunM : (T₂ →ₙ T₁) → (TFun T₁ →ₙ TFun T₂). We can build such a function easily, using precomposition (i.e., a function f ↦ - ∘ f). It also is contravariant, so we just need to build a map of type (T₂ →ₙ T₁) → (nat ⇀ T₂) →ₙ (nat ⇀ T₁). But this is just a composition over a finite map. As it happens, it is a library function, fdMap. The only technicality left is making our argument m monotone (fdMap expects a monotone argument), which we do by equipping the source and target types with trivial preorders. Thus, we arrive at the following definition.
  Definition TFunM (m : T2 -n> T1) : TFun T1 -n> TFun T2 :=
    fdMap (disc_m m) ▹.

End TypeFunctorDefs.

After building our definitions, we can start building an input module for the solution. In general, the functors can have both negative and positive recursive occurrences, so the input module type allows for it. In our case, we can just forget the second argument, which denotes the positive occurrence.
There are a few additional properties we need to exhibit now: first, the action of the functor on morphisms has to be a nonexpansive map itself. This is easy to show, since we only used nonexpansive components in our definition. Besides that, we need to show that the definition is functorial, i.e., that it preserves compositions and identities. This is not difficult either, since all of the components of our definitions preserve those. Finally, we need to show that the space that our functor defines is non-empty. We do this by providing a map from the single-element space, 1, into TFun 1. We pick the constant map that disregards the world and returns the empty uniform predicate (note that this map *does* inhabit TFun 1!)
This constitutes the equation that describes our space of semantic types.
Module F <: SimplInput (CBUlt).
  Import CBUlt.
  Open Scope cat_scope.

  Definition F (T1 T2 : cofeType) := cofeFromType (TFun T1).
  Local Obligation Tactic := intros.

  Program Instance FArr : BiFMap F :=
    fun T1 T2 T3 T4 ⇒ n[(TFunM)] <M< Mfst.
  Next Obligation.
    intros m1 m2 Eqm; unfold TFunM; rewrite Eqm; reflexivity.
  Qed.
  Next Obligation.
    intros m1 m2 Eqm x; unfold TFunM; simpl morph; rewrite Eqm; reflexivity.
  Qed.

  Instance FFun : BiFunctor F.
  Proof.
    split; intros; unfold fmorph; simpl morph; unfold TFunM.
    - rewrite disc_m_comp, <- fdMap_comp, <- ucomp_precomp.
      intros x; simpl morph; reflexivity.
    - rewrite disc_m_id, fdMap_id, pid_precomp.
      intros x; simpl morph; reflexivity.
  Qed.

  Program Definition empty_UPC : UPC :=
    exist (up_cr (const False)) _.
  Next Obligation.
    intros k v HR; contradiction HR.
  Qed.

  Definition F_ne : 1 -t> F 1 1 :=
    umconst (pcconst (empty_UPC)).
End F.

Now we are almost set. The final problem is that the solution requires the action of the functor on morphisms to be contractive, while ours is "only" nonexpansive. However, we can use a generic construction that halves all the distances on the metric space, which makes the maps contractive. The end result in the UPred space that we are using corresponds to subtracting one from the step-index.
Module F_In := InputHalve(F).

Finally, we are set to build a solution of our recursive domain equation. We do this by instantiating the Solution functor.
Module Import Fix := Solution(CBUlt)(F_In).

The solution we get consists of a complete metric space, DInfO, which is our space of semantic types, and an isomorphism between DInfO and 1/2 (TFun DInfO), which we can use to go between the two forms when we need to do so.
First, we rename DInfO to HatT. This space will denote the semantic types that we store in the world.
Definition HatT := DInfO.

The semantic types we will be using to interpret our syntax, T, are simply the monotone maps from worlds to UPC. The worlds, in turn, are finite maps from nat to HatT.
Definition T := TFun HatT.
Definition W := nat -f> HatT.

Finally, we get morphisms from HatT to 1/2 T. We will use those whenever we need to check that some values satisfy the predicate that is stored in the world (since it is stored in the folded form).
WARNING: Since ı goes from HatT to 1/2 T, the distance under ı is larger. Thus, we need n+1-equality to rewrite under a ı in an n-equality. This is not visible with the current notation, since the distance function for each space is implicit.
Definition ı : HatT -t> (halve (cofeFromType T)) := Unfold.
Definition ı' : (halve (cofeFromType T)) -t> HatT := Fold.

The final bit of information we get from the Solution functor shows that ı and ı' form an isomorphism.
Lemma iso T : ı' (ı T) == T.
Proof.
  apply (FU_id T).
Qed.

Lemma isoR T : ı (ı' T) == T.
Proof.
  apply (UF_id T).
Qed.

HatT that we received from the solution is a complete metric space. However, our space of types is monotone with respect to the evolution of the worlds — and finite maps take into account the possible evolution of their codomains. To make sure this works, we extend HatT with a trivial preorder.
Instance HatT_preo : preoType HatT := disc_preo HatT.
Instance HatT_pcm : pcofe HatT := disc_pc HatT.
Instance HatT_ext : extensible HatT := disc_ext HatT.

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
    | |- Proper (pord ==> pord) ?R ⇒ intros ?t1 ?t2 EQt
  end; simpl morph; try_rew EQt; reflexivity.

Obligation Tactic := intros; simp_rew || eauto with typeclass_instances.

Interpretation

Worlds and heaps

Now we are ready to start building our interpretations. We begin by building an interpretation of worlds: a relation that states whether a heap matches a given world (at a given step-index). The statement is simple: a heap h matches the world w if for any location k which w maps to a semantic type R, k is in the domain of h, and the value stored at h k matches the type R. Note the use of the isomorphism ı to unfold the type R. We also show that the interpretation of the worlds preserves equality and *expands* the distance by one step. The latter is the effect of using ı to unfold the semantic type. The interpretation is invariant with respect to the order on worlds.
For technical reasons, which we will explore further ahead, we use a discrete preorder for the heaps in this definition (instead of the default extension ordering.)
NOTE: an alternative statement could potentially use lifting the operations to the option type (and saying something to the effect of ∀ k, (n, h k) ∈ ı ((w k) w), but in practice it would probably be less readable.
Program Definition interpW (w : W) : @UPred heap (@disc_preo _ discreteType) :=
  mkUPred (fun n h ⇒ ∀ k R (HLu : w k = Some R),
                      ∃ v, h k = Some v ∧ proj1_sig (ı R w) n v) _.
Next Obligation.
  intros n m h1 h2 Hle Hsub HH k R HLu.
  specialize (HH _ _ HLu); destruct HH as [v [HLuv HRv]].
  simpl in Hsub; subst h2.
  ∃ v; split; [assumption | rewrite Hle; assumption].
Qed.

Instance interpW_equiv : Proper (equiv ==> equiv) interpW.
Proof.
  intros w1 w2 EQw n h; split; intros HH k R HLu.
  - assert (EQR := EQw k); rewrite HLu in EQR.
    destruct (w1 k) as [R' |] eqn: HLu'; [simpl in EQR | contradiction].
    specialize (HH _ _ HLu'); destruct HH as [v [HLuv HRv]].
    eexists; split; [eassumption |].
    eapply (equiv_morph (ı R)); [rewrite <- EQR; reflexivity | symmetry; eassumption |].
    assumption.
  - assert (EQR := EQw k); rewrite HLu in EQR.
    destruct (w2 k) as [R' |] eqn: HLu'; [simpl in EQR | contradiction].
    specialize (HH _ _ HLu'); destruct HH as [v [HLuv HRv]].
    eexists; split; [eassumption |].
    eapply (equiv_morph (ı R)); [rewrite EQR; reflexivity | eassumption |].
    assumption.
Qed.

Instance interpW_dist n : Proper (dist (S n) ==> dist n) interpW.
Proof.
  intros w1 w2 EQw m h HLt; split; intros HH k R HLu.
  - assert (EQR := EQw k); rewrite HLu in EQR.
    destruct (w1 k) as [R' |] eqn: HLu'; [do 3 red in EQR | contradiction].
    specialize (HH _ _ HLu'); destruct HH as [v [HLuv HRv]].
    apply dist_mono in EQw; assert (HT : ı R w2 = n = ı R' w1) by (rewrite EQw, EQR; reflexivity).
    eexists; split; [eassumption | apply HT, HRv; assumption].
  - assert (EQR := EQw k); rewrite HLu in EQR.
    destruct (w2 k) as [R' |] eqn: HLu'; [do 3 red in EQR | contradiction].
    specialize (HH _ _ HLu'); destruct HH as [v [HLuv HRv]].
    apply dist_mono in EQw; assert (HT : ı R' w2 = n = ı R w1) by (rewrite EQw, EQR; reflexivity).
    eexists; split; [eassumption | apply HT, HRv; assumption].
Qed.

Evaluation closure

With the interpretation of worlds ready, we can define the interpretation of computations. As in Fμ, we use the generic definition of evaluation closure, which means we need to provide a reduction relation along with some properties. As the reduction relation we simply pick an uncurried version of the step relation. Now we need to show that it behaves well with the order we choose for the exp × heap type. This, however, is not true with the usual extension ordering for heaps. Thus, we use the discrete order on heaps in the evaluation closure.
The only question that remains is what predicate should be satisfied when the computation terminates. We have several constraints here: we want the final expression to match the semantic type we close over (at some world), and we need the final heap to match the same world. However, since the computation can allocate new locations in the heap, we need to allow the world to evolve according to what the computation did. This means that we need to allow to pick a future world at which both the interpretation of the type and the world will be satisfied. We use a cartesian product construction and a bounded existential quantification (on the UPred level) to make these notions explicit. Finally, we can show that our evaluation closure preserves equality and distance (with the caveat stemming from our interpretation of worlds), and that it is contravariant with respect to the order on the worlds and covariant with respect to the order on types. We also provide a convenient unfolding lemma, and a lemma that simplifies the proofs for values.
Section EvalCL.

  Definition step' (eh1 eh2 : exp × heap) :=
    let (e1, h1) := eh1 in
    let (e2, h2) := eh2 in e1 || h1 ↦ e2 || h2.

  Local Instance eqOH : preoType heap | 0 := @disc_preo heap discreteType.
  Local Open Scope upred_scope.

  Instance irr_proper : Proper (pord --> impl) (irr step').
  Proof.
    intros [e h1] [e' h2] [EQe EQh] HIrr; simpl in *; subst; assumption.
  Qed.

  Lemma extend_step : ext_step step'.
  Proof.
    intros [e h1] [ee h2] [e' h2'] [EQe EQh] HStep; simpl in *; subst.
    eexists (_, _); simpl; eauto.
  Qed.

  Program Definition evalR (w : W) (R : T) : UPred (exp × heap) :=
    evalCl step' extend_step _ (∃ w' ∈ pord w, inclM (R w') × interpW w').

  Global Instance evalR_equiv : Proper (equiv ==> equiv ==> equiv) evalR.
  Proof.
    intros w1 w2 EQw R1 R2 EQR; apply eval_equiv.
    intros n h; split; intros [w' HT]; ∃ w'; [rewrite <- EQw, <- EQR | rewrite EQw, EQR]; assumption.
  Qed.

  Global Instance evalR_dist n : Proper (dist (S n) ==> dist n ==> dist n) evalR.
  Proof.
    intros w1 w2 EQw R1 R2 EQR; apply eval_dist; intros m h HLt; split; intros [w' [HSub [HT Hh]]].
    - eexists; split; [eapply extend_sub; eassumption | assert (HH := extend_dist _ _ _ _ EQw HSub); split].
      + apply (met_morph_nonexp _ _ R1) in HH; apply EQR, HH, HT; auto with arith.
      + eapply interpW_dist, Hh; [symmetry |]; eassumption.
    - symmetry in EQw; eexists; split; [eapply extend_sub; eassumption |].
      assert (HH := extend_dist _ _ _ _ EQw HSub); split.
      + apply (met_morph_nonexp _ _ R1) in HH; apply HH, EQR, HT; auto with arith.
      + eapply interpW_dist, Hh; [symmetry |]; eassumption.
  Qed.

  Global Instance evalR_pord : Proper (pord --> pord ==> pord) evalR.
  Proof.
    intros w1 w2 Subw R1 R2 SubR; apply eval_pord; intros n h [w' [HSub [HT Hh]]].
    unfold flip in Subw; ∃ w'; split; [etransitivity; eassumption |].
    split; [rewrite <- SubR |]; assumption.
  Qed.

  Lemma evalR_simpl R w n e h :
    evalR w R n (e, h) ==
    ((irred e h → ∃ w', w ⊑ w' ∧ inclM (R w') n e ∧ interpW w' n h) ∧
     ∀ e' h' (HS : e || h ↦ e' || h'), (▹ evalR w R)%up n (e', h')).
  Proof.
    unfold evalR at 1; rewrite evalCl_eq; fold (evalR w R).
    split; intros [HIrr HStep].
    - split; intros; [| apply HStep; assumption].
       apply HIrr; intros [e' h'] HS; eapply H; eassumption.
    - split; intros; [| destruct t' as [e' h']; apply HStep; assumption].
      apply HIrr; clear - H; intros e' h' HS; apply (H (e', h')); assumption.
  Qed.
  Global Opaque evalR.

  Lemma eval_val {R : T} {n e h w} (w' : W)
        (HIrr : irred e h)
        (HSub : w ⊑ w')
        (HT : ` (R w') n e)
        (Hh : interpW w' n h) :
    evalR w R n (e, h).
  Proof.
    rewrite evalR_simpl; split; [| intros; exfalso; irred].
    now eauto.
  Qed.

End EvalCL.

Unit type

With the auxiliary definitions behind us, we can begin defining the interpretation of types. We start with the unit, for which we simply pick the constant relation that only contains the unique value of the type.
Inductive unitR : exp → Prop :=
| RUnit : unitR eUnit.
Program Definition unit_rel : UPC := exist (up_cr unitR) _.
Next Obligation.
  intros n e HR; inversion_clear HR; split;
  [isval | construction_closed].
Qed.
Definition rel_unit : T := pcconst unit_rel.

Product type

As usual for products, the interpretation is pointwise: the only expressions that belong to the interpretations are pairs of expressions which themselves are in the appropriate interpretations. The indices are just passed along.
Following the pattern set in Fμ, we show that the definition forms a proper operator on T by checking that it's a uniform predicate that only contains closed values, and that it behaves well with respect to the worlds and the component types.
Inductive prodR : UPC → UPC → nat → exp → Prop :=
| RProd n e1 e2 (R1 R2 : UPC)
        (H1 : ` R1 n e1)
        (H2 : ` R2 n e2) :
    prodR R1 R2 n 〈e1, e2〉.
Program Definition prodR_upc RL RR : UPC := exist (mkUPred (prodR RL RR) _) _.
Next Obligation.
  intros n m t t' HLe HSub HProd; simpl in HSub; subst t'.
  inversion_clear HProd; apply RProd; eapply uni_pred; eassumption || reflexivity.
Qed.
Next Obligation.
  intros n e HP; simpl in *; inversion_clear HP.
  apply (proj2_sig RL) in H1; apply (proj2_sig RR) in H2.
  destruct H1 as [[v1 EQv1] HCv1]; destruct H2 as [[v2 EQv2] HCv2]; subst.
  split; [isval | construction_closed].
Qed.

Instance prodR_equiv : Proper (equiv ==> equiv ==> equiv) prodR_upc.
Proof.
  intros RL1 RL2 EQRL RR1 RR2 EQRR; split; intros HProd; inversion_clear HProd;
  apply RProd; (apply EQRL || apply EQRR); assumption.
Qed.

Instance prodR_dist n : Proper (dist n ==> dist n ==> dist n) prodR_upc.
Proof.
  intros RL1 RL2 EQRL RR1 RR2 EQRR; split; intros HProd; inversion_clear HProd;
  apply RProd; (apply EQRL || apply EQRR); assumption.
Qed.

Instance prodR_mono : Proper (pord ==> pord ==> pord) prodR_upc.
Proof.
  intros RL1 RL2 EQRL RR1 RR2 EQRR n v HProd.
  inversion_clear HProd; apply RProd; [apply EQRL | apply EQRR]; assumption.
Qed.

Program Definition rel_prod (RL RR : T) : T :=
  m[(fun w ⇒ prodR_upc (RL w) (RR w))].

Inductive sumR : UPC → UPC → nat → exp → Prop :=
| RInL (RL RR : UPC) n e
       (HRL : ` RL n e) :
    sumR RL RR n (ıL e)
| RInR (RL RR : UPC) n e
       (HRR : ` RR n e) :
    sumR RL RR n (ıR e).
Program Definition sumR_upc RL RR : UPC := exist (mkUPred (sumR RL RR) _) _.
Next Obligation.
  intros n m t t' HLe HSub HSum; simpl in HSub; subst t'.
  inversion_clear HSum; [apply RInL | apply RInR]; rewrite HLe; assumption.
Qed.
Next Obligation.
  intros n e HH; simpl in *; inversion_clear HH.
  - apply (proj2_sig RL) in HRL; destruct HRL as [[v EQv] HCv]; subst.
    split; [isval | construction_closed].
  - apply (proj2_sig RR) in HRR; destruct HRR as [[v EQv] HCv]; subst.
    split; [isval | construction_closed].
Qed.

Instance sumR_equiv : Proper (equiv ==> equiv ==> equiv) sumR_upc.
Proof.
  intros RL1 RL2 EQRL RR1 RR2 EQRR; split; intros HH;
  (inversion_clear HH; [apply RInL, EQRL | apply RInR, EQRR]); assumption.
Qed.

Instance sumR_dist n : Proper (dist n ==> dist n ==> dist n) sumR_upc.
Proof.
  intros RL1 RL2 EQRL RR1 RR2 EQRR; split; intros HH;
  (inversion_clear HH; [apply RInL, EQRL | apply RInR, EQRR]); assumption.
Qed.

Instance sumR_pord : Proper (pord ==> pord ==> pord) sumR_upc.
Proof.
  intros RL1 RL2 EQRL RR1 RR2 EQRR n h HH;
  (inversion_clear HH; [apply RInL, EQRL | apply RInR, EQRR]); assumption.
Qed.

Program Definition rel_sum (RL RR : T) : T :=
  m[(fun w ⇒ sumR_upc (RL w) (RR w))].

Function type

The interpretation of the arrow type follows the usual approach of the logical relations. There are, however, a couple things of note. First, notice that the functions are recursive: we substitute both the argument and the function itself into the body of the function in the evaluation closure. This forces us to actually consume a step-index when unfolding a function (note HLt argument of the HArg hypothesis uses a strict order). Second, the world might evolve between the function definition and the call site: the substitution should thus work for any future world of w. Third, similarly to using any argument ea in the appropriate semantic type, we also need a heap h — and much like the argument it has to be "good", i.e., match the world w'. Except for those points of interest, the definition is standard.
Having defined the underlying relation, we proceed to make it an operator on T in the usual fashion.
Inductive funR : T → T → W → nat → exp → Prop :=
| RFun w (RA RV : T) e n
       (HC : closed 2 e)
       (HArg : ∀ w' ea h m (HLt : m < n) (HSub : w ⊑ w')
                      (HArg : ` (RA w') m ea) (Hh : interpW w' m h),
                 evalR w' RV m (subst (λ e) 0 (subst ea 0 e), h)) :
    funR RA RV w n (λ e).
Program Definition funR_upc RA RV w : UPC :=
  exist (mkUPred (funR RA RV w) _) _.
Next Obligation.
  intros n m t t' HLe HSub HFun; simpl in HSub; subst t'.
  inversion_clear HFun; apply RFun; [assumption | intros].
  apply HArg; eauto with arith.
Qed.
Next Obligation.
  intros n e HP; inversion_clear HP; clear HArg.
  split; [isval | construction_closed].
Qed.

Instance funR_equiv : Proper (equiv ==> equiv ==> equiv ==> equiv) funR_upc.
Proof.
  intros RA1 RA2 EQRA RV1 RV2 EQRV w1 w2 EQw; split; intros HFun; inversion_clear HFun;
  (apply RFun; [assumption | intros]).
  - rewrite <- EQRV; apply HArg; rewrite ?EQw; try assumption; [].
    apply EQRA, HArg0.
  - rewrite EQRV; apply HArg; rewrite <- ?EQw; try assumption; [].
    apply EQRA, HArg0.
Qed.

Ltac mrewrite EQ := eapply mono_dist in EQ; [rewrite EQ | omega].

Instance funR_dist n : Proper (dist n ==> dist n ==> dist n ==> dist n) funR_upc.
Proof.
  intros RA1 RA2 EQRA RV1 RV2 EQRV w1 w2 EQw m t HLt; split; intros HFun; inversion_clear HFun;
  (apply RFun; [assumption | intros]; destruct n as [| n]; [now inversion HLt |]).
  - symmetry in EQw; assert (EQw' := extend_dist _ _ _ _ EQw HSub).
    assert (HSub2 := extend_sub _ _ _ _ EQw HSub).
    eapply evalR_dist, (HArg (extend w' w1)); eauto with arith; [| |].
    + symmetry; apply dist_mono; assumption.
    + assert (HA : RA2 w' = S n = RA2 (extend w' w1)) by (apply met_morph_nonexp, EQw').
      apply EQRA, HA, HArg0; eauto with arith.
    + eapply interpW_dist, Hh; [symmetry; eassumption | eauto with arith].
  - assert (EQw' := extend_dist _ _ _ _ EQw HSub).
    assert (HSub2 := extend_sub _ _ _ _ EQw HSub).
    eapply evalR_dist, (HArg (extend w' w2)); eauto with arith; [| |].
    + apply dist_mono; assumption.
    + assert (HA : RA2 w' = S n = RA2 (extend w' w2)) by (apply met_morph_nonexp, EQw').
      apply HA, EQRA, HArg0; eauto with arith.
    + eapply interpW_dist, Hh; [symmetry; eassumption | eauto with arith].
Qed.

Instance funR_mono RA RV : Proper (pord ==> pord) (funR_upc RA RV).
Proof.
  intros w1 w2 EQw n v HFun; inversion_clear HFun; apply RFun; [assumption | intros].
  rewrite <- EQw in HSub; eapply HArg; eassumption.
Qed.

Program Definition rel_fun (RA RV : T) : T := m[(funR_upc RA RV)].

Reference types

Finally we arrive at the most interesting part of the interpretation: the reference type. In the previous definitions the worlds were virtually unused; we only used them in the function types to accomodate the relation on computations. Here, however, we have to state what makes a location a proper value of the reference type. The obvious answer would be "when the type it is assigned by the world" matches the interpretation of the reference type. This, however, would be too strong: it is enough to say we cannot tell the (semantic) type on the heap apart from the interpretation of the (syntactic) type of the reference — or, in other words, that they are n-equal in any future world. Note that again the type stored in the world, Rw, has to be coerced by ı to be applied to the world.
Once we build our definition, we proceed in the usual way to show it's an operator on T.
Inductive refR : T → W → nat → exp → Prop :=
| RRef (w : W) (R : T) (Rw : HatT) l n
       (HLup : w l = Some Rw)
       (HEqn : R = n = ı Rw) :
    refR R w n (eLoc l).
Program Definition refR_upc R w : UPC := exist (mkUPred (refR R w) _) _.
Next Obligation.
  intros n m t t' HLe HSub HRef; simpl in HSub; subst t'.
  inversion_clear HRef; eapply RRef; [eassumption | intros].
  eapply mono_dist, HEqn; assumption.
Qed.
Next Obligation.
  intros n e HP; simpl in *; inversion_clear HP.
  split; [isval | construction_closed].
Qed.

Instance refR_equiv : Proper (equiv ==> equiv ==> equiv) refR_upc.
Proof.
  intros R1 R2 EQR w1 w2 EQw; split; intros HRef; inversion_clear HRef.
  - assert (EQRW := EQw l); rewrite HLup in EQRW.
    destruct (w2 l) as [Rw' |] eqn: HLup2; [simpl in EQRW | contradiction].
    eapply RRef; [eassumption | intros].
    rewrite <- EQR, <- EQRW; assumption.
  - assert (EQRW := EQw l); rewrite HLup in EQRW.
    destruct (w1 l) as [Rw' |] eqn: HLup2; [simpl in EQRW | contradiction].
    eapply RRef; [eassumption | intros].
    rewrite EQR, EQRW; assumption.
Qed.

Instance refR_dist n : Proper (dist n ==> dist n ==> dist n) refR_upc.
Proof.
  intros R1 R2 EQR w1 w2 EQw m e HLt; split; intros HRef; inversion_clear HRef;
  (destruct n as [| n]; [now inversion HLt |]).
  - assert (EQRW := EQw l); rewrite HLup in EQRW; destruct (w2 l) as [Rw' |] eqn: HLup2;
    [do 3 red in EQRW | contradiction]; eapply RRef; [eassumption | intros].
    apply (mono_dist _ _ m) in EQR; [| now auto with arith]; rewrite <- EQR, HEqn.
    apply (mono_dist _ _ (S m)) in EQRW; [| now auto with arith].
    apply ı in EQRW; apply EQRW.
  - assert (EQRW := EQw l); rewrite HLup in EQRW; destruct (w1 l) as [Rw' |] eqn: HLup2;
    [do 3 red in EQRW | contradiction]; eapply RRef; [eassumption | intros].
    apply (mono_dist _ _ m) in EQR; [| now auto with arith];
    apply (mono_dist _ _ (S m)) in EQRW; [| now auto with arith].
    rewrite EQR, EQRW; apply HEqn; assumption.
Qed.

Instance refR_mono R : Proper (pord ==> pord) (refR_upc R).
Proof.
  intros w1 w2 HSubw k e HRef; inversion_clear HRef.
  assert (HEq := HSubw l); rewrite HLup in HEq; clear HLup.
  destruct (w2 l) as [Rw' |] eqn: HLup2; [| contradiction]; simpl in HEq.
  apply RRef with Rw'; [assumption | intros].
  rewrite <- HEq; assumption.
Qed.

Program Definition rel_ref (R : T) : T := m[(refR_upc R)].

Tying the Knot: the Interpretation Functions

The definitions above provide all the constructions we need to build the interpretation of types. Now we just need to build a simple fix-point and use the appropriate construction for each type.

Open Scope lr_scope.

Reserved Notation "'V[[' τ ']]'".

Fixpoint interpT (τ : type) : T :=
  match τ with
    | () ⇒ rel_unit
    | σ × τ ⇒ rel_prod V[[ σ ]] V[[ τ ]]
| σ + τ ⇒ rel_sum V[[ σ ]] V[[ τ ]]
| ref τ ⇒ rel_ref V[[ τ ]]
| σ → τ ⇒ rel_fun V[[ σ ]] V[[ τ ]]
end where "'V[[' τ ']]'" := (interpT τ) : lr_scope.

As usual, we need two additional derived forms: the interpretation that is closed under evaluation, and the interpretation of typing contexts. The first one will be simply using the evaluation closure defined before, but starting from any well-typed heap (which also forces us to use the explicit downwards-closure, much the same as in functions). The second is a simple pointwise extension of the interpretation of types.
Definition intE τ w n e :=
  ∀ m h (HLe : m ≤ n) (Hh : interpW w m h), evalR w V[[ τ ]] m (e, h).

Program Definition interpE τ w := mkUPred (intE τ w) _.
Next Obligation.
  intros n1 n2 e e' HLe1 HSub HE m h HLe2 Hh; simpl in HSub; subst e'.
  apply HE, Hh; etransitivity; eassumption.
Qed.

Notation "'E[[' τ ']]'" := (interpE τ) : lr_scope.

Require Import List.

Inductive VCR: env type → W → nat → env exp → Prop :=
| EmptyR k w :
    VCR nil w k nil
| ConsR w k e τ Γ ρ
        (Hhd : ` (V[[ τ ]] w) k e)
        (Htl : VCR Γ w k ρ) :
    VCR (Some τ :: Γ) w k (Some e :: ρ).

We specify a discrete preorder for environments of values, in order to show the interpretation of contexts is uniform.
Instance envval_preo : preoType (env exp) := @disc_preo _ discreteType.

Program Definition interpC Γ w : UPred (env exp) := mkUPred (VCR Γ w) _.
Next Obligation.
  intros n m ρ ρ' Le Sub H; simpl in Sub; subst ρ'; induction H; constructor; [| now auto].
  rewrite Le; assumption.
Qed.

Notation "'C[[' Γ ']]'" := (interpC Γ) : lr_scope.

Interpretation of contexts is also covariant with respect to the order on the worlds.
Instance VCR_mono Gamma : Proper (pord ==> pord) (interpC Gamma).
Proof.
  intros w1 w2 HSubw k ρ HRef; induction HRef; constructor; [|].
  - rewrite <- HSubw; assumption.
  - apply IHHRef; assumption.
Qed.

The Logical Relation

The definition of the logical relation is standard: for any closing substitution that is related to the typing context at some world w and index n, the substituted term is in the interpretation of expressions at the appropriate type for w and n.
Definition log Γ e τ :=
  ∀ ρ (HCL : closed 0 (substEnv ρ 0 e)) w n
         (HC : C[[ Γ ]] w n ρ),
    E[[ τ ]] w n (substEnv ρ 0 e).
Notation " Γ ⊧ e : τ " := (log Γ e τ) (at level 50, e at next level) : lr_scope.

Properties of the interpretations.

As usual, we need some additional properties of the interpretations. In this case, this is relatively simple: we only need to show several facts about the contexts (relating lookup in the typing context to a lookup in the substitution and closedness of the substitution), as well as simple facts about allocation.

Lemma interpC_closed {Γ w k ρ} (Hint: C[[ Γ ]] w k ρ) : closed 0 ρ.
Proof.
  induction Hint; [construction_closed |].
  apply (proj2_sig (V[[τ]] w)) in Hhd; destruct Hhd as [_ HC].
  unfold closed in HC; construction_closed.
Qed.

Lemma interpC_lookup {n w x} {Γ : env type} {τ γ}
      (HFnd : lookup x Γ = Some τ)
      (HRE : C[[ Γ ]] w n γ) :
  ∃ e, lookup x γ = Some e ∧ ` (V[[τ]] w) n e.
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; [| assumption].
    rewrite <- raw_insert_zero, lookup_insert_bingo; reflexivity.
  - rewrite lookup_successor in *; simpl in *; clear dependent e.
    destruct (IHHRE _ HFnd) as [v [HFnd' HR] ]; clear IHHRE HFnd.
    ∃ v; split; assumption.
Qed.

There is always an element outside the domain of a finite map. Useful whenever we need to allocate something in a heap.
Lemma findom_exists_notin (h : heap) :
  ∃ k, ¬ k ∈ dom h.
Proof.
  destruct h as [xs SSxs]; unfold dom; simpl.
  revert SSxs; generalize (map fst xs); clear xs; intros xs SSxs.
  destruct xs as [| x xs]; [∃ O; tauto | ∃ (S (last xs x)) ].
  intros HIn; assert (HT := SS_last_le _ _ _ SSxs HIn); clear SSxs HIn.
  contradiction (le_Sn_n _ HT).
Qed.

Lemma alloc_ext {l h w n} R
      (HFresh : ¬ l ∈ dom h)
      (HInterp : interpW w n h) :
  w ⊑ w [l ↦ R].
Proof.
  intros k; destruct (w k) as [vk |] eqn: HLk; [| exact I].
  rewrite fdUpdate_neq, HLk; [reflexivity |].
  rewrite fdLookup_notin_strong in HFresh; specialize (HInterp _ _ HLk).
  destruct HInterp as [v [HLuv _] ]; congruence.
Qed.

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.
As with Fμ, the proofs proceed by well-founded induction on the step-index, since this way the proof follows closely the definition of the evaluation closure. We also use a simple tactic that unfold the definition of evaluation closure and — in the reducible case — checks how the reduction could occur.

Definition wf_ind_lt := well_founded_induction Wf_nat.lt_wf.

Ltac eval_simpl :=
  match goal with
    | |- pred (evalR ?w ?R) ?n (?e, ?h) ⇒
      is_var n;
      let HIrr := fresh "HIrr" in
      let HS := fresh "HS" in
      rewrite evalR_simpl; split; [intros HIrr
      | intros ? ? HS; destruct n as [| n]; [exact I |]; inversion HS; subst; clear HS]
  end.

Open Scope upred_scope.

Variables


Lemma compat_var Γ x τ (HLu : lookup x Γ = Some τ) : Γ ⊧ #x : τ.
Proof.
  intros γ HCl w n HC.
  destruct (interpC_lookup HLu HC) as [e [HLuv HInt] ].
  assert (HCγ := interpC_closed HC).
  change x with (0 + x)%nat; erewrite substEnv_lookup; try (apply _ || eassumption); [].
  destruct (proj2_sig (V[[τ]] w) _ _ HInt) as [[v EQv] _]; subst e.
  intros k h HLe Hh.
  apply eval_val with w; [irred | reflexivity | | assumption].
  rewrite HLe; apply HInt.
Qed.

Unit


Lemma compat_unit Γ : Γ ⊧ eUnit : ().
Proof.
  intros γ _ w n HC m h HLe Hh; simpl_subst_goal.
  apply eval_val with w; [irred | reflexivity | apply RUnit | assumption].
Qed.

Products


Lemma compat_pair_aux n w e1 e2 h τ1 τ2
      (HVal : irred e1 h →
              ∃ w', w ⊑ w' ∧ ` (V[[τ1]] w') n e1 ∧ evalR w' V[[τ2]] n (e2, h))
      (HRed : ∀ e1' h' (HS : e1 || h ↦ e1' || h'),
                (▹ evalR w V[[τ1]]) n (e1', h') ∧
                ∀ w' (HSub : w ⊑ w'), E[[τ2]] w' n e2) :
  evalR w V[[τ1 × τ2]] n (〈e1, e2〉, h).
Proof.
  revert e1 e2 h HVal HRed; induction n using wf_ind_lt; rename H into HInd; intros.
  eval_simpl.
  - clear HInd HRed; edestruct HVal as [w' [HSub [HV1 HE2] ] ]; [irred | clear HVal].
    destruct (proj2_sig (V[[τ1]] w') _ _ HV1) as [[v1 EQ] _]; subst.
    rewrite evalR_simpl in HE2; apply proj1 in HE2.
    edestruct HE2 as [w'' [HSub' [HV2 Hh] ] ]; [irred | clear HE2].
    ∃ w''; split; [etransitivity; eassumption | split; [| assumption] ].
    rewrite HSub' in HV1; simpl; split; assumption.
  - clear HVal; specialize (HRed _ _ HS0); destruct HRed as [HLL HLR]; simpl in HLL.
    apply HInd; [now auto with arith | intros HIrr | intros]; clear HInd.
    + rewrite evalR_simpl in HLL; apply proj1 in HLL; specialize (HLL HIrr).
      destruct HLL as [w' [HSub [HV1 Hh] ] ]; ∃ w'.
      do 2 (split; [assumption |]).
      specialize (HLR _ HSub); rewrite <- Le.le_n_Sn in HLR; now apply HLR.
    + split; [| setoid_rewrite Le.le_n_Sn; assumption].
      rewrite evalR_simpl in HLL; apply HLL; assumption.
  - apply HInd; [now auto with arith | intros HIrred; clear HInd | intros; irred].
    edestruct HVal as [w' [HSub [HV1 HE2] ] ]; [irred | clear HVal HRed].
    rewrite <- Le.le_n_Sn in HV1; ∃ w'; do 2 (split; [assumption |]).
    rewrite evalR_simpl in HE2; apply HE2; assumption.
Qed.

Lemma compat_pair Γ e1 e2 τ1 τ2 (HL1 : Γ ⊧ e1 : τ1) (HL2 : Γ ⊧ e2 : τ2) :
  Γ ⊧ 〈e1, e2〉 : τ1 × τ2.
Proof.
  intros γ HCl w n HC m h HLe Hh; simpl_subst_all; inversion_closed_in HCl.
  specialize (HL1 _ H0 _ _ HC _ _ HLe Hh); specialize (HL2 _ H); clear Hh.
  revert HL1; generalize (substEnv γ 0 e1); clear e1 H0; intros e1 HL1.
  revert HL2; generalize (substEnv γ 0 e2); clear e2 H; intros e2 HL2.
  apply compat_pair_aux; [intros HIrr | intros].
  - rewrite evalR_simpl in HL1; apply proj1 in HL1; specialize (HL1 HIrr).
    destruct HL1 as [w' [HSub [HV1 Hh] ] ]; ∃ w'; rewrite HSub in HC.
    do 2 (split; [assumption |]); eapply HL2; eassumption.
  - split; [| intros; apply HL2; rewrite HLe, <- HSub; assumption].
    rewrite evalR_simpl in HL1; apply HL1, HS.
Qed.

Lemma compat_proj1 Γ e τ1 τ2 (HL : Γ ⊧ e : τ1 × τ2) : Γ ⊧ π1 e : τ1.
Proof.
  intros γ HCl w n HC; simpl_subst_all; inversion_closed_in HCl; intros m h HLe Hh.
  specialize (HL _ H _ _ HC _ _ HLe Hh); clear n HLe Hh H HC.
  revert h HL; generalize (substEnv γ 0 e); clear e.
  induction m using wf_ind_lt; intros; rename H into HInd; eval_simpl.
  - exfalso; rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HRL Hh] ] ]; [irred | clear HL].
    simpl in HRL; inversion HRL; subst; clear HRL.
    destruct (proj2_sig (V[[τ1]] w') _ _ H1) as [[v1 EQ1] _];
      destruct (proj2_sig (V[[τ2]] w') _ _ H2) as [[v2 EQ2] _]; subst; irred.
  - rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HRL Hh] ] ]; [irred | clear HL; inversion_clear HRL].
    rewrite <- Le.le_n_Sn in *; apply eval_val with w'; [irred |..]; assumption.
  - apply HInd, HL, HS0; now auto with arith.
Qed.

Lemma compat_proj2 Γ e τ1 τ2 (HL : Γ ⊧ e : τ1 × τ2) : Γ ⊧ π2 e : τ2.
Proof.
  intros γ HCl w n HC; simpl_subst_all; inversion_closed_in HCl; intros m h HLe Hh.
  specialize (HL _ H _ _ HC _ _ HLe Hh); clear n HLe Hh H HC.
  revert h HL; generalize (substEnv γ 0 e); clear e.
  induction m using wf_ind_lt; intros; rename H into HInd; eval_simpl.
  - exfalso; rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HRL Hh] ] ]; [irred | clear HL].
    simpl in HRL; inversion HRL; subst; clear HRL.
    destruct (proj2_sig (V[[τ1]] w') _ _ H1) as [[v1 EQ1] _];
      destruct (proj2_sig (V[[τ2]] w') _ _ H2) as [[v2 EQ2] _]; subst; irred.
  - rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HRL Hh] ] ]; [irred | clear HL]; inversion_clear HRL.
    rewrite <- Le.le_n_Sn in *; apply eval_val with w'; [irred |..]; assumption.
  - apply HInd, HL, HS0; now auto with arith.
Qed.

Sums


Lemma compat_inl Γ e τ1 τ2 (HL : Γ ⊧ e : τ1) : Γ ⊧ ıL e : (τ1 + τ2).
Proof.
  intros γ HCl w n HC m h HLe Hh; simpl_subst_all; inversion_closed_in HCl.
  specialize (HL _ H _ _ HC _ _ HLe Hh); clear n HLe H Hh HC.
  revert h HL; generalize (substEnv γ 0 e); clear e.
  induction m using wf_ind_lt; rename H into HInd; intros; eval_simpl.
  - rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HR Hh] ] ]; [irred | clear HL HIrr].
    ∃ w'; repeat split; [assumption | simpl; left; assumption | assumption].
  - apply HInd, HL, HS0; now auto with arith.
Qed.

Lemma compat_inr Γ e τ1 τ2 (HL : Γ ⊧ e : τ2) : Γ ⊧ ıR e : (τ1 + τ2).
Proof.
  intros γ HCl w n HC m h HLe Hh; simpl_subst_all; inversion_closed_in HCl.
  specialize (HL _ H _ _ HC _ _ HLe Hh); clear n HLe H Hh HC.
  revert h HL; generalize (substEnv γ 0 e); clear e.
  induction m using wf_ind_lt; rename H into HInd; intros; eval_simpl.
  - rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HR Hh] ] ]; [irred | clear HL HIrr].
    ∃ w'; repeat split; [assumption | simpl; right; assumption | assumption].
  - apply HInd, HL, HS0; now auto with arith.
Qed.

Lemma compat_case Γ e eL eR τ1 τ2 τ
      (HL : Γ ⊧ e : (τ1 + τ2))
      (HLL : insert 0 τ1 Γ ⊧ eL : τ)
      (HLR : insert 0 τ2 Γ ⊧ eR : τ) :
  Γ ⊧ eCase e eL eR : τ.
Proof.
  intros γ HCl w n HC m h HLe Hh; simpl_subst_all; inversion_closed_in HCl.
  rename H into HCR; rename H0 into HCL; specialize (HL _ H1 _ _ HC _ _ HLe Hh); clear H1 Hh.
  apply fold_closed in HCL; apply fold_closed in HCR; rewrite (interpC_closed HC) in ×.
  rewrite <- HLe in HC; revert h HL; generalize (substEnv γ 0 e); clear e n HLe.
  induction m using wf_ind_lt; rename H into HInd; intros; eval_simpl.
  - exfalso; rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [_ [HR _] ] ]; [irred | clear HL].
    simpl in HR; inversion HR; subst; clear HR.
    + destruct (proj2_sig (V[[τ1]] w') _ _ HRL) as [[v EQ] _]; subst; irred.
    + destruct (proj2_sig (V[[τ2]] w') _ _ HRR) as [[v EQ] _]; subst; irred.
  - simpl; clear HInd HLR HCR; rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HR Hh] ] ]; [irred | clear HL; inversion_clear HR].
    rewrite HSub, Le.le_n_Sn; eapply (HLL (Some (v : exp) :: γ)); [| | reflexivity | assumption].
    + unfold closed; simpl; rewrite lift_subst_2 by auto with arith; simpl.
      destruct (proj2_sig (V[[τ1]] w') _ _ HRL) as [_ HCv]; unfold closed in HCv.
      congruence.
    + rewrite HSub in HC; rewrite raw_insert_zero; constructor; assumption.
  - simpl; clear HInd HLL HCL; rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HR Hh] ] ]; [irred | inversion_clear HR; clear HL].
    rewrite HSub, Le.le_n_Sn; eapply (HLR (Some (v : exp) :: γ)); [| | reflexivity | assumption].
    + unfold closed; simpl; rewrite lift_subst_2 by auto with arith; simpl.
      destruct (proj2_sig (V[[τ2]] w') _ _ HRR) as [_ HCv].
      congruence.
    + rewrite HSub in HC; rewrite raw_insert_zero; constructor; assumption.
  - apply HInd, HL, HS0; [now auto with arith |].
    rewrite Le.le_n_Sn; assumption.
Qed.

References


Lemma compat_ref Γ e τ (HL : Γ ⊧ e : τ) : Γ ⊧ new e : ref τ.
Proof.
  intros γ HCl w n HC m h HLe Hh; simpl_subst_all; inversion_closed_in HCl.
  specialize (HL _ H _ _ HC _ _ HLe Hh); clear n H HC HLe Hh.
  revert h HL; generalize (substEnv γ 0 e); clear e.
  induction m using wf_ind_lt; intros; rename H into HInd; eval_simpl.
  - exfalso; rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [_ [HT _] ] ]; [irred | clear HL].
    simpl in HT; destruct (proj2_sig (V[[τ]] w') _ _ HT) as [[v EQ] _]; subst.
    destruct (findom_exists_notin h) as [l HNIn]; irred.
  - simpl; clear HInd; rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HT Hh] ] ]; [irred | clear HL].
    assert (HSub' := alloc_ext (ı' V[[τ]]) HFresh Hh).
    apply eval_val with (w' [l ↦ ı' V[[τ]]]); [irred | etransitivity; eassumption | ..].
    + eapply RRef; [apply fdUpdate_eq |].
      rewrite isoR; reflexivity.
    + intros k R HLu; destruct (Peano_dec.eq_nat_dec l k) as [EQ | NEq]; subst.
      × rewrite fdUpdate_eq in HLu; inversion_clear HLu.
        ∃ v; split; [apply fdUpdate_eq |].
        apply isoR; rewrite <- HSub', Le.le_n_Sn; assumption.
      × rewrite fdUpdate_neq in HLu by assumption; rewrite fdUpdate_neq by assumption.
        specialize (Hh _ _ HLu); destruct Hh as [v' Hh].
        ∃ v'; rewrite (Le.le_n_Sn m), <- HSub'; assumption.
  - apply HInd, HL, HS0; now auto with arith.
Qed.

Lemma compat_deref Γ e τ (HL : Γ ⊧ e : ref τ) : Γ ⊧ ! e : τ.
Proof.
  intros γ HCl w n HC m h HLe Hh; simpl_subst_all; inversion_closed_in HCl.
  specialize (HL _ H _ _ HC _ _ HLe Hh); clear n H HC HLe Hh.
  revert h HL; generalize (substEnv γ 0 e); clear e.
  induction m using wf_ind_lt; rename H into HInd; intros; eval_simpl.
  - exfalso; rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [_ [HT Hh] ] ]; [irred | clear HL].
    simpl in HT; inversion HT; subst; clear HT.
    specialize (Hh _ _ HLup); destruct Hh as [v [HLu _] ]; irred.
  - clear HInd; rewrite evalR_simpl in HL; apply proj1 in HL.
    edestruct HL as [w' [HSub [HT Hh] ] ]; [irred | inversion_clear HT; clear HL].
    rewrite <- Le.le_n_Sn in Hh; apply eval_val with w'; [irred | assumption | | assumption].
    apply HEqn; [now auto with arith |].
    specialize (Hh _ _ HLup); destruct Hh as [v' [HLup' HT] ].
    rewrite HLookup in HLup'; inversion_clear HLup'; assumption.
  - apply HInd, HL, HS0; now auto with arith.
Qed.

Lemma compat_assign_aux w n e1 e2 h τ
      (HVal : irred e1 h →
              ∃ w', w ⊑ w' ∧ ` (V[[ref τ]] w') n e1 ∧ evalR w' V[[τ]] n (e2, h))
      (HRed : ∀ e1' h' (HS : e1 || h ↦ e1' || h'),
                (▹ evalR w V[[ref τ]]) n (e1', h') ∧
                ∀ w' (HSub : w ⊑ w'), E[[τ]] w' n e2) :
  evalR w V[[ () ]] n (e1 ::= e2, h).
Proof.
  revert e1 e2 h HVal HRed; induction n using wf_ind_lt; rename H into HInd; intros.
  eval_simpl.
  - exfalso; edestruct HVal as [w' [_ [HV1 HE2] ] ]; [irred | clear HVal HInd HRed].
    simpl in HV1; inversion HV1; subst; clear HV1 HEqn.
    rewrite evalR_simpl in HE2; apply proj1 in HE2; change (eLoc l) with (vLoc l : exp) in HIrr.
    edestruct HE2 as [w'' [HSub [HV Hh] ] ]; [irred | clear HE2; simpl in HIrr].
    destruct (proj2_sig (V[[τ]] w'') _ _ HV) as [[v EQ] _]; subst.
    specialize (HSub l); rewrite HLup in HSub; destruct (w'' l) as [Rw' |] eqn: HLup'; [| contradiction].
    specialize (Hh _ _ HLup'); destruct Hh as [v' [HLuv' _] ].
    assert (HDom : l ∈ dom h) by (rewrite fdLookup_in_strong; eexists; eassumption).
    irred.
  - clear - HVal; edestruct HVal as [w' [HSub [HVL HE] ] ]; [irred | clear HVal].
    rewrite evalR_simpl in HE; apply proj1 in HE.
    edestruct HE as [w'' [HSub' [HVV Hh] ] ]; [irred | clear HE].
    apply eval_val with w''; [irred | etransitivity; eassumption | now apply RUnit |].
    intros k R HLup; destruct (Peano_dec.eq_nat_dec l k) as [EQ | NEQ]; subst.
    + eexists; split; [apply fdUpdate_eq |].
      simpl in HVL; inversion_clear HVL.
      specialize (HSub' k); rewrite HLup, HLup0 in HSub'.
      simpl in HSub'; rewrite HSub' in HEqn.
      apply HEqn; [now auto with arith |].
      rewrite Le.le_n_Sn; assumption.
    + rewrite fdUpdate_neq by assumption; specialize (Hh _ _ HLup); clear - Hh.
      setoid_rewrite (Le.le_n_Sn n); assumption.
  - simpl in HRed; destruct (HRed _ _ HS0) as [HE1 HL2]; clear HVal HRed.
    apply HInd; [now auto with arith | intros HIrr | intros]; clear HInd.
    + rewrite evalR_simpl in HE1; apply proj1 in HE1; specialize (HE1 HIrr).
      destruct HE1 as [w' [HSub [HV1 Hh] ] ]; ∃ w'.
      do 2 (split; [assumption |]).
      apply HL2; [| now auto with arith |]; assumption.
    + split; [| setoid_rewrite (Le.le_n_Sn n); assumption].
      rewrite evalR_simpl in HE1; apply HE1, HS.
  - apply HInd; [now auto with arith | intros HIrr | intros; irred].
    edestruct HVal as [w' [HSub [HVL HE] ] ]; [irred | clear HVal HIrr HRed HInd].
    rewrite <- Le.le_n_Sn in HVL; ∃ w'.
    do 2 (split; [assumption |]); apply HE, HS0.
Qed.

Lemma compat_assign Γ e1 e2 τ (HL1 : Γ ⊧ e1 : ref τ) (HL2 : Γ ⊧ e2 : τ) :
  Γ ⊧ e1 ::= e2 : ().
Proof.
  intros γ HCl w n HC m h HLe Hh; simpl_subst_all; inversion_closed_in HCl.
  specialize (HL1 _ H0 _ _ HC _ _ HLe Hh); revert HL1; generalize (substEnv γ 0 e1); clear e1 H0 Hh; intros e1 HL1.
  specialize (HL2 _ H); revert HL2; generalize (substEnv γ 0 e2); clear e2 H; intros e2 HL2.
  apply compat_assign_aux with τ; [intros HIrr | intros].
  - rewrite evalR_simpl in HL1; apply proj1 in HL1; specialize (HL1 HIrr).
    destruct HL1 as [w' [HSub [HRT Hh] ] ]; ∃ w'.
    rewrite HSub in HC; do 2 (split; [assumption |]); eapply HL2; eassumption.
  - split; [| intros; apply HL2; rewrite <- HSub, HLe; assumption].
    rewrite evalR_simpl in HL1; apply HL1, HS.
Qed.

Arrows

Lemma compat_fun Γ e τ1 τ2 (HL : insert O τ1 (insert O (τ1 → τ2) Γ) ⊧ e : τ2) :
  Γ ⊧ λ e : (τ1 → τ2).
Proof.
  intros γ HCl w n HC m h HLe Hh; simpl_subst_all; inversion_closed_in HCl.
  change 2 with (1 + 1)%nat in *; rename H into HCl.
  rewrite <- lift_lift_fuse with (k := 0) in × by auto with arith.
  rewrite <- !lift_lift_fuse with (k := 0) in HCl by auto with arith.
  rewrite !(interpC_closed HC) in *; simpl plus in *; apply fold_closed in HCl.
  apply eval_val with w; [irred | reflexivity | | assumption].
  rewrite <- HLe in HC; clear n Hh HLe.
  revert w HC; induction m using wf_ind_lt; rename H into HInd; intros.
  simpl; apply RFun; [construction_closed | intros].
  destruct (proj2_sig (V[[τ1]] w') _ _ HArg) as [[va EQv] HCva]; subst.
  rewrite subst_subst, (closed_subst_invariant _ _ HCva) by auto.
  simpl_lift_goal; rewrite HCl.
  specialize (HL (Some (va : exp) :: Some (λ (substEnv γ 2 e)) :: γ)); simpl_subst_in HL.
  eapply HL; [| | reflexivity | assumption]; clear HL; simpl.
  - unfold closed; clear -HCl HCva; rewrite !lift_subst_2, HCva by auto; simpl; rewrite HCl.
    simpl_lift_goal; erewrite closed_lift_invariant; [reflexivity | eassumption | now auto with arith].
  - rewrite !raw_insert_zero; apply ConsR; [assumption |].
    rewrite <- (Lt.lt_le_weak _ _ HLt), HSub in HC.
    apply ConsR; [simpl; apply HInd |]; assumption.
Qed.

Lemma compat_app_aux w n e1 e2 h τ σ
      (HVal : irred e1 h →
              ∃ w', w ⊑ w' ∧ ` (V[[σ → τ]] w') n e1 ∧ evalR w' V[[σ]] n (e2, h))
      (HRed : ∀ e1' h' (HS : e1 || h ↦ e1' || h'),
                (▹ evalR w V[[σ → τ]]) n (e1', h') ∧
                ∀ w' (HSub : w ⊑ w'), E[[σ]] w' n e2) :
  evalR w V[[τ]] n (e1 @ e2, h).
Proof.
  revert e1 e2 h HVal HRed; induction n using wf_ind_lt; intros; rename H into HInd.
  eval_simpl.
  - exfalso; edestruct HVal as [w' [HSub [HVF HEA] ] ]; [irred | clear HVal HRed HInd].
    simpl in HVF; inversion HVF; subst; clear HVF HArg HC.
    rewrite evalR_simpl in HEA; apply proj1 in HEA; change (λ e) with (vFun e : exp) in HIrr.
    edestruct HEA as [w'' [_ [HVA _] ] ]; [irred | clear HEA].
    destruct (proj2_sig (V[[σ]] w'') _ _ HVA) as [[v EQ] _]; subst; irred.
  - edestruct HVal as [w' [HSub [HVF HEA] ] ]; [irred | clear HInd HVal HRed].
    rewrite evalR_simpl in HEA; apply proj1 in HEA.
    edestruct HEA as [w'' [HSub' [HVA Hh] ] ]; [irred | clear HEA].
    inversion_clear HVF.
    rewrite <- Le.le_n_Sn in HVA, Hh; simpl; rewrite HSub, HSub'.
    eapply HArg; assumption || auto with arith.
  - destruct (HRed _ _ HS0) as [HEF HLA]; clear HVal HRed.
    apply HInd; [now auto with arith | intros HIrr | intros]; clear HInd.
    + simpl in HEF; rewrite evalR_simpl in HEF; apply proj1 in HEF.
      destruct (HEF HIrr) as [w' [HSub [HVF Hh] ] ]; clear HEF HIrr.
      ∃ w'; do 2 (split; [assumption |]); apply HLA; assumption || auto with arith.
    + intros; split; [| setoid_rewrite Le.le_n_Sn; assumption].
      simpl in HEF; rewrite evalR_simpl in HEF; apply HEF, HS.
  - edestruct HVal as [w' [HSub [HVF HEA] ] ]; [irred | clear HRed HVal].
    apply HInd; [now auto with arith | intros _ | intros; irred].
    rewrite <- Le.le_n_Sn in HVF; ∃ w'.
    do 2 (split; [assumption |]); apply HEA, HS0.
Qed.

Lemma compat_app Γ e1 e2 σ τ (HL1 : Γ ⊧ e1 : (σ → τ)) (HL2 : Γ ⊧ e2 : σ) :
  Γ ⊧ e1 @ e2 : τ.
Proof.
  intros γ HCl w n HC m h HLe Hh; simpl_subst_all; inversion_closed_in HCl.
  specialize (HL1 _ H0 _ _ HC _ _ HLe Hh); specialize (HL2 _ H); rewrite <- HLe in HC.
  revert HL1; generalize (substEnv γ 0 e1); clear e1 H0; intros e1 HL1.
  revert HL2; generalize (substEnv γ 0 e2); clear e2 H; intros e2 HL2; clear n HLe Hh.
  apply compat_app_aux with σ; [intros HIrr | intros].
  - rewrite evalR_simpl in HL1; apply proj1 in HL1; specialize (HL1 HIrr).
    destruct HL1 as [w' [HSub [HVF Hh] ] ]; rewrite HSub in HC; ∃ w'.
    do 2 (split; [assumption |]); eapply HL2; eassumption || reflexivity.
  - split; [| intros; apply HL2; rewrite <- HSub; assumption].
    rewrite evalR_simpl in HL1; apply HL1, HS.
Qed.

Hint Resolve compat_var compat_unit compat_pair compat_proj1 compat_proj2
     compat_case compat_inl compat_inr compat_fun compat_app
     compat_ref compat_deref compat_assign : compat.

Theorem fundamental : ∀ Γ e τ, [Γ ⊢ e : τ] → Γ ⊧ e : τ.
Proof.
  intros Γ e τ HTyp; induction HTyp; eauto with compat.
Qed.

Lemma heap_empty n : interpW fdEmpty n fdEmpty.
Proof.
  intros k R HLu; discriminate.
Qed.

Theorem safety : ∀ e τ n e' h'
                       (HT : [nil ⊢ e : τ])
                       (Hc : closed 0 e)
                       (Hredn : step_n n e fdEmpty e' h')
                       (Hirred : irred e' h'),
                  ∃ (v : val), e' = v.
Proof.
  intros; apply fundamental in HT; unfold log in HT.
  specialize (HT nil Hc fdEmpty n (EmptyR _ _)); simpl in HT; clear Hc.
  specialize (HT _ _ (le_n _) (heap_empty _)); revert HT; induction Hredn; intros.
  - rewrite evalR_simpl in HT; apply proj1 in HT; specialize (HT Hirred).
    destruct HT as [w' [_ [HV _] ] ]; apply (proj2_sig (V[[τ]] w') _ _ HV).
  - apply IHHredn, HT, HStep; assumption.
Qed.