---
title     : "TypedBarendregt: Raw terms with types (broken)"
layout    : page
permalink : /TypedBarendregt
---

This version uses raw terms. Substitution presumes that no
generation of fresh names is required.

The substitution algorithm is based on one by McBride.
It is given a map from names to terms. Say the mapping of a
name is trivial if it takes a name to a term consisting of
just the variable with that name. No fresh names are required
if the mapping on each variable is either trivial or to a
closed term. However, the proof of correctness currently
contains a hole, and may be difficult to repair.

## Imports

\begin{code}
module TypedBarendregt where
\end{code}

\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List using (List; []; _∷_; _++_; map; foldr; filter)
open import Data.Nat using (ℕ; zero; suc; _+_; _⊔_; _≤_; _≟_)
open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (¬?)
import Collections

pattern [_]     x      =  x ∷ []
pattern [_,_]   x y    =  x ∷ y ∷ []
pattern [_,_,_] x y z  =  x ∷ y ∷ z ∷ []
\end{code}


## Syntax

\begin{code}
infix   4  _∋_`:_
infix   4  _⊢_`:_
infixl  5  _,_`:_
infixr  6  _`→_
infix   6  `λ_`→_
infixl  7  `if0_then_else_
infix   8  `suc_ `pred_ `Y_
infixl  9  _·_

Id : Set
Id = ℕ

data Type : Set where
  `ℕ   : Type
  _`→_ : Type → Type → Type

data Ctx : Set where
  ε      : Ctx
  _,_`:_ : Ctx → Id → Type → Ctx

data Term : Set where
  `_              : Id → Term
  `λ_`→_          : Id → Term → Term
  _·_             : Term → Term → Term
  `zero           : Term    
  `suc_           : Term → Term
  `pred_          : Term → Term
  `if0_then_else_ : Term → Term → Term → Term
  `Y_             : Term → Term

data _∋_`:_ : Ctx → Id → Type → Set where

  Z : ∀ {Γ A x}
      --------------------
    → Γ , x `: A ∋ x `: A

  S : ∀ {Γ A B x w}
    → w ≢ x
    → Γ ∋ w `: B
      --------------------
    → Γ , x `: A ∋ w `: B

data _⊢_`:_ : Ctx → Term → Type → Set where

  Ax : ∀ {Γ A x}
    → Γ ∋ x `: A
      --------------
    → Γ ⊢ ` x `: A

  ⊢λ : ∀ {Γ x N A B}
    → Γ , x `: A ⊢ N `: B
      --------------------------
    → Γ ⊢ (`λ x `→ N) `: A `→ B

  _·_ : ∀ {Γ L M A B}
    → Γ ⊢ L `: A `→ B
    → Γ ⊢ M `: A
      ----------------
    → Γ ⊢ L · M `: B

  ⊢zero : ∀ {Γ}
      ----------------
    → Γ ⊢ `zero `: `ℕ

  ⊢suc : ∀ {Γ M}
    → Γ ⊢ M `: `ℕ
      -----------------
    → Γ ⊢ `suc M `: `ℕ

  ⊢pred : ∀ {Γ M}
    → Γ ⊢ M `: `ℕ
      ------------------
    → Γ ⊢ `pred M `: `ℕ

  ⊢if0 : ∀ {Γ L M N A}
    → Γ ⊢ L `: `ℕ
    → Γ ⊢ M `: A
    → Γ ⊢ N `: A
      ------------------------------
    → Γ ⊢ `if0 L then M else N `: A

  ⊢Y : ∀ {Γ M A}
    → Γ ⊢ M `: A `→ A
      ----------------
    → Γ ⊢ `Y M `: A
\end{code}

## Test examples

\begin{code}
m n p s z : Id
m = 0
n = 1
p = 2
s = 3
z = 4

s≢z : s ≢ z
s≢z ()

n≢z : n ≢ z
n≢z ()

n≢s : n ≢ s
n≢s ()

m≢z : m ≢ z
m≢z ()

m≢s : m ≢ s
m≢s ()

m≢n : m ≢ n
m≢n ()

p≢n : p ≢ n
p≢n ()

p≢m : p ≢ m
p≢m ()

two : Term
two = `suc `suc `zero

⊢two : ε ⊢ two `: `ℕ
⊢two = ⊢suc (⊢suc ⊢zero)

plus : Term
plus = `Y (`λ p `→ `λ m `→ `λ n `→
            `if0 ` m then ` n else `suc (` p · (`pred (` m)) · ` n))

⊢plus : ε ⊢ plus `: `ℕ `→ `ℕ `→ `ℕ
⊢plus = (⊢Y (⊢λ (⊢λ (⊢λ (⊢if0 (Ax ⊢m) (Ax ⊢n) (⊢suc (Ax ⊢p · (⊢pred (Ax ⊢m)) · Ax ⊢n)))))))
  where
  ⊢p = S p≢n (S p≢m Z)
  ⊢m = S m≢n Z
  ⊢n = Z

four : Term
four = plus · two · two

⊢four : ε ⊢ four `: `ℕ
⊢four = ⊢plus · ⊢two · ⊢two

Ch : Type
Ch = (`ℕ `→ `ℕ) `→ `ℕ `→ `ℕ

twoCh : Term
twoCh = `λ s `→ `λ z `→ (` s · (` s · ` z))

⊢twoCh : ε ⊢ twoCh `: Ch
⊢twoCh = (⊢λ (⊢λ (Ax ⊢s · (Ax ⊢s · Ax ⊢z))))
  where
  ⊢s = S s≢z Z
  ⊢z = Z

plusCh : Term
plusCh = `λ m `→ `λ n `→ `λ s `→ `λ z `→
           ` m · ` s · (` n · ` s · ` z)

