https://github.com/UlfNorell/agda-summer-school/ substitute function

STLC.agda

module STLC where

open import Prelude
open import Data.List

infixr 7 _=>_
data Type : Set where
  nat : Type
  _=>_ : (a b : Type) → Type

Name = String

Cxt = List (Name × Type)

data Term (Γ : Cxt) : Type → Set where
    var : ∀ {a} (x : Name) (i : (x , a) ∈ Γ) → Term Γ a
    lit : Nat → Term Γ nat
    suc : Term Γ (nat => nat)
    app : ∀ {a b} → Term Γ (a => b) → Term Γ a → Term Γ b
    lam : ∀ {b} (x : Name) (a : Type) → Term ((x , a) ∷ Γ) b → Term Γ (a => b)

El : Type → Set
El nat      = Nat
El (a => b) = El a → El b

Env : Cxt → Set
Env Γ = All (El ∘ snd) Γ

eval : ∀ {Γ a} → Term Γ a → Env Γ → El a
eval (var x i) e = lookup∈ e i
eval (lit x) e = x
eval suc e = suc
eval (app t t₁) e = eval t e (eval t₁ e)
eval (lam x a t) e y = eval t (y ∷ e)

weakenLookup : ∀ {a : Set} (Γ₁ : List a) {Γ x y} → x ∈ (Γ₁ ++ Γ) → x ∈ (Γ₁ ++ y ∷ Γ)
weakenLookup [] (zero refl) = suc (zero refl)
weakenLookup [] (suc i) = suc (suc i)
weakenLookup (x ∷ Γ₁) (zero p) = zero p
weakenLookup (x ∷ Γ₁) (suc i) = suc (weakenLookup Γ₁ i)

--   Γ₁ , Γ ⊢ t : A    Γ ⊢ x : B
-- -------------------------------
--   Γ₁, x : B, Γ ⊢ t : A
weaken : ∀ Γ₁ {Γ x a} → Term (Γ₁ ++ Γ) a → Term (Γ₁ ++ x ∷ Γ) a
weaken Γ₁ (var x i) = var x (weakenLookup Γ₁ i)
weaken Γ₁ (lit x) = lit x
weaken Γ₁ suc = suc
weaken Γ₁ (app t t₁) = app (weaken Γ₁ t) (weaken Γ₁ t₁)
weaken Γ₁ (lam x a t) = lam x a (weaken ((x , a) ∷ Γ₁) t)

substVar : ∀ Γ₁ {Γ x a b} → Term Γ a → (y : Name) → (y , b) ∈ (Γ₁ ++ (x , a) ∷ Γ) → Term (Γ₁ ++ Γ) b
substVar [] t x (zero refl) = t
substVar [] t y (suc i) = var y i
substVar (._ ∷ Γ₁) t y (zero p) = var y (zero p)
substVar (x ∷ Γ₁) t y (suc i) = weaken [] (substVar Γ₁ t y i)

--   Γ ⊢ t : A     Γ₁, x : A, Γ ⊢ s : B
-- --------------------------------------
--   Γ₁, Γ ⊢ [x / t] s : B
substitute : ∀ Γ₁ {Γ x a b} → Term Γ a → Term (Γ₁ ++ (x , a) ∷ Γ) b → Term (Γ₁ ++ Γ) b
substitute Γ₁ t (var y i) = substVar Γ₁ t y i
substitute Γ₁ t (lit n) = lit n
substitute Γ₁ t suc = suc
substitute Γ₁ t (app s s₁) = app (substitute Γ₁ t s) (substitute Γ₁ t s₁)
substitute Γ₁ t (lam x a s) = lam x a (substitute ((x , a) ∷ Γ₁) t s) 

two-body : Term (("x", nat) ∷ []) nat
two-body = app suc (var "x" (zero refl))

two-arg : Term [] nat
two-arg = lit 1

two : Term [] nat
two = app (lam "x" nat two-body) two-arg

example1 : eval two [] ≡ 2
example1 = refl

example2 : eval (substitute [] two-arg two-body) [] ≡ 2
example2 = refl

infixr 5 _+++_
_+++_ : ∀ {a b} {A : Set a} {P : A → Set b} {xs ys : List A} → All P xs → All P ys → All P (xs ++ ys)
[] +++ ys = ys
(x ∷ xs) +++ ys = x ∷ xs +++ ys

postulate
  eval-weaken : ∀ Γ₁ {Γ a x} → (t : Term (Γ₁ ++ Γ) a) →
                              (env₁ : Env Γ₁) →
                              (env₂ : Env Γ) →
                              (e : El (snd x)) → 
                              eval (weaken Γ₁ {x = x} t) (env₁ +++ e ∷ env₂) ≡ eval t (env₁ +++ env₂)