From 84f79d3ab7f2cea99a8ce21458913dfc56388bda Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Tue, 3 Jul 2018 12:51:44 -0300
Subject: [PATCH] setup for bisimulation

---
 src/plta/DeBruijn.lagda |   4 +-
 src/plta/More.lagda     | 365 ++++++++++++++++++++++------------------
 2 files changed, 204 insertions(+), 165 deletions(-)

diff --git a/src/plta/DeBruijn.lagda b/src/plta/DeBruijn.lagda
index 15f533c7..629a3852 100644
--- a/src/plta/DeBruijn.lagda
+++ b/src/plta/DeBruijn.lagda
@@ -330,13 +330,13 @@ judgements:
 * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ ``
 
 They correspond to the following inherently-typed variables.
--- \begin{code}
+\begin{code}
 _ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ
 _ = Z
 
 _ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ ⇒ `ℕ
 _ = S Z
--- \end{code}
+\end{code}
 In the given context, `"z"` is represented by `Z`, and `"s"` by `S Z`.
 
 ### Terms and the typing judgement
diff --git a/src/plta/More.lagda b/src/plta/More.lagda
index 1d720430..5b59b682 100644
--- a/src/plta/More.lagda
+++ b/src/plta/More.lagda
@@ -18,7 +18,6 @@ description will be informal.  We show how to formalise a few
 of the constructs, but leave the rest as an exercise for the
 reader.
 
-
 ## Imports
 
 \begin{code}
@@ -37,17 +36,20 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
 ## Syntax
 
 \begin{code}
-infixl 6 _,_
 infix  4 _⊢_
 infix  4 _∋_
-infixr 5 _⇒_
-infixr 6 _`⊎_
-infixr 7 _`×_
+infixl 5 _,_
 
-infix  4 ƛ_
-infix  4 μ_
-infixl 5 _·_
-infix  6 S_
+infixr 7 _⇒_
+infixr 8 _`⊎_
+infixr 9 _`×_
+
+infix  5 ƛ_
+infix  5 μ_
+infixl 7 _·_
+infix  8 `suc_
+infix  9 `_
+infix  9 S_
 
 data Type : Set where
   `ℕ    : Type
@@ -59,7 +61,7 @@ data Type : Set where
   `List : Type → Type
 
 data Env : Set where
-  ε   : Env
+  ∅   : Env
   _,_ : Env → Type → Env
 
 data _∋_ : Env → Type → Set where
@@ -75,7 +77,7 @@ data _∋_ : Env → Type → Set where
 
 data _⊢_ : Env → Type → Set where
 
-  ⌊_⌋ : ∀ {Γ} {A}
+  `_ : ∀ {Γ} {A}
     → Γ ∋ A
       ------
     → Γ ⊢ A
