CoDebruijn scoped syntax of untyped lambda calculus

CoDebruijn.agda

module CoDebruijn where

open import Data.Product using (_×_; _,_; ∃-syntax)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

data Context : Set where
  O : Context
  1+_ : Context → Context

data Singleton : Context → Set where
  one : Singleton (1+ O)

-- Relevant cover
data Cover : Context → Context → Context → Set where
  O : Cover O O O
  1+_ : {Γ Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → Cover (1+ Γ) (1+ Γ₁) (1+ Γ₂)
  1+ˡ_ : {Γ Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → Cover (1+ Γ) (1+ Γ₁) Γ₂
  1+ʳ_ : {Γ Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → Cover (1+ Γ) Γ₁ (1+ Γ₂)

-- Context update for a single binder
data Extend₁ (Γ : Context) : Context → Set where
  extend : Extend₁ Γ (1+ Γ)  -- the bound variable is used
  refl : Extend₁ Γ Γ         -- the bound variable is not used

data RTerm (Γ : Context) : Set where
  Var : Singleton Γ → RTerm Γ
  App : {Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → RTerm Γ₁ → RTerm Γ₂ → RTerm Γ
  Lam : {Γ₁ : Context} → Extend₁ Γ Γ₁ → RTerm Γ₁ → RTerm Γ

data Thinning : Context → Context → Set where
  O : Thinning O O
  1+_ : {Γ Γ₁ : Context} → Thinning Γ Γ₁ → Thinning (1+ Γ) (1+ Γ₁)
  1/_ : {Γ Γ₁ : Context} → Thinning Γ Γ₁ → Thinning (1+ Γ) Γ₁

data Term (Γ : Context) : Set where
  Weaken : {Γ₁ : Context} → Thinning Γ Γ₁ → RTerm Γ₁ → Term Γ

data RSubst : Context → Context → Set where
  [] : RSubst O O
  ⦅_⦆_∷_ : {Γ Γ₀ Γ₁ Γ₂ : Context} → Cover Γ₀ Γ₁ Γ₂ → RTerm Γ₁ → RSubst Γ Γ₂ → RSubst (1+ Γ) Γ₀

data Subst (Γ₁ Γ₂ : Context) : Set where
  Weaken : {Γ₃ : Context} → Thinning Γ₂ Γ₃ → RSubst Γ₁ Γ₃ → Subst Γ₁ Γ₂

Thinnings→Cover : {Γ Γ₁ Γ₂ : Context} → Thinning Γ Γ₁ → Thinning Γ Γ₂ → ∃[ Δ ] Thinning Γ Δ × Cover Δ Γ₁ Γ₂
Thinnings→Cover O O = O , O , O
Thinnings→Cover (1+ θ₁) (1+ θ₂) = let Δ , θ , c = Thinnings→Cover θ₁ θ₂ in 1+ Δ , 1+ θ , 1+ c
Thinnings→Cover (1+ θ₁) (1/ θ₂) = let Δ , θ , c = Thinnings→Cover θ₁ θ₂ in 1+ Δ , 1+ θ , 1+ˡ c
Thinnings→Cover (1/ θ₁) (1+ θ₂) = let Δ , θ , c = Thinnings→Cover θ₁ θ₂ in 1+ Δ , 1+ θ , 1+ʳ c
Thinnings→Cover (1/ θ₁) (1/ θ₂) = let Δ , θ , c = Thinnings→Cover θ₁ θ₂ in Δ , 1/ θ , c

_∷ˢ_ : {Γ₁ Γ₂ : Context} → Term Γ₂ → Subst Γ₁ Γ₂ → Subst (1+ Γ₁) Γ₂
Weaken θ t ∷ˢ Weaken θ₁ s = let Δ , θ′ , c′ = Thinnings→Cover θ θ₁ in Weaken θ′ (⦅ c′ ⦆ t ∷ s)

Thinning-trans : {Γ₁ Γ₂ Γ₃ : Context} → Thinning Γ₁ Γ₂ → Thinning Γ₂ Γ₃ → Thinning Γ₁ Γ₃
Thinning-trans O O = O
Thinning-trans (1+ θ₁) (1+ θ₂) = 1+ Thinning-trans θ₁ θ₂
Thinning-trans (1+ θ₁) (1/ θ₂) = 1/ Thinning-trans θ₁ θ₂
Thinning-trans (1/ θ₁) θ₂ = 1/ Thinning-trans θ₁ θ₂

Cover→Thinning : {Γ Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → Thinning Γ Γ₁ × Thinning Γ Γ₂
Cover→Thinning O = O , O
Cover→Thinning (1+ c) = let θ₁ , θ₂ = Cover→Thinning c in 1+ θ₁ , 1+ θ₂
Cover→Thinning (1+ˡ c) = let θ₁ , θ₂ = Cover→Thinning c in 1+ θ₁ , 1/ θ₂
Cover→Thinning (1+ʳ c) = let θ₁ , θ₂ = Cover→Thinning c in 1/ θ₁ , 1+ θ₂

inv-∷ˢ : {Γ₁ Γ₂ : Context} → Subst (1+ Γ₁) Γ₂ → Term Γ₂ × Subst Γ₁ Γ₂
inv-∷ˢ (Weaken θ (⦅ c ⦆ t ∷ s)) = let θ₁ , θ₂ = Cover→Thinning c in Weaken (Thinning-trans θ θ₁) t , Weaken (Thinning-trans θ θ₂) s

≥O : {Γ : Context} → Thinning Γ O
≥O {O} = O
≥O {1+ Γ} = 1/ ≥O

weaken-subst : {Γ₁ Γ₂ Γ₃ : Context} → Subst Γ₁ Γ₂ → Thinning Γ₁ Γ₃ → Subst Γ₃ Γ₂
weaken-subst s O = Weaken ≥O []
weaken-subst s (1+ θ) = let t₂ , s₂ = inv-∷ˢ s in t₂ ∷ˢ weaken-subst s₂ θ
weaken-subst s (1/ θ) = let _ , s₂ = inv-∷ˢ s in weaken-subst s₂ θ

Cover-Oʳ : {Γ Γ₁ : Context} → Cover Γ Γ₁ O → Γ ≡ Γ₁
Cover-Oʳ O = refl
Cover-Oʳ (1+ˡ c) with Cover-Oʳ c
... | refl = refl

inv-one : {Γ : Context} → RSubst (1+ O) Γ → RTerm Γ
inv-one (⦅ c ⦆ t ∷ []) with Cover-Oʳ c
... | refl = t

min-Cover : {Γ₁ Γ₂ Γ₃ Δ₁ Δ₂ : Context} → Cover Γ₁ Γ₂ Γ₃ → Cover Γ₃ Δ₁ Δ₂ → ∃[ E₁ ] ∃[ E₂ ] Cover E₁ Γ₂ Δ₁ × Cover E₂ Γ₂ Δ₂ × Cover Γ₁ E₁ E₂
min-Cover O O = O , O , O , O , O
min-Cover (1+ c) (1+ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ c₁ , 1+ c₂ , 1+ c′
min-Cover (1+ c) (1+ˡ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ c₁ , 1+ˡ c₂ , 1+ c′
min-Cover (1+ c) (1+ʳ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ˡ c₁ , 1+ c₂ , 1+ c′
min-Cover (1+ˡ c) θ = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ˡ c₁ , 1+ˡ c₂ , 1+ c′
min-Cover (1+ʳ c) (1+ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ʳ c₁ , 1+ʳ c₂ , 1+ c′
min-Cover (1+ʳ c) (1+ˡ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , E₂ , 1+ʳ c₁ , c₂ , 1+ˡ c′
min-Cover (1+ʳ c) (1+ʳ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in E₁ , 1+ E₂ , c₁ , 1+ʳ c₂ , 1+ʳ c′

min-Coverˡ : {Γ₁ Γ₂ Γ₃ Δ₁ Δ₂ : Context} → Cover Γ₁ Γ₂ Γ₃ → Cover Γ₃ Δ₁ Δ₂ → ∃[ E₁ ] Cover E₁ Γ₂ Δ₁ × Cover Γ₁ E₁ Δ₂
min-Coverˡ O O = O , O , O
min-Coverˡ (1+ c) (1+ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ c₂ , 1+ c′
min-Coverˡ (1+ c) (1+ˡ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ c₂ , 1+ˡ c′
min-Coverˡ (1+ c) (1+ʳ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ˡ c₂ , 1+ c′
min-Coverˡ (1+ˡ c) θ = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ˡ c₂ , 1+ˡ c′
min-Coverˡ (1+ʳ c) (1+ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ʳ c₂ , 1+ c′
min-Coverˡ (1+ʳ c) (1+ˡ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ʳ c₂ , 1+ˡ c′
min-Coverˡ (1+ʳ c) (1+ʳ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in E₂ , c₂ , 1+ʳ c′

min-Coverʳ : {Γ₁ Γ₂ Γ₃ Δ₁ Δ₂ : Context} → Cover Γ₁ Γ₂ Γ₃ → Cover Γ₃ Δ₁ Δ₂ → ∃[ E₂ ] Cover E₂ Γ₂ Δ₂ × Cover Γ₁ Δ₁ E₂
min-Coverʳ O O = O , O , O
min-Coverʳ (1+ c) (1+ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ c₂ , 1+ c′
min-Coverʳ (1+ c) (1+ˡ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ˡ c₂ , 1+ c′
min-Coverʳ (1+ c) (1+ʳ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ c₂ , 1+ʳ c′
min-Coverʳ (1+ˡ c) θ = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ˡ c₂ , 1+ʳ c′
min-Coverʳ (1+ʳ c) (1+ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ʳ c₂ , 1+ c′
min-Coverʳ (1+ʳ c) (1+ˡ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in E₂ , c₂ , 1+ˡ c′
min-Coverʳ (1+ʳ c) (1+ʳ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ʳ c₂ , 1+ʳ c′

split-subst : {Γ₀ Δ₀ Γ₁ Γ₂ : Context} → RSubst Γ₀ Δ₀ → Cover Γ₀ Γ₁ Γ₂ → ∃[ Δ₁ ] ∃[ Δ₂ ] RSubst Γ₁ Δ₁ × RSubst Γ₂ Δ₂ × Cover Δ₀ Δ₁ Δ₂
split-subst [] O = _ , _ , [] , [] , O
split-subst (⦅ c ⦆ t ∷ s) (1+ θ) =
  let Δ₁ , Δ₂ , s₁ , s₂ , θ′ = split-subst s θ in
  let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ′ in
  _ , _ , ⦅ c₁ ⦆ t ∷ s₁ , ⦅ c₂ ⦆ t ∷ s₂ , c′
split-subst (⦅ c ⦆ t ∷ s) (1+ˡ θ) =
  let Δ₁ , Δ₂ , s₁ , s₂ , θ′ = split-subst s θ in
  let E₁ , c₁ , c′ = min-Coverˡ c θ′ in
  _ , _ , ⦅ c₁ ⦆ t ∷ s₁ , s₂ , c′
split-subst (⦅ c ⦆ t ∷ s) (1+ʳ θ) =
  let Δ₁ , Δ₂ , s₁ , s₂ , θ′ = split-subst s θ in
  let E₂ , c₂ , c′ = min-Coverʳ c θ′ in
  _ , _ , s₁ , ⦅ c₂ ⦆ t ∷ s₂ , c′

coverʳ : {Γ : Context} → Cover Γ O Γ
coverʳ {O} = O
coverʳ {1+ Γ} = 1+ʳ coverʳ {Γ}

1+-rsubst : {Γ Δ : Context} → RSubst Γ Δ → RSubst (1+ Γ) (1+ Δ)
1+-rsubst θ = ⦅ 1+ˡ coverʳ ⦆ Var one ∷ θ

extend-subst : {Γ Δ Γ₁ : Context} → RSubst Γ Δ → Extend₁ Γ Γ₁ → ∃[ Δ₁ ] RSubst Γ₁ Δ₁ × Extend₁ Δ Δ₁
extend-subst s extend = _ , 1+-rsubst s , extend
extend-subst s refl = _ , s , refl

rsubst : {Γ₁ Γ₂ : Context} → RSubst Γ₁ Γ₂ → RTerm Γ₁ → RTerm Γ₂
rsubst s (Var one) = inv-one s
rsubst s (App θ t₁ t₂) =
  let _ , _ , s₁ , s₂ , θ′ = split-subst s θ in
  App θ′ (rsubst s₁ t₁) (rsubst s₂ t₂)
rsubst s (Lam θ t) =
  let _ , s₁ , θ₁ = extend-subst s θ in
  Lam θ₁ (rsubst s₁ t)
 
subst : {Γ₁ Γ₂ : Context} → Subst Γ₁ Γ₂ → Term Γ₁ → Term Γ₂
subst s (Weaken θ t) with weaken-subst s θ
... | Weaken θ′ s′ = Weaken θ′ (rsubst s′ t)