* Unit 9 --- Substitution and α-Equivalence
:PROPERTIES:
:CUSTOM_ID: unit-9-substitution-and-α-equivalence
:END:
*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]]

** Goals
:PROPERTIES:
:CUSTOM_ID: goals
:END:
- Implement =subst= (substitution) for de Bruijn terms
- Implement =lift= (index shifting) --- the key operation that avoids capture
- Prove fundamental substitution lemmas

** Sources
:PROPERTIES:
:CUSTOM_ID: sources
:END:
- syndikos/lean4-stlc =Syntax.lean= and =Reduction.lean=
- chenson2018/LeanScratch: https://github.com/chenson2018/LeanScratch
- PLFA Part 2: https://plfa.github.io/

** Exercises
:PROPERTIES:
:CUSTOM_ID: exercises
:END:
#+begin_src lean
open DBTerm  -- from Unit 8

-- 9.1 — Lift: shift all *free* variables above a cutoff by k
-- Lift is the engine that makes substitution work under binders.
-- When we go under a λ, existing de Bruijn indices need to shift by 1
-- because a new binder appears.
def lift (t : DBTerm) (cutoff k : Nat) : DBTerm :=
  match t with
  | var n => if n < cutoff then var n else var (n + k)
  | lam body => lam (lift body (cutoff + 1) k)
  | app f a => app (lift f cutoff k) (lift a cutoff k)

-- Verify: lifting the identity function
-- lift (λ. 0) 0 1  should produce  λ. 0  (bound variables inside λ are untouched)
#eval lift idDB 0 1

-- 9.2 — Substitution: replace variable `idx` with `s` in term `t`
-- This is capture-avoiding substitution via de Bruijn arithmetic.
-- Under a λ, the target index shifts by 1 and the replacement gets lifted.
def subst (t : DBTerm) (idx : Nat) (s : DBTerm) : DBTerm :=
  match t with
  | var n =>
      if n < idx then var n
      else if n == idx then s              -- found the variable to replace
      else var (n - 1)                     -- shift remaining vars down
  | lam body => lam (subst body (idx + 1) (lift s 0 1))
  | app f a => app (subst f idx s) (subst a idx s)

-- Test: substitute λ. 0 for variable 0 in (λ. 0) -- should be identity
-- Actually: [0 ↦ λ.0] (λ. 0)  — nothing changes (0 is bound)
#eval subst (lam (var 0)) 0 (lam (var 0))

-- 9.3 — Single-step β-reduction (preview of next unit)
-- β: (λ. t) s  →  subst t 0 s
def betaRedex : DBTerm := app (lam (var 0)) (lam (var 0))  -- (λx. x) (λy. y) → ...y...

-- Compute the result of one β step on this term
#eval subst (var 0) 0 (lam (var 0))  -- should be lam (var 0) (= λy. y)

-- 9.4 — Lemma: Substitution under a lambda
-- If we substitute for index 0 in a term that's already shifted,
-- the lift in the body handles the shift correctly.
-- Prove this property:
lemma subst_lift_commute (t s : DBTerm) (n : Nat) :
    subst (lift t 0 1) (n+1) (lift s 0 1) = lift (subst t n s) 0 1 :=
  by
    sorry

-- This lemma is *critical* for proving preservation/type safety later.
-- It says that shifting before and after substitution agree.
#+end_src

*** Why this matters
:PROPERTIES:
:CUSTOM_ID: why-this-matters
:END:
Substitution is the core operation of operational semantics. Doing it right
(no variable capture) is the hardest part of formalizing lambda calculi.
de Bruijn indices make capture impossible --- the arithmetic is mechanical.
The lemmas here are boilerplate you prove once, then reuse everywhere.

--------------

← [[file:08-syntax-representation.org][Previous: Unit 8]] · Next: [[file:10-small-step-semantics.org][Unit 10 --- Small-Step Semantics]]