FLOLAC-STLC2.agda

Intrinsically-typed de Bruijn representation of simply typed lambda calculus
============================================================================

\begin{code}
open import Data.Nat
open import Data.Empty
  hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
  hiding ([_])
\end{code}

Fixity declartion
-----------------

\begin{code}
infix  3 _⊢_ _=β_

infixr 7 _→̇_

infixr 5 ƛ_
infixl 7 _·_
infixl 8 _[_] _⟪_⟫
infixr 9 ᵒ_ `_ #_
\end{code}

Types
-----

We only deal with function types and a ground type ⋆.

\begin{code}
data Type : Set where
  ⋆   : Type
  _→̇_ : Type → Type → Type
\end{code}

Context
-------

\begin{code}
infixl 7 _⧺_
infixl 6 _,_
infix  4 _∋_

data Context : Set where
  ∅   :                  Context
  _,_ : Context → Type → Context
\end{code}

For convenience, we use symbols

  * `A`, `B`, `C` for types
  * `Γ`, `Δ`, and `Ξ` for contexts

In Agda this convention can be achieved by the keyword `variable` as follows.

\begin{code}
variable
  Γ Δ Ξ : Context
  A B C : Type
\end{code}

Membership
----------

`Γ ∋ A` means that A is a member of Γ.

There are two ways of estabilishing the judgement Γ ∋ A.

  1. `Γ , A ∋ A` for any `Γ` and `A`, as we know that `A` is in the
  0-th position.

  2. If `x : Γ ∋ A` is a proof that `A` is in `Γ`, then `Γ , B ∋ A`
     holds.

How should we name these inference rules? Note that if we interpret
the proof of `Γ ∋ A` as the position of `A` in `Γ`, then 1. should be
Z (for zero) and 2. should be S (for successor).

\begin{code}
data _∋_ : Context → Type → Set where
  Z   ---------
    : Γ , A ∋ A

  S_ : Γ     ∋ A
       ---------
     → Γ , B ∋ A

variable
  x     : Γ ∋ A
\end{code}

For example, `S Z : ∅ , A , B ∋ A` means `A` is in the first position. That is,

\begin{code}
_ : ∅ , A , B ∋ A
_ = S Z
\end{code}

Lookup is just `_‼_` in Haskell. Agda is a total language, but
`lookup` can only be partial with this type. We work around this
problem by postulating `⊥`, as we only use `lookup` for examples.

\begin{code}
⊥-elim : ∀ {T : Set} → ⊥ → T
⊥-elim ()

lookup : Context → ℕ → Type
lookup (Γ , A) zero     =  A
lookup (Γ , B) (suc n)  =  lookup Γ n
lookup ∅       _        =  ⊥-elim impossible
  where postulate impossible : ⊥
\end{code}

If `lookup Γ n` finds the element in the n-th position, then the
memberhsip proof can be produced algorithmatically. Hence we can
transform a natural number to a membership proof.

\begin{code}
count : (n : ℕ) → Γ ∋ lookup Γ n
count {Γ = Γ , _} zero     =  Z
count {Γ = Γ , _} (suc n)  =  S (count n)
count {Γ = ∅    }  _        =  ⊥-elim impossible
  where postulate impossible : ⊥
\end{code}

### Examples

\begin{code}
_ :  ∅ , A , B ∋ A
_ = count 1

_ : ∅ , B , A ∋ A
_ = count 0
\end{code}

Shifting
--------

      (Aₙ , ... , A₁, A₀)
        |    |     |   |
        ↓    ↓     ↓   ↓
    ↦ (Aₙ , ... , A₁, A₀, B)

       n+1         2   1  0

\begin{code}
ext
  : (∀ {A}   →     Γ ∋ A →     Δ ∋ A)
    ---------------------------------
  → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
ext ρ Z      =  Z
ext ρ (S x)  =  S (ρ x)
\end{code}

Concatenation
-------------

\begin{code}
_⧺_ : Context → Context → Context
Γ ⧺ ∅       = Γ
Γ ⧺ (Δ , x) = Γ ⧺ Δ , x
\end{code}

Terms = typing rules
--------------------

First off, since the typing rules for simply typed lambda calculus are
syntax-directed, we combine the term formation rules with the typing
rules.

Therefore, the typing judgement consists of only a context `Γ` and a
`Type` with inference rules as term constructs. The collection of
terms in simply typed lambda calculus is defined as an inducitve family
indexed by a (given) context and a type.

\begin{code}
data _⊢_ (Γ : Context) : Type → Set where
\end{code}

In our formal development we will use the position of λ to which the
bound variable refer for the name of a variable.  For example,

    λ x. λ y. y

will be represented by

    λ λ 0

This representation is called de Bruijn representation and the nubmer
is a de Bruijn index. It also makes α-equivalence an equality on
λ-terms.

Note that we have

    Γ ∋ (x : A)
    -----------
    Γ ⊢ x : A

in our informal development where `x` is now merely a number pointing
to the position of `A` in `Γ`. We introduce a term `x` for a free
variable in `Γ` just by giving its position in the context.
Given `Γ ⊢ M : A`, the context Γ is the set of possibly free variables in `M`.

\begin{code}
  `_ : Γ ∋ A
       -----
     → Γ ⊢ A
