realize.agda

module realize where
open import Relation.Nullary
import Data.Unit as U
import Data.Empty as E
open import Data.Product
open import Data.Sum
open import Data.Nat

data Lam : Set where
  var : ℕ → Lam
  lam : Lam → Lam
  app : Lam → Lam → Lam

weaken : Lam → Lam
weaken t = go 0 t
  where go : ℕ → Lam → Lam
        go n (var x) with x ≤? n
        ... | yes p = var x
        ... | no ¬p = var (suc x)
        go n (lam t) = lam (go (suc n) t)
        go n (app t₁ t₂) = app (go n t₁) (go n t₂)

subst : Lam → ℕ → Lam → Lam
subst t₁ n (var x) with n ≟ x
... | yes p = t₁
... | no ¬p = var x
subst t₁ n (lam t₂) = lam (subst (weaken t₁) (suc n) t₂)
subst t₁ n (app t₂ t₃) = app (subst t₁ n t₂) (subst t₁ n t₃)

data Norm : Lam → Lam → Set where
  lam : ∀ {t} → Norm (lam t) (lam t)
  app : ∀ {t₁ t₂ t₃ t₄}
      → Norm t₁ (lam t₃)
      → Norm (subst t₂ 0 t₃) t₄
      → Norm (app t₁ t₂) t₄

test : Norm (app (lam (var 0)) (lam (var 0))) (lam (var zero))
test = app lam lam


data P : Set where
  _⇒_ : P → P → P
  _∧_ : P → P → P
  _∨_ : P → P → P
  ⊥   : P
  ⊤   : P

π₁ : Lam → Lam
π₁ t = app t (lam (lam (var 1)))

π₂ : Lam → Lam
π₂ t = app t (lam (lam (var 0)))

_⊨_ : Lam → P → Set
l ⊨ (p ⇒ p₁) = (a : Lam) → a ⊨ p → app l a ⊨ p₁
l ⊨ (p ∧ p₁) = (π₁ l ⊨ p) × (π₂ l ⊨ p₁)
l ⊨ (p ∨ p₁) =
  (Norm (π₁ l) (lam (lam (var 1))) × π₂ l ⊨ p) ⊎
  (Norm (π₁ l) (lam (lam (var 0))) × π₂ l ⊨ p₁)
l ⊨ ⊥ = U.⊤
l ⊨ ⊤ = E.⊥


test₂ : lam (lam (lam (var zero))) ⊨ ((⊤ ∧ ⊤) ∨ ⊥)
test₂ = inj₂ (app lam lam , U.tt)