{-# OPTIONS --safe #-}

module Problem11 where

data Term : Set where
  Ref : Term
  Sop : Term
  Kop : Term
  App : Term → Term → Term

variable M N P M₁ M₂ M₃ N₁ N₂ : Term

data _↦_ : Term → Term → Set where
  red-S : (App (App (App Sop M) N) P) ↦ (App (App M P) (App N P))
  red-K : (App (App Kop M) N) ↦ M
  red-left : M₁ ↦ M₂ → App M₁ N ↦ App M₂ N
  red-right : N₁ ↦ N₂ → App M N₁ ↦ App M N₂
  red-trans : M ↦ N → N ↦ P → M ↦ P

open import Relation.Binary.Reasoning.Base.Partial _↦_ red-trans

ident : Term
ident = App (App Sop Kop) Kop

ident-red : App ident M ↦ M
ident-red {M} = begin
  App (App (App Sop Kop) Kop) M ∼⟨ red-S ⟩
  App (App Kop M) (App Kop M)   ∼⟨ red-K ⟩
  M                             ∎

const-sop : Term
const-sop = App Kop Sop

const-sop-red : App const-sop M ↦ Sop
const-sop-red = red-K

const-kop : Term
const-kop = App Kop Kop

const-kop-red : App const-kop M ↦ Kop
const-kop-red = red-K

app-app : Term → Term → Term
app-app M N = App (App Sop M) N

app-app-red : App (app-app M₁ M₂) M₃ ↦ App (App M₁ M₃) (App M₂ M₃)
app-app-red = red-S

lambda : Term → Term
lambda Ref = ident
lambda Sop = App Kop Sop
lambda Kop = App Kop Kop
lambda (App M N) = app-app (lambda M) (lambda N)

substitution : Term → Term → Term
substitution Ref N = N
substitution Sop N = Sop
substitution Kop N = Kop
substitution (App M₁ M₂) N = App (substitution M₁ N) (substitution M₂ N)

beta : ∀ M N → (App (lambda M) N) ↦ (substitution M N)
beta Ref N = ident-red
beta Sop N = const-sop-red
beta Kop N = const-kop-red
beta (App M₁ M₂) N = begin
  App (app-app (lambda M₁) (lambda M₂)) N     ∼⟨ app-app-red ⟩
  App (App (lambda M₁) N) (App (lambda M₂) N) ∼⟨ red-left (beta M₁ N) ⟩
  App (substitution M₁ N) (App (lambda M₂) N) ∼⟨ red-right (beta M₂ N) ⟩
  App (substitution M₁ N) (substitution M₂ N) ∎