\end{code}

The definition of application is straightforward.

\begin{code}
  _·_ : Γ ⊢ A →̇ B
      → Γ ⊢ A
        -----
      → Γ ⊢ B
\end{code}

In the informal development it takes a variable x and a term M to
form λ x. M.  Since the name of a variable does not matter at all in
our formal development λ now takes a term M only.

Moreover, the position of a variable in the context `Γ , A` now refers
to the innermost λ. Hence our definition

\begin{code}
  ƛ_
    : Γ , A ⊢ B
      ---------
    → Γ ⊢ A →̇ B
\end{code}

For example, ` Z : (∅ , A) ⊢ A is a variable of type A under the
context (∅ , A).  After abstraction, ƛ ` Z : ∅ ⊢ A →̇ A is an
abstraction under the empty context whose body is only a variable
refering to the variable bound by λ.

As you may have observed, this inductive family Γ ⊢ A is just
a variant of the natural deduction for propositional logic where
inference rules are viewed as term constructs.

For convenience, the following symbols denote a term.

\begin{code}
variable
  M N L M′ N′ L′ : Γ ⊢ A
\end{code}

Also for convenience, we compute the proof of `Γ ∋ A` by giving its
position n (as a natural). In short, define # n as ` (count n)

\begin{code}
#_ : (n : ℕ) → Γ ⊢ lookup Γ n
# n  =  ` count n
\end{code}

### Examples

\begin{code}
nat : Type → Type
nat A = (A →̇ A) →̇ A →̇ A
\end{code}

Recall that the Church numberal c₀ for 0 is

    λ f x. x

In the de Bruijn representation, λ f x. x becomes

    λ λ 0

\begin{code}
c₀ : ∀ {A} → ∅ ⊢ nat A
c₀ = ƛ ƛ # 0
\end{code}

Similarly, c₁ ≡ λ f x. f x becomes

    λ λ 1 0

\begin{code}
c₁ : ∀ {A} → ∅ ⊢ nat A
c₁ = ƛ ƛ # 1 · # 0
\end{code}

The addition of two Church numerals defined as

    λ n. λ m. λ f. λ x. n f (m f x)

becomes

    λ λ λ λ 3 1 (2 1 0)

\begin{code}
add : ∀ {A} → ∅ ⊢ nat A →̇ nat A →̇ nat A
add = ƛ ƛ ƛ ƛ # 3 · # 1 · (# 2 · # 1 · # 0)
\end{code}

### Exercise

Translate the following terms in the informal development to de
Bruijn representation.

    1. (id)   λ x. x
    2. (fst)  λ x y. x
    3. (if)   λ b x y. b x y
    4. (succ) λ n. λ f x. f (n f x)

\begin{code}
id : ∅ ⊢ A →̇ A
id = ƛ ` Z

fst : ∅ ⊢ A →̇ B →̇ A
fst = ƛ ƛ ` (S Z)

bool : Type → Type
bool A = A →̇ A →̇ A

