open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _*_; _<_; _≤?_; z≤n; s≤s)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂; module ≡-Reasoning)
open ≡-Reasoning
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Decidable using (True; toWitness)

-- #### Exercise `More` (recommended and practice)

-- Formalise the remaining constructs defined in this chapter.
-- Make your changes in this file.
-- Evaluate each example, applied to data as needed,
-- to confirm it returns the expected answer:

--   * sums (recommended)
--   * unit type (practice)
--   * an alternative formulation of unit type (practice)
--   * empty type (recommended)
--   * lists (practice)

-- Please delimit any code you add as follows:

--     -- begin
--     -- end

-- Fixities

infix  4 _⊢_
infix  4 _∋_
infixl 5 _,_

infixr 7 _⇒_
infixr 9 _`×_
-- begin
infixr 8 _`⊎_
-- end

infix  5 ƛ_
infix  5 μ_
infixl 7 _·_
infixl 8 _`*_
infix  8 `suc_
infix  9 `_
infix  9 S_

-- Types

data Type : Set where
  `ℕ    : Type
  _⇒_   : Type → Type → Type
  Nat   : Type
  _`×_  : Type → Type → Type
  -- begin
  _`⊎_  : Type → Type → Type
  `⊤    : Type
  `⊥    : Type
  `List : Type → Type
  -- end

-- Contexts

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

-- Variables and the lookup judgment

data _∋_ : Context → Type → Set where

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

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

-- Terms and the typing judgment

data _⊢_ : Context → Type → Set where

  -- variables

  `_ : ∀ {Γ A}
    → Γ ∋ A
      -----
    → Γ ⊢ A

  -- functions

  ƛ_  :  ∀ {Γ A B}
    → Γ , A ⊢ B
      ---------
    → Γ ⊢ A ⇒ B

  _·_ : ∀ {Γ A B}
    → Γ ⊢ A ⇒ B
    → Γ ⊢ A
      ---------
    → Γ ⊢ B

  -- naturals

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

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

  case : ∀ {Γ A}
    → Γ ⊢ `ℕ
    → Γ ⊢ A
    → Γ , `ℕ ⊢ A
      -----
    → Γ ⊢ A

  -- fixpoint

  μ_ : ∀ {Γ A}
    → Γ , A ⊢ A
      ----------
    → Γ ⊢ A

  -- primitive numbers

  con : ∀ {Γ}
    → ℕ
      -------
    → Γ ⊢ Nat

  _`*_ : ∀ {Γ}
    → Γ ⊢ Nat
    → Γ ⊢ Nat
      -------
    → Γ ⊢ Nat

  -- let

  `let : ∀ {Γ A B}
    → Γ ⊢ A
    → Γ , A ⊢ B
      ----------
    → Γ ⊢ B

  -- products

  `⟨_,_⟩ : ∀ {Γ A B}
    → Γ ⊢ A
    → Γ ⊢ B
      -----------
    → Γ ⊢ A `× B

  `proj₁ : ∀ {Γ A B}
    → Γ ⊢ A `× B
      -----------
    → Γ ⊢ A

  `proj₂ : ∀ {Γ A B}
    → Γ ⊢ A `× B
      -----------
    → Γ ⊢ B

  -- alternative formulation of products

  case× : ∀ {Γ A B C}
    → Γ ⊢ A `× B
    → Γ , A , B ⊢ C
      --------------
    → Γ ⊢ C

  -- begin

  -- sums

  `inj₁ : ∀ {Γ A B}
    → Γ ⊢ A
    → Γ ⊢ A `⊎ B

  `inj₂ : ∀ {Γ A B}
    → Γ ⊢ B
    → Γ ⊢ A `⊎ B

  case⊎_[inj₁⇒_|inj₂⇒_] : ∀ {Γ A B C}
    → Γ ⊢ A `⊎ B
    → Γ , A ⊢ C
    → Γ , B ⊢ C
    → Γ ⊢ C

  -- unit

  `tt : ∀ {Γ}
    → Γ ⊢ `⊤

  case⊤_[tt⇒_] : ∀ {Γ A}
    → Γ ⊢ `⊤
    → Γ ⊢ A
    → Γ ⊢ A

  -- empty

  -- This is called `⊥-elim` in Agda.
  case⊥ : ∀ {Γ C}
    → Γ ⊢ `⊥
    → Γ ⊢ C

  -- lists

  `[] : ∀ {Γ A}
    → Γ ⊢ `List A

  _`∷_ : ∀ {Γ A}
    → Γ ⊢ A
    → Γ ⊢ `List A
    → Γ ⊢ `List A

  caseL_[[]⇒_|x∷y⇒_] : ∀ {Γ A B}
    → Γ ⊢ `List A
    → Γ ⊢ B
    → Γ , A , `List A ⊢ B
    → Γ ⊢ B

  -- end

-- Renaming

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

rename : ∀ {Γ Δ}
  → (∀ {A} → Γ ∋ A → Δ ∋ A)
    -----------------------
  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
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 ρ (con n)                         =  con n
rename ρ (M `* N)                        =  rename ρ M `* rename ρ N
rename ρ (`let M N)                      =  `let (rename ρ M) (rename (ext ρ) N)
rename ρ `⟨ M , N ⟩                      =  `⟨ rename ρ M , rename ρ N ⟩
rename ρ (`proj₁ L)                      =  `proj₁ (rename ρ L)
rename ρ (`proj₂ L)                      =  `proj₂ (rename ρ L)
rename ρ (case× L M)                     =  case× (rename ρ L) (rename (ext (ext ρ)) M)
-- begin
rename ρ (`inj₁ M)                       = `inj₁ (rename ρ M)
rename ρ (`inj₂ M)                       = `inj₂ (rename ρ M)
rename ρ (case⊎ M [inj₁⇒ M₁ |inj₂⇒ M₂ ]) = case⊎ rename ρ M [inj₁⇒ rename (ext ρ) M₁
                                                            |inj₂⇒ rename (ext ρ) M₂ ]
rename ρ `tt                             = `tt
rename ρ case⊤ M [tt⇒ M₁ ]               = case⊤ rename ρ M [tt⇒ rename ρ M₁ ]
rename ρ (case⊥ M)                       = case⊥ (rename ρ M)
rename ρ `[]                             = `[]
rename ρ (M₁ `∷ M₂)                      = (rename ρ M₁) `∷ (rename ρ M₂)
rename ρ caseL M [[]⇒ M₁ |x∷y⇒ M₂ ]      = caseL rename ρ M [[]⇒  rename ρ M₁
                                                            |x∷y⇒ rename (ext (ext ρ)) M₂ ]
-- end

-- Simultaneous Substitution

exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B)
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 σ (con n)                         =  con n
subst σ (M `* N)                        =  subst σ M `* subst σ N
subst σ (`let M N)                      =  `let (subst σ M) (subst (exts σ) N)
subst σ `⟨ M , N ⟩                      =  `⟨ subst σ M , subst σ N ⟩
subst σ (`proj₁ L)                      =  `proj₁ (subst σ L)
subst σ (`proj₂ L)                      =  `proj₂ (subst σ L)
subst σ (case× L M)                     =  case× (subst σ L) (subst (exts (exts σ)) M)
-- begin
subst σ (`inj₁ M)                       = `inj₁ (subst σ M)
subst σ (`inj₂ M)                       = `inj₂ (subst σ M)
subst σ (case⊎ M [inj₁⇒ M₁ |inj₂⇒ M₂ ]) = case⊎ subst σ M [inj₁⇒ subst (exts σ) M₁
                                                          |inj₂⇒ subst (exts σ) M₂ ]
subst σ `tt                             = `tt
subst σ case⊤ M [tt⇒ M₁ ]               = case⊤ subst σ M [tt⇒ subst σ M₁ ]
subst σ (case⊥ M)                       = case⊥ (subst σ M)
subst σ `[]                             = `[]
subst σ (M₁ `∷ M₂)                      = (subst σ M₁) `∷ (subst σ M₂)
subst σ caseL M [[]⇒ M₁ |x∷y⇒ M₂ ]      = caseL subst σ M [[]⇒  subst σ M₁
                                                          |x∷y⇒ subst (exts (exts σ)) M₂ ]
-- end

-- Single and double substitution

substZero : ∀ {Γ}{A B} → Γ ⊢ A → Γ , A ∋ B → Γ ⊢ B
substZero V Z      =  V
substZero V (S x)  =  ` x