@@ -95,7 +97,7 @@ data _⊢_ : Env → Type → Set where
       ----------
     → Γ ⊢ `ℕ
 
-  `suc : ∀ {Γ}
+  `suc_ : ∀ {Γ}
     → Γ ⊢ `ℕ
       -------
     → Γ ⊢ `ℕ
@@ -190,69 +192,69 @@ Simultaneous substitution, a la McBride
 
 \begin{code}
 ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
-ext σ Z      =  Z
-ext σ (S x)  =  S (σ x)
+ext ρ Z      =  Z
+ext ρ (S x)  =  S (ρ x)
 
 rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
-rename σ (⌊ n ⌋)         =  ⌊ σ n ⌋
-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 σ (μ N)           =  μ (rename (ext σ) N)
-rename σ `⟨ M , N ⟩      =  `⟨ rename σ M , rename σ N ⟩
-rename σ (`proj₁ L)      =  `proj₁ (rename σ L)
-rename σ (`proj₂ L)      =  `proj₂ (rename σ L)
-rename σ (`inj₁ M)       =  `inj₁ (rename σ M)
-rename σ (`inj₂ N)       =  `inj₂ (rename σ N)
-rename σ (`case⊎ L M N)  =  `case⊎ (rename σ L) (rename (ext σ) M) (rename (ext σ) N)
-rename σ `tt             =  `tt
-rename σ (`case⊥ L)      =  `case⊥ (rename σ L)
-rename σ `[]             =  `[]
-rename σ (M `∷ N)        =  (rename σ M) `∷ (rename σ N)
-rename σ (`caseL L M N)  =  `caseL (rename σ L) (rename σ M) (rename (ext (ext σ)) N)
-rename σ (`let M N)      =  `let (rename σ M) (rename (ext σ) N)
+rename ρ (` x)           =  ` (ρ x)
+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 ρ (μ N)           =  μ (rename (ext ρ) N)
+rename ρ `⟨ M , N ⟩      =  `⟨ rename ρ M , rename ρ N ⟩
+rename ρ (`proj₁ L)      =  `proj₁ (rename ρ L)
+rename ρ (`proj₂ L)      =  `proj₂ (rename ρ L)
+rename ρ (`inj₁ M)       =  `inj₁ (rename ρ M)
+rename ρ (`inj₂ N)       =  `inj₂ (rename ρ N)
+rename ρ (`case⊎ L M N)  =  `case⊎ (rename ρ L) (rename (ext ρ) M) (rename (ext ρ) N)
+rename ρ `tt             =  `tt
+rename ρ (`case⊥ L)      =  `case⊥ (rename ρ L)
+rename ρ `[]             =  `[]
+rename ρ (M `∷ N)        =  (rename ρ M) `∷ (rename ρ N)
+rename ρ (`caseL L M N)  =  `caseL (rename ρ L) (rename ρ M) (rename (ext (ext ρ)) N)
+rename ρ (`let M N)      =  `let (rename ρ M) (rename (ext ρ) N)
 \end{code}
 
 ## Substitution
 
 \begin{code}
 exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B)
-exts ρ Z      =  ⌊ Z ⌋
-exts ρ (S x)  =  rename S_ (ρ x)
+exts σ Z      =  ` Z
+exts σ (S x)  =  rename S_ (σ x)
 
 subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ ⊢ C → Δ ⊢ C)