if : ∅ ⊢ bool A →̇ A →̇ A →̇ A
if = ƛ ` Z

succ : ∅ ⊢ nat A →̇ nat A
succ = ƛ ƛ ƛ ` (S Z) · ((`(S (S Z)) · ` (S Z)) · ` Z)

\end{code}

Parallel Substitution
---------------------

To define substitution, it is actually easier to define substitution
for all free variable at once instead of one.

\begin{code}
Rename : Context → Context → Set
Rename Γ Δ = ∀ {A} → Γ ∋ A → Δ ∋ A

Subst : Context → Context → Set
Subst Γ Δ = ∀ {A} → Γ ∋ A → Δ ⊢ A
\end{code}

As the de Bruijn index points to the position of a λ abstraction
starting from the innermost λ, we need to increment/decrement the
number when visiting/leaving λ.

For example, substituting M for x in the following term

    x : A → A ⊢ x (λ y. y)

becomes

    0 (λ 0) [ M / 0 ] ≡ M (λ [ M ↑ / 1 ])

where M ↑ indicates that the de Bruijn index of a free variable which
is incremented.

Therefore, a renaming function ρ : ∀ {A} → Γ ∋ A → Δ ∋ A
becomes ext ρ : ∀ {A B} → Γ , B ∋ A → Δ , B ∋ A where B is the type of
argument when visiting an abstraction λ.

\begin{code}
rename : Rename Γ Δ
  → (Γ ⊢ A)
  → (Δ ⊢ A)
rename ρ (` x)   = ` ρ x
rename ρ (M · N) = rename ρ M · rename ρ N
rename ρ (ƛ M)   = ƛ rename (ext ρ) M
\end{code}

Similarly, we proceed with a substitution σ : ∀ {A} → Γ ∋ A → Δ ⊢ A.
Note that

    rename S_ : ∀ {A} → Γ ∋ A → Γ , B ∋ A

merely enlarges the context and increments the de Bruijn index for
every Γ ∋ A.

\begin{code}
exts : Subst Γ Δ → Subst (Γ , A) (Δ , A)
exts σ Z     = ` Z
exts σ (S p) = rename S_ (σ p)

_⟪_⟫
  : Γ ⊢ A
  → Subst Γ Δ
  → Δ ⊢ A
