Type Safety in 10 Easy, 4 Medium, and 1 Hard Lemma using Step-indexed Logical Relations

```
{-# OPTIONS --rewriting #-}
module rewriting.examples.BlogTypeSafety10Easy4Med1Hard where

open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat
open import Data.Nat.Properties using (≤-refl)
open import Data.List using (List; []; _∷_)
open import Data.Product using (_,_;_×_; proj₁; proj₂; Σ-syntax; ∃-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit using (⊤; tt)
open import Data.Unit.Polymorphic renaming (⊤ to topᵖ; tt to ttᵖ)
open import Relation.Binary.PropositionalEquality as Eq
  using (_≡_; _≢_; refl; sym; cong; subst; trans)
open import Relation.Nullary using (¬_; yes; no)
```

Ok, so logical relations are overkill for proving type safety. The
proof technique is better suited to proving more interesting
properties such as parametricity, program equivalence, and the gradual
guarantee.  Nevertheless, understanding a proof of type safety via
logical relations is a helpful stepping stone to understanding these
more complex use cases, especially when the logical relations employ
more advanced techniques, such as step indexing.  In this blog post I
prove type safety of a cast calculus (an intermediate language of the
gradually typed lambda calculus).  The proof is in Agda and the proof
uses step-indexed logical relations because the presence of the
unknown type (aka. dynamic type) prevents the use of logical relations
that are only indexed by types. To reduce the clutter of reasoning
about step indexing, we conduct the proof using a temporal logic, in
the spirit of the LSLR logic of Dreyer, Ahmed, and Birkedal (LMCS 2011),
that we embed in Agda.

This is a literate Agda file, so most of the details are here, but it
imports several items whose root on github is here:

    https://github.com/jsiek/abstract-binding-trees/tree/master/src

This post is based on work with Philip Wadler and Peter Thiemann.

## Review of the Cast Calculus

```
open import Var
open import rewriting.examples.Cast
```

We review the syntax and reduction rules of this cast calculus.  Just
like the lambda calculus, types include base types (Booleans and
natural numbers), and function types. To support gradual typing, we
include the unknown type ★.

    ι ::= 𝔹 | ℕ
    A,B,C,G,H ::= ι | A ⇒ B | ★

The ground types are 

    G,H ::= ι | ★⇒★

Just like the lambda calculus, there are variables (de Bruijn
indices), lambdas, and application. We throw in literals
(Booleans and natural numbers).  Also, to support gradual typing, we
include a term `M ⟨ G !⟩` for injecting from a ground type `G` to the
unknown type, and a term `M ⟨ H ?⟩` for projecting from the unknown
type back out to a ground type.  Finally, we include the `blame` term
to represent trapped runtime errors.

    L,M,N ::= ` x | ƛ N | L · M | $ k | M ⟨ G !⟩ | M ⟨ H ?⟩ | blame

This cast calculus is somewhat unusual in that it only includes
injections and projections but not the other kinds of casts that one
typically has in a cast calculus, such as a cast from one function type
`★ ⇒ ℕ` to another function type `ℕ ⇒ ℕ`. That is OK because those
other casts can still be expressed in this cast calculus.

The values include lambdas, literals, and injected values.

    V,W ::= ƛ N | $ c | V ⟨ G !⟩

The reduction rules make use of frames, which are defined as follows.

    F ::= □· M | V ·□ | □⟨ G !⟩ | □⟨ H ?⟩

The operation `F ⟦ M ⟧` plugs a term into a frame.

The reduction rules of the cast calculus are as follows:

    (ξ)        If M —→ N, then F ⟦ M ⟧ —→ F ⟦ N ⟧
    (ξ-blame)  F ⟦ blame ⟧ —→ blame
    (β)        (ƛ N) · W —→ N [ W ]
    (collapse) V ⟨ G !⟩ ⟨ G ?⟩ —→ V
    (collide)  If G ≢ H, then V ⟨ G !⟩ ⟨ H ?⟩ —→ blame.


## A First Attempt at a Logical Relation for Type Safety

The following is a first attempt to define a logical relation for type
safety for the cast calculus. The predicate ℰ expresses the semantic
notion of a term being well typed at a given type A. Here "semantic"
means "runtime behavior". We define that a term M is semantically well
typed at type A if it satisfies "progress" and "preservation". The
progress part says that M is either (1) a semantic value at type `A`,
(2) reducible, or (3) an error. The preservation part says that if M
reduces to N, then N is also semantically well typed at A.

    ℰ⟦_⟧ : (A : Type) → Term → Set
    ℰ⟦ A ⟧ M = (𝒱 ⟦ A ⟧ M ⊎ reducible M ⊎ Blame M)
                × (∀ N → (M —→ N) → ℰ⟦ A ⟧ N)

The predicate 𝒱 expresses the semantic notion of a value being well
typed at some type A. For a base type `ι` (𝔹 or ℕ), the value must be
the appropriate kind of literal (Boolean or natural number). For a
function type `A ⇒ B`, the value must be a lambda expression `ƛ N`,
and furthermore, substituting any value `W` that is semantically well
typed at `A` into the body `N` produces a term that is semantically
well typed at `B`. For the unknown type `★`, the value must be
an injection of a value `V` from some ground type `G`, and `V`
must be semantically well typed at `G`.

    𝒱⟦_⟧ : (A : Type) → Term → Set
    𝒱⟦ ι ⟧ ($ c) = ι ≡ typeof c
    𝒱⟦ A ⇒ B ⟧ (ƛ N) = ∀ W → 𝒱⟦ A ⟧ W → ℰ⟦ B ⟧ (N [ W ])
    𝒱⟦ ★ ⟧ (V ⟨ G !⟩) = Value V × 𝒱⟦ gnd⇒ty G ⟧ V
    𝒱⟦ _ ⟧ _ = ⊥

Note that the definitions of ℰ and 𝒱 are recursive. Unfortunately they
are not proper definitions of (total) functions because there is no
guarantee of their termination. For simple languages, like the Simply
Typed Lambda Calculus, 𝒱 can be defined by recursion on the type
`A`. However, here we have the unknown type `★` and the recursion in that
clause invokes `𝒱⟦ gnd⇒ty G ⟧ V`, but `gnd⇒ty G` is
not a structural part of `★` (nothing is).
(The definition of ℰ above is also problematic, but one could
reformulate ℰ to remove the recursion in ℰ.)

## An Explicitly Step-indexed Logical Relation for Type Safety

We can force the definitions of ℰ and 𝒱 to terminate using
step-indexing (aka. the "gasoline" technique), which was first applied
to logical relations by Appel and McAllester (TOPLAS 2001). We add a
parameter k (a natural number) to ℰ and 𝒱, and decrement k on each
recursive call. When k is zero, ℰ and 𝒱 accept all terms. Thus, the
meaning of `ℰ⟦ A ⟧ M k` is that term `M` is guaranteed to behave
according to type `A` for `k` reduction steps, but after that there
are no guarantees.

    ℰ⟦_⟧ : (A : Type) → Term → ℕ → Set
    ℰ⟦ A ⟧ M 0 = ⊤
    ℰ⟦ A ⟧ M (suc k) = (𝒱 ⟦ A ⟧ M k ⊎ reducible M ⊎ Blame M)
                        × (∀ N → (M —→ N) → ℰ⟦ A ⟧ N k)

    𝒱⟦_⟧ : (A : Type) → Term → ℕ → Set
    𝒱⟦ A ⟧ M 0 = ⊤
    𝒱⟦ ι ⟧ ($ ι′ c) (suc k) = ι ≡ ι′
    𝒱⟦ A ⇒ B ⟧ (ƛ N) (suc k) = ∀ W → 𝒱⟦ A ⟧ W k → ℰ⟦ B ⟧ (N [ W ]) k
    𝒱⟦ ★ ⟧ (V ⟨ G !⟩) (suc k) = Value V × 𝒱⟦ gnd⇒ty G ⟧ V k
    𝒱⟦ _ ⟧ _ (suc k) = ⊥

We now have proper definitions of ℰ and 𝒱 but proving theorems about
these definitions involves a fair bit of reasoning about the step
indices, which is tedious, especially in Agda because it's support for
automating proofs about arithmetic is cumbersome to use.  To
streamline the definitions and proofs that involve step indexing,
Dreyer, Ahmed, and Birkedal (2011) propose the use of a temporal logic
that hides the step indexing. Next we discuss the embedding of such a
logic in Agda.


## Step-indexed Logic

```
open import rewriting.examples.StepIndexedLogic2
```

Our Step-indexed Logic (SIL) includes first-order logic (i.e., a logic
with "and", "or", "implies", "for all", etc.). To distinguish its
connectives from Agda's, we add a superscript "o". So "and" is written
`×ᵒ`, "implies" is written `→ᵒ`, and so on.  SIL also includes a
notion of time in which there is a clock counting down. The logic is
designed in such a way that if a formula `P` is true at some time then
`P` stays true in the future (at lower counts). So formulas are
downward closed.  When the clock reaches zero, every formula becomes
true.  Furthermore, the logic includes a "later" operator, written `▷ᵒ
P`, meaning that `P` is true one clock tick in the future. When we use
SIL to reason about the cast calculus, one clock tick will correspond
to one reduction step.

Just as `Set` is the type of true/false formulas in Agda, `Setᵒ` is
the type of true/false formulas in SIL. It is a record that bundles
the formula itself, represented with a function of type `ℕ → Set`,
with proofs that the formula is downward closed and true at zero.

    record Setᵒ : Set₁ where
      field
        # : ℕ → Set
        down : downClosed #
        tz : # 0                -- tz short for true at zero
    open Setᵒ public

For example, the "false" proposition is false at every time except zero.

    ⊥ᵒ : Setᵒ
    ⊥ᵒ = record { # = λ { zero → ⊤ ; (suc k) → ⊥ }
                ; down = ... ; tz = ... }

The "and" proposition `P ×ᵒ Q` is true at a given time `k` if both `P`
and `Q` are true at time `k`.

    _×ᵒ_ : Setᵒ → Setᵒ → Setᵒ
    P ×ᵒ Q = record { # = λ k → # P k × # Q k
                    ; down = ... ; tz = ... }

The "for all" proposition `∀ᵒ[ a ] P` is true at a given time `k` if
the predicate `P` is true for all `a` at time `k`.

    ∀ᵒ : ∀{A : Set} → (A → Setᵒ) → Setᵒ
    ∀ᵒ{A} P = record { # = λ k → ∀ (a : A) → # (P a) k
                     ; down = ... ; tz = ... }

The "exists" proposition `∃ᵒ[ a ] P` is true at a given time `k` if
the predicate `P` is true for some `a` at time `k`. However, we
must require that the type `A` is inhabited so that this proposition
is true at time zero.

    ∃ᵒ : ∀{A : Set}{{_ : Inhabited A}} → (A → Setᵒ) → Setᵒ
    ∃ᵒ{A} P = record { # = λ k → Σ[ a ∈ A ] # (P a) k
                         ; down = ... ; tz = ... }

We embed arbitrary Agda formulas into the step-indexed logic with the
following constant operator, written `S ᵒ`, which is true if and only
if `S` is true, except at time zero, when `S ᵒ` has to be true.

    _ᵒ  : Set → Setᵒ
    S ᵒ = record { # = λ { zero → ⊤ ; (suc k) → S }
                 ; down = ... ; tz = ... }

Next we discuss the most important and interesting of the propositions,
the one for defining a recursive predicate. The following is a first
attempt at writing down the type of this proposition. The idea is that
this constructor of recursive predicates works like the Y-combinator
in that it turns a non-recursive predicate into a recursive one.

    μᵒ : ∀{A}
       → (A → (A → Setᵒ) → Setᵒ)
         -----------------------
       → A → Setᵒ

The non-recursive predicate has type `A → (A → Setᵒ) → Setᵒ`. It has
an extra parameter `(A → Setᵒ)` that will be bound to the
recursive predicate itself. To clarify, lets look at an example.
Suppose we want to define multi-step reduction according to
the following rules:

                M —→ L    L —→* N
    -------     ------------------
    M —→* M     M —→* N

We would first define a non-recursive predicate that has an extra
parameter, let us name it `R` for recursion. Inside the definition of
`mreduce`, we use `R` is the place where we would recursively use
`mreduce`, as follows.

    mreduce : Term × Term → (Term × Term → Setᵒ) → Setᵒ
    mreduce (M , N) R = (M ≡ N)ᵒ ⊎ᵒ (∃ᵒ[ L ] (M —→ L)ᵒ ×ᵒ R (L , N))

Because we use `∃ᵒ` with a Term, we need to prove that Term is inhabited.

```
instance
  TermInhabited : Inhabited Term
  TermInhabited = record { elt = `  }

```
We then apply the `μᵒ` proposition to `mreduce` to
obtain the desired recursive predicate `—→*`.

    _—→*_ : Term → Term → Setᵒ
    M —→* N = μᵒ mreduce (M , N)

The problem with the above story is that it's not possible in Agda (to
my knowledge) to construct a recursive predicate from an arbitrary
function of type `A → (A → Setᵒ) → Setᵒ`. Instead, we need to place
restrictions on the function. In particular, if we make sure that the
recursion never happens "now", but only "later", then it becomes
possible to construct `μᵒ`. We define the `Setˢ` type in Agda to
capture this restriction. (The superscript "s" stands for step
indexed.) Furthermore, to allow the nesting of recursive definitions,
we must generalize from a single predicate parameter to an environment
of predicates. The type of the environment is given by a `Context`:

    Context : Set₁
    Context = List Set