-subst ρ (⌊ k ⌋)         =  ρ k
-subst ρ (ƛ N)           =  ƛ (subst (exts ρ) N)
-subst ρ (L · M)         =  (subst ρ L) · (subst ρ M)
-subst ρ (`zero)         =  `zero
-subst ρ (`suc M)        =  `suc (subst ρ M)
-subst ρ (`caseℕ L M N)  =  `caseℕ (subst ρ L) (subst ρ M) (subst (exts ρ) N)
-subst ρ (μ N)           =  μ (subst (exts ρ) N)
-subst ρ `⟨ M , N ⟩      =  `⟨ subst ρ M , subst ρ N ⟩
-subst ρ (`proj₁ L)      =  `proj₁ (subst ρ L)
-subst ρ (`proj₂ L)      =  `proj₂ (subst ρ L)
-subst ρ (`inj₁ M)       =  `inj₁ (subst ρ M)
-subst ρ (`inj₂ N)       =  `inj₂ (subst ρ N)
-subst ρ (`case⊎ L M N)  =  `case⊎ (subst ρ L) (subst (exts ρ) M) (subst (exts ρ) N)
-subst ρ `tt             =  `tt
-subst ρ (`case⊥ L)      =  `case⊥ (subst ρ L)
-subst ρ `[]             =  `[]
-subst ρ (M `∷ N)        =  (subst ρ M) `∷ (subst ρ N)
-subst ρ (`caseL L M N)  =  `caseL (subst ρ L) (subst ρ M) (subst (exts (exts ρ)) N)
-subst ρ (`let M N)      =  `let (subst ρ M) (subst (exts ρ) N)
+subst σ (` k)         =  σ k
+subst σ (ƛ N)           =  ƛ (subst (exts σ) N)
+subst σ (L · M)         =  (subst σ L) · (subst σ M)
+subst σ (`zero)         =  `zero
+subst σ (`suc M)        =  `suc (subst σ M)
+subst σ (`caseℕ L M N)  =  `caseℕ (subst σ L) (subst σ M) (subst (exts σ) N)
+subst σ (μ N)           =  μ (subst (exts σ) N)
+subst σ `⟨ M , N ⟩      =  `⟨ subst σ M , subst σ N ⟩
+subst σ (`proj₁ L)      =  `proj₁ (subst σ L)
+subst σ (`proj₂ L)      =  `proj₂ (subst σ L)
+subst σ (`inj₁ M)       =  `inj₁ (subst σ M)
+subst σ (`inj₂ N)       =  `inj₂ (subst σ N)
+subst σ (`case⊎ L M N)  =  `case⊎ (subst σ L) (subst (exts σ) M) (subst (exts σ) N)
+subst σ `tt             =  `tt
+subst σ (`case⊥ L)      =  `case⊥ (subst σ L)
+subst σ `[]             =  `[]
+subst σ (M `∷ N)        =  (subst σ M) `∷ (subst σ N)
+subst σ (`caseL L M N)  =  `caseL (subst σ L) (subst σ M) (subst (exts (exts σ)) N)
+subst σ (`let M N)      =  `let (subst σ M) (subst (exts σ) N)
 
 _[_] : ∀ {Γ A B}
   → Γ , A ⊢ B
   → Γ ⊢ A
   ------------
   → Γ ⊢ B
-_[_] {Γ} {A} N V =  subst {Γ , A} {Γ} ρ N
+_[_] {Γ} {A} N V =  subst {Γ , A} {Γ} σ N
   where
-  ρ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
-  ρ Z      =  V
-  ρ (S x)  =  ⌊ x ⌋
+  σ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
+  σ Z      =  V
+  σ (S x)  =  ` x
 
 _[_][_] : ∀ {Γ A B C}
   → Γ , A , B ⊢ C
@@ -260,12 +262,12 @@ _[_][_] : ∀ {Γ A B C}
   → Γ ⊢ B
     ---------------
   → Γ ⊢ C
-_[_][_] {Γ} {A} {B} N V W =  subst {Γ , A , B} {Γ} ρ N
+_[_][_] {Γ} {A} {B} N V W =  subst {Γ , A , B} {Γ} σ N
   where
-  ρ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C
-  ρ Z          =  W
-  ρ (S Z)      =  V
-  ρ (S (S x))  =  ⌊ x ⌋
+  σ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C
+  σ Z          =  W
+  σ (S Z)      =  V
+  σ (S (S x))  =  ` x
 \end{code}
 
 ## Value
@@ -323,172 +325,172 @@ not fixed by the given arguments.
 ## Reduction step
 
 \begin{code}
-infix 2 _⟶_
+infix 2 _—→_
 
-data _⟶_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
   ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
-    → L ⟶ L′
+    → L —→ L′
       -----------------
-    → L · M ⟶ L′ · M
+    → L · M —→ L′ · M
 
   ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
     → Value V
-    → M ⟶ M′
+    → M —→ M′
       -----------------
-    → V · M ⟶ V · M′
+    → V · M —→ V · M′
 
   β-⇒ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
     → Value W
       ---------------------
-    → (ƛ N) · W ⟶ N [ W ]
+    → (ƛ N) · W —→ N [ W ]
 
   ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
-    → M ⟶ M′
+    → M —→ M′
       -------------------
-    → `suc M ⟶ `suc M′
+    → `suc M —→ `suc M′
 
   ξ-caseℕ : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
-    → L ⟶ L′
+    → L —→ L′
       -------------------------------
-    → `caseℕ L M N ⟶ `caseℕ L′ M N
+    → `caseℕ L M N —→ `caseℕ L′ M N
 
   β-ℕ₁ :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
       -----------------------
-    → `caseℕ `zero M N ⟶ M
+    → `caseℕ `zero M N —→ M
 
   β-ℕ₂ : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
     → Value V
       --------------------------------
-    → `caseℕ (`suc V) M N ⟶ N [ V ]
+    → `caseℕ (`suc V) M N —→ N [ V ]
 
   β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
       ------------------
-    → μ N ⟶ N [ μ N ]
+    → μ N —→ N [ μ N ]
 
   ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B}
-    → M ⟶ M′
+    → M —→ M′
       --------------------------
-    → `⟨ M , N ⟩ ⟶ `⟨ M′ , N ⟩
+    → `⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
 
   ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B}
     → Value V
-    → N ⟶ N′
+    → N —→ N′
       --------------------------
-    → `⟨ V , N ⟩ ⟶ `⟨ V , N′ ⟩
+    → `⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
 
   ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
-    → L ⟶ L′
+    → L —→ L′
       -----------------------
-    → `proj₁ L ⟶ `proj₁ L′
+    → `proj₁ L —→ `proj₁ L′
 
   ξ-proj₂ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
-    → L ⟶ L′
+    → L —→ L′
       -----------------------
-    → `proj₂ L ⟶ `proj₂ L′
+    → `proj₂ L —→ `proj₂ L′
 
   β-×₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
     → Value V
     → Value W
       ------------------------
-    → `proj₁ `⟨ V , W ⟩ ⟶ V
+    → `proj₁ `⟨ V , W ⟩ —→ V
 
   β-×₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
     → Value V
     → Value W
       ------------------------
-    → `proj₂ `⟨ V , W ⟩ ⟶ W
+    → `proj₂ `⟨ V , W ⟩ —→ W
 
   ξ-inj₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A}
-    → M ⟶ M′
+    → M —→ M′
       -----------------------------
-    → `inj₁ {B = B} M ⟶ `inj₁ M′
+    → `inj₁ {B = B} M —→ `inj₁ M′
 
   ξ-inj₂ : ∀ {Γ A B} {N N′ : Γ ⊢ B}
-    → N ⟶ N′
+    → N —→ N′
       -----------------------------
-    → `inj₂ {A = A} N ⟶ `inj₂ N′
+    → `inj₂ {A = A} N —→ `inj₂ N′
 
   ξ-case⊎ : ∀ {Γ A B C} {L L′ : Γ ⊢ A `⊎ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
-    → L ⟶ L′
+    → L —→ L′
       -------------------------------
-    → `case⊎ L M N ⟶ `case⊎ L′ M N
+    → `case⊎ L M N —→ `case⊎ L′ M N
 
   β-⊎₁ : ∀ {Γ A B C} {V : Γ ⊢ A} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
     → Value V
       ---------------------------------
-    → `case⊎ (`inj₁ V) M N ⟶ M [ V ]
+    → `case⊎ (`inj₁ V) M N —→ M [ V ]
 
   β-⊎₂ : ∀ {Γ A B C} {W : Γ ⊢ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
     → Value W
       ---------------------------------
-    → `case⊎ (`inj₂ W) M N ⟶ N [ W ]
+    → `case⊎ (`inj₂ W) M N —→ N [ W ]
 
   ξ-case⊥ : ∀ {Γ A} {L L′ : Γ ⊢ `⊥}
-    → L ⟶ L′
+    → L —→ L′
       -------------------------------
-    → `case⊥ {A = A} L ⟶ `case⊥ L′
+    → `case⊥ {A = A} L —→ `case⊥ L′
 
   ξ-∷₁ : ∀ {Γ A} {M M′ : Γ ⊢ A} {N : Γ ⊢ `List A}
