<commit_before>---
title     : "Properties: Progress and Preservation"
layout    : page
prev      : /Lambda/
permalink : /Properties/
next      : /DeBruijn/
---

```
module plfa.part2.Properties where
```

This chapter covers properties of the simply-typed lambda calculus, as
introduced in the previous chapter.  The most important of these
properties are progress and preservation.  We introduce these below,
and show how to combine them to get Agda to compute reduction
sequences for us.


## Imports

```
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product
  using (_×_; proj₁; proj₂; ∃; ∃-syntax)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Function using (_∘_)
open import plfa.part1.Isomorphism
open import plfa.part2.Lambda
```


## Introduction

The last chapter introduced simply-typed lambda calculus,
including the notions of closed terms, terms that are values,
reducing one term to another, and well-typed terms.

Ultimately, we would like to show that we can keep reducing a term
until we reach a value.  For instance, in the last chapter we showed
that two plus two is four,

    plus · two · two  —↠  `suc `suc `suc `suc `zero

which was proved by a long chain of reductions, ending in the value
on the right.  Every term in the chain had the same type, `` `ℕ ``.
We also saw a second, similar example involving Church numerals.

What we might expect is that every term is either a value or can take
a reduction step.  As we will see, this property does _not_ hold for
every term, but it does hold for every closed, well-typed term.

_Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such
that `M —→ N`.

So, either we have a value, and we are done, or we can take a reduction step.
In the latter case, we would like to apply progress again. But to do so we need
to know that the term yielded by the reduction is itself closed and well typed.
It turns out that this property holds whenever we start with a closed,
well-typed term.

_Preservation_: If `∅ ⊢ M ⦂ A` and `M —→ N` then `∅ ⊢ N ⦂ A`.

This gives us a recipe for automating evaluation. Start with a closed
and well-typed term.  By progress, it is either a value, in which case
we are done, or it reduces to some other term.  By preservation, that
other term will itself be closed and well typed.  Repeat.  We will
either loop forever, in which case evaluation does not terminate, or
we will eventually reach a value, which is guaranteed to be closed and
of the same type as the original term.  We will turn this recipe into
Agda code that can compute for us the reduction sequence of `plus · two · two`,
and its Church numeral variant.

(The development in this chapter was inspired by the corresponding
development in _Software Foundations_, Volume _Programming Language
Foundations_, Chapter _StlcProp_.  It will turn out that one of our technical choices
— to introduce an explicit judgment `Γ ∋ x ⦂ A` in place of
treating a context as a function from identifiers to types —
permits a simpler development. In particular, we can prove substitution preserves
types without needing to develop a separate inductive definition of the
`appears_free_in` relation.)


## Values do not reduce

We start with an easy observation. Values do not reduce:
```
V¬—→ : ∀ {M N}
  → Value M
    ----------
  → ¬ (M —→ N)
V¬—→ V-ƛ        ()
V¬—→ V-zero     ()
V¬—→ (V-suc VM) (ξ-suc M—→N) = V¬—→ VM M—→N
```
We consider the three possibilities for values:

* If it is an abstraction then no reduction applies

* If it is zero then no reduction applies

* If it is a successor then rule `ξ-suc` may apply,
  but in that case the successor is itself of a value
  that reduces, which by induction cannot occur.

As a corollary, terms that reduce are not values:
```
—→¬V : ∀ {M N}
  → M —→ N
    ---------
  → ¬ Value M
—→¬V M—→N VM  =  V¬—→ VM M—→N
```
If we expand out the negations, we have

    V¬—→ : ∀ {M N} → Value M → M —→ N → ⊥
    —→¬V : ∀ {M N} → M —→ N → Value M → ⊥

which are the same function with the arguments swapped.


#### Exercise `Canonical-≃` (practice)

Well-typed values must take one of a small number of _canonical forms_,
which provide an analogue of the `Value` relation that relates values
to their types.  A lambda expression must have a function type,
and a zero or successor expression must be a natural.
Further, the body of a function must be well typed in a context
containing only its bound variable, and the argument of successor
must itself be canonical:
```
infix  4 Canonical_⦂_

data Canonical_⦂_ : Term → Type → Set where

  C-ƛ : ∀ {x A N B}
    → ∅ , x ⦂ A ⊢ N ⦂ B
      -----------------------------
    → Canonical (ƛ x ⇒ N) ⦂ (A ⇒ B)

  C-zero :
      --------------------
      Canonical `zero ⦂ `ℕ

  C-suc : ∀ {V}
    → Canonical V ⦂ `ℕ
      ---------------------
    → Canonical `suc V ⦂ `ℕ