We represent an environment of recursive predicates with a tuple of
the following type.

    RecEnv : Context → Set₁
    RecEnv [] = topᵖ 
    RecEnv (A ∷ Γ) = (A → Setᵒ) × RecEnv Γ

We use de Bruijn indices to represent the variables that refer to the
recursive predicates, which we define as follows.

    data _∋_ : Context → Set → Set₁ where
      zeroˢ : ∀{Γ}{A} → (A ∷ Γ) ∋ A
      sucˢ : ∀{Γ}{A}{B} → Γ ∋ B → (A ∷ Γ) ∋ B

For each variable, we track whether it has been used "now" or not. So
we define `Time` as follows. The `Later` constructor does double duty
to mean a predicate has either been used "later" or not at all.

    data Time : Set where
      Now : Time
      Later : Time

The following defines a list of times, one for each variable in `Γ`.

    data Times : Context → Set₁ where
      ∅ : Times []
      cons : ∀{Γ}{A} → Time → Times Γ → Times (A ∷ Γ)

The `Setˢ` type is a record indexed by the type of the environment and
by the time for each variable. The representation of `Setˢ` (the `#`
field) is a function that maps an environment of predicates
(one predicate for each in-scope μ) to a `Setᵒ`.

    record Setˢ (Γ : Context) (ts : Times Γ) : Set₁ where
      field
        # : RecEnv Γ → Setᵒ 
        ...
    open Setˢ public

We define variants of all the propositional connectives to work on
Setˢ.

The "later" operator `▷ˢ` asserts that `P` is true in the future, so the
predicate `▷ˢ P` can safely say that any use of recursive predicate in
`P` happens `Later`.

    laters : ∀ (Γ : Context) → Times Γ
    laters [] = ∅
    laters (A ∷ Γ) = cons Later (laters Γ)

    ▷ˢ : ∀{Γ}{ts : Times Γ}
       → Setˢ Γ ts
         -----------------
       → Setˢ Γ (laters Γ)

The "and" operator, `P ×ˢ Q` is categorized as `Later` for a variable
only if both `P` and `Q` are `Later` for that variable. Otherwise it
is `Now`.  We use the following function to make this choice:

    choose : Kind → Kind → Kind
    choose Now Now = Now
    choose Now Later = Now
    choose Later Now = Now
    choose Later Later = Later

We define `combine` to apply `choose` to a list of times.

    combine : ∀{Γ} (ts₁ ts₂ : Times Γ) → Times Γ
    combine {[]} ts₁ ts₂ = ∅
    combine {A ∷ Γ} (cons x ts₁) (cons y ts₂) =
        cons (choose x y) (combine ts₁ ts₂)

Here's the type of the "and" operator:

    _×ˢ_ : ∀{Γ}{ts₁ ts₂ : Times Γ} → Setˢ Γ ts₁ → Setˢ Γ ts₂
       → Setˢ Γ (combine ts₁ ts₂)

The other propositions follow a similar pattern.

The membership formula `a ∈ x` is true when `a` is in the predicate
bound to variable `x` in the environment. The time for `x` is required
to be `Now`.

    var-now : ∀ (Γ : Context) → ∀{A} → (x : Γ ∋ A) → Times Γ
    var-now (B ∷ Γ) zeroˢ = cons Now (laters Γ)
    var-now (B ∷ Γ) (sucˢ x) = cons Later (var-now Γ x)

    _∈_ : ∀{Γ}{A}
       → A
       → (x : Γ ∋ A)
       → Setˢ Γ (var-now Γ x)
    a ∈ x =
      record { # = λ δ → (lookup x δ) a
             ; ... }

The `μˢ` formula defines a (possibly nested) recursive predicate.

    μˢ : ∀{Γ}{ts : Times Γ}{A}
       → (A → Setˢ (A ∷ Γ) (cons Later ts))
         ----------------------------------
       → (A → Setˢ Γ ts)

It takes a non-recursive predicate from `A` to `Setˢ` and produces a
recursive predicate in `A`. Note that the variable `zeroˢ`, the
one introduced by this `μˢ`, is required to have time `Later`.

If the recursive predicate is not nested inside other recursive
predicates, then you can directly use the following `μᵒ` operator.

    μᵒ : ∀{A}
       → (A → Setˢ (A ∷ []) (cons Later ∅))
         ----------------------------------
       → (A → Setᵒ)

Let's revisit the example of defining multi-step reduction.  The
non-recursive `mreduce` predicate is defined as follows.

```
mreduce : Term × Term → Setˢ ((Term × Term) ∷ []) (cons Later ∅)
mreduce (M , N) = (M ≡ N)ˢ ⊎ˢ (∃ˢ[ L ] (M —→ L)ˢ ×ˢ ▷ˢ (((L , N) ∈ zeroˢ)))
```

Note that the `R` parameter has become implicit; it has moved into the
environment. Also the application `R (L , N)` is replaced by
`▷ˢ ((L , N) ∈ zeroˢ)`, where the de Bruijn index `zeroˢ` refers to
the predicate `R` in the environment.

We define the recursive predicate `M —→* N` by applying `μᵒ`
to `mreduce`.

```
infix  _—→*_
_—→*_ : Term → Term → Setᵒ
M —→* N = μᵒ mreduce (M , N)
```

