Normalization proof for SK combinator calculus using Agda

sknorm.agda

{-# OPTIONS --rewriting #-}
module sknorm where

open import Agda.Primitive
open import Level
open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.Equality.Rewrite
open import Data.Product
open import Data.Empty

module I where
  infixr 5 _⇒_
  infixl 5 _$_

  postulate
    Ty : Set
    Tm : Ty → Set

  variable
    A B C : Ty

  variable
    t u v : Tm A

  postulate
    ι   : Ty
    _⇒_ : Ty → Ty → Ty
    _$_ : Tm (A ⇒ B) → Tm A → Tm B
    K   : Tm (A ⇒ B ⇒ A)
    S   : Tm ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)

    Kβ  : K $ t $ u ≡ t
    Sβ  : S $ t $ u $ v ≡ (t $ v) $ (u $ v)

  {-# REWRITE Kβ Sβ #-}

  data Nf : (A : Ty) → Tm A → Set where
    K₀ : Nf (A ⇒ B ⇒ A) K
    K₁ : Nf A t → Nf (B ⇒ A) (K $ t)
    S₀ : Nf ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C) S
    S₁ : Nf (A ⇒ B ⇒ C) t → Nf ((A ⇒ B) ⇒ A ⇒ C) (S $ t)
    S₂ : Nf (A ⇒ B ⇒ C) t → Nf (A ⇒ B) u → Nf (A ⇒ C) (S $ t $ u)

record Model {i} : Set (lsuc i) where
  open I using (A ; B ; C ; t ; u ; v)

  infixr 5 _⇒_
  infixl 5 _$_

  field
    Ty  : Set i
    Tm  : Ty → Set i

    ι   : Ty
    _⇒_ : Ty → Ty → Ty
    _$_ : {A B : Ty} → Tm (A ⇒ B) → Tm A → Tm B
    K   : {A B : Ty} → Tm (A ⇒ B ⇒ A)
    S   : {A B C : Ty} → Tm ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)

    Kβ  : {A B : Ty} → {t : Tm A} → {u : Tm B} →
          K $ t $ u ≡ t
    Sβ  : {A B C : Ty} → {t : Tm (A ⇒ B ⇒ C)} → {u : Tm (A ⇒ B)} → {v : Tm A} →
          S $ t $ u $ v ≡ (t $ v) $ (u $ v)

  postulate
    ⟦_⟧T : I.Ty → Ty
    ⟦ι⟧T : ⟦ I.ι ⟧T ≡ ι
    ⟦⇒⟧T : ⟦ A I.⇒ B ⟧T ≡ ⟦ A ⟧T ⇒ ⟦ B ⟧T
    {-# REWRITE ⟦ι⟧T ⟦⇒⟧T #-}

    ⟦_⟧t : I.Tm A → Tm ⟦ A ⟧T
    ⟦$⟧t : ⟦ t I.$ u ⟧t ≡ ⟦ t ⟧t $ ⟦ u ⟧t
    ⟦K⟧t : ⟦ I.K {A} {B} ⟧t ≡ K {⟦ A ⟧T} {⟦ B ⟧T}
    ⟦S⟧t : ⟦ I.S {A} {B} {C} ⟧t ≡ S {⟦ A ⟧T} {⟦ B ⟧T}{⟦ C ⟧T}
    {-# REWRITE ⟦$⟧t ⟦K⟧t ⟦S⟧t #-}

open I using () renaming (A to A' ; B to B' ; C to C' ; t to t' ; u to u' ; v to v')

record DepModel {i} : Set (lsuc i) where

  infixr 5 _⇒_
  infixl 5 _$_

  field
    Ty  : I.Ty → Set i
    Tm  : Ty A' → I.Tm A' → Set i

    ι   : Ty I.ι
    _⇒_ : Ty A' → Ty B' → Ty (A' I.⇒ B')

    _$_ : {A : Ty A'} → {B : Ty B'} →
          Tm (A ⇒ B) t' → Tm A u' → Tm B (t' I.$ u')

    K   : {A : Ty A'} → {B : Ty B'} → Tm (A ⇒ B ⇒ A) I.K
    S   : {A : Ty A'} → {B : Ty B'} → {C : Ty C'} →
          Tm ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C) I.S

    Kβ  : {A : Ty A'} → {B : Ty B'} → {t : Tm A t'} → {u : Tm B u'} → K $ t $ u ≡ t
    Sβ  : {A : Ty A'} → {B : Ty B'} → {C : Ty C'} →
          {t : Tm (A ⇒ B ⇒ C) t'} → {u : Tm (A ⇒ B) u'} → {v : Tm A v'} →
          S $ t $ u $ v ≡ (t $ v) $ (u $ v)

  postulate
    ⟦_⟧T : (A' : I.Ty) → Ty A'
    ⟦ι⟧T : ⟦ I.ι ⟧T ≡ ι
    ⟦⇒⟧T : ⟦ A' I.⇒ B' ⟧T ≡ ⟦ A' ⟧T ⇒ ⟦ B' ⟧T
    {-# REWRITE ⟦ι⟧T ⟦⇒⟧T #-}

    ⟦_⟧t : (t' : I.Tm A') → Tm ⟦ A' ⟧T t'
    ⟦$⟧t : ⟦ t' I.$ u' ⟧t ≡ ⟦ t' ⟧t $ ⟦ u' ⟧t
    ⟦K⟧t : ⟦ I.K {A'} {B'} ⟧t ≡ K {A'} {B'} {⟦ A' ⟧T} {⟦ B' ⟧T}
    ⟦S⟧t : ⟦ I.S {A'} {B'} {C'} ⟧t ≡ S {A'} {B'} {C'} {⟦ A' ⟧T} {⟦ B' ⟧T}{⟦ C' ⟧T}
    {-# REWRITE ⟦$⟧t ⟦K⟧t ⟦S⟧t #-}

Norm : DepModel
Norm = record
  { Ty  = λ A' → Σ (I.Tm A' → Set) (λ P → ({t' : I.Tm A'} → P t' → I.Nf A' t'))
  ; Tm  = λ where (PA , QA) t' → Lift _ (PA t')
  ; ι   = (λ _ → ⊥) , λ where ()
  ; _⇒_ = λ where {A'} (PA , QA) (PB , QB) → (λ f' → ({t' : I.Tm A'} → PA t' → PB (f' I.$ t')) × I.Nf _ f') , proj₂
  ; _$_ = λ A t → lift (proj₁ (lower A) (lower t))
  ; K   = λ where {A = (PA , QA)} → lift ((λ a → (λ b → a) , (I.K₁ (QA a))) , I.K₀)
  ; S   = lift ((λ where (p , q) → (λ where (p' , q') → (λ a → proj₁ (p a) (p' a)) , I.S₂ q q') , I.S₁ q) , I.S₀)
  ; Kβ  = refl
  ; Sβ  = refl
  }

norm : (t : I.Tm I.A) → I.Nf I.A t
norm {A} t = proj₂ ⟦ A ⟧T (lower ⟦ t ⟧t)
  where open DepModel Norm