```

Show that `Canonical V ⦂ A` is isomorphic to `(∅ ⊢ V ⦂ A) × (Value V)`,
that is, the canonical forms are exactly the well-typed values.

```
-- Your code goes here
```

## Progress

We would like to show that every term is either a value or takes a
reduction step.  However, this is not true in general.  The term

    `zero · `suc `zero

is neither a value nor can take a reduction step. And if `` s ⦂ `ℕ ⇒ `ℕ ``
then the term

     s · `zero

cannot reduce because we do not know which function is bound to the
free variable `s`.  The first of those terms is ill typed, and the
second has a free variable.  Every term that is well typed and closed
has the desired property.

_Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such
that `M —→ N`.

To formulate this property, we first introduce a relation that
captures what it means for a term `M` to make progress:
```
data Progress (M : Term) : Set where

  step : ∀ {N}
    → M —→ N
      ----------
    → Progress M

  done :
      Value M
      ----------
    → Progress M
```
A term `M` makes progress if either it can take a step, meaning there
exists a term `N` such that `M —→ N`, or if it is done, meaning that
`M` is a value.

If a term is well typed in the empty context then it satisfies progress:
```
progress : ∀ {M A}
  → ∅ ⊢ M ⦂ A
    ----------
  → Progress M
progress (⊢` ())
progress (⊢ƛ ⊢N)                            =  done V-ƛ
progress (⊢L · ⊢M) with progress ⊢L
... | step L—→L′                            =  step (ξ-·₁ L—→L′)
... | done V-ƛ with progress ⊢M
...   | step M—→M′                          =  step (ξ-·₂ V-ƛ M—→M′)
...   | done VM                             =  step (β-ƛ VM)
progress ⊢zero                              =  done V-zero
progress (⊢suc ⊢M) with progress ⊢M
...  | step M—→M′                           =  step (ξ-suc M—→M′)
...  | done VM                              =  done (V-suc VM)
progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L
... | step L—→L′                            =  step (ξ-case L—→L′)
... | done (V-zero)                         =  step β-zero
... | done (V-suc VL)                       =  step (β-suc VL)
progress (⊢μ ⊢M)                            =  step β-μ
```
We induct on the evidence that the term is well typed.
Let's unpack the first three cases:

* The term cannot be a variable, since no variable is well typed
  in the empty context.

* If the term is a lambda abstraction then it is a value.

* If the term is an application `L · M`, recursively apply
  progress to the derivation that `L` is well typed:

  + If the term steps, we have evidence that `L —→ L′`,
    which by `ξ-·₁` means that our original term steps
    to `L′ · M`

  + If the term is done, we have evidence that `L` is
    a value, which must be a lambda abstraction.
    Recursively apply progress to the derivation
    that `M` is well typed:

    - If the term steps, we have evidence that `M —→ M′`,
      which by `ξ-·₂` means that our original term steps
      to `L · M′`.  Step `ξ-·₂` applies only if we have
      evidence that `L` is a value, but progress on that
      subterm has already supplied the required evidence.

    - If the term is done, we have evidence that `M` is
      a value, so our original term steps by `β-ƛ`.

The remaining cases are similar.  If by induction we have a
`step` case we apply a `ξ` rule, and if we have a `done` case
then either we have a value or apply a `β` rule.  For fixpoint,
no induction is required as the `β` rule applies immediately.

Our code reads neatly in part because we consider the
`step` option before the `done` option. We could, of course,
do it the other way around, but then the `...` abbreviation
no longer works, and we will need to write out all the arguments
in full. In general, the rule of thumb is to consider the easy case
(here `step`) before the hard case (here `done`).
If you have two hard cases, you will have to expand out `...`
or introduce subsidiary functions.

Instead of defining a data type for `Progress M`, we could
have formulated progress using disjunction and existentials:
```
postulate
  progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M —→ N)
```
This leads to a less perspicuous proof.  Instead of the mnemonic `done`
and `step` we use `inj₁` and `inj₂`, and the term `N` is no longer
implicit and so must be written out in full.  In the case for `β-ƛ`
this requires that we match against the lambda expression `L` to
determine its bound variable and body, `ƛ x ⇒ N`, so we can show that
`L · M` reduces to `N [ x := M ]`.

#### Exercise `Progress-≃` (practice)

Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.

```
-- Your code goes here
```

#### Exercise `progress′` (practice)

Write out the proof of `progress′` in full, and compare it to the
proof of `progress` above.

```
-- Your code goes here
```

#### Exercise `value?` (practice)

Combine `progress` and `—→¬V` to write a program that decides
whether a well-typed term is a value:
```
postulate
  value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)
```

## Prelude to preservation

The other property we wish to prove, preservation of typing under
reduction, turns out to require considerably more work.  The proof has
three key steps.

The first step is to show that types are preserved by _renaming_.

_Renaming_:
Let `Γ` and `Δ` be two contexts such that every variable that
appears in `Γ` also appears with the same type in `Δ`.  Then
if any term is typeable under `Γ`, it has the same type under `Δ`.

In symbols:

    ∀ {x A} → Γ ∋ x ⦂ A  →  Δ ∋ x ⦂ A
    ---------------------------------
    ∀ {M A} → Γ ⊢ M ⦂ A  →  Δ ⊢ M ⦂ A

Three important corollaries follow.  The _weaken_ lemma asserts that a term
which is well typed in the empty context is also well typed in an arbitrary
context.  The _drop_ lemma asserts that a term which is well typed in a context
where the same variable appears twice remains well typed if we drop the shadowed
occurrence. The _swap_ lemma asserts that a term which is well typed in a
context remains well typed if we swap two variables.

(Renaming is similar to the _context invariance_ lemma in _Software
Foundations_, but it does not require the definition of
`appears_free_in` nor the `free_in_context` lemma.)

The second step is to show that types are preserved by
_substitution_.

_Substitution_:
Say we have a closed term `V` of type `A`, and under the
assumption that `x` has type `A` the term `N` has type `B`.
Then substituting `V` for `x` in `N` yields a term that
also has type `B`.

In symbols:

    ∅ ⊢ V ⦂ A
    Γ , x ⦂ A ⊢ N ⦂ B
    --------------------
    Γ ⊢ N [ x := V ] ⦂ B

The result does not depend on `V` being a value, but it does
require that `V` be closed; recall that we restricted our attention
to substitution by closed terms in order to avoid the need to
rename bound variables.  The term into which we are substituting
is typed in an arbitrary context `Γ`, extended by the variable
`x` for which we are substituting; and the result term is typed
in `Γ`.

The lemma establishes that substitution composes well with typing:
typing the components separately guarantees that the result of
combining them is also well typed.

The third step is to show preservation.

_Preservation_:
If `∅ ⊢ M ⦂ A` and `M —→ N` then `∅ ⊢ N ⦂ A`.

The proof is by induction over the possible reductions, and
the substitution lemma is crucial in showing that each of the
`β` rules that uses substitution preserves types.

We now proceed with our three-step programme.


## Renaming

We often need to "rebase" a type derivation, replacing a derivation
`Γ ⊢ M ⦂ A` by a related derivation `Δ ⊢ M ⦂ A`.  We may do so as long
as every variable that appears in `Γ` also appears in `Δ`, and with
the same type.

Three of the rules for typing (lambda abstraction, case on naturals,
and fixpoint) have hypotheses that extend the context to include a
bound variable. In each of these rules, `Γ` appears in the conclusion
and `Γ , x ⦂ A` appears in a hypothesis.  Thus:

    Γ , x ⦂ A ⊢ N ⦂ B
    ------------------- ⊢ƛ
    Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B

for lambda expressions, and similarly for case and fixpoint.  To deal
with this situation, we first prove a lemma showing that if one context maps to another,
this is still true after adding the same variable to
both contexts:
```
ext : ∀ {Γ Δ}
  → (∀ {x A}     →         Γ ∋ x ⦂ A →         Δ ∋ x ⦂ A)
    -----------------------------------------------------
  → (∀ {x y A B} → Γ , y ⦂ B ∋ x ⦂ A → Δ , y ⦂ B ∋ x ⦂ A)
ext ρ Z           =  Z
ext ρ (S x≢y ∋x)  =  S x≢y (ρ ∋x)
```
Let `ρ` be the name of the map that takes evidence that
`x` appears in `Γ` to evidence that `x` appears in `Δ`.
The proof is by case analysis of the evidence that `x` appears
in the extended map `Γ , y ⦂ B`:

* If `x` is the same as `y`, we used `Z` to access the last variable
in the extended `Γ`; and can similarly use `Z` to access the last
variable in the extended `Δ`.

* If `x` differs from `y`, then we used `S` to skip over the last
variable in the extended `Γ`, where `x≢y` is evidence that `x` and `y`
differ, and `∋x` is the evidence that `x` appears in `Γ`; and we can
similarly use `S` to skip over the last variable in the extended `Δ`,
applying `ρ` to find the evidence that `x` appears in `Δ`.

With the extension lemma under our belts, it is straightforward to
prove renaming preserves types:
```
rename : ∀ {Γ Δ}
  → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
    ----------------------------------
  → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename ρ (⊢` ∋w)           =  ⊢` (ρ ∋w)
rename ρ (⊢ƛ ⊢N)           =  ⊢ƛ (rename (ext ρ) ⊢N)
rename ρ (⊢L · ⊢M)         =  (rename ρ ⊢L) · (rename ρ ⊢M)
rename ρ ⊢zero             =  ⊢zero
rename ρ (⊢suc ⊢M)         =  ⊢suc (rename ρ ⊢M)
rename ρ (⊢case ⊢L ⊢M ⊢N)  =  ⊢case (rename ρ ⊢L) (rename ρ ⊢M) (rename (ext ρ) ⊢N)
rename ρ (⊢μ ⊢M)           =  ⊢μ (rename (ext ρ) ⊢M)
```
As before, let `ρ` be the name of the map that takes evidence that
`x` appears in `Γ` to evidence that `x` appears in `Δ`.  We induct
on the evidence that `M` is well typed in `Γ`.  Let's unpack the<commit_msg>Properties: fix typo<commit_after>---
title     : "Properties: Progress and Preservation"
layout    : page
prev      : /Lambda/
permalink : /Properties/
next      : /DeBruijn/
---