_[_] : ∀ {Γ A B}
  → Γ , A ⊢ B
  → Γ ⊢ A
    ---------
  → Γ ⊢ B
_[_] {Γ} {A} N V =  subst {Γ , A} {Γ} (substZero V) N

substZeroOne : ∀ {Γ A B C}
  → Γ ⊢ A
  → Γ ⊢ B
  → Γ , A , B ∋ C → Γ ⊢ C
substZeroOne V W Z          =  W
substZeroOne V W (S Z)      =  V
substZeroOne V W (S (S x))  =  ` x

_[_][_] : ∀ {Γ A B C}
  → Γ , A , B ⊢ C
  → Γ ⊢ A
  → Γ ⊢ B
    -------------
  → Γ ⊢ C
_[_][_] {Γ} {A} {B} N V W =  subst {Γ , A , B} {Γ} (substZeroOne V W) N

-- Values

data Value : ∀ {Γ A} → Γ ⊢ A → Set where

  -- functions

  V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
      ---------------------------
    → Value (ƛ N)

  -- naturals

  V-zero : ∀ {Γ}
      -----------------
    → Value (`zero {Γ})

  V-suc_ : ∀ {Γ} {V : Γ ⊢ `ℕ}
    → Value V
      --------------
    → Value (`suc V)

  -- primitives

  V-con : ∀ {Γ n}
      -----------------
    → Value (con {Γ} n)

  -- products

  V-⟨_,_⟩ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
    → Value V
    → Value W
      ----------------
    → Value `⟨ V , W ⟩

  -- begin

  -- sums

  V-inj₁ :  ∀ {Γ A B} {V : Γ ⊢ A}
    → Value V
    → Value (`inj₁ {B = B} V)

  V-inj₂ :  ∀ {Γ A B} {V : Γ ⊢ B}
    → Value V
    → Value (`inj₂ {A = A} V)

  -- unit

  V-tt : ∀ {Γ}
    → Value {Γ = Γ} `tt

  -- lists

  V-[] :  ∀ {Γ A}
    → Value {Γ = Γ} (`[] {A = A})

  V-∷ :  ∀ {Γ A} {V₁ : Γ ⊢ A} {V₂ : Γ ⊢ `List A}
    → Value V₁
    → Value V₂
    → Value (V₁ `∷ V₂)

  -- end

-- Reduction

infix 2 _—→_

data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where

  -- functions

  ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
    → L —→ L′
      ---------------
    → L · M —→ L′ · M

  ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
    → Value V
    → M —→ M′
      ---------------
    → V · M —→ V · M′

  β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {V : Γ ⊢ A}
    → Value V
      --------------------
    → (ƛ N) · V —→ N [ V ]

  -- naturals

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

  ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
    → L —→ L′
      -------------------------
    → case L M N —→ case L′ M N

  β-zero :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
      -------------------
    → case `zero M N —→ M

  β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
    → Value V
      ----------------------------
    → case (`suc V) M N —→ N [ V ]

  -- fixpoint

  β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
      ----------------
    → μ N —→ N [ μ N ]

  -- primitive numbers

  ξ-*₁ : ∀ {Γ} {L L′ M : Γ ⊢ Nat}
    → L —→ L′
      -----------------
    → L `* M —→ L′ `* M

  ξ-*₂ : ∀ {Γ} {V M M′ : Γ ⊢ Nat}
    → Value V
    → M —→ M′
      -----------------
    → V `* M —→ V `* M′

  δ-* : ∀ {Γ c d}
      ---------------------------------
    → con {Γ} c `* con d —→ con (c * d)

  -- let

  ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B}
    → M —→ M′
      ---------------------
    → `let M N —→ `let M′ N

  β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B}
    → Value V
      -------------------
    → `let V N —→ N [ V ]

  -- products

  ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B}
    → M —→ M′
      -------------------------
    → `⟨ M , N ⟩ —→ `⟨ M′ , N ⟩

  ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B}
    → Value V
    → N —→ N′
      -------------------------
    → `⟨ V , N ⟩ —→ `⟨ V , N′ ⟩

  ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
    → L —→ L′
      ---------------------
    → `proj₁ L —→ `proj₁ L′

  ξ-proj₂ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
    → L —→ L′
      ---------------------
    → `proj₂ L —→ `proj₂ L′

  β-proj₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
    → Value V
    → Value W
      ----------------------
    → `proj₁ `⟨ V , W ⟩ —→ V

  β-proj₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
    → Value V
    → Value W
      ----------------------
    → `proj₂ `⟨ V , W ⟩ —→ W

  -- alternative formulation of products

  ξ-case× : ∀ {Γ A B C} {L L′ : Γ ⊢ A `× B} {M : Γ , A , B ⊢ C}
    → L —→ L′
      -----------------------
    → case× L M —→ case× L′ M

  β-case× : ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {M : Γ , A , B ⊢ C}
    → Value V
    → Value W
      ----------------------------------
    → case× `⟨ V , W ⟩ M —→ M [ V ][ W ]

  -- begin

  -- sums

  ξ-inj₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A}
    → M —→ M′
      -----------------------------------
    → `inj₁ {B = B} M —→ `inj₁ {B = B} M′

  ξ-inj₂ : ∀ {Γ A B} {M M′ : Γ ⊢ B}
    → M —→ M′
      -----------------------------------
    → `inj₂ {A = A} M —→ `inj₂ {A = A} M′

  ξ-case⊎ : ∀ {Γ A B C} {M M′ : Γ ⊢ A `⊎ B} {M₁ : Γ , A ⊢ C} {M₂ : Γ , B ⊢ C}
    → M —→ M′
      ---------------------------------------------------------------
    → case⊎ M [inj₁⇒ M₁ |inj₂⇒ M₂ ] —→ case⊎ M′ [inj₁⇒ M₁ |inj₂⇒ M₂ ]

  β-case⊎-inj₁ : ∀ {Γ A B C} {M : Γ ⊢ A} {M₁ : Γ , A ⊢ C} {M₂ : Γ , B ⊢ C}
    → Value M
      -------------------------------------------------
    → case⊎ (`inj₁ M) [inj₁⇒ M₁ |inj₂⇒ M₂ ] —→ M₁ [ M ]

  β-case⊎-inj₂ : ∀ {Γ A B C} {M : Γ ⊢ B} {M₁ : Γ , A ⊢ C} {M₂ : Γ , B ⊢ C}
    → Value M
      -------------------------------------------------
    → case⊎ (`inj₂ M) [inj₁⇒ M₁ |inj₂⇒ M₂ ] —→ M₂ [ M ]

  -- unit

  ξ-case⊤ : ∀ {Γ A} {M M′ : Γ ⊢ `⊤} {M₁ : Γ ⊢ A}
    → M —→ M′
      ---------------------------------------
    → case⊤ M [tt⇒ M₁ ] —→ case⊤ M′ [tt⇒ M₁ ]

  β-case⊤ : ∀ {Γ A} {M₁ : Γ ⊢ A}
      -------------------------
    → case⊤ `tt [tt⇒ M₁ ] —→ M₁

  -- empty

  ξ-case⊥ : ∀ {Γ C} {M M′ : Γ ⊢ `⊥}
    → M —→ M′
      -----------------------------------
    → case⊥ {C = C} M —→ case⊥ {C = C} M′

  -- lists

  ξ-∷₁ : ∀ {Γ A} {M₁ M₁′ : Γ ⊢ A} {M₂ : Γ ⊢ `List A}
    → M₁ —→ M₁′
      -------------------------
    → (M₁ `∷ M₂) —→ (M₁′ `∷ M₂)

  ξ-∷₂ : ∀ {Γ A} {M₁ : Γ ⊢ A} {M₂ M₂′ : Γ ⊢ `List A}
    → Value M₁
    → M₂ —→ M₂′
      -------------------------
    → (M₁ `∷ M₂) —→ (M₁ `∷ M₂′)

  ξ-caseL : ∀ {Γ A B} {M M′ : Γ ⊢ `List A} {M₁ : Γ ⊢ B} {M₂ : Γ , A , `List A ⊢ B}
    → M —→ M′
      ---------------------------------------------------------
    → caseL M [[]⇒ M₁ |x∷y⇒ M₂ ] —→ caseL M′ [[]⇒ M₁ |x∷y⇒ M₂ ]

  β-caseL-[] : ∀ {Γ A B} {M₁ : Γ ⊢ B} {M₂ : Γ , A , `List A ⊢ B}
      ----------------------------------
    → caseL `[] [[]⇒ M₁ |x∷y⇒ M₂ ] —→ M₁

  β-caseL-∷ : ∀ {Γ A B} {N₁ : Γ ⊢ A} {N₂ : Γ ⊢ `List A} {M₁ : Γ ⊢ B} {M₂ : Γ , A , `List A ⊢ B}
    → Value N₁
    → Value N₂
      ------------------------------------------------------
    → caseL (N₁ `∷ N₂) [[]⇒ M₁ |x∷y⇒ M₂ ] —→ M₂ [ N₁ ][ N₂ ]
    -- → caseL (N₁ `∷ N₂) [[]⇒ M₁ |x∷y⇒ M₂ ] —→ (M₂ [ rename S_ N₂ ] [ N₁ ])

  -- end

-- Values do not reduce

V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A}
  → Value M
    ----------
  → ¬ (M —→ N)
V¬—→ (V-suc VM)   (ξ-suc M—→M′)     =  V¬—→ VM M—→M′
V¬—→ V-⟨ VM , _ ⟩ (ξ-⟨,⟩₁ M—→M′)    =  V¬—→ VM M—→M′
V¬—→ V-⟨ _ , VN ⟩ (ξ-⟨,⟩₂ _ N—→N′)  =  V¬—→ VN N—→N′
-- begin
V¬—→ (V-inj₁ VM)  (ξ-inj₁ M—→M′)    =  V¬—→ VM M—→M′
V¬—→ (V-inj₂ VM)  (ξ-inj₂ M—→M′)    =  V¬—→ VM M—→M′
V¬—→ (V-∷ VM _)   (ξ-∷₁ M—→M′)      =  V¬—→ VM M—→M′
V¬—→ (V-∷ _ VN)   (ξ-∷₂ _ N—→N′)    =  V¬—→ VN N—→N′
-- end

-- Progress

data Progress {A} (M : ∅ ⊢ A) : Set where

  step : ∀ {N : ∅ ⊢ A}
    → M —→ N
      ----------
    → Progress M

  done :
      Value M
      ----------
    → Progress M

progress : ∀ {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 (μ N)                              =  step β-μ
progress (con n)                            =  done V-con
progress (L `* M) with progress L
...    | step L—→L′                         =  step (ξ-*₁ L—→L′)
...    | done V-con with progress M
...        | step M—→M′                     =  step (ξ-*₂ V-con M—→M′)
...        | done V-con                     =  step δ-*
progress (`let M N) with progress M
...    | step M—→M′                         =  step (ξ-let M—→M′)
...    | done VM                            =  step (β-let VM)
progress `⟨ M , N ⟩ with progress M
...    | step M—→M′                         =  step (ξ-⟨,⟩₁ M—→M′)
...    | done VM with progress N
...        | step N—→N′                     =  step (ξ-⟨,⟩₂ VM N—→N′)
...        | done VN                        =  done (V-⟨ VM , VN ⟩)
progress (`proj₁ L) with progress L
...    | step L—→L′                         =  step (ξ-proj₁ L—→L′)
...    | done (V-⟨ VM , VN ⟩)               =  step (β-proj₁ VM VN)
progress (`proj₂ L) with progress L
...    | step L—→L′                         =  step (ξ-proj₂ L—→L′)
...    | done (V-⟨ VM , VN ⟩)               =  step (β-proj₂ VM VN)
progress (case× L M) with progress L
...    | step L—→L′                         =  step (ξ-case× L—→L′)
...    | done (V-⟨ VM , VN ⟩)               =  step (β-case× VM VN)
-- begin
progress (`inj₁ M) with progress M
...    | step M—→M′                         =  step (ξ-inj₁ M—→M′)
...    | done VM                            =  done (V-inj₁ VM)
progress (`inj₂ M) with progress M
...    | step M—→M′                         =  step (ξ-inj₂ M—→M′)
...    | done VM                            =  done (V-inj₂ VM)
progress case⊎ M [inj₁⇒ M₁ |inj₂⇒ M₂ ] with progress M
...    | step M—→M′                         =  step (ξ-case⊎ M—→M′)
...    | done (V-inj₁ VM)                   =  step (β-case⊎-inj₁ VM)
...    | done (V-inj₂ VM)                   =  step (β-case⊎-inj₂ VM)
progress `tt                                = done V-tt
progress case⊤ M [tt⇒ M₁ ] with progress M
...    | step M—→M′                         =  step (ξ-case⊤ M—→M′)
...    | done V-tt                          =  step β-case⊤
progress (case⊥ M) with progress M
...    | step M—→M′                         =  step (ξ-case⊥ M—→M′)
progress `[]                                =  done V-[]
progress (M₁ `∷ M₂) with progress M₁ | progress M₂
...    | step M₁—→M₁′ | _                   =  step (ξ-∷₁ M₁—→M₁′)
...    | done VM₁     | step M₂—→M₂′        =  step (ξ-∷₂ VM₁ M₂—→M₂′)
...    | done VM₁     | done VM₂            =  done (V-∷ VM₁ VM₂)
progress caseL M [[]⇒ M₁ |x∷y⇒ M₂ ] with progress M
...    | step M—→M′                         =  step (ξ-caseL M—→M′)
...    | done V-[]                          =  step β-caseL-[]
...    | done (V-∷ VM₁ VM₂)                 =  step (β-caseL-∷ VM₁ VM₂)
-- end

-- #### Exercise `double-subst` (stretch)

-- Show that a double substitution is equivalent to two single
-- substitutions.
-- ```agda
-- postulate
--   double-subst :
--     ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {N : Γ , A , B ⊢ C} →
--       N [ V ][ W ] ≡ (N [ rename S_ W ]) [ V ]
-- ```
-- Note the arguments need to be swapped and `W` needs to have
-- its context adjusted via renaming in order for the right-hand
-- side to be well typed.

_⇒ₛ_ : Context → Context → Set
Γ₁ ⇒ₛ Γ₂ = ∀ {A} → Γ₁ ∋ A → Γ₂ ⊢ A

exts' : ∀ {Γ₁ Γ₂ A} → (Γ₁ ⇒ₛ Γ₂) → ((Γ₁ , A) ⇒ₛ (Γ₂ , A))
exts' σ Z      =  ` Z
exts' σ (S x)  =  rename S_ (σ x)

_,,_ : Context → Context → Context
Γ₁ ,, ∅        = Γ₁
Γ₁ ,, (Γ₂ , t) = (Γ₁ ,, Γ₂) , t

exts* : ∀ {Γ₁ Γ₂} Γ → (Γ₁ ⇒ₛ Γ₂) → ((Γ₁ ,, Γ) ⇒ₛ (Γ₂ ,, Γ))
exts* ∅       σ = σ
exts* (Γ , t) σ = exts (exts* Γ σ)

double-subst' :
  ∀ {Γ A B C} Γ' (V : Γ ⊢ A) (W : Γ ⊢ B) (N : (Γ , A , B) ,, Γ' ⊢ C) →
    subst (exts* Γ' (substZeroOne V W)) N ≡
    subst (exts* Γ' (substZero V)) (subst (exts* Γ' (substZero (rename S_ W))) N)
double-subst' Γ' V W (` x) = {!!}
double-subst' Γ' V W (ƛ N) = cong ƛ_ (double-subst' (Γ' , _) V W N)
double-subst' Γ' V W (N₁ · N₂) = cong₂ _·_ (double-subst' Γ' V W N₁) (double-subst' Γ' V W N₂)
double-subst' Γ' V W `zero = {!!}
double-subst' Γ' V W (`suc N) = {!!}
double-subst' Γ' V W (case N N₁ N₂) = {!!}
double-subst' Γ' V W (μ N) = {!!}
double-subst' Γ' V W (con x) = {!!}
double-subst' Γ' V W (N `* N₁) = {!!}
double-subst' Γ' V W (`let N N₁) = {!!}
double-subst' Γ' V W `⟨ N , N₁ ⟩ = {!!}
double-subst' Γ' V W (`proj₁ N) = {!!}
double-subst' Γ' V W (`proj₂ N) = {!!}
double-subst' Γ' V W (case× N N₁) = {!!}
double-subst' Γ' V W (`inj₁ N) = {!!}
double-subst' Γ' V W (`inj₂ N) = {!!}
double-subst' Γ' V W case⊎ N [inj₁⇒ N₁ |inj₂⇒ N₂ ] = {!!}
double-subst' Γ' V W `tt = {!!}
double-subst' Γ' V W case⊤ N [tt⇒ N₁ ] = {!!}
double-subst' Γ' V W (case⊥ N) = {!!}
double-subst' Γ' V W `[] = {!!}
double-subst' Γ' V W (N `∷ N₁) = {!!}
double-subst' Γ' V W caseL N [[]⇒ N₁ |x∷y⇒ N₂ ] = {!!}

double-subst :
  ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {N : Γ , A , B ⊢ C} →
    N [ V ][ W ] ≡ (N [ rename S_ W ]) [ V ]
double-subst {Γ} {A} {B} {C} {V} {W} {N} =
  begin
    (N [ V ][ W ])
  ≡⟨⟩
    subst (substZeroOne V W) N
  ≡⟨ double-subst' ∅ V W N ⟩
    subst (substZero V) (subst (substZero (rename S_ W)) N)
  ≡⟨⟩
    ((N [ rename S_ W ]) [ V ])
  ∎