(` x)   ⟪ σ ⟫ = σ x
(M · N) ⟪ σ ⟫ = M ⟪ σ ⟫ · N ⟪ σ ⟫
(ƛ M)   ⟪ σ ⟫ = ƛ M ⟪ exts σ ⟫
\end{code}

Singleton Substitution
----------------------

Note that we only need to substitute the free variable corresponding
to the outermost λ, i.e.

    (λ x. M) N -→ M [ N / x ]

where the free occurrence of x in M points to the outermost λ.
Thus it suffices to define singleton subsitution for the non-empty
context

    Γ , x : A

which appears in the typing rule

    Γ , x : A ⊢ M : B
    ----------------------
    Γ ⊢ λ x : A. M : A → B

It follows that the singleton substitution is a special case
of parallel substitution given by

    σN : ∀ {A} → Γ , B ∋ A → Γ ⊢ A

for some `N : Γ ⊢ B` so that `_⟪ σN ⟫ : Γ , B ⊢ A → Γ ⊢ A`.

\begin{code}
subst-zero : {B : Type}
  → Γ ⊢ B
  → Subst (Γ , B) Γ
subst-zero N Z     =  N
subst-zero _ (S x) =  ` x

_[_] : Γ , B ⊢ A
     → Γ ⊢ B
       ---------
     → Γ ⊢ A
_[_] N M =  N ⟪ subst-zero M ⟫
\end{code}

Single-step reduction
---------------------

In our informal development -→β is defined only for beta-redex
followed by one-step full β-reduction. These two rules can be combined
altogether.

\begin{code}
infix 3 _-→_
data _-→_ {Γ} : (M N : Γ ⊢ A) → Set where
  β-ƛ·
    : (ƛ M) · N -→ M [ N ]

  ξ-ƛ
    :   M -→ M′
    → ƛ M -→ ƛ M′
  ξ-·ₗ
    :     L -→ L′
      ---------------
    → L · M -→ L′ · M
  ξ-·ᵣ
    :     M -→ M′
      ---------------
    → L · M -→ L · M′
\end{code}

Reduction sequence of -→
--------------------------------------

The reduction sequence M -↠ N from M to N is just a list of reductions
such that the RHS of a head reduction must be the LHS of the tail of
reductions.

\begin{code}
data _-↠_ {Γ A} : (M N : Γ ⊢ A) → Set where
  _∎ : (M : Γ ⊢ A)
    → M -↠ M       -- empty list

  _-→⟨_⟩_
    : ∀ L          -- this can usually be inferred by the following reduction
    → L -→ M       -- the head of a list
    → M -↠ N       -- the tail
      -------
    → L -↠ N

infix  2 _-↠_
infixr 2 _-→⟨_⟩_
infix 3 _∎
\end{code}

The relation -↠ is also transitive in the sense that

    if L -↠ M and M -↠ N then L -↠ N

the proof itself is in fact the concatenation of two lists.

\begin{code}
_-↠⟨_⟩_ : ∀ L
  → L -↠ M → M -↠ N
  -----------------
  → L -↠ N
M -↠⟨ L-↠M ⟩ M-↠N = {!!}

infixr 2 _-↠⟨_⟩_
\end{code}

### Exercise

Show that -↠ is a congruence. That is, show the following lemmas.

\begin{code}
ƛ-↠ : M -↠ M′
      -----------
    → ƛ M -↠ ƛ M′
ƛ-↠ M-↠M′       = {!!}

·-↠ : M -↠ M′
    → N -↠ N′
    → M · N -↠ M′ · N′
·-↠ M-↠M′ N-↠N′ = {!!}
\end{code}

Computational equality
----------------------

In (untyped) lambda calculus, we say that two terms M and N are
computationally equal denoted by M =β N if either

    1. M -→ N

    2. M =β M

    3. M =β N
       ------
       N =β M

    4. L =β M    M =β N
       ----------------
           L =β N

Correspondingly, we introduce an inductive type family
where each case is a constrctor of that type family:

\begin{code}
data _=β_ {Γ : Context} : Γ ⊢ A → Γ ⊢ A → Set where
  =β-beta
    : M -→ N → M =β N

  =β-refl
    : M =β M

  =β-sym
    : N =β M → M =β N

  =β-trans
    : L =β M → M =β N
    → L =β N
\end{code}

Homework Solution in Agda
-------------------------

Show that if M -↠ N and M is in normal form then M ≡ N (every two
α-equivalent terms are exactly equal in de Bruijn representation).


\end{code}
HW2 : M -↠ N → (∀ N → ¬ (M -→ N)) → M ≡ N
HW2 M-↠N M↛ = {!!}
\end{code}

Normal form
-----------

Recall that a term M is in normal form if M --̸→ N for any N.  This
property can be characterised completely by its syntax. The
characterisation is given as follows:

    λ x₁ x₂ ⋯ xₙ. x N₁ N₂ ⋯ ⋯ ⋯ Nₘ
    │             ╰── Neutral ──╯│
    ╰────────── Normal ──────────╯

where x is a (free or bound) variable, Nᵢ's are all in normal form,
and n and m can be zero. The syntax is devided into two categories:

  * neutral terms: the neutral part indicates a spine of normal terms
    starting from a variable

  * normal terms: a sequence of abstractions λ followed by neutral
    terms

Neutral terms are those normal terms which do not create any further
β-redexs during substitution. This characterisation is defined as two
mutually-defiend inductive families.

\begin{code}
data Neutral : Γ ⊢ A → Set
data Normal  : Γ ⊢ A → Set

data Neutral where
  `_  : (x : Γ ∋ A)
    → Neutral (` x)
  _·_ : Neutral L
    → Normal M
    → Neutral (L · M)

data Normal where
  ᵒ_  : Neutral M → Normal M
  ƛ_  : Normal M  → Normal (ƛ M)
\end{code}

The soundness of characterisation is proved by induction on the
derivation of Normal M (resp. Neutral M) and if necessary on M -→ M.

The completeness is proved by induction on the derivation of M
(or Γ ⊢ M : A) and by contradiction using ⊥-elim : ⊥ → A.  so that we
can deduce any property we need once we derive a contradication ⊥.

Proofs are left as exercises.

### Exercise

\begin{code}
normal-soundness  : Normal M  → ¬ (M -→ N)
neutral-soundness : Neutral M → ¬ (M -→ M′)

normal-soundness  M = {!!}
neutral-soundness M = {!!}

normal-completeness
  : (M : Γ ⊢ A) → (∀ N → ¬ (M -→ N))
  → Normal M
normal-completeness M = {!!}
\end{code}

Preservation
------------

Preservation theorem is trivial in this formal development, since

  M -→ N

is an inductive family indexed by two terms of the same type.

Progress
--------

Progress theorem state that every well-typed term M is either

  1. in normal form or
  2. reducible

so we introduce a predicate `Progress` over well-typed terms M for
this statement.

\begin{code}
data Progress (M : Γ ⊢ A) : Set where
  step
    : M -→ N
      ----------
    → Progress M

  done : Normal M
    → Progress M
\end{code}