```
module plfa.part2.Properties where
```

This chapter covers properties of the simply-typed lambda calculus, as
introduced in the previous chapter.  The most important of these
properties are progress and preservation.  We introduce these below,
and show how to combine them to get Agda to compute reduction
sequences for us.


## Imports

```
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product
  using (_×_; proj₁; proj₂; ∃; ∃-syntax)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Function using (_∘_)
open import plfa.part1.Isomorphism
open import plfa.part2.Lambda
```


## Introduction

The last chapter introduced simply-typed lambda calculus,
including the notions of closed terms, terms that are values,
reducing one term to another, and well-typed terms.

Ultimately, we would like to show that we can keep reducing a term
until we reach a value.  For instance, in the last chapter we showed
that two plus two is four,

    plus · two · two  —↠  `suc `suc `suc `suc `zero

which was proved by a long chain of reductions, ending in the value
on the right.  Every term in the chain had the same type, `` `ℕ ``.
We also saw a second, similar example involving Church numerals.

What we might expect is that every term is either a value or can take
a reduction step.  As we will see, this property does _not_ hold for
every term, but it does hold for every closed, well-typed term.

_Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such
that `M —→ N`.

So, either we have a value, and we are done, or we can take a reduction step.
In the latter case, we would like to apply progress again. But to do so we need
to know that the term yielded by the reduction is itself closed and well typed.
It turns out that this property holds whenever we start with a closed,
well-typed term.