Here are a couple uses of the multi-step reduction relation.

```
X₀ : #($ (Num ) —→* $ (Num )) 
X₀ = inj₁ refl

X₁ : #((ƛ ($ (Num ))) · $ (Num ) —→* $ (Num )) 
X₁ = inj₂ (_ , (β ($̬ _) , inj₁ refl))
```

## Proofs in Step-indexed Logic

Just like first-orderd logic, SIL comes with rules of deduction for
carrying out proofs. The judgement form is `𝒫 ⊢ᵒ P`, where `𝒫` is a
list of assumptions and `P` is a formula.  The judgement `𝒫 ⊢ᵒ P` is
true iff for every time `k`, all of `𝒫` are true at `k` implies that `P`
is true at `k`. So in Agda we have the following definition.

    Πᵒ : List Setᵒ → Setᵒ
    Πᵒ [] = ⊤ᵒ
    Πᵒ (P ∷ 𝒫) = P ×ᵒ Πᵒ 𝒫 

    _⊢ᵒ_ : List Setᵒ → Setᵒ → Set
    𝒫 ⊢ᵒ P = ∀ k → # (Πᵒ 𝒫) k → # P k

Many of the deduction rules are the same as in first order logic.
For example, here are the introduction and elimination rules
for conjunction. We use the same notation as Agda, but with
a superscript "o".

    _,ᵒ_ : ∀{𝒫 : List Setᵒ }{P Q : Setᵒ}
      → 𝒫 ⊢ᵒ P
      → 𝒫 ⊢ᵒ Q
        ------------
      → 𝒫 ⊢ᵒ P ×ᵒ Q

    proj₁ᵒ : ∀{𝒫 : List Setᵒ }{P Q : Setᵒ}
      → 𝒫 ⊢ᵒ P ×ᵒ Q
        ------------
      → 𝒫 ⊢ᵒ P

    proj₂ᵒ : ∀{𝒫 : List Setᵒ }{P Q : Setᵒ}
      → 𝒫 ⊢ᵒ P ×ᵒ Q
        ------------
      → 𝒫 ⊢ᵒ Q

The introduction rule for a constant formula `S ᵒ` is straightforward.
A proof of `S` in regular Agda is sufficient to build a proof of `S ᵒ`
in SIL.

    constᵒI : ∀{𝒫}{S : Set}
       → S
       → 𝒫 ⊢ᵒ S ᵒ

On the other hand, given a proof of `S ᵒ` in SIL, one cannot obtain a
proof of `S` directly in Agda. That is, the following rule is invalid
because `𝒫` could be false at every index.

    bogus-constᵒE : ∀ {𝒫}{S : Set}{R : Setᵒ}
       → 𝒫 ⊢ᵒ S ᵒ
       → S

Instead, we have an elimination rule in continuation-passing style.
That is, if we have a proof of `S ᵒ` and need to prove some arbitrary
goal `R`, then it suffices to prove `R` under the assumption that `S`
is true.

    constᵒE : ∀ {𝒫}{S : Set}{R : Setᵒ}
       → 𝒫 ⊢ᵒ S ᵒ
       → (S → 𝒫 ⊢ᵒ R)
       → 𝒫 ⊢ᵒ R

Analogous to `subst` in Agda's standard library, SIL has `substᵒ`
which says that if `P` and `Q` are equivalent, then a proof of `P` gives
a proof of `Q`.

    substᵒ : ∀{𝒫}{P Q : Setᵒ}
      → P ≡ᵒ Q
        -------------------
      → 𝒫 ⊢ᵒ P  →  𝒫 ⊢ᵒ Q

The deduction rules also include ones for the "later" operator.  As we
mentioned earlier, if a proposition is true now it will also be true
later.

    monoᵒ : ∀ {𝒫}{P}
       → 𝒫 ⊢ᵒ P
         -----------
       → 𝒫 ⊢ᵒ  ▷ᵒ P

One can transport induction on natural numbers into SIL to obtain the
following Löb rule, which states that when proving any property `P`,
one is allowed to assume that `P` is true later.

    lobᵒ : ∀ {𝒫}{P}
       → (▷ᵒ P) ∷ 𝒫 ⊢ᵒ P
         -----------------------
       → 𝒫 ⊢ᵒ P

For comparison, here's induction on natural numbers

      P 0
    → (∀ k → P k → P (suc k))
    → ∀ n → P n

In the world of SIL, propositions are always true at zero, so the base
case `P 0` is not necessary. The induction step `(∀ k → P k → P (suc k))`
is similar to the premise `(▷ᵒ P) ∷ 𝒫 ⊢ᵒ P` because `▷ᵒ` subtracts one.