Progress theorm is proved by induction on the derviation of Γ ⊢ M : A
in the informal and formal developments.

\begin{code}
progress : (M : Γ ⊢ A)
  → Progress M
progress M = {!!}
\end{code}

Progress Theorem can be proved without `Normal`. Then, why bother?
Despite of being logically equivalent, the proof becomes really ugly!
Try the following exericse at your own risk.

\begin{code}
data Progress′ (M : Γ ⊢ A) : Set where
  step
    : (r : M -→ N)
      ----------
    → Progress′ M

  done : (M↓ : (N : Γ ⊢ A) → M -→ N → ⊥)
    → Progress′ M

progress′ : (M : Γ ⊢ A) → Progress′ M
progress′ M = {!!}
\end{code}

STLC.agda

module STLC where

open import Data.Nat
open import Data.Empty
  hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
  hiding ([_])


infix  3 _⊢_ _=β_

infixr 7 _→̇_

infixr 5 ƛ_
infixl 7 _·_
infixl 8 _[_] _⟪_⟫
infixr 9 ᵒ_ `_ #_


data Type : Set where
  ⋆   : Type
  _→̇_ : Type → Type → Type


infixl 7 _⧺_
infixl 6 _,_
infix  4 _∋_

data Context : Set where
  ∅   :                  Context
  _,_ : Context → Type → Context


variable
  Γ Δ Ξ : Context
  A B C : Type


data _∋_ : Context → Type → Set where
  Z   ---------
    : Γ , A ∋ A

  S_ : Γ     ∋ A
       ---------
     → Γ , B ∋ A

variable
  x     : Γ ∋ A


_ : ∅ , A , B ∋ A
_ = S Z


⊥-elim : ∀ {T : Set} → ⊥ → T
⊥-elim ()

lookup : Context → ℕ → Type
lookup (Γ , A) zero     =  A
lookup (Γ , B) (suc n)  =  lookup Γ n
lookup ∅       _        =  ⊥-elim impossible
  where postulate impossible : ⊥


count : (n : ℕ) → Γ ∋ lookup Γ n
count {Γ = Γ , _} zero     =  Z
count {Γ = Γ , _} (suc n)  =  S (count n)
count {Γ = ∅    }  _        =  ⊥-elim impossible
  where postulate impossible : ⊥


_ :  ∅ , A , B ∋ A
_ = count 1

_ : ∅ , B , A ∋ A
_ = count 0


ext
  : (∀ {A}   →     Γ ∋ A →     Δ ∋ A)
    ---------------------------------
  → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
ext ρ Z      =  Z
ext ρ (S x)  =  S (ρ x)


_⧺_ : Context → Context → Context
Γ ⧺ ∅       = Γ
Γ ⧺ (Δ , x) = Γ ⧺ Δ , x


data _⊢_ (Γ : Context) : Type → Set where


  `_ : Γ ∋ A
       -----
     → Γ ⊢ A


  _·_ : Γ ⊢ A →̇ B
      → Γ ⊢ A
        -----
      → Γ ⊢ B


  ƛ_
    : Γ , A ⊢ B
      ---------
    → Γ ⊢ A →̇ B


variable
  M N L M′ N′ L′ : Γ ⊢ A


#_ : (n : ℕ) → Γ ⊢ lookup Γ n
# n  =  ` count n


nat : Type → Type
nat A = (A →̇ A) →̇ A →̇ A


c₀ : ∀ {A} → ∅ ⊢ nat A
c₀ = ƛ ƛ # 0


c₁ : ∀ {A} → ∅ ⊢ nat A
c₁ = ƛ ƛ # 1 · # 0


add : ∀ {A} → ∅ ⊢ nat A →̇ nat A →̇ nat A
add = ƛ ƛ ƛ ƛ # 3 · # 1 · (# 2 · # 1 · # 0)


id : ∅ ⊢ A →̇ A
id = ƛ ` Z

fst : ∅ ⊢ A →̇ B →̇ A
fst = ƛ ƛ ` (S Z)

bool : Type → Type
bool A = A →̇ A →̇ A

if : ∅ ⊢ bool A →̇ A →̇ A →̇ A
if = ƛ ` Z

succ : ∅ ⊢ nat A →̇ nat A
succ = ƛ ` Z


Rename : Context → Context → Set
Rename Γ Δ = ∀ {A} → Γ ∋ A → Δ ∋ A