_Preservation_: If `∅ ⊢ M ⦂ A` and `M —→ N` then `∅ ⊢ N ⦂ A`.

This gives us a recipe for automating evaluation. Start with a closed
and well-typed term.  By progress, it is either a value, in which case
we are done, or it reduces to some other term.  By preservation, that
other term will itself be closed and well typed.  Repeat.  We will
either loop forever, in which case evaluation does not terminate, or
we will eventually reach a value, which is guaranteed to be closed and
of the same type as the original term.  We will turn this recipe into
Agda code that can compute for us the reduction sequence of `plus · two · two`,
and its Church numeral variant.

(The development in this chapter was inspired by the corresponding
development in _Software Foundations_, Volume _Programming Language
Foundations_, Chapter _StlcProp_.  It will turn out that one of our technical choices
— to introduce an explicit judgment `Γ ∋ x ⦂ A` in place of
treating a context as a function from identifiers to types —
permits a simpler development. In particular, we can prove substitution preserves
types without needing to develop a separate inductive definition of the
`appears_free_in` relation.)


## Values do not reduce

We start with an easy observation. Values do not reduce:
```
V¬—→ : ∀ {M N}
  → Value M
    ----------
  → ¬ (M —→ N)
V¬—→ V-ƛ        ()
V¬—→ V-zero     ()
V¬—→ (V-suc VM) (ξ-suc M—→N) = V¬—→ VM M—→N
```
We consider the three possibilities for values:

* If it is an abstraction then no reduction applies

* If it is zero then no reduction applies

* If it is a successor then rule `ξ-suc` may apply,
  but in that case the successor is itself of a value
  that reduces, which by induction cannot occur.

As a corollary, terms that reduce are not values:
```
—→¬V : ∀ {M N}
  → M —→ N
    ---------
  → ¬ Value M
—→¬V M—→N VM  =  V¬—→ VM M—→N
```
If we expand out the negations, we have

    V¬—→ : ∀ {M N} → Value M → M —→ N → ⊥
    —→¬V : ∀ {M N} → M —→ N → Value M → ⊥

which are the same function with the arguments swapped.


#### Exercise `Canonical-≃` (practice)

Well-typed values must take one of a small number of _canonical forms_,
which provide an analogue of the `Value` relation that relates values
to their types.  A lambda expression must have a function type,
and a zero or successor expression must be a natural.
Further, the body of a function must be well typed in a context
containing only its bound variable, and the argument of successor
must itself be canonical:
```
infix  4 Canonical_⦂_

data Canonical_⦂_ : Term → Type → Set where

  C-ƛ : ∀ {x A N B}
    → ∅ , x ⦂ A ⊢ N ⦂ B
      -----------------------------
    → Canonical (ƛ x ⇒ N) ⦂ (A ⇒ B)

  C-zero :
      --------------------
      Canonical `zero ⦂ `ℕ

  C-suc : ∀ {V}
    → Canonical V ⦂ `ℕ
      ---------------------
    → Canonical `suc V ⦂ `ℕ
```

Show that `Canonical V ⦂ A` is isomorphic to `(∅ ⊢ V ⦂ A) × (Value V)`,
that is, the canonical forms are exactly the well-typed values.

```
-- Your code goes here
```

## Progress

We would like to show that every term is either a value or takes a
reduction step.  However, this is not true in general.  The term

    `zero · `suc `zero

is neither a value nor can take a reduction step. And if `` s ⦂ `ℕ ⇒ `ℕ ``
then the term

     s · `zero

cannot reduce because we do not know which function is bound to the
free variable `s`.  The first of those terms is ill typed, and the
second has a free variable.  Every term that is well typed and closed
has the desired property.

_Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such
that `M —→ N`.

To formulate this property, we first introduce a relation that
captures what it means for a term `M` to make progress:
```
data Progress (M : Term) : Set where

  step : ∀ {N}
    → M —→ N
      ----------
    → Progress M

  done :
      Value M
      ----------
    → Progress M
```
A term `M` makes progress if either it can take a step, meaning there
exists a term `N` such that `M —→ N`, or if it is done, meaning that
`M` is a value.

If a term is well typed in the empty context then it satisfies progress:
```
progress : ∀ {M A}
  → ∅ ⊢ M ⦂ A
    ----------
  → Progress M