-    → M ⟶ M′
+    → M —→ M′
       -------------------
-    → M `∷ N ⟶ M′ `∷ N
+    → M `∷ N —→ M′ `∷ N
 
   ξ-∷₂ : ∀ {Γ A} {V : Γ ⊢ A} {N N′ : Γ ⊢ `List A}
     → Value V
-    → N ⟶ N′
+    → N —→ N′
       -------------------
-    → V `∷ N ⟶ V `∷ N′
+    → V `∷ N —→ V `∷ N′
 
   ξ-caseL : ∀ {Γ A B} {L L′ : Γ ⊢ `List A} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
-    → L ⟶ L′
+    → L —→ L′
       -------------------------------
-    → `caseL L M N ⟶ `caseL L′ M N
+    → `caseL L M N —→ `caseL L′ M N
 
   β-List₁ : ∀ {Γ A B} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
       ---------------------
-    → `caseL `[] M N ⟶ M
+    → `caseL `[] M N —→ M
 
   β-List₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ `List A}
     {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
     → Value V
     → Value W
       -------------------------------------
-    → `caseL (V `∷ W) M N ⟶ N [ V ][ W ]
+    → `caseL (V `∷ W) M N —→ N [ V ][ W ]
 
   ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B}
-    → M ⟶ M′
+    → M —→ M′
       -----------------------
-    → `let M N ⟶ `let M′ N
+    → `let M N —→ `let M′ N
 
   β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B}
     → Value V
       ---------------------
-    → `let V N ⟶ N [ V ]
+    → `let V N —→ N [ V ]
 \end{code}
 
 ## Reflexive and transitive closure
 
 \begin{code}
-infix  2 _⟶*_
+infix  2 _—↠_
 infix 1 begin_
-infixr 2 _⟶⟨_⟩_
+infixr 2 _—→⟨_⟩_
 infix 3 _∎
 
-data _⟶*_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
   _∎ : ∀ {Γ A} (M : Γ ⊢ A)
       --------
-    → M ⟶* M
+    → M —↠ M
 
-  _⟶⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
-    → L ⟶ M
-    → M ⟶* N
+  _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+    → L —→ M
+    → M —↠ N
       ---------
-    → L ⟶* N
+    → L —↠ N
 
-begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M ⟶* N) → (M ⟶* N)
-begin M⟶*N = M⟶*N
+begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M —↠ N) → (M —↠ N)
+begin M—↠N = M—↠N
 \end{code}
 
 
@@ -496,33 +498,33 @@ begin M⟶*N = M⟶*N
 
 Values do not reduce.
 \begin{code}
-Value-lemma : ∀ {Γ A} {M N : Γ ⊢ A} → Value M → ¬ (M ⟶ N)
+Value-lemma : ∀ {Γ A} {M N : Γ ⊢ A} → Value M → ¬ (M —→ N)
 Value-lemma Fun         ()
 Value-lemma Zero        ()
-Value-lemma (Suc VM)    (ξ-suc M⟶M′)     =  Value-lemma VM M⟶M′
-Value-lemma (Pair VM _) (ξ-⟨,⟩₁ M⟶M′)    =  Value-lemma VM M⟶M′
-Value-lemma (Pair _ VN) (ξ-⟨,⟩₂ _ N⟶N′)  =  Value-lemma VN N⟶N′
-Value-lemma (Inj₁ VM)   (ξ-inj₁ M⟶M′)    =  Value-lemma VM M⟶M′
-Value-lemma (Inj₂ VN)   (ξ-inj₂ N⟶N′)    =  Value-lemma VN N⟶N′
+Value-lemma (Suc VM)    (ξ-suc M—→M′)     =  Value-lemma VM M—→M′
+Value-lemma (Pair VM _) (ξ-⟨,⟩₁ M—→M′)    =  Value-lemma VM M—→M′
+Value-lemma (Pair _ VN) (ξ-⟨,⟩₂ _ N—→N′)  =  Value-lemma VN N—→N′
+Value-lemma (Inj₁ VM)   (ξ-inj₁ M—→M′)    =  Value-lemma VM M—→M′
+Value-lemma (Inj₂ VN)   (ξ-inj₂ N—→N′)    =  Value-lemma VN N—→N′
 Value-lemma TT          ()
 Value-lemma Nil         ()
-Value-lemma (Cons VM _) (ξ-∷₁ M⟶M′)      =  Value-lemma VM M⟶M′
-Value-lemma (Cons _ VN) (ξ-∷₂ _ N⟶N′)    =  Value-lemma VN N⟶N′
+Value-lemma (Cons VM _) (ξ-∷₁ M—→M′)      =  Value-lemma VM M—→M′
+Value-lemma (Cons _ VN) (ξ-∷₂ _ N—→N′)    =  Value-lemma VN N—→N′
 \end{code}
 
 As a corollary, terms that reduce are not values.
 \begin{code}
-⟶-corollary : ∀ {Γ A} {M N : Γ ⊢ A} → (M ⟶ N) → ¬ Value M
-⟶-corollary M⟶N VM  =  Value-lemma VM M⟶N
+—→-corollary : ∀ {Γ A} {M N : Γ ⊢ A} → (M —→ N) → ¬ Value M
+—→-corollary M—→N VM  =  Value-lemma VM M—→N
 \end{code}
 
 
 ## Progress
 
 \begin{code}
-data Progress {A} (M : ε ⊢ A) : Set where
-  step : ∀ {N : ε ⊢ A}
-    → M ⟶ N
+data Progress {A} (M : ∅ ⊢ A) : Set where
+  step : ∀ {N : ∅ ⊢ A}
+    → M —→ N
       -------------
     → Progress M
   done :
@@ -530,60 +532,60 @@ data Progress {A} (M : ε ⊢ A) : Set where
       ----------
     → Progress M
 
-progress : ∀ {A} → (M : ε ⊢ A) → Progress M
-progress ⌊ () ⌋
+progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
+progress (` ())
 progress (ƛ N)                             =  done Fun
 progress (L · M) with progress L
-...    | step L⟶L′                       =  step (ξ-·₁ L⟶L′)
+...    | step L—→L′                       =  step (ξ-·₁ L—→L′)
 ...    | done Fun with progress M
-...        | step M⟶M′                   =  step (ξ-·₂ Fun M⟶M′)
+...        | step M—→M′                   =  step (ξ-·₂ Fun M—→M′)
 ...        | done VM                       =  step (β-⇒ VM)
 progress (`zero)                           =  done Zero
 progress (`suc M) with progress M
-...    | step M⟶M′                       =  step (ξ-suc M⟶M′)
+...    | step M—→M′                       =  step (ξ-suc M—→M′)
 ...    | done VM                           =  done (Suc VM)
 progress (`caseℕ L M N) with progress L
-...    | step L⟶L′                       =  step (ξ-caseℕ L⟶L′)
+...    | step L—→L′                       =  step (ξ-caseℕ L—→L′)
 ...    | done Zero                         =  step β-ℕ₁
 ...    | done (Suc VL)                     =  step (β-ℕ₂ VL)
 progress (μ N)                             =  step β-μ
 progress `⟨ M , N ⟩ with progress M
-...    | step M⟶M′                       =  step (ξ-⟨,⟩₁ M⟶M′)
+...    | step M—→M′                       =  step (ξ-⟨,⟩₁ M—→M′)
 ...    | done VM with progress N
-...        | step N⟶N′                   =  step (ξ-⟨,⟩₂ VM N⟶N′)
+...        | step N—→N′                   =  step (ξ-⟨,⟩₂ VM N—→N′)
 ...        | done VN                       =  done (Pair VM VN)
 progress (`proj₁ L) with progress L
-...    | step L⟶L′                       =  step (ξ-proj₁ L⟶L′)
+...    | step L—→L′                       =  step (ξ-proj₁ L—→L′)
 ...    | done (Pair VM VN)                 =  step (β-×₁ VM VN)
 progress (`proj₂ L) with progress L
-...    | step L⟶L′                       =  step (ξ-proj₂ L⟶L′)
+...    | step L—→L′                       =  step (ξ-proj₂ L—→L′)
 ...    | done (Pair VM VN)                 =  step (β-×₂ VM VN)
 progress (`inj₁ M) with progress M
-...    | step M⟶M′                       =  step (ξ-inj₁ M⟶M′)
+...    | step M—→M′                       =  step (ξ-inj₁ M—→M′)
 ...    | done VM                           =  done (Inj₁ VM)
 progress (`inj₂ N) with progress N
-...    | step N⟶N′                       =  step (ξ-inj₂ N⟶N′)
+...    | step N—→N′                       =  step (ξ-inj₂ N—→N′)
 ...    | done VN                           =  done (Inj₂ VN)
 progress (`case⊎ L M N) with progress L
-...    | step L⟶L′                       =  step (ξ-case⊎ L⟶L′)
+...    | step L—→L′                       =  step (ξ-case⊎ L—→L′)
 ...    | done (Inj₁ VV)                    =  step (β-⊎₁ VV)
 ...    | done (Inj₂ VW)                    =  step (β-⊎₂ VW)
 progress (`tt)                             =  done TT
 progress (`case⊥ {A = A} L) with progress L
-...    | step L⟶L′                       =  step (ξ-case⊥ {A = A} L⟶L′)
+...    | step L—→L′                       =  step (ξ-case⊥ {A = A} L—→L′)
 ...    | done ()
 progress (`[])                             =  done Nil
 progress (M `∷ N) with progress M
-...    | step M⟶M′                       =  step (ξ-∷₁ M⟶M′)
+...    | step M—→M′                       =  step (ξ-∷₁ M—→M′)
 ...    | done VM with progress N
-...        | step N⟶N′                   =  step (ξ-∷₂ VM N⟶N′)
+...        | step N—→N′                   =  step (ξ-∷₂ VM N—→N′)
 ...        | done VN                       =  done (Cons VM VN)
 progress (`caseL L M N) with progress L
-...    | step L⟶L′                       =  step (ξ-caseL L⟶L′)
+...    | step L—→L′                       =  step (ξ-caseL L—→L′)
 ...    | done Nil                          =  step β-List₁
 ...    | done (Cons VV VW)                 =  step (β-List₂ VV VW)
 progress (`let M N) with progress M
-...    | step M⟶M′                       =  step (ξ-let M⟶M′)
+...    | step M—→M′                       =  step (ξ-let M—→M′)
 ...    | done VM                           =  step (β-let VM)
 \end{code}
 
@@ -591,27 +593,64 @@ progress (`let M N) with progress M
 ## Normalise
 
 \begin{code}
-Gas : Set
-Gas = ℕ
+data Gas : Set where
+  gas : ℕ → Gas
 
-data Normalise {A} (M : ε ⊢ A) : Set where
-  normal : ∀ {N : ε ⊢ A}
-    → Gas
-    → M ⟶* N
-      -----------
-    → Normalise M
+data Finished {Γ A} (N : Γ ⊢ A) : Set where
 
-normalise : ∀ {A} → ℕ → (L : ε ⊢ A) → Normalise L
-normalise zero    L                         =  normal zero (L ∎)
-normalise (suc g) L with progress L
-...    | done VL                            =  normal (suc zero) (L ∎)
-...    | step {M} L⟶M with normalise g M
-...        | normal h M⟶*N                =  normal (suc h) (L ⟶⟨ L⟶M ⟩ M⟶*N)
+   done :
+       Value N
+       ----------
+     → Finished N
+
+   out-of-gas :
+       ----------
+       Finished N
+
+data Steps : ∀ {A} → ∅ ⊢ A → Set where
+
+  steps : ∀ {A} {L N : ∅ ⊢ A}
+    → L —↠ N
+    → Finished N
+      ----------
+    → Steps L
+
+eval : ∀ {A}
+  → Gas
+  → (L : ∅ ⊢ A)
+    -----------
+  → Steps L
+eval (gas zero)    L                     =  steps (L ∎) out-of-gas
+eval (gas (suc m)) L with progress L
+... | done VL                            =  steps (L ∎) (done VL)
+... | step {M} L—→M with eval (gas m) M
+...    | steps M—↠N fin                  =  steps (L —→⟨ L—→M ⟩ M—↠N) fin
 \end{code}
 
 
 ## Bisimulation
 
+\begin{code}
+data _~_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set where
 
+  ~` : ∀ {Γ A} {x : Γ ∋ A}
+     -------------
+   → (` x) ~ (` x)
 
+  ~ƛ : ∀ {Γ A B} {N N′ : Γ , A ⊢ B}
+    → N ~ N′
+      --------------
+    → (ƛ N) ~ (ƛ N′)
+
+  ~· : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
+    → L ~ L′
+    → M ~ M′
+      -------------------
+    → (L · M) ~ (L′ · M′)
+
+  ~let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N N′ : Γ , A ⊢ B}
+    → M ~ M′
+    → N ~ N′
+      --------------------------
+    → (`let M N) ~ ((ƛ N′) · M′)
 \end{code}