The following is a handy proof rule that turns a proof of `P` in SIL
into an assumption in Agda that `P` is true for some positive natural
number.

    ⊢ᵒ-sucP : ∀{𝒫}{P Q : Setᵒ}
       → 𝒫 ⊢ᵒ P
       → (∀{n} → # P (suc n) → 𝒫 ⊢ᵒ Q)
       → 𝒫 ⊢ᵒ Q

As usual for temporal logics (or more generally, for modal logics),
there are distribution rules that push "later" through the other
logical connectives. For example, the following rule distributes
"later" through conjunction.

    ▷× : ∀{𝒫} {P Q : Setᵒ}
       → 𝒫 ⊢ᵒ (▷ᵒ (P ×ᵒ Q))
         ----------------------
       → 𝒫 ⊢ᵒ (▷ᵒ P) ×ᵒ (▷ᵒ Q)

This project was the first time for me conducting nontrivial proofs in
a modal logic, and it took some getting use to!


## Defining a Logical Relation for Type Safety

With the Step-indexed Logic in hand, we are ready to define a logical
relation for type safety. The two predicates ℰ and 𝒱 are mutually
recursive, so we combine them into a single recursive predicate named
`ℰ⊎𝒱` that takes a sum type, where the left side is for ℰ and the
right side is for 𝒱. We shall define `ℰ⊎𝒱` by an application of
`μᵒ`, so we first need to define the non-recursive version of
`ℰ⊎𝒱`, which we call `pre-ℰ⊎𝒱`, defined below. It simply dispatches to
the non-recursive `pre-ℰ` and `pre-ℰ` which we define next.

```
ℰ⊎𝒱-type : Set
ℰ⊎𝒱-type = (Type × Term) ⊎ (Type × Term)

ℰ⊎𝒱-ctx : Context
ℰ⊎𝒱-ctx = ℰ⊎𝒱-type ∷ []

pre-ℰ : Type → Term → Setˢ ℰ⊎𝒱-ctx (cons Later ∅)
pre-𝒱 : Type → Term → Setˢ ℰ⊎𝒱-ctx (cons Later ∅)

pre-ℰ⊎𝒱 : ℰ⊎𝒱-type → Setˢ ℰ⊎𝒱-ctx (cons Later ∅)
pre-ℰ⊎𝒱 (inj₁ (A , V)) = pre-𝒱 A V
pre-ℰ⊎𝒱 (inj₂ (A , M)) = pre-ℰ A M
```

To improve the readability of our definitions, we define the following
notation for recursive applications of the ℰ and 𝒱 predicates.

```
ℰˢ⟦_⟧ : Type → Term → Setˢ ℰ⊎𝒱-ctx (cons Now ∅)
ℰˢ⟦ A ⟧ M = (inj₂ (A , M)) ∈ zeroˢ

𝒱ˢ⟦_⟧ : Type → Term → Setˢ ℰ⊎𝒱-ctx (cons Now ∅)
𝒱ˢ⟦ A ⟧ V = (inj₁ (A , V)) ∈ zeroˢ
```

The definition of `pre-ℰ` and `pre-𝒱` below are of similar form to the
explicitly step-indexed definition of ℰ and 𝒱 above, however the
parameter `k` is gone and all of the logical connectives have a
superscript `s`, indicating that we're building a `Setˢ`.  Also,
note that all the uses of `ℰˢ` and `𝒱ˢ` are guarded by the later
operator `▷ˢ`. Finally, in the definition of `pre-ℰ`, we do not use `▷ˢ
(𝒱⟦ A ⟧ M)` but instead use `pre-𝒱 A M` because we need to say in that
spot that `M` is a semantic value now, not later.

```
pre-ℰ A M = (pre-𝒱 A M ⊎ˢ (reducible M)ˢ ⊎ˢ (Blame M)ˢ)
             ×ˢ (∀ˢ[ N ] (M —→ N)ˢ →ˢ ▷ˢ (ℰˢ⟦ A ⟧ N))

pre-𝒱 ★ (V ⟨ G !⟩ )      = (Value V)ˢ ×ˢ ▷ˢ (𝒱ˢ⟦ gnd⇒ty G ⟧ V)
pre-𝒱 ($ₜ ι) ($ c)        = (ι ≡ typeof c)ˢ
pre-𝒱 (A ⇒ B) (ƛ N)      = ∀ˢ[ W ] ▷ˢ (𝒱ˢ⟦ A ⟧ W) →ˢ ▷ˢ (ℰˢ⟦ B ⟧ (N [ W ]))
pre-𝒱 A M                = ⊥ ˢ
```

We define ℰ and 𝒱 by creating a recursive predicate (apply `μᵒ` to
`pre-ℰ⊎𝒱`) and then apply it to an argument injected with either `inj₁`
for 𝒱 or `inj₂` for ℰ.

```
ℰ⊎𝒱 : ℰ⊎𝒱-type → Setᵒ
ℰ⊎𝒱 X = μᵒ pre-ℰ⊎𝒱 X

ℰ⟦_⟧ : Type → Term → Setᵒ
ℰ⟦ A ⟧ M = ℰ⊎𝒱 (inj₂ (A , M))

𝒱⟦_⟧ : Type → Term → Setᵒ
𝒱⟦ A ⟧ V = ℰ⊎𝒱 (inj₁ (A , V))
```

To succinctly talk about the two aspects of ℰ, we define semantic
`progress` and `preservation` as follows.

```
progress : Type → Term → Setᵒ
progress A M = 𝒱⟦ A ⟧ M ⊎ᵒ (reducible M)ᵒ ⊎ᵒ (Blame M)ᵒ

preservation : Type → Term → Setᵒ
preservation A M = ∀ᵒ[ N ] ((M —→ N)ᵒ →ᵒ ▷ᵒ (ℰ⟦ A ⟧ N))
```

We can prove that ℰ is indeed equivalent to progress and preservation
by use of the `fixpointᵒ` theorem in SIL.

```
ℰ-stmt : ∀{A}{M}
  → ℰ⟦ A ⟧ M ≡ᵒ progress A M ×ᵒ preservation A M
ℰ-stmt {A}{M} =
  ℰ⟦ A ⟧ M                                                    ⩦⟨ ≡ᵒ-refl refl ⟩
  μᵒ pre-ℰ⊎𝒱 (inj₂ (A , M))              ⩦⟨ fixpointᵒ pre-ℰ⊎𝒱 (inj₂ (A , M)) ⟩
  # (pre-ℰ⊎𝒱 (inj₂ (A , M))) (ℰ⊎𝒱 , ttᵖ)
             ⩦⟨ cong-×ᵒ (cong-⊎ᵒ (≡ᵒ-sym (fixpointᵒ pre-ℰ⊎𝒱 (inj₁ (A , M))))
                                      (≡ᵒ-refl refl)) (≡ᵒ-refl refl) ⟩
  progress A M ×ᵒ preservation A M
  ∎
```

For convenience, we define introduction and elimination rules for ℰ.

```
ℰ-intro : ∀ {𝒫}{A}{M}
  → 𝒫 ⊢ᵒ progress A M
  → 𝒫 ⊢ᵒ preservation A M
    ----------------------
  → 𝒫 ⊢ᵒ ℰ⟦ A ⟧ M
ℰ-intro 𝒫⊢prog 𝒫⊢pres = substᵒ (≡ᵒ-sym ℰ-stmt) (𝒫⊢prog ,ᵒ 𝒫⊢pres)

ℰ-progress : ∀ {𝒫}{A}{M}
  → 𝒫 ⊢ᵒ ℰ⟦ A ⟧ M
  → 𝒫 ⊢ᵒ progress A M
ℰ-progress 𝒫⊢ℰM = proj₁ᵒ (substᵒ ℰ-stmt 𝒫⊢ℰM )

ℰ-preservation : ∀ {𝒫}{A}{M}
  → 𝒫 ⊢ᵒ ℰ⟦ A ⟧ M
  → 𝒫 ⊢ᵒ preservation A M
ℰ-preservation 𝒫⊢ℰM = proj₂ᵒ (substᵒ ℰ-stmt 𝒫⊢ℰM )
```

Similarly, we can derive the expected equations for 𝒱.

```
𝒱-base : ∀{ι}{c : Lit} → (𝒱⟦ $ₜ ι ⟧ ($ c)) ≡ᵒ (ι ≡ typeof c)ᵒ
𝒱-base = ≡ᵒ-intro λ k → (λ x → x) , (λ x → x)

𝒱-dyn : ∀{G}{V} → 𝒱⟦ ★ ⟧ (V ⟨ G !⟩) ≡ᵒ ((Value V)ᵒ ×ᵒ ▷ᵒ (𝒱⟦ gnd⇒ty G ⟧ V))
𝒱-dyn {G}{V} =
   let X = (inj₁ (★ , V ⟨ G !⟩)) in
   𝒱⟦ ★ ⟧ (V ⟨ G !⟩)                              ⩦⟨ ≡ᵒ-refl refl ⟩
   ℰ⊎𝒱 X                                          ⩦⟨ fixpointᵒ pre-ℰ⊎𝒱 X ⟩
   # (pre-ℰ⊎𝒱 X) (ℰ⊎𝒱 , ttᵖ)                     ⩦⟨ ≡ᵒ-refl refl ⟩ 
   (Value V)ᵒ ×ᵒ ▷ᵒ (𝒱⟦ gnd⇒ty G ⟧ V)             ∎

𝒱-fun : ∀{A B}{N}
   → 𝒱⟦ A ⇒ B ⟧ (ƛ N)
      ≡ᵒ (∀ᵒ[ W ] ((▷ᵒ (𝒱⟦ A ⟧ W)) →ᵒ (▷ᵒ (ℰ⟦ B ⟧ (N [ W ])))))
𝒱-fun {A}{B}{N} =
   let X = (inj₁ (A ⇒ B , ƛ N)) in
   𝒱⟦ A ⇒ B ⟧ (ƛ N)                                         ⩦⟨ ≡ᵒ-refl refl ⟩
   ℰ⊎𝒱 X                                            ⩦⟨ fixpointᵒ pre-ℰ⊎𝒱 X ⟩
   # (pre-ℰ⊎𝒱 X) (ℰ⊎𝒱 , ttᵖ)                               ⩦⟨ ≡ᵒ-refl refl ⟩ 
   (∀ᵒ[ W ] ((▷ᵒ (𝒱⟦ A ⟧ W)) →ᵒ (▷ᵒ (ℰ⟦ B ⟧ (N [ W ])))))   ∎
```

We have defined `𝒱` such that it only accepts terms that are syntactic
values. (We included `Value V` in the case for `★` of `pre-𝒱`.)

```
𝒱⇒Value : ∀ {k} A M
   → # (𝒱⟦ A ⟧ M) (suc k)
     ---------------------
   → Value M
𝒱⇒Value ★ (M ⟨ G !⟩) (v , _) = v 〈 G 〉
𝒱⇒Value ($ₜ ι) ($ c) 𝒱M = $̬ c
𝒱⇒Value (A ⇒ B) (ƛ N) 𝒱M = ƛ̬ N
```

A value `V` in 𝒱 is also in ℰ. The definition of `progress` includes
values, and to prove preservation we note that a value is irreducible.

```
𝒱⇒ℰ : ∀{A}{𝒫}{V}
   → 𝒫 ⊢ᵒ 𝒱⟦ A ⟧ V
     ---------------
   → 𝒫 ⊢ᵒ ℰ⟦ A ⟧ V
𝒱⇒ℰ {A}{𝒫}{V} 𝒫⊢𝒱V = ℰ-intro prog pres
    where
    prog = inj₁ᵒ 𝒫⊢𝒱V
    pres = Λᵒ[ N ] →ᵒI (constᵒE Zᵒ λ V—→N →
             ⊢ᵒ-sucP (⊢ᵒ-weaken 𝒫⊢𝒱V) λ 𝒱V →
                ⊥-elim (value-irreducible (𝒱⇒Value A V 𝒱V ) V—→N))
```

## Semantic Type Safety for Open Terms

The `ℰ` predicate applies to closed terms, that is, terms without any
free variables, such as a whole program. However, we'll need a notion
of semantic type safety that also includes open terms. The standard
way to define safety for an open term `M` is to substitute the free
variables for values and then use `ℰ`. That is, we apply a
substitution `γ` to `M` where all the values in `γ` must be
semantically well typed. The following `𝓖` expresses this contraint on
`γ`.

```
𝓖⟦_⟧ : (Γ : List Type) → Subst → List Setᵒ
𝓖⟦ [] ⟧ σ = []
𝓖⟦ A ∷ Γ ⟧ σ = (𝒱⟦ A ⟧ (σ )) ∷ 𝓖⟦ Γ ⟧ (λ x → σ (suc x))
```

A term `M` is semantically well typed at `A` in context `Γ` if, 
for any well-typed substitution `γ`, we have `ℰ⟦ A ⟧ (⟪ γ ⟫ M)`.

```
_⊨_⦂_ : List Type → Term → Type → Set
Γ ⊨ M ⦂ A = ∀ (γ : Subst) → 𝓖⟦ Γ ⟧ γ ⊢ᵒ ℰ⟦ A ⟧ (⟪ γ ⟫ M)
```

## The Fundamental Lemma via Compatibility Lemmas

The main lemma on our way to proving type safety is the Fundamental
Lemma, which states that well-typed programs are semantically type
safe. That is, well-typed programs behave as expected according to
their types.

    fundamental : ∀ {Γ A} → (M : Term)
      → Γ ⊢ M ⦂ A
        ----------
      → Γ ⊨ M ⦂ A

The proof of `fundamental` is by induction on the typing derivation,
with each case dispatching to a compatibility lemma.

The compatibility lemma for number literals is proved by showing that
`$ (Num n)` is in `𝒱⟦ $ₜ ′ℕ ⟧` via the definition of `𝒱` and then
apply the `𝒱⇒ℰ` lemma.

```
compatible-nat : ∀{Γ}{n : ℕ}
     -----------------------
   → Γ ⊨ $ (Num n) ⦂ ($ₜ ′ℕ)
compatible-nat {Γ}{n} γ = 𝒱⇒ℰ (substᵒ (≡ᵒ-sym 𝒱-base) (constᵒI refl))
```

The compability lemma for Boolean literals is the same.

```
compatible-bool : ∀{Γ}{b : 𝔹}
     --------------------------
   → Γ ⊨ ($ (Bool b)) ⦂ ($ₜ ′𝔹)
compatible-bool {Γ}{b} γ = 𝒱⇒ℰ (substᵒ (≡ᵒ-sym 𝒱-base) (constᵒI refl))
```

The compatibility lemma for the `blame` term is similar to the `𝒱⇒ℰ`
lemma in that `blame` is one of the alternatives allowed in `progress`
and `blame` is irreducible.

```
ℰ-blame : ∀{𝒫}{A} → 𝒫 ⊢ᵒ ℰ⟦ A ⟧ blame
ℰ-blame {𝒫}{A} = ℰ-intro prog pres
    where
    prog = inj₂ᵒ (inj₂ᵒ (constᵒI isBlame))
    pres = Λᵒ[ N ] →ᵒI (constᵒE Zᵒ λ blame→ → ⊥-elim (blame-irreducible blame→))

compatible-blame : ∀{Γ}{A}
     -------------
   → Γ ⊨ blame ⦂ A
compatible-blame {Γ}{A} γ = ℰ-blame
```

The compatibility lemma for variables makes use of the premise that
the values in the environment are semantically well typed.
The following lemma proves that for any variable `y` in `Γ`,
`γ` in `𝓖⟦ Γ ⟧` imples that `γ y` in `𝒱⟦ A ⟧`.

```
lookup-𝓖 : (Γ : List Type) → (γ : Subst)
  → ∀ {A}{y} → (Γ ∋ y ⦂ A)
  → 𝓖⟦ Γ ⟧ γ ⊢ᵒ 𝒱⟦ A ⟧ (γ y)
lookup-𝓖 (B ∷ Γ) γ {A} {zero} refl = Zᵒ
lookup-𝓖 (B ∷ Γ) γ {A} {suc y} ∋y =
    Sᵒ (lookup-𝓖 Γ (λ x → γ (suc x)) ∋y) 
```

Once we have `γ y` in `𝒱⟦ A ⟧`, we conclude by applying the `𝒱⇒ℰ`
lemma. (The `sub-var` lemma just says that `⟪ γ ⟫ (` x) ≡ γ x`.)

```
compatibility-var : ∀ {Γ A x}
  → Γ ∋ x ⦂ A
    -----------
  → Γ ⊨ ` x ⦂ A
compatibility-var {Γ}{A}{x} ∋x γ rewrite sub-var γ x = 𝒱⇒ℰ (lookup-𝓖 Γ γ ∋x)
```

The next compatibility lemma is for lambda abstraction.  To show that
`ƛ N` is in `ℰ⟦A ⇒ B⟧` we shows that `ƛ N` is in `𝒱⟦A ⇒ B⟧`.  According
to that definition, we need to show that for any argument value `W` in
`𝒱⟦ A ⟧` (later), we have `(⟪ ext γ ⟫ N) [ W ]` in `ℰ⟦ B ⟧` (also later).  But
that follows almost directly from the premise that `N` is semantically
type safe. From that premise we have

    ▷ᵒ ℰ ⟦ B ⟧ (⟪ W • γ ⟫ N)

and the Abstract Binding Tree library provides rewrites for the
following equation

    ⟪ W • γ ⟫ N = (⟪ ext γ ⟫ N) [ W ]

which gives us what we need:

    ▷ᵒ ℰ ⟦ B ⟧ (⟪ ext γ ⟫ N) [ W ]

Here's all the details in Agda:
```
compatible-lambda : ∀{Γ}{A}{B}{N}
   → (A ∷ Γ) ⊨ N ⦂ B
     -------------------
   → Γ ⊨ (ƛ N) ⦂ (A ⇒ B)
compatible-lambda {Γ}{A}{B}{N} ⊨N γ = 𝒱⇒ℰ ⊢𝒱λN
 where
 ⊢𝒱λN : 𝓖⟦ Γ ⟧ γ ⊢ᵒ 𝒱⟦ A ⇒ B ⟧ (ƛ (⟪ ext γ ⟫ N))
 ⊢𝒱λN = (substᵒ (≡ᵒ-sym 𝒱-fun) (Λᵒ[ W ] →ᵒI ▷𝓔N[W]))
  where
  ▷𝓔N[W] : ∀{W} → ▷ᵒ 𝒱⟦ A ⟧ W ∷ 𝓖⟦ Γ ⟧ γ  ⊢ᵒ  ▷ᵒ ℰ⟦ B ⟧ ((⟪ ext γ ⟫ N) [ W ])
  ▷𝓔N[W] {W} = appᵒ (Sᵒ (▷→ (monoᵒ (→ᵒI (⊨N (W • γ)))))) Zᵒ
```

The next few compatibility lemmas, for application, injection, and
projection all involve reasoning about the reduction of one or two
subexpressions.  Instead of duplicating this reasoning, the standard
approach is to put that reasoning in the "bind" lemma, which we
discuss next.

## Interlude: the "Bind" Lemma

The bind lemma says that if we have an expression `N` with a
subexpression `M` (so `N` is equal to plugging `M` into
an appropriate frame `F`, i.e. `N = F ⟦ M ⟧`), if
`M` is semantically safe, then to prove `ℰ⟦ A ⟧ (F ⟦ M ⟧)`
it suffices to prove that `ℰ⟦ A ⟧ (F ⟦ V ⟧))`
for some semantically safe value `V` that `M` reduced to.

    ℰ-bind : ∀{𝒫}{A}{B}{F}{M}
       → 𝒫 ⊢ᵒ ℰ⟦ B ⟧ M
       → 𝒫 ⊢ᵒ (∀ᵒ[ V ] (M —↠ V)ᵒ →ᵒ 𝒱⟦ B ⟧ V →ᵒ ℰ⟦ A ⟧ (F ⟦ V ⟧))
         ----------------------------------------------------------
       → 𝒫 ⊢ᵒ ℰ⟦ A ⟧ (F ⟦ M ⟧)

In the title of this blog post I alluded to one hard lemma. This is
the one!

We begin by creating some names for parts of the statement of this
lemma. First we have a name for the second premise.

```
𝒱V→ℰF[V] : Type → Type → Frame → Term → Setᵒ
𝒱V→ℰF[V] A B F M = ∀ᵒ[ V ] (M —↠ V)ᵒ →ᵒ 𝒱⟦ B ⟧ V →ᵒ ℰ⟦ A ⟧ (F ⟦ V ⟧)
```

Then we have a name for the two premises and the conclusion, with the
implications expressed in SIL.

```
ℰ-bind-M : Type → Type → Frame → Term → Setᵒ
ℰ-bind-M A B F M = ℰ⟦ B ⟧ M →ᵒ 𝒱V→ℰF[V] A B F M →ᵒ ℰ⟦ A ⟧ (F ⟦ M ⟧)
```

The following adds universal quantification (in SIL) over the term `M`.

```
ℰ-bind-prop : Type → Type → Frame → Setᵒ
ℰ-bind-prop A B F = ∀ᵒ[ M ] ℰ-bind-M A B F M
```

We shall need the `𝒱V→ℰF[V]` property to be preserved under reverse
reduction, i.e., expansion. The proof is as follows. We need to show
that `ℰ⟦ A ⟧ (F ⟦ V ⟧)` under the assumption that `M′ —↠ V` and
`𝒱⟦ B ⟧ V`. With the first premise `M —→ M′`, we obtain `M —↠ V`. Then we
apply the second premise to conclude that `ℰ⟦ A ⟧ (F ⟦ V ⟧)`.

```
𝒱V→ℰF[V]-expansion : ∀{𝒫}{A}{B}{F}{M}{M′}
   → M —→ M′
   → 𝒫 ⊢ᵒ 𝒱V→ℰF[V] A B F M
     -----------------------
   → 𝒫 ⊢ᵒ 𝒱V→ℰF[V] A B F M′
𝒱V→ℰF[V]-expansion {𝒫}{A}{B}{F}{M}{M′} M→M′ 𝒱V→ℰF[V][M] =
   Λᵒ[ V ]
    let M′→V→ℰFV : 𝒱⟦ B ⟧ V ∷ (M′ —↠ V)ᵒ ∷ 𝒫 ⊢ᵒ ℰ⟦ A ⟧ (F ⟦ V ⟧)
        M′→V→ℰFV = ⊢ᵒ-sucP (Sᵒ Zᵒ) λ M′→V → 
                     let M—↠V = constᵒI (M —→⟨ M→M′ ⟩ M′→V) in
                     let M→V→ℰFV = ⊢ᵒ-weaken(⊢ᵒ-weaken(instᵒ 𝒱V→ℰF[V][M] V)) in
                     appᵒ (appᵒ M→V→ℰFV M—↠V) Zᵒ in
    →ᵒI (→ᵒI M′→V→ℰFV)
```

We now proceed to prove the `ℰ-bind` lemma by way of an auxilliary
lemma `ℰ-bind-aux` that restates the lemma so that the term `M` is
universally quantified in SIL (instead of Agda), so that we can do the
proof by Löb induction, that is, by use of the `lobᵒ` rule of SIL.
So after the use of `lobᵒ`, it remains to prove that `ℰ⟦ A ⟧ (F ⟦ M ⟧)`,
but now we have the additional assumption that we can apply the
bind lemma in the future to any term, i.e., we have `▷ᵒ ℰ-bind-prop A B F`.
From the premise `ℰ⟦ B ⟧ M` we have that `M` satisfies progress,
so either (1) it is a semantic value, (2) it can reduce, or (3) it is blame.
We proceed by reasoning about each of these three cases.

* `M` is already a value, so it can multi-step reduce to itself in
  zero steps, and then we apply the `𝒱V→ℰF[V]` premise to immediately
  conclude.

* `M` is reducible.
  Now to prove `ℰ⟦ A ⟧ (F ⟦ M ⟧)` we need to prove progress and preservation.
  The progress part is immediate, because by rule `ξ` we have
  `F ⟦ M ⟧ —→ F ⟦ M′ ⟧` because `M —→ M′ for some `M′`.
  The preservation part is more involved.
  We are given that `F ⟦ M ⟧ —→ N` and need to prove that `▷ᵒ (ℰ⟦ A ⟧ N)`.
  By the `frame-inv2` lemma, we obtain an `M′` such that `M —→ M′`
  and `N ≡ F ⟦ M′ ⟧`. So we need to prove that `▷ᵒ (ℰ⟦ A ⟧ (F ⟦ M′ ⟧))`
  We shall obtain this via the induction hypothesis, and for that we
  need to prove (1) `▷ᵒ ℰ⟦ B ⟧ M′` and (2) `▷ᵒ (𝒱V→ℰF[V] A B F M′)`.
  We obtain (1) from the preservation part of `ℰ⟦ B ⟧ M`.
  We obtain (2) by the `𝒱V→ℰF[V]-expansion` lemma and shift it to later
  using `monoᵒ`.

* `M` is blame. We need to show `ℰ⟦ A ⟧ (F ⟦ blame ⟧)`.
   For the progress part, we have the reduction `F ⟦ blame ⟧ —→ blame`
   by rule `ξ-blame`. For preservation, we have `F ⟦ blame ⟧ —→ N`
   and need to prove that `▷ᵒ (ℰ⟦ A ⟧ N)`. The `blame-frame`
   lemma tells us that `N ≡ blame`, so we conclude by use of
   `ℰ-blame` and then `monoᵒ`.

```
open import rewriting.examples.CastDeterministic
  using (frame-inv2; deterministic)

ℰ-bind-aux : ∀{𝒫}{A}{B}{F} → 𝒫 ⊢ᵒ ℰ-bind-prop A B F
ℰ-bind-aux {𝒫}{A}{B}{F} = lobᵒ (Λᵒ[ M ] →ᵒI (→ᵒI Goal))
  where
  Goal : ∀{M} → (𝒱V→ℰF[V] A B F M) ∷ ℰ⟦ B ⟧ M ∷ ▷ᵒ ℰ-bind-prop A B F ∷ 𝒫
                 ⊢ᵒ ℰ⟦ A ⟧ (F ⟦ M ⟧)
  Goal{M} =
   case3ᵒ (ℰ-progress (Sᵒ Zᵒ)) Mval Mred Mblame
   where
   𝒫′ = (𝒱V→ℰF[V] A B F M) ∷ ℰ⟦ B ⟧ M ∷ ▷ᵒ ℰ-bind-prop A B F ∷ 𝒫

   Mval : 𝒱⟦ B ⟧ M ∷ 𝒫′ ⊢ᵒ ℰ⟦ A ⟧ (F ⟦ M ⟧)
   Mval =
     let 𝒱V→ℰF[V][M] = λ V → (M —↠ V)ᵒ →ᵒ 𝒱⟦ B ⟧ V →ᵒ ℰ⟦ A ⟧ (F ⟦ V ⟧) in
     appᵒ (appᵒ (instᵒ{P = 𝒱V→ℰF[V][M]} (Sᵒ Zᵒ) M) (constᵒI (M END))) Zᵒ

   Mred : (reducible M)ᵒ ∷ 𝒫′ ⊢ᵒ ℰ⟦ A ⟧ (F ⟦ M ⟧)
   Mred = ℰ-intro progressMred preservationMred
    where
    progressMred : (reducible M)ᵒ ∷ 𝒫′ ⊢ᵒ progress A (F ⟦ M ⟧)
    progressMred = inj₂ᵒ (inj₁ᵒ (constᵒE Zᵒ λ {(M′ , M→M′) →
                                            constᵒI (_ , (ξ F M→M′))}))

    preservationMred : (reducible M)ᵒ ∷ 𝒫′ ⊢ᵒ preservation A (F ⟦ M ⟧)
    preservationMred = (constᵒE Zᵒ λ redM →
                ⊢ᵒ-weaken (Λᵒ[ N ] →ᵒI (constᵒE Zᵒ λ FM→N →
                                          ⊢ᵒ-weaken (redM⇒▷ℰN redM FM→N))))
     where
     redM⇒▷ℰN : ∀{N} → reducible M → (F ⟦ M ⟧ —→ N) → 𝒫′ ⊢ᵒ ▷ᵒ (ℰ⟦ A ⟧ N)
     redM⇒▷ℰN {N} rM FM→N =
      let finv = frame-inv2{M}{N}{F} rM FM→N in
      let M′ = proj₁ finv in
      let M→M′ = proj₁ (proj₂ finv) in
      let N≡ = proj₂ (proj₂ finv) in
      let ▷ℰM′ : 𝒫′ ⊢ᵒ ▷ᵒ ℰ⟦ B ⟧ M′
          ▷ℰM′ = appᵒ (instᵒ{P = λ N → (M —→ N)ᵒ →ᵒ ▷ᵒ (ℰ⟦ B ⟧ N)}
                        (ℰ-preservation (Sᵒ Zᵒ)) M′)
                      (constᵒI M→M′) in
      let ▷M′→V→𝒱V→ℰFV : 𝒫′ ⊢ᵒ ▷ᵒ (𝒱V→ℰF[V] A B F M′)
          ▷M′→V→𝒱V→ℰFV = monoᵒ (𝒱V→ℰF[V]-expansion{𝒫′}{A}{B} M→M′ Zᵒ) in
      let IH : 𝒫′ ⊢ᵒ ▷ᵒ ℰ-bind-prop A B F
          IH = Sᵒ (Sᵒ Zᵒ) in
      let ▷ℰFM′ : 𝒫′ ⊢ᵒ ▷ᵒ (ℰ⟦ A ⟧ (F ⟦ M′ ⟧))
          ▷ℰFM′ = frame-prop-lemma IH ▷ℰM′ ▷M′→V→𝒱V→ℰFV in
      subst (λ N → 𝒫′ ⊢ᵒ ▷ᵒ ℰ⟦ A ⟧ N) (sym N≡) ▷ℰFM′
      where
      frame-prop-lemma : ∀{𝒫}{A}{B}{M}{F}
         → 𝒫 ⊢ᵒ ▷ᵒ ℰ-bind-prop A B F  →  𝒫 ⊢ᵒ ▷ᵒ ℰ⟦ B ⟧ M
         → 𝒫 ⊢ᵒ ▷ᵒ 𝒱V→ℰF[V] A B F M   →  𝒫 ⊢ᵒ ▷ᵒ (ℰ⟦ A ⟧ (F ⟦ M ⟧))
      frame-prop-lemma{𝒫}{A}{B}{M}{F} IH ℰM V→FV =
       appᵒ(▷→ (appᵒ(▷→ (instᵒ(▷∀{P = λ M → ℰ-bind-M A B F M} IH) M)) ℰM)) V→FV

   Mblame : (Blame M)ᵒ ∷ 𝒫′ ⊢ᵒ ℰ⟦ A ⟧ (F ⟦ M ⟧)
   Mblame = ℰ-intro progressMblame
            (constᵒE Zᵒ λ blameM →
               ⊢ᵒ-weaken (Λᵒ[ N ] →ᵒI (constᵒE Zᵒ λ FM→N →
                                        ⊢ᵒ-weaken (blameM⇒▷ℰN blameM FM→N))))
    where
    progressMblame : (Blame M)ᵒ ∷ 𝒫′ ⊢ᵒ progress A (F ⟦ M ⟧)
    progressMblame =
       inj₂ᵒ (inj₁ᵒ (constᵒE Zᵒ λ {isBlame → constᵒI (_ , (ξ-blame F))}))

    blameM⇒▷ℰN : ∀{N} → Blame M → (F ⟦ M ⟧ —→ N)
       → 𝒫′ ⊢ᵒ ▷ᵒ (ℰ⟦ A ⟧ N)
    blameM⇒▷ℰN {N} isBlame FM→N =
        let eq = blame-frame FM→N in
        subst (λ N → 𝒫′ ⊢ᵒ ▷ᵒ ℰ⟦ A ⟧ N) (sym eq) (monoᵒ ℰ-blame)
```

The `ℰ-bind` lemma follows as a corollary of `ℰ-bind-aux`.

```
ℰ-bind : ∀{𝒫}{A}{B}{F}{M}
   → 𝒫 ⊢ᵒ ℰ⟦ B ⟧ M
   → 𝒫 ⊢ᵒ (∀ᵒ[ V ] (M —↠ V)ᵒ →ᵒ 𝒱⟦ B ⟧ V →ᵒ ℰ⟦ A ⟧ (F ⟦ V ⟧))
     ----------------------------------------------------------
   → 𝒫 ⊢ᵒ ℰ⟦ A ⟧ (F ⟦ M ⟧)
ℰ-bind {𝒫}{A}{B}{F}{M} ⊢ℰM ⊢𝒱V→ℰFV =
  appᵒ (appᵒ (instᵒ{𝒫}{P = λ M → ℰ-bind-M A B F M} ℰ-bind-aux M) ⊢ℰM) ⊢𝒱V→ℰFV
```

## More Compatibility Lemmas

The next compatibility lemma to prove is the one for function
application.  For that we'll need the following elimination lemma for
a value `V` in `𝒱⟦ A ⇒ B ⟧`.

```
safe-body : List Setᵒ → Term → Type → Type → Set
safe-body 𝒫 N A B = ∀{W} → 𝒫 ⊢ᵒ (▷ᵒ (𝒱⟦ A ⟧ W)) →ᵒ (▷ᵒ (ℰ⟦ B ⟧ (N [ W ])))

𝒱-fun-elim : ∀{𝒫}{A}{B}{V}{R}
   → 𝒫 ⊢ᵒ 𝒱⟦ A ⇒ B ⟧ V
   → (∀ N → V ≡ ƛ N → safe-body 𝒫 N A B → 𝒫 ⊢ᵒ R)
    ------------------------------------------------
   → 𝒫 ⊢ᵒ R
𝒱-fun-elim {𝒫}{A}{B}{V}{R} ⊢𝒱V cont =
  ⊢ᵒ-sucP ⊢𝒱V λ { 𝒱Vsn → G {V} 𝒱Vsn ⊢𝒱V cont}
  where
  G : ∀{V}{n}
     → # (𝒱⟦ A ⇒ B ⟧ V) (suc n)
     → 𝒫 ⊢ᵒ 𝒱⟦ A ⇒ B ⟧ V
     → (∀ N → V ≡ ƛ N → safe-body 𝒫 N A B → 𝒫 ⊢ᵒ R)
     → 𝒫 ⊢ᵒ R
  G{ƛ N}{n} 𝒱V ⊢𝒱V cont = cont N refl λ {W} →
      instᵒ{P = λ W → (▷ᵒ (𝒱⟦ A ⟧ W)) →ᵒ (▷ᵒ (ℰ⟦ B ⟧ (N [ W ])))}
                 (substᵒ 𝒱-fun ⊢𝒱V) W
```

The proof of compatibility for application, given below, starts with
two uses of the `ℰ-bind` lemma, once for subexpression `L` and again
for `M`.  So we obtain that `L` reduces to value `V` and `M` reduces
to `W` and that `𝒱⟦ A ⇒ B ⟧ V` and `𝒱⟦ A ⟧ W`.  At this point, our
goal is to show that `ℰ⟦ B ⟧ (V · W)`.  Next we use the elimination
lemma on `𝒱⟦ A ⇒ B ⟧ V` which tells us that `V` is a lambda
abstraction `ƛ N` with a semantically safe body `N`.  We thus obtain
the `progress` part of `ℰ⟦ B ⟧ (V · W)` because `(ƛ N) · W —→ N [ W ]`.
For the preservation part, we need to show that `ℰ⟦ B ⟧ (N [ W ])`,
but that follows from `𝒱⟦ A ⟧ W` and that `N` is a semantically safe
body.

```
compatible-app : ∀{Γ}{A}{B}{L}{M}
   → Γ ⊨ L ⦂ (A ⇒ B)
   → Γ ⊨ M ⦂ A
     -------------------
   → Γ ⊨ L · M ⦂ B
compatible-app {Γ}{A}{B}{L}{M} ⊨L ⊨M γ = ⊢ℰLM
 where
 ⊢ℰLM : 𝓖⟦ Γ ⟧ γ ⊢ᵒ ℰ⟦ B ⟧ (⟪ γ ⟫ (L · M))
 ⊢ℰLM = ℰ-bind {F = □· (⟪ γ ⟫ M)} (⊨L γ) (Λᵒ[ V ] →ᵒI (→ᵒI ⊢ℰVM))
  where
  𝒫₁ = λ V → 𝒱⟦ A ⇒ B ⟧ V ∷ (⟪ γ ⟫ L —↠ V)ᵒ ∷ 𝓖⟦ Γ ⟧ γ
  ⊢ℰVM : ∀{V} → 𝒫₁ V ⊢ᵒ ℰ⟦ B ⟧ (V · ⟪ γ ⟫ M)
  ⊢ℰVM {V} = ⊢ᵒ-sucP Zᵒ λ 𝒱Vsn →
       let v = 𝒱⇒Value (A ⇒ B) V 𝒱Vsn in
       let 𝒫₁⊢ℰM : 𝒫₁ V ⊢ᵒ ℰ⟦ A ⟧ (⟪ γ ⟫ M)
           𝒫₁⊢ℰM = Sᵒ (Sᵒ (⊨M γ)) in
       ℰ-bind {F = v ·□} 𝒫₁⊢ℰM (Λᵒ[ V ] →ᵒI (→ᵒI ⊢ℰVW))
   where
   𝒫₂ = λ V W → 𝒱⟦ A ⟧ W ∷ (⟪ γ ⟫ M —↠ W)ᵒ ∷ 𝒱⟦ A ⇒ B ⟧ V ∷ (⟪ γ ⟫ L —↠ V)ᵒ
                 ∷ 𝓖⟦ Γ ⟧ γ
   ⊢ℰVW : ∀{V W} → 𝒫₂ V W ⊢ᵒ ℰ⟦ B ⟧ (V · W)
   ⊢ℰVW {V}{W} =
     let ⊢𝒱V : 𝒫₂ V W ⊢ᵒ 𝒱⟦ A ⇒ B ⟧ V
         ⊢𝒱V = Sᵒ (Sᵒ Zᵒ) in
     let ⊢𝒱W : 𝒫₂ V W ⊢ᵒ 𝒱⟦ A ⟧ W
         ⊢𝒱W = Zᵒ in
     ⊢ᵒ-sucP ⊢𝒱W λ 𝒱Wsn →
     let w = 𝒱⇒Value A W 𝒱Wsn in
     𝒱-fun-elim ⊢𝒱V λ {N′ refl 𝒱W→ℰNW →
     let prog : 𝒫₂ (ƛ N′) W ⊢ᵒ progress B (ƛ N′ · W)
         prog = (inj₂ᵒ (inj₁ᵒ (constᵒI (_ , (β w))))) in
     let pres : 𝒫₂ (ƛ N′) W ⊢ᵒ preservation B (ƛ N′ · W)
         pres = Λᵒ[ N ] →ᵒI (constᵒE Zᵒ λ {r →
                let ⊢▷ℰN′W = appᵒ 𝒱W→ℰNW (monoᵒ ⊢𝒱W) in
                let eq = deterministic r (β w) in
                ⊢ᵒ-weaken (subst (λ N → 𝒫₂ (ƛ N′) W ⊢ᵒ ▷ᵒ ℰ⟦ B ⟧ N)
                                 (sym eq) ⊢▷ℰN′W)}) in
     ℰ-intro prog pres
     }
```

The compability lemma for an injection cast also begins with applying
the bind lemma to subexpression `M`, taking us from `ℰ⟦ gnd⇒ty G ⟧ M`
to `𝒱⟦ gnd⇒ty G ⟧ V`. This also gives us that `V` is a syntactic
value via `𝒱⇒Value`. So we have `𝒱⟦ ★ ⟧ (V ⟨ G !⟩)` and then
conclude using `𝒱⇒ℰ`.

```
compatible-inject : ∀{Γ}{G}{M}
  → Γ ⊨ M ⦂ gnd⇒ty G
    --------------------
  → Γ ⊨ M ⟨ G !⟩ ⦂ ★
compatible-inject {Γ}{G}{M} ⊨M γ = ℰMg!
 where
 ℰMg! : 𝓖⟦ Γ ⟧ γ ⊢ᵒ ℰ⟦ ★ ⟧ ((⟪ γ ⟫ M) ⟨ G !⟩)
 ℰMg! = ℰ-bind {F = □⟨ G !⟩} (⊨M γ) (Λᵒ[ V ] →ᵒI (→ᵒI ⊢ℰVg!))
  where
  𝒫₁ = λ V → 𝒱⟦ gnd⇒ty G ⟧ V ∷ (⟪ γ ⟫ M —↠ V)ᵒ ∷ 𝓖⟦ Γ ⟧ γ
  ⊢ℰVg! : ∀{V} → 𝒫₁ V ⊢ᵒ ℰ⟦ ★ ⟧ (V ⟨ G !⟩)
  ⊢ℰVg!{V} =
   ⊢ᵒ-sucP Zᵒ λ 𝒱Vsn →
   let v = 𝒱⇒Value (gnd⇒ty G) V 𝒱Vsn in
   𝒱⇒ℰ (substᵒ (≡ᵒ-sym 𝒱-dyn) (constᵒI v ,ᵒ monoᵒ Zᵒ))
```

The last compatibility lemma is for a projection cast.
Here we also need an elimination lemma, this time for
a value `V` of type `★`.

```
𝒱-dyn-elim : ∀{𝒫}{V}{R}
   → 𝒫 ⊢ᵒ 𝒱⟦ ★ ⟧ V
   → (∀ W G → V ≡ W ⟨ G !⟩
             → 𝒫 ⊢ᵒ ((Value W)ᵒ ×ᵒ ▷ᵒ (𝒱⟦ gnd⇒ty G ⟧ W))
             → 𝒫 ⊢ᵒ R)
     ----------------------------------------------
   → 𝒫 ⊢ᵒ R
𝒱-dyn-elim {𝒫}{V}{R} ⊢𝒱V cont =
  ⊢ᵒ-sucP ⊢𝒱V λ { 𝒱Vsn → G 𝒱Vsn ⊢𝒱V cont }
  where
  G : ∀{V}{n}
      → # (𝒱⟦ ★ ⟧ V) (suc n)
      → 𝒫 ⊢ᵒ 𝒱⟦ ★ ⟧ V
      → (∀ W G → V ≡ W ⟨ G !⟩
               → 𝒫 ⊢ᵒ ((Value W)ᵒ ×ᵒ ▷ᵒ (𝒱⟦ gnd⇒ty G ⟧ W))
               → 𝒫 ⊢ᵒ R)
      → 𝒫 ⊢ᵒ R
  G {W ⟨ G !⟩}{n} 𝒱Vsn ⊢𝒱V cont
      with 𝒱⇒Value ★ (W ⟨ G !⟩) 𝒱Vsn
  ... | w 〈 _ 〉 =
      let ⊢▷𝒱W = proj₂ᵒ (substᵒ (𝒱-dyn{V = W}) ⊢𝒱V) in
      cont W _ refl (constᵒI w ,ᵒ ⊢▷𝒱W)
```

The compatibility lemma for a projection `M ⟨ H ?⟩` begins by using
`ℰ-bind` on the subexpression `M` to obtain a value `V` where
`⟪ γ ⟫ M —↠ V` and `𝒱⟦ ★ ⟧ V`. We then apply lemma `𝒱-dyn-elim`
to compose `V` into an injection `W ⟨ G !⟩` of a value `W`
where `▷ᵒ 𝒱⟦ G ⟧ W`. We need to show `ℰ⟦ H ⟧ (W ⟨ G !⟩ ⟨ H ?⟩)`.
The progress part comes from showing that it reduces to `W`
(if `G ≡ H`) or to `blame`. The preservation part is from
`▷ᵒ 𝒱⟦ G ⟧ W` (in the `G ≡ H` case) or because `ℰ⟦ H ⟧ blame`.

```
compatible-project : ∀{Γ}{H}{M}
  → Γ ⊨ M ⦂ ★
    -----------------------------
  → Γ ⊨ M ⟨ H ?⟩ ⦂ gnd⇒ty H
compatible-project {Γ}{H}{M} ⊨M γ = ℰMh?
 where
 ℰMh? : 𝓖⟦ Γ ⟧ γ ⊢ᵒ ℰ⟦ gnd⇒ty H ⟧ ((⟪ γ ⟫ M) ⟨ H ?⟩)
 ℰMh? = ℰ-bind {F = □⟨ H ?⟩} (⊨M γ) (Λᵒ[ V ] →ᵒI (→ᵒI ⊢ℰVh?))
  where
  𝒫₁ = λ V → 𝒱⟦ ★ ⟧ V ∷ (⟪ γ ⟫ M —↠ V)ᵒ ∷ 𝓖⟦ Γ ⟧ γ
  ⊢ℰVh? : ∀{V} → 𝒫₁ V ⊢ᵒ ℰ⟦ gnd⇒ty H ⟧ (V ⟨ H ?⟩)
  ⊢ℰVh?{V} =
   let ⊢𝒱V : 𝒫₁ V ⊢ᵒ 𝒱⟦ ★ ⟧ V
       ⊢𝒱V = Zᵒ in
   𝒱-dyn-elim ⊢𝒱V λ { W G refl ⊢w×▷𝒱W →
   let ⊢w = proj₁ᵒ ⊢w×▷𝒱W in
   let ▷𝒱W = proj₂ᵒ ⊢w×▷𝒱W in
   ⊢ᵒ-sucP ⊢w λ{n} w →
   let prog : 𝒫₁ (W ⟨ G !⟩) ⊢ᵒ progress (gnd⇒ty H) ((W ⟨ G !⟩) ⟨ H ?⟩)
       prog = inj₂ᵒ (inj₁ᵒ (constᵒI (reduce-inj-proj w))) in
   let pres : 𝒫₁ (W ⟨ G !⟩) ⊢ᵒ preservation (gnd⇒ty H)((W ⟨ G !⟩) ⟨ H ?⟩)
       pres = Λᵒ[ N ] →ᵒI (constᵒE Zᵒ λ r → ⊢ᵒ-weaken (Goal r w ▷𝒱W)) in
   ℰ-intro prog pres
   }
    where
    reduce-inj-proj : ∀{G}{H}{W} → Value W → reducible ((W ⟨ G !⟩) ⟨ H ?⟩)
    reduce-inj-proj {G} {H} {W} w
        with G ≡ᵍ H
    ... | yes refl = W , (collapse w  refl)
    ... | no neq = blame , (collide w neq refl)
    
    Goal : ∀{W}{G}{H}{N}
       → (W ⟨ G !⟩ ⟨ H ?⟩) —→ N
       → Value W
       → 𝒫₁ (W ⟨ G !⟩) ⊢ᵒ ▷ᵒ 𝒱⟦ gnd⇒ty G ⟧ W
       → 𝒫₁ (W ⟨ G !⟩) ⊢ᵒ ▷ᵒ ℰ⟦ gnd⇒ty H ⟧ N
    Goal (ξξ □⟨ H ?⟩ refl refl r) w ▷𝒱W =
        ⊥-elim (value-irreducible (w 〈 _ 〉) r)
    Goal {W} (ξξ-blame □⟨ H ?⟩ ())
    Goal {W}{G}{G}{W} (collapse{H} w′ refl) w ▷𝒱W =
       ▷→▷ ▷𝒱W (𝒱⇒ℰ Zᵒ)
    Goal {W} (collide x x₁ x₂) w ▷𝒱W = monoᵒ ℰ-blame
```

## Fundamental Lemma

The Fundamental Lemma states that a syntactically well-typed term is
also a semantically well-typed term. Or given how we have defined the
logical relations, it means that a well-typed term satisfies progress
and preservation.

```
fundamental : ∀ {Γ A} → (M : Term)
  → Γ ⊢ M ⦂ A
    ----------
  → Γ ⊨ M ⦂ A
fundamental {Γ} {A} .(` _) (⊢` ∋x) =
    compatibility-var ∋x
fundamental {Γ} {.($ₜ ′ℕ)} .($ (Num _)) (⊢$ (Num n)) =
    compatible-nat
fundamental {Γ} {.($ₜ ′𝔹)} .($ (Bool _)) (⊢$ (Bool b)) =
    compatible-bool
fundamental {Γ} {A} (L · M) (⊢· ⊢L ⊢M) =
    compatible-app{L = L}{M} (fundamental L ⊢L) (fundamental M ⊢M)
fundamental {Γ} {.(_ ⇒ _)} (ƛ N) (⊢ƛ ⊢N) =
    compatible-lambda {N = N} (fundamental N ⊢N)
fundamental {Γ} {.★} (M ⟨ G !⟩) (⊢⟨!⟩ ⊢M) =
    compatible-inject {M = M} (fundamental M ⊢M)
fundamental {Γ} {A} (M ⟨ H ?⟩) (⊢⟨?⟩ ⊢M H) =
    compatible-project {M = M} (fundamental M ⊢M)
fundamental {Γ} {A} .blame ⊢blame = compatible-blame
```

## Proof of Type Safety

For the Type Safety theorem, we need to consider multi-step reduction.
So we first prove the following lemma which states that if
`M —↠ N` and `M` is in `ℰ⟦ A ⟧`, then `N` satisfies progress.
The lemma is by induction on the multi-step reduction, using
the preservation part of `ℰ⟦ A ⟧` at each step.

```
sem-type-safety : ∀ {A} → (M N : Term)
  → (r : M —↠ N)
  → # (ℰ⟦ A ⟧ M) (suc (len r))
    ---------------------------------------------
  → Value N  ⊎  (∃[ N′ ] (N —→ N′))  ⊎  N ≡ blame   
sem-type-safety {A} M .M (.M END) (inj₁ 𝒱M , presM) =
    inj₁ (𝒱⇒Value A M 𝒱M)
sem-type-safety {A} M .M (.M END) (inj₂ (inj₁ r) , presM) =
    inj₂ (inj₁ r)
sem-type-safety {A} M .M (.M END) (inj₂ (inj₂ isBlame) , presM) =
    inj₂ (inj₂ refl)
sem-type-safety {A} M N (_—→⟨_⟩_ .M {M′} M→M′ M′→N) (_ , presM) =
    let ℰM′ : # (ℰ⟦ A ⟧ M′) (suc (len M′→N))
        ℰM′ = presM M′ (suc (suc (len M′→N))) ≤-refl M→M′ in
    sem-type-safety M′ N M′→N ℰM′
```

The Type Safety theorem is then a corollary of the Fundamental Lemma
together with the above lemma regarding multi-step reduction.

```
type-safety : ∀ {A} → (M N : Term)
  → [] ⊢ M ⦂ A
  → M —↠ N
    ---------------------------------------------
  → Value N  ⊎  (∃[ N′ ] (N —→ N′))  ⊎  N ≡ blame   
type-safety M N ⊢M M→N =
  let ℰM = ⊢ᵒ-elim ((fundamental M ⊢M) id) (suc (len M→N)) tt in
  sem-type-safety M N M→N ℰM 
```