progress (⊢` ())
progress (⊢ƛ ⊢N)                            =  done V-ƛ
progress (⊢L · ⊢M) with progress ⊢L
... | step L—→L′                            =  step (ξ-·₁ L—→L′)
... | done V-ƛ with progress ⊢M
...   | step M—→M′                          =  step (ξ-·₂ V-ƛ M—→M′)
...   | done VM                             =  step (β-ƛ VM)
progress ⊢zero                              =  done V-zero
progress (⊢suc ⊢M) with progress ⊢M
...  | step M—→M′                           =  step (ξ-suc M—→M′)
...  | done VM                              =  done (V-suc VM)
progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L
... | step L—→L′                            =  step (ξ-case L—→L′)
... | done (V-zero)                         =  step β-zero
... | done (V-suc VL)                       =  step (β-suc VL)
progress (⊢μ ⊢M)                            =  step β-μ
```
We induct on the evidence that the term is well typed.
Let's unpack the first three cases:

* The term cannot be a variable, since no variable is well typed
  in the empty context.

* If the term is a lambda abstraction then it is a value.

* If the term is an application `L · M`, recursively apply
  progress to the derivation that `L` is well typed:

  + If the term steps, we have evidence that `L —→ L′`,
    which by `ξ-·₁` means that our original term steps
    to `L′ · M`

  + If the term is done, we have evidence that `L` is
    a value, which must be a lambda abstraction.
    Recursively apply progress to the derivation
    that `M` is well typed:

    - If the term steps, we have evidence that `M —→ M′`,
      which by `ξ-·₂` means that our original term steps
      to `L · M′`.  Step `ξ-·₂` applies only if we have
      evidence that `L` is a value, but progress on that
      subterm has already supplied the required evidence.

    - If the term is done, we have evidence that `M` is
      a value, so our original term steps by `β-ƛ`.

The remaining cases are similar.  If by induction we have a
`step` case we apply a `ξ` rule, and if we have a `done` case
then either we have a value or apply a `β` rule.  For fixpoint,
no induction is required as the `β` rule applies immediately.

Our code reads neatly in part because we consider the
`step` option before the `done` option. We could, of course,
do it the other way around, but then the `...` abbreviation
no longer works, and we will need to write out all the arguments
in full. In general, the rule of thumb is to consider the easy case
(here `step`) before the hard case (here `done`).
If you have two hard cases, you will have to expand out `...`
or introduce subsidiary functions.

Instead of defining a data type for `Progress M`, we could
have formulated progress using disjunction and existentials:
```
postulate
  progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M —→ N)
```
This leads to a less perspicuous proof.  Instead of the mnemonic `done`
and `step` we use `inj₁` and `inj₂`, and the term `N` is no longer
implicit and so must be written out in full.  In the case for `β-ƛ`
this requires that we match against the lambda expression `L` to
determine its bound variable and body, `ƛ x ⇒ N`, so we can show that
`L · M` reduces to `N [ x := M ]`.

#### Exercise `Progress-≃` (practice)

Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.

```
-- Your code goes here
```

#### Exercise `progress′` (practice)

Write out the proof of `progress′` in full, and compare it to the
proof of `progress` above.

```
-- Your code goes here
```

#### Exercise `value?` (practice)

Combine `progress` and `—→¬V` to write a program that decides
whether a well-typed term is a value:
```
postulate
  value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)
```

## Prelude to preservation

The other property we wish to prove, preservation of typing under
reduction, turns out to require considerably more work.  The proof has
three key steps.

The first step is to show that types are preserved by _renaming_.

_Renaming_:
Let `Γ` and `Δ` be two contexts such that every variable that
appears in `Γ` also appears with the same type in `Δ`.  Then
if any term is typeable under `Γ`, it has the same type under `Δ`.

In symbols:

    ∀ {x A} → Γ ∋ x ⦂ A  →  Δ ∋ x ⦂ A
    ---------------------------------
    ∀ {M A} → Γ ⊢ M ⦂ A  →  Δ ⊢ M ⦂ A

Three important corollaries follow.  The _weaken_ lemma asserts that a term
which is well typed in the empty context is also well typed in an arbitrary
context.  The _drop_ lemma asserts that a term which is well typed in a context
where the same variable appears twice remains well typed if we drop the shadowed
occurrence. The _swap_ lemma asserts that a term which is well typed in a
context remains well typed if we swap two variables.

(Renaming is similar to the _context invariance_ lemma in _Software
Foundations_, but it does not require the definition of
`appears_free_in` nor the `free_in_context` lemma.)

The second step is to show that types are preserved by
_substitution_.

_Substitution_:
Say we have a closed term `V` of type `A`, and under the
assumption that `x` has type `A` the term `N` has type `B`.
Then substituting `V` for `x` in `N` yields a term that
also has type `B`.

In symbols:

    ∅ ⊢ V ⦂ A
    Γ , x ⦂ A ⊢ N ⦂ B
    --------------------
    Γ ⊢ N [ x := V ] ⦂ B

The result does not depend on `V` being a value, but it does
require that `V` be closed; recall that we restricted our attention
to substitution by closed terms in order to avoid the need to
rename bound variables.  The term into which we are substituting
is typed in an arbitrary context `Γ`, extended by the variable
`x` for which we are substituting; and the result term is typed
in `Γ`.

The lemma establishes that substitution composes well with typing:
typing the components separately guarantees that the result of
combining them is also well typed.

The third step is to show preservation.

_Preservation_:
If `∅ ⊢ M ⦂ A` and `M —→ N` then `∅ ⊢ N ⦂ A`.

The proof is by induction over the possible reductions, and
the substitution lemma is crucial in showing that each of the
`β` rules that uses substitution preserves types.

We now proceed with our three-step programme.


## Renaming

We often need to "rebase" a type derivation, replacing a derivation
`Γ ⊢ M ⦂ A` by a related derivation `Δ ⊢ M ⦂ A`.  We may do so as long
as every variable that appears in `Γ` also appears in `Δ`, and with
the same type.

Three of the rules for typing (lambda abstraction, case on naturals,
and fixpoint) have hypotheses that extend the context to include a
bound variable. In each of these rules, `Γ` appears in the conclusion
and `Γ , x ⦂ A` appears in a hypothesis.  Thus:

    Γ , x ⦂ A ⊢ N ⦂ B
    ------------------- ⊢ƛ
    Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B

for lambda expressions, and similarly for case and fixpoint.  To deal
with this situation, we first prove a lemma showing that if one context maps to another,
this is still true after adding the same variable to
both contexts:
```
ext : ∀ {Γ Δ}
  → (∀ {x A}     →         Γ ∋ x ⦂ A →         Δ ∋ x ⦂ A)
    -----------------------------------------------------
  → (∀ {x y A B} → Γ , y ⦂ B ∋ x ⦂ A → Δ , y ⦂ B ∋ x ⦂ A)
ext ρ Z           =  Z
ext ρ (S x≢y ∋x)  =  S x≢y (ρ ∋x)
```
Let `ρ` be the name of the map that takes evidence that
`x` appears in `Γ` to evidence that `x` appears in `Δ`.
The proof is by case analysis of the evidence that `x` appears
in the extended context `Γ , y ⦂ B`:

* If `x` is the same as `y`, we used `Z` to access the last variable
in the extended `Γ`; and can similarly use `Z` to access the last
variable in the extended `Δ`.

* If `x` differs from `y`, then we used `S` to skip over the last
variable in the extended `Γ`, where `x≢y` is evidence that `x` and `y`
differ, and `∋x` is the evidence that `x` appears in `Γ`; and we can
similarly use `S` to skip over the last variable in the extended `Δ`,
applying `ρ` to find the evidence that `x` appears in `Δ`.

With the extension lemma under our belts, it is straightforward to
prove renaming preserves types:
```
rename : ∀ {Γ Δ}
  → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
    ----------------------------------
  → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename ρ (⊢` ∋w)           =  ⊢` (ρ ∋w)
rename ρ (⊢ƛ ⊢N)           =  ⊢ƛ (rename (ext ρ) ⊢N)
rename ρ (⊢L · ⊢M)         =  (rename ρ ⊢L) · (rename ρ ⊢M)
rename ρ ⊢zero             =  ⊢zero
rename ρ (⊢suc ⊢M)         =  ⊢suc (rename ρ ⊢M)
rename ρ (⊢case ⊢L ⊢M ⊢N)  =  ⊢case (rename ρ ⊢L) (rename ρ ⊢M) (rename (ext ρ) ⊢N)
rename ρ (⊢μ ⊢M)           =  ⊢μ (rename (ext ρ) ⊢M)
```
As before, let `ρ` be the name of the map that takes evidence that
`x` appears in `Γ` to evidence that `x` appears in `Δ`.  We induct
on the evidence that `M` is well typed in `Γ`.  Let's unpack the
{'fraction_non_alphanumeric': 0.10920503467087318, 'fraction_numerical': 0.0002629070952052319, 'mean_word_length': 2.707810405751188, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7569956', 'n_tokens_mistral': 10569, 'n_tokens_neox': 9854, 'n_words': 5303}