Subst : Context → Context → Set
Subst Γ Δ = ∀ {A} → Γ ∋ A → Δ ⊢ A


rename : Rename Γ Δ
  → (Γ ⊢ A)
  → (Δ ⊢ A)
rename ρ (` x)   = ` ρ x
rename ρ (M · N) = rename ρ M · rename ρ N
rename ρ (ƛ M)   = ƛ rename (ext ρ) M


exts : Subst Γ Δ → Subst (Γ , A) (Δ , A)
exts σ Z     = ` Z
exts σ (S p) = rename S_ (σ p)

_⟪_⟫
  : Γ ⊢ A
  → Subst Γ Δ
  → Δ ⊢ A
(` x)   ⟪ σ ⟫ = σ x
(M · N) ⟪ σ ⟫ = M ⟪ σ ⟫ · N ⟪ σ ⟫
(ƛ M)   ⟪ σ ⟫ = ƛ M ⟪ exts σ ⟫


subst-zero : {B : Type}
  → Γ ⊢ B
  → Subst (Γ , B) Γ
subst-zero N Z     =  N
subst-zero _ (S x) =  ` x

_[_] : Γ , B ⊢ A
     → Γ ⊢ B
       ---------
     → Γ ⊢ A
_[_] N M =  N ⟪ subst-zero M ⟫


infix 3 _-→_
data _-→_ {Γ} : (M N : Γ ⊢ A) → Set where
  β-ƛ·
    : (ƛ M) · N -→ M [ N ]

  ξ-ƛ
    :   M -→ M′
    → ƛ M -→ ƛ M′
  ξ-·ₗ
    :     L -→ L′
      ---------------
    → L · M -→ L′ · M
  ξ-·ᵣ
    :     M -→ M′
      ---------------
    → L · M -→ L · M′


data _-↠_ {Γ A} : (M N : Γ ⊢ A) → Set where
  _∎ : (M : Γ ⊢ A)
    → M -↠ M       -- empty list

  _-→⟨_⟩_
    : ∀ L          -- this can usually be inferred by the following reduction
    → L -→ M       -- the head of a list
    → M -↠ N       -- the tail
      -------
    → L -↠ N

infix  2 _-↠_
infixr 2 _-→⟨_⟩_
infix 3 _∎


_-↠⟨_⟩_ : ∀ L
  → L -↠ M → M -↠ N
  -----------------
  → L -↠ N
M -↠⟨ L-↠M ⟩ M-↠N = {!!}

infixr 2 _-↠⟨_⟩_


ƛ-↠ : M -↠ M′
      -----------
    → ƛ M -↠ ƛ M′
ƛ-↠ M-↠M′       = {!!}

·-↠ : M -↠ M′
    → N -↠ N′
    → M · N -↠ M′ · N′
·-↠ M-↠M′ N-↠N′ = {!!}


data _=β_ {Γ : Context} : Γ ⊢ A → Γ ⊢ A → Set where
  =β-beta
    : M -→ N → M =β N

  =β-refl
    : M =β M

  =β-sym
    : N =β M → M =β N

  =β-trans
    : L =β M → M =β N
    → L =β N


data Neutral : Γ ⊢ A → Set
data Normal  : Γ ⊢ A → Set

data Neutral where
  `_  : (x : Γ ∋ A)
    → Neutral (` x)
  _·_ : Neutral L
    → Normal M
    → Neutral (L · M)

data Normal where
  ᵒ_  : Neutral M → Normal M
  ƛ_  : Normal M  → Normal (ƛ M)


normal-soundness  : Normal M  → ¬ (M -→ N)
neutral-soundness : Neutral M → ¬ (M -→ M′)

normal-soundness  M = {!!}
neutral-soundness M = {!!}

normal-completeness
  : (M : Γ ⊢ A) → (∀ N → ¬ (M -→ N))
  → Normal M
normal-completeness M = {!!}


data Progress (M : Γ ⊢ A) : Set where
  step
    : M -→ N
      ----------
    → Progress M

  done : Normal M
    → Progress M


progress : (M : Γ ⊢ A)
  → Progress M
progress M = {!!}


data Progress′ (M : Γ ⊢ A) : Set where
  step
    : (r : M -→ N)
      ----------
    → Progress′ M

  done : (M↓ : (N : Γ ⊢ A) → M -→ N → ⊥)
    → Progress′ M

progress′ : (M : Γ ⊢ A) → Progress′ M
progress′ M = {!!}