⊢plusCh : ε ⊢ plusCh `: Ch `→ Ch `→ Ch
⊢plusCh = (⊢λ (⊢λ (⊢λ (⊢λ (Ax ⊢m ·  Ax ⊢s · (Ax ⊢n · Ax ⊢s · Ax ⊢z))))))
  where
  ⊢m = S m≢z (S m≢s (S m≢n Z))
  ⊢n = S n≢z (S n≢s Z)
  ⊢s = S s≢z Z
  ⊢z = Z

fromCh : Term
fromCh = `λ m `→ ` m · (`λ s `→ `suc ` s) · `zero

⊢fromCh : ε ⊢ fromCh `: Ch `→ `ℕ
⊢fromCh = (⊢λ (Ax ⊢m · (⊢λ (⊢suc (Ax ⊢s))) · ⊢zero))
  where
  ⊢m = Z
  ⊢s = Z

fourCh : Term
fourCh = fromCh · (plusCh · twoCh · twoCh)

⊢fourCh : ε ⊢ fourCh `: `ℕ
⊢fourCh = ⊢fromCh · (⊢plusCh · ⊢twoCh · ⊢twoCh)
\end{code}


## Erasure

\begin{code}
lookup : ∀ {Γ x A} → Γ ∋ x `: A → Id
lookup {Γ , x `: A} Z          =  x
lookup {Γ , x `: A} (S w≢ ⊢w)  =  lookup {Γ} ⊢w

erase : ∀ {Γ M A} → Γ ⊢ M `: A → Term
erase (Ax ⊢w)           =  ` lookup ⊢w
erase (⊢λ {x = x} ⊢N)   =  `λ x `→ erase ⊢N
erase (⊢L · ⊢M)         =  erase ⊢L · erase ⊢M
erase (⊢zero)           =  `zero
erase (⊢suc ⊢M)         =  `suc (erase ⊢M)
erase (⊢pred ⊢M)        =  `pred (erase ⊢M)
erase (⊢if0 ⊢L ⊢M ⊢N)   =  `if0 (erase ⊢L) then (erase ⊢M) else (erase ⊢N)
erase (⊢Y ⊢M)           =  `Y (erase ⊢M)
\end{code}

### Properties of erasure

\begin{code}
cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {s t u v x y} → 
                               s ≡ t → u ≡ v → x ≡ y → f s u x ≡ f t v y
cong₃ f refl refl refl = refl

lookup-lemma : ∀ {Γ x A} → (⊢x : Γ ∋ x `: A) → lookup ⊢x ≡ x
lookup-lemma Z          =  refl
lookup-lemma (S w≢ ⊢w)  =  lookup-lemma ⊢w

erase-lemma : ∀ {Γ M A} → (⊢M : Γ ⊢ M `: A) → erase ⊢M ≡ M
erase-lemma (Ax ⊢x)          =  cong `_ (lookup-lemma ⊢x)
erase-lemma (⊢λ {x = x} ⊢N)  =  cong (`λ x `→_) (erase-lemma ⊢N)
erase-lemma (⊢L · ⊢M)        =  cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M)
erase-lemma (⊢zero)          =  refl
erase-lemma (⊢suc ⊢M)        =  cong `suc_ (erase-lemma ⊢M)
erase-lemma (⊢pred ⊢M)       =  cong `pred_ (erase-lemma ⊢M)
erase-lemma (⊢if0 ⊢L ⊢M ⊢N)  =  cong₃ `if0_then_else_
                                  (erase-lemma ⊢L) (erase-lemma ⊢M) (erase-lemma ⊢N)
erase-lemma (⊢Y ⊢M)          =  cong `Y_ (erase-lemma ⊢M)
\end{code}


## Substitution

### Lists as sets

\begin{code}
open Collections (Id) (_≟_) hiding (_∉_)
\end{code}

### Free variables

\begin{code}
free : Term → List Id
free (` x)                   =  [ x ]
free (`λ x `→ N)             =  free N \\ x
free (L · M)                 =  free L ++ free M
free (`zero)                 =  []
free (`suc M)                =  free M
free (`pred M)               =  free M
free (`if0 L then M else N)  =  free L ++ free M ++ free N
free (`Y M)                  =  free M
\end{code}

### Maps

\begin{code}
tm-∅ : Id → Term
tm-∅ x = ` x

id-∅ : Id → Id
id-∅ x = x

infixl 5 _,_↦_

_,_↦_ : ∀ {X : Set} → (Id → X) → Id → X → (Id → X)
(ρ , x ↦ y) w with w ≟ x
...               | yes _   =  y
...               | no  _   =  ρ w
\end{code}

### Fresh identifier

\begin{code}
fresh : List Id → Id
fresh = foldr _⊔_ 0 ∘ map suc

⊔-lemma : ∀ {w xs} → w ∈ xs → suc w ≤ fresh xs
⊔-lemma {_} {_ ∷ xs} here        =  m≤m⊔n _ (fresh xs)
⊔-lemma {_} {_ ∷ xs} (there x∈)  =  ≤-trans (⊔-lemma x∈) (n≤m⊔n _ (fresh xs))

fresh-lemma : ∀ {x xs} → x ∈ xs → x ≢ fresh xs
fresh-lemma x∈ refl =  1+n≰n (⊔-lemma x∈)
\end{code}

### Imposing the Barendregt Convention

\begin{code}
rename : List Id → (Id → Id) → Term → Term
rename ys σ (` x) = ` σ x
rename ys σ (`λ x `→ M) = `λ y `→ rename (y ∷ ys) (σ , x ↦ y) M
  where
  y = fresh ys 
rename ys σ (L · M) =  rename ys σ L · rename ys σ M
rename ys σ `zero =  `zero
rename ys σ (`suc M) =  `suc (rename ys σ M)
rename ys σ (`pred M) =  `pred (rename ys σ M)
rename ys σ (`if0 L then M else N) =
   `if0 (rename ys σ L) then (rename ys σ M) else (rename ys σ N) 
rename ys σ (`Y M) =  `Y (rename ys σ M)

barendregt : Term → Term
barendregt M = rename (free M) id-∅ M
\end{code}

Some test cases.
\begin{code}
_ : barendregt plus ≡
  `Y (`λ 0 `→ (`λ 1 `→ (`λ 2 `→
    `if0 ` 1 then ` 2 else `suc (` 0) · (`pred (` 1)) · (` 2))))
_ = refl

_ : barendregt plusCh ≡
  (`λ 0 `→ (`λ 1 `→ (`λ 2 `→ (`λ 3 `→ (` 0) · (` 2) · ((` 1) · (` 2) · (` 3))))))
_ = refl
\end{code}


### Substitution

\begin{code}
subst : (Id → Term) → Term → Term
subst ρ (` x)        =  ρ x
subst ρ (`λ x `→ N)  =  `λ x `→ subst (ρ , x ↦ ` x) N
subst ρ (L · M)      =  subst ρ L · subst ρ M
subst ρ (`zero)      =  `zero
subst ρ (`suc M)     =  `suc (subst ρ M)
subst ρ (`pred M)    =  `pred (subst ρ M)
subst ρ (`if0 L then M else N)
  =  `if0 (subst ρ L) then (subst ρ M) else (subst ρ N)
subst ρ (`Y M)       =  `Y (subst ρ M)  
                       
_[_:=_] : Term → Id → Term → Term
N [ x := M ]  =  subst (tm-∅ , x ↦ M) N
\end{code}

### Testing substitution

\begin{code}
_ : (` s · ` s · ` z) [ z := `zero ] ≡ (` s · ` s · `zero)
_ = refl

_ : (` s · ` s · ` z) [ s := (`λ m `→ `suc ` m) ] [ z := `zero ] 
      ≡ (`λ m `→ `suc ` m) · (`λ m `→ `suc ` m) · `zero
_ = refl

_ : (`λ m `→ ` m ·  ` n) [ n := ` s · ` z ]
      ≡ `λ m `→ ` m · (` s · ` z)
_ = refl

_ : subst (tm-∅ , m ↦ two , n ↦ four) (` m · ` n)  ≡ (two · four)
_ = refl
\end{code}


## Values

\begin{code}
data Value : Term → Set where

  Zero :
      ----------
      Value `zero

  Suc : ∀ {V}
    → Value V
      --------------
    → Value (`suc V)
      
  Fun : ∀ {x N}
      ---------------
    → Value (`λ x `→ N)
\end{code}

## Reduction

\begin{code}
infix 4 _⟶_

data _⟶_ : Term → Term → Set where

  ξ-·₁ : ∀ {L L′ M}
    → L ⟶ L′
      -----------------
    → L · M ⟶ L′ · M

  ξ-·₂ : ∀ {V M M′}
    → Value V
    → M ⟶ M′
      -----------------
    → V · M ⟶ V · M′

  β-→ : ∀ {x N V}
    → Value V
      ---------------------------------
    → (`λ x `→ N) · V ⟶ N [ x := V ]

  ξ-suc : ∀ {M M′}
    → M ⟶ M′
      -------------------
    → `suc M ⟶ `suc M′

  ξ-pred : ∀ {M M′}
    → M ⟶ M′
      ---------------------
    → `pred M ⟶ `pred M′

  β-pred-zero :
      ----------------------
      `pred `zero ⟶ `zero

  β-pred-suc : ∀ {V}
    → Value V
      ---------------------
    → `pred (`suc V) ⟶ V

  ξ-if0 : ∀ {L L′ M N}
    → L ⟶ L′
      -----------------------------------------------
    → `if0 L then M else N ⟶ `if0 L′ then M else N

  β-if0-zero : ∀ {M N}
      -------------------------------
    → `if0 `zero then M else N ⟶ M
  
  β-if0-suc : ∀ {V M N}
    → Value V
      ----------------------------------
    → `if0 (`suc V) then M else N ⟶ N

  ξ-Y : ∀ {M M′}
    → M ⟶ M′
      ---------------
    → `Y M ⟶ `Y M′

  β-Y : ∀ {F x N}
    → F ≡ `λ x `→ N
      -------------------------
    → `Y F ⟶ N [ x := `Y F ]
\end{code}

## Reflexive and transitive closure

\begin{code}
infix  2 _⟶*_
infix 1 begin_
infixr 2 _⟶⟨_⟩_
infix 3 _∎

data _⟶*_ : Term → Term → Set where

  _∎ : ∀ (M : Term)
      -------------
    → M ⟶* M

  _⟶⟨_⟩_ : ∀ (L : Term) {M N}
    → L ⟶ M
    → M ⟶* N
      ---------
    → L ⟶* N

begin_ : ∀ {M N} → (M ⟶* N) → (M ⟶* N)
begin M⟶*N = M⟶*N
\end{code}

## Sample execution

\begin{code}
_ : plus · two · two ⟶* (`suc (`suc (`suc (`suc `zero))))
_ = 
  begin
    plus · two · two
  ⟶⟨ ξ-·₁ (ξ-·₁ (β-Y refl)) ⟩
    (`λ m `→ (`λ n `→ `if0 ` m then ` n else
      `suc (plus · (`pred (` m)) · (` n))))  · two · two
  ⟶⟨ ξ-·₁ (β-→ (Suc (Suc Zero))) ⟩
    (`λ n `→ `if0 two then ` n else
      `suc (plus · (`pred two) · (` n))) · two
  ⟶⟨ β-→ (Suc (Suc Zero)) ⟩
   `if0 two then two else
     `suc (plus · (`pred two) · two)
  ⟶⟨ β-if0-suc (Suc Zero) ⟩
   `suc (plus · (`pred two) · two)
  ⟶⟨ ξ-suc (ξ-·₁ (ξ-·₁ (β-Y refl))) ⟩
   `suc ((`λ m `→ (`λ n `→ `if0 ` m then ` n else
     `suc (plus · (`pred (` m)) · (` n)))) · (`pred two) · two)
  ⟶⟨ ξ-suc (ξ-·₁ (ξ-·₂ Fun (β-pred-suc (Suc Zero)))) ⟩
   `suc ((`λ m `→ (`λ n `→ `if0 ` m then ` n else
     `suc (plus · (`pred (` m)) · (` n)))) · (`suc `zero) · two)
  ⟶⟨ ξ-suc (ξ-·₁ (β-→ (Suc Zero))) ⟩
   `suc ((`λ n `→ `if0 `suc `zero then ` n else
     `suc (plus · (`pred (`suc `zero)) · (` n)))) · two
  ⟶⟨ ξ-suc (β-→ (Suc (Suc Zero))) ⟩
   `suc (`if0 `suc `zero then two else
     `suc (plus · (`pred (`suc `zero)) · two))
  ⟶⟨ ξ-suc (β-if0-suc Zero) ⟩
   `suc (`suc (plus · (`pred (`suc `zero)) · two))
  ⟶⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ (β-Y refl)))) ⟩
   `suc (`suc ((`λ m `→ (`λ n `→ `if0 ` m then ` n else 
     `suc (plus · (`pred (` m)) · (` n)))) · (`pred (`suc `zero)) · two))
  ⟶⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₂ Fun (β-pred-suc Zero)))) ⟩
   `suc (`suc ((`λ m `→ (`λ n `→ `if0 ` m then ` n else
     `suc (plus · (`pred (` m)) · (` n)))) · `zero · two))
  ⟶⟨ ξ-suc (ξ-suc (ξ-·₁ (β-→ Zero))) ⟩
   `suc (`suc ((`λ n `→ `if0 `zero then ` n else
     `suc (plus · (`pred `zero) · (` n))) · two))
  ⟶⟨ ξ-suc (ξ-suc (β-→ (Suc (Suc Zero)))) ⟩
   `suc (`suc (`if0 `zero then two else
     `suc (plus · (`pred `zero) · two)))
  ⟶⟨ ξ-suc (ξ-suc β-if0-zero) ⟩
   `suc (`suc (`suc (`suc `zero)))
  ∎
\end{code}

## Values do not reduce

Values do not reduce.
\begin{code}
Val-⟶ : ∀ {M N} → Value M → ¬ (M ⟶ N)
Val-⟶ Fun ()
Val-⟶ Zero ()
Val-⟶ (Suc VM) (ξ-suc M⟶N)  =  Val-⟶ VM M⟶N
\end{code}

As a corollary, terms that reduce are not values.
\begin{code}
⟶-Val : ∀ {M N} → (M ⟶ N) → ¬ Value M
⟶-Val M⟶N VM  =  Val-⟶ VM M⟶N
\end{code}

## Reduction is deterministic

\begin{code}
det : ∀ {M M′ M″}
  → (M ⟶ M′)
  → (M ⟶ M″)
    ----------
  → M′ ≡ M″
det (ξ-·₁ L⟶L′) (ξ-·₁ L⟶L″) =  cong₂ _·_ (det L⟶L′ L⟶L″) refl
det (ξ-·₁ L⟶L′) (ξ-·₂ VL _) = ⊥-elim (Val-⟶ VL L⟶L′)
det (ξ-·₁ L⟶L′) (β-→ _) = ⊥-elim (Val-⟶ Fun L⟶L′)
det (ξ-·₂ VL _) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ VL L⟶L″)
det (ξ-·₂ _ M⟶M′) (ξ-·₂ _ M⟶M″) = cong₂ _·_ refl (det M⟶M′ M⟶M″)
det (ξ-·₂ _ M⟶M′) (β-→ VM) = ⊥-elim (Val-⟶ VM M⟶M′)
det (β-→ VM) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ Fun L⟶L″)
det (β-→ VM) (ξ-·₂ _ M⟶M″) = ⊥-elim (Val-⟶ VM M⟶M″)
det (β-→ _) (β-→ _) = refl
det (ξ-suc M⟶M′) (ξ-suc M⟶M″) = cong `suc_ (det M⟶M′ M⟶M″)
det (ξ-pred M⟶M′) (ξ-pred M⟶M″) = cong `pred_ (det M⟶M′ M⟶M″)
det (ξ-pred M⟶M′) β-pred-zero = ⊥-elim (Val-⟶ Zero M⟶M′)
det (ξ-pred M⟶M′) (β-pred-suc VM) = ⊥-elim (Val-⟶ (Suc VM) M⟶M′)
det β-pred-zero (ξ-pred M⟶M′) = ⊥-elim (Val-⟶ Zero M⟶M′)
det β-pred-zero β-pred-zero = refl
det (β-pred-suc VM) (ξ-pred M⟶M′) = ⊥-elim (Val-⟶ (Suc VM) M⟶M′)
det (β-pred-suc _) (β-pred-suc _) = refl
det (ξ-if0 L⟶L′) (ξ-if0 L⟶L″) = cong₃ `if0_then_else_ (det L⟶L′ L⟶L″) refl refl
det (ξ-if0 L⟶L′) β-if0-zero = ⊥-elim (Val-⟶ Zero L⟶L′)
det (ξ-if0 L⟶L′) (β-if0-suc VL) = ⊥-elim (Val-⟶ (Suc VL) L⟶L′)
det β-if0-zero (ξ-if0 L⟶L″) = ⊥-elim (Val-⟶ Zero L⟶L″)
det β-if0-zero β-if0-zero = refl
det (β-if0-suc VL) (ξ-if0 L⟶L″) = ⊥-elim (Val-⟶ (Suc VL) L⟶L″)
det (β-if0-suc _) (β-if0-suc _) = refl
det (ξ-Y M⟶M′) (ξ-Y M⟶M″) = cong `Y_ (det M⟶M′ M⟶M″)
det (ξ-Y M⟶M′) (β-Y refl) = ⊥-elim (Val-⟶ Fun M⟶M′)
det (β-Y refl) (ξ-Y M⟶M″) = ⊥-elim (Val-⟶ Fun M⟶M″)
det (β-Y refl) (β-Y refl) = refl
\end{code}

Almost half the lines in the above proof are redundant, for example

    det (ξ-·₁ L⟶L′) (ξ-·₂ VL _) = ⊥-elim (Val-⟶ VL L⟶L′)
    det (ξ-·₂ VL _) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ VL L⟶L″)
 
are essentially identical. What we might like to do is delete the
redundant lines and add

    det M⟶M′ M⟶M″ = sym (det M⟶M″ M⟶M′)

to the bottom of the proof. But this does not work. The termination
checker complains, because the arguments have merely switched order
and neither is smaller.

## Canonical forms

\begin{code}
data Canonical : Term → Type → Set where

  Zero : 
      -------------------
      Canonical `zero `ℕ

  Suc : ∀ {V}
    → Canonical V `ℕ
      ----------------------
    → Canonical (`suc V) `ℕ
 
  Fun : ∀ {x N A B}
    → ε , x `: A ⊢ N `: B
      -------------------------------
    → Canonical (`λ x `→ N) (A `→ B)
\end{code}

## Canonical forms lemma

Every typed value is canonical.

\begin{code}
canonical : ∀ {V A}
  → ε ⊢ V `: A
  → Value V
    -------------
  → Canonical V A
canonical ⊢zero      Zero      =  Zero
canonical (⊢suc ⊢V)  (Suc VV)  =  Suc (canonical ⊢V VV)
canonical (⊢λ ⊢N)    Fun       =  Fun ⊢N
\end{code}

Every canonical form has a type and a value.

\begin{code}
type : ∀ {V A}
  → Canonical V A
    --------------
  → ε ⊢ V `: A
type Zero              =  ⊢zero
type (Suc CV)          =  ⊢suc (type CV)
type (Fun {x = x} ⊢N)  =  ⊢λ ⊢N

value : ∀ {V A}
  → Canonical V A
    -------------
  → Value V
value Zero         =  Zero
value (Suc CV)     =  Suc (value CV)
value (Fun ⊢N)     =  Fun
\end{code}
    
## Progress

\begin{code}
data Progress (M : Term) (A : Type) : Set where
  step : ∀ {N}
    → M ⟶ N
      ----------
    → Progress M A
  done :
      Canonical M A
      -------------
    → Progress M A

progress : ∀ {M A} → ε ⊢ M `: A → Progress M A
progress (Ax ())
progress (⊢λ ⊢N)                           =  done (Fun ⊢N)
progress (⊢L · ⊢M) with progress ⊢L
...    | step L⟶L′                       =  step (ξ-·₁ L⟶L′)
...    | done (Fun _) with progress ⊢M
...            | step M⟶M′               =  step (ξ-·₂ Fun M⟶M′)
...            | done CM                   =  step (β-→ (value CM))
progress ⊢zero                             =  done Zero
progress (⊢suc ⊢M) with progress ⊢M
...    | step M⟶M′                       =  step (ξ-suc M⟶M′)
...    | done CM                           =  done (Suc CM)
progress (⊢pred ⊢M) with progress ⊢M
...    | step M⟶M′                       =  step (ξ-pred M⟶M′)
...    | done Zero                         =  step β-pred-zero
...    | done (Suc CM)                     =  step (β-pred-suc (value CM))
progress (⊢if0 ⊢L ⊢M ⊢N) with progress ⊢L
...    | step L⟶L′                       =  step (ξ-if0 L⟶L′)
...    | done Zero                         =  step β-if0-zero
...    | done (Suc CM)                     =  step (β-if0-suc (value CM))
progress (⊢Y ⊢M) with progress ⊢M
...    | step M⟶M′                       =  step (ξ-Y M⟶M′)
...    | done (Fun _)                      =  step (β-Y refl)
\end{code}


## Preservation

### Domain of an environment

\begin{code}
{-
dom : Ctx → List Id
dom ε            =  []
dom (Γ , x `: A)  =  x ∷ dom Γ

dom-lemma : ∀ {Γ y B} → Γ ∋ y `: B → y ∈ dom Γ
dom-lemma Z           =  here
dom-lemma (S x≢y ⊢y)  =  there (dom-lemma ⊢y)

free-lemma : ∀ {Γ M A} → Γ ⊢ M `: A → free M ⊆ dom Γ
free-lemma (Ax ⊢x) w∈ with w∈
...                      | here         =  dom-lemma ⊢x
...                      | there ()   
free-lemma {Γ} (⊢λ {N = N} ⊢N)          =  ∷-to-\\ (free-lemma ⊢N)
free-lemma (⊢L · ⊢M) w∈ with ++-to-⊎ w∈
...                        | inj₁ ∈L    = free-lemma ⊢L ∈L
...                        | inj₂ ∈M    = free-lemma ⊢M ∈M
free-lemma ⊢zero ()
free-lemma (⊢suc ⊢M) w∈                 = free-lemma ⊢M w∈
free-lemma (⊢pred ⊢M) w∈                = free-lemma ⊢M w∈
free-lemma (⊢if0 ⊢L ⊢M ⊢N) w∈
        with ++-to-⊎ w∈
...         | inj₁ ∈L                   = free-lemma ⊢L ∈L
...         | inj₂ ∈MN with ++-to-⊎ ∈MN
...                       | inj₁ ∈M     = free-lemma ⊢M ∈M
...                       | inj₂ ∈N     = free-lemma ⊢N ∈N
free-lemma (⊢Y ⊢M) w∈                   = free-lemma ⊢M w∈       
-}
\end{code}

### Renaming

\begin{code}
⊢rename : ∀ {Γ Δ}
  → (∀ {x A} → Γ ∋ x `: A  →  Δ ∋ x `: A)
    --------------------------------------------------
  → (∀ {M A} → Γ ⊢ M `: A  →  Δ ⊢ M `: A)
⊢rename ⊢σ (Ax ⊢x)          =  Ax (⊢σ ⊢x)
⊢rename {Γ} {Δ} ⊢σ (⊢λ {x = x} {N = N} {A = A} ⊢N)
                            =  ⊢λ (⊢rename {Γ′} {Δ′} ⊢σ′ ⊢N)
  where
  Γ′   =  Γ , x `: A
  Δ′   =  Δ , x `: A

  ⊢σ′ : ∀ {w B} → Γ′ ∋ w `: B → Δ′ ∋ w `: B
  ⊢σ′ Z          =  Z
  ⊢σ′ (S w≢ ⊢w)  =  S w≢ (⊢σ ⊢w)

⊢rename ⊢σ (⊢L · ⊢M)        =  ⊢rename ⊢σ ⊢L · ⊢rename ⊢σ ⊢M
⊢rename ⊢σ (⊢zero)          =  ⊢zero
⊢rename ⊢σ (⊢suc ⊢M)        =  ⊢suc (⊢rename ⊢σ ⊢M)
⊢rename ⊢σ (⊢pred ⊢M)       =  ⊢pred (⊢rename ⊢σ ⊢M)
⊢rename ⊢σ (⊢if0 ⊢L ⊢M ⊢N)
  = ⊢if0 (⊢rename ⊢σ ⊢L) (⊢rename ⊢σ ⊢M) (⊢rename ⊢σ ⊢N)
⊢rename ⊢σ (⊢Y ⊢M)          =  ⊢Y (⊢rename ⊢σ ⊢M)
\end{code}

### Check that a context and term satisfy Barendregt

\begin{code}
infix 3 _∉_
infix 3 _||_

_∉_ : Id → Ctx → Set
x ∉ Γ = ∀ {A} → ¬ (Γ ∋ x `: A)

data ok : ∀ {Γ M A} → (Γ ⊢ M `: A) → Set where

  ok-Ax : ∀ {Γ A x} {⊢x : Γ ∋ x `: A}
      -----------
    → ok (Ax ⊢x) 

  ok-λ : ∀ {Γ x N A B} {⊢N : Γ , x `: A ⊢ N `: B}
    → x ∉ Γ
    → ok ⊢N
      -----------
    → ok (⊢λ ⊢N)

  ok-· : ∀ {Γ L M A B} {⊢L : Γ ⊢ L `: A `→ B} {⊢M : Γ ⊢ M `: A}
    → ok ⊢L
    → ok ⊢M
      ------------
    → ok (⊢L · ⊢M)

  ok-zero : ∀ {Γ}
      ---------------
    → ok (⊢zero {Γ})

  ok-suc : ∀ {Γ M} {⊢M : Γ ⊢ M `: `ℕ}
    → ok ⊢M
      -------------
    → ok (⊢suc ⊢M)
  
  ok-pred : ∀ {Γ M} {⊢M : Γ ⊢ M `: `ℕ}
    → ok ⊢M
      --------------
    → ok (⊢pred ⊢M)

  okif0 : ∀ {Γ L M N A} {⊢L : Γ ⊢ L `: `ℕ} {⊢M : Γ ⊢ M `: A} {⊢N : Γ ⊢ N `: A}
    → ok ⊢L
    → ok ⊢M
    → ok ⊢N
      ------------------
    → ok (⊢if0 ⊢L ⊢M ⊢N)

  ok-Y : ∀ {Γ M A} {⊢M : Γ ⊢ M `: A `→ A}
    → ok ⊢M
      -------------
    → ok (⊢Y ⊢M)

bar-lemma : ∀ {Γ M A}
  → (⊢M : Γ ⊢ M `: A)
    ----------------------
  → Γ ⊢ barendregt M `: A
bar-lemma = {!!}

ok-lemma : ∀ {Γ M A}
  → (⊢M : Γ ⊢ M `: A)
    ------------------
  → ok (bar-lemma ⊢M)
ok-lemma = {!!}  
  
data  _||_ : Ctx → Term → Set where

  B-var : ∀ {Γ x}
    → x ∉ Γ
      -------------------
    → Γ || ` x

  B-λ : ∀ {Γ x N}
    → ∀ {A} → Γ , x `: A || N
      ------------------------
    → Γ || `λ x `→ N

  B-· : ∀ {Γ L M}
    → Γ || L
    → Γ || M
      ----------
    → Γ || L · M

  B-zero : ∀ {Γ}
      -----------
    → Γ || `zero

  B-suc : ∀ {Γ M}
    → Γ || M
      ------------
    → Γ || `suc M

  B-if0 : ∀ {Γ L M N}
    → Γ || L
    → Γ || M
    → Γ || N
      --------------------------
    → Γ || `if0 L then M else N

  B-Y : ∀ {Γ M}
    → Γ || M
      ----------
    → Γ || `Y M
\end{code}




### Substitution preserves types

\begin{code}
{-
⊢subst : ∀ {Γ Δ ρ}
  → (∀ {x A} → Δ ∋ x `: A  →  Γ ∋ x `: A)
  → (∀ {x A} → Γ ∋ x `: A  →  Δ ⊢ ρ x `: A)
    --------------------------------------------------------------
  → (∀ {M A} → (⊢M : Γ ⊢ M `: A) →  ok ⊢M  →  Δ ⊢ subst ρ M `: A)
-}
⊢subst : ∀ {Γ Δ ρ}
  → (∀ {x A} → Γ ∋ x `: A  →  Δ ⊢ ρ x `: A)
    ---------------------------------------------
  → (∀ {M A} → Γ ⊢ M `: A →  Δ ⊢ subst ρ M `: A)
⊢subst ⊢ρ (Ax ⊢x)                =  ⊢ρ ⊢x
⊢subst {Γ} {Δ} {ρ} ⊢ρ (⊢λ {x = x} {N = N} {A = A} ⊢N)
    = ⊢λ {x = x} {A = A} (⊢subst {Γ′} {Δ′} {ρ′} ⊢ρ′ ⊢N)
  where
  Γ′  =  Γ , x `: A
  Δ′  =  Δ , x `: A
  ρ′  =  ρ , x ↦ ` x

  ⊢σ : ∀ {w C} → Δ ∋ w `: C → Δ′ ∋ w `: C
  ⊢σ ⊢w  =  S {!!} ⊢w
    -- this follows because w in Δ implies w in Γ,
    -- and w in Γ implies w ≢ x.

  ⊢ρ′ : ∀ {w C} → Γ′ ∋ w `: C → Δ′ ⊢ ρ′ w `: C
  ⊢ρ′ {w} Z with w ≟ x
  ...         | yes _             =  Ax Z
  ...         | no  w≢            =  ⊥-elim (w≢ refl)
  ⊢ρ′ {w} (S w≢ ⊢w) with w ≟ x
  ...         | yes refl          =  ⊥-elim (w≢ refl)
  ...         | no  _             =  ⊢rename {Δ} {Δ′} ⊢σ (⊢ρ ⊢w)

⊢subst ⊢ρ (⊢L · ⊢M)              =  ⊢subst ⊢ρ ⊢L · ⊢subst ⊢ρ ⊢M
⊢subst ⊢ρ ⊢zero                  =  ⊢zero
⊢subst ⊢ρ (⊢suc ⊢M)              =  ⊢suc (⊢subst ⊢ρ ⊢M)
⊢subst ⊢ρ (⊢pred ⊢M)             =  ⊢pred (⊢subst ⊢ρ ⊢M)
⊢subst ⊢ρ (⊢if0 ⊢L ⊢M ⊢N)
    =  ⊢if0 (⊢subst ⊢ρ ⊢L) (⊢subst ⊢ρ ⊢M) (⊢subst ⊢ρ ⊢N)
⊢subst ⊢ρ (⊢Y ⊢M)                =  ⊢Y (⊢subst ⊢ρ ⊢M)
\end{code}

Let's look at examples.  Assume `M` is closed.  Example 1.

    subst (tm-∅ , "x" ↦ M) (`λ "y" `→ ` "x")  ≡  `λ "y" `→ M

Example 2.

      subst (tm-∅ , "y" ↦ ` "y" , "x" ↦ M) (`λ "y" `→ ` "x" · ` "y")
    ≡
      `λ "y" `→ subst (tm-∅ , "y" ↦ ` "y" , "x" ↦ M , "y" ↦ ` "y") (` "x" · ` "y")
    ≡
      `λ "y" `→ (M · ` "y")

The hypotheses of the theorem appear to be violated. Drat!

\begin{code}
⊢substitution : ∀ {Γ x A N B M}
  → Γ , x `: A ⊢ N `: B
  → Γ ⊢ M `: A
    ----------------------
  → Γ ⊢ N [ x := M ] `: B
⊢substitution {Γ} {x} {A} {N} {B} {M} ⊢N ⊢M =
  ⊢subst {Γ′} {Γ} {ρ} ⊢ρ {N} {B} ⊢N
  where
  Γ′     =  Γ , x `: A
  ρ      =  tm-∅ , x ↦ M
  ⊢ρ : ∀ {w B} → Γ′ ∋ w `: B → Γ ⊢ ρ w `: B
  ⊢ρ {w} Z         with w ≟ x
  ...                 | yes _     =  ⊢M
  ...                 | no  w≢    =  ⊥-elim (w≢ refl)
  ⊢ρ {w} (S w≢ ⊢w) with w ≟ x
  ...                 | yes refl  =  ⊥-elim (w≢ refl)
  ...                 | no  _     =  Ax ⊢w
\end{code}

### Preservation

\begin{code}
preservation : ∀ {Γ M N A}
  →  Γ ⊢ M `: A
  →  M ⟶ N
     ---------
  →  Γ ⊢ N `: A
preservation (Ax ⊢x) ()
preservation (⊢λ ⊢N) ()
preservation (⊢L · ⊢M)              (ξ-·₁ L⟶)    =  preservation ⊢L L⟶ · ⊢M
preservation (⊢V · ⊢M)              (ξ-·₂ _ M⟶)  =  ⊢V · preservation ⊢M M⟶
preservation ((⊢λ ⊢N) · ⊢W)         (β-→ _)       =  ⊢substitution ⊢N ⊢W
preservation (⊢zero)                ()
preservation (⊢suc ⊢M)              (ξ-suc M⟶)   =  ⊢suc (preservation ⊢M M⟶)
preservation (⊢pred ⊢M)             (ξ-pred M⟶)  =  ⊢pred (preservation ⊢M M⟶)
preservation (⊢pred ⊢zero)          (β-pred-zero)  =  ⊢zero
preservation (⊢pred (⊢suc ⊢M))      (β-pred-suc _) =  ⊢M
preservation (⊢if0 ⊢L ⊢M ⊢N)        (ξ-if0 L⟶)   =  ⊢if0 (preservation ⊢L L⟶) ⊢M ⊢N
preservation (⊢if0 ⊢zero ⊢M ⊢N)     β-if0-zero     =  ⊢M
preservation (⊢if0 (⊢suc ⊢V) ⊢M ⊢N) (β-if0-suc _)  =  ⊢N
preservation (⊢Y ⊢M)                (ξ-Y M⟶)     =  ⊢Y (preservation ⊢M M⟶)
preservation (⊢Y (⊢λ ⊢N))           (β-Y refl)     =  ⊢substitution ⊢N (⊢Y (⊢λ ⊢N))
\end{code}

## Normalise

\begin{code}
data Normalise {M A} (⊢M : ε ⊢ M `: A) : Set where
  out-of-gas : ∀ {N} → M ⟶* N → ε ⊢ N `: A → Normalise ⊢M
  normal     : ∀ {V} → ℕ → Canonical V A → M ⟶* V → Normalise ⊢M

normalise : ∀ {L A} → ℕ → (⊢L : ε ⊢ L `: A) → Normalise ⊢L
normalise {L} zero    ⊢L                   =  out-of-gas (L ∎) ⊢L
normalise {L} (suc m) ⊢L with progress ⊢L
...  | done CL                             =  normal (suc m) CL (L ∎)
...  | step L⟶M with preservation ⊢L L⟶M
...      | ⊢M with normalise m ⊢M
...          | out-of-gas M⟶*N ⊢N        =  out-of-gas (L ⟶⟨ L⟶M ⟩ M⟶*N) ⊢N
...          | normal n CV M⟶*V          =  normal n CV (L ⟶⟨ L⟶M ⟩ M⟶*V)
\end{code}

