LP.agda

module LP where

open import Data.Empty using () renaming (⊥ to Empty)
open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
open import Data.Unit using () renaming (⊤ to Unit ; tt to unit)
open import Relation.Binary.PropositionalEquality as P -- using (_≡_ ; refl; cong₂; subst)


data Cx (X : Set) : Set where
  ∅   : Cx X
  _,_ : Cx X → X → Cx X


data Var (X : Set) : Cx X → X → Set where
  top : ∀ {Γ A} → Var X (Γ , A) A
  pop : ∀ {Γ A B} → Var X Γ A → Var X (Γ , B) A


x₀ : ∀ {X Γ A} → Var X (Γ , A) A
x₀ = top

x₁ : ∀ {X Γ A B} → Var X ((Γ , A) , B) A
x₁ = pop x₀

x₂ : ∀ {X Γ A B C} → Var X (((Γ , A) , B) , C) A
x₂ = pop x₁


module S4 where
  data Ty : Set where
    ⊥  : Ty
    _⊃_ : Ty → Ty → Ty
    _∧_ : Ty → Ty → Ty
    □_  : Ty → Ty

  data Tm (Γ Δ : Cx Ty) : Ty → Set where
    var  : ∀ {A} → Var Ty Γ A → Tm Γ Δ A
    lam  : ∀ {A B} → Tm (Γ , A) Δ B → Tm Γ Δ (A ⊃ B)
    app  : ∀ {A B} → Tm Γ Δ (A ⊃ B) → Tm Γ Δ A → Tm Γ Δ B
    *var : ∀ {A} → Var Ty Δ A → Tm Γ Δ A
    up   : ∀ {A} → Tm ∅ Δ A → Tm Γ Δ (□ A)
    down : ∀ {A C} → Tm Γ Δ (□ A) → Tm Γ (Δ , A) C → Tm Γ Δ C
    pair : ∀ {A B} → Tm Γ Δ A → Tm Γ Δ B → Tm Γ Δ (A ∧ B)
    fst  : ∀ {A B} → Tm Γ Δ (A ∧ B) → Tm Γ Δ A
    snd  : ∀ {A B} → Tm Γ Δ (A ∧ B) → Tm Γ Δ B

  ⟦_⟧ᴬ : Ty → Set
  ⟦ ⊥ ⟧ᴬ    = Empty
  ⟦ A ⊃ B ⟧ᴬ = ⟦ A ⟧ᴬ → ⟦ B ⟧ᴬ
  ⟦ A ∧ B ⟧ᴬ = ⟦ A ⟧ᴬ × ⟦ B ⟧ᴬ
  ⟦ □ A ⟧ᴬ = ⟦ A ⟧ᴬ

  ⟦_⟧ᴳ : Cx Ty → Set
  ⟦ ∅ ⟧ᴳ       = Unit
  ⟦ (Γ , A) ⟧ᴳ = ⟦ Γ ⟧ᴳ × ⟦ A ⟧ᴬ

  ⟦_⟧ˣ : ∀ {Γ A} → Var Ty Γ A → ⟦ Γ ⟧ᴳ → ⟦ A ⟧ᴬ
  ⟦ top ⟧ˣ   (γ , a) = a
  ⟦ pop x ⟧ˣ (γ , b) = ⟦ x ⟧ˣ γ

  ⟦_⟧ : ∀ {Γ Δ A} → Tm Γ Δ A → ⟦ Γ ⟧ᴳ → ⟦ Δ ⟧ᴳ → ⟦ A ⟧ᴬ
  ⟦ var x ⟧      γ δ = ⟦ x ⟧ˣ γ
  ⟦ lam t ⟧      γ δ = λ a → ⟦ t ⟧ (γ , a) δ
  ⟦ app t₁ t₂ ⟧  γ δ = (⟦ t₁ ⟧ γ δ) (⟦ t₂ ⟧ γ δ)
  ⟦ *var x ⟧     γ δ = ⟦ x ⟧ˣ δ
  ⟦ up t ⟧       γ δ = ⟦ t ⟧ unit δ
  ⟦ down t₁ t₂ ⟧ γ δ = ⟦ t₂ ⟧ γ (δ , ⟦ t₁ ⟧ γ δ)
  ⟦ pair t₁ t₂ ⟧ γ δ = (⟦ t₁ ⟧ γ δ , ⟦ t₂ ⟧ γ δ)
  ⟦ fst t ⟧      γ δ = proj₁ (⟦ t ⟧ γ δ)
  ⟦ snd t ⟧      γ δ = proj₂ (⟦ t ⟧ γ δ)

  infixr 5 _⊃_
  infixl 10 _∧_

  v₀ : ∀ {Γ Δ A} → Tm (Γ , A) Δ A
  v₀ = var x₀

  v₁ : ∀ {Γ Δ A B} → Tm ((Γ , A) , B) Δ A
  v₁ = var x₁

  v₂ : ∀ {Γ Δ A B C} → Tm (((Γ , A) , B) , C) Δ A
  v₂ = var x₂

  *v₀ : ∀ {Γ Δ A} → Tm Γ (Δ , A) A
  *v₀ = *var x₀

  *v₁ : ∀ {Γ Δ A B} → Tm Γ ((Δ , A) , B) A
  *v₁ = *var x₁

  *v₂ : ∀ {Γ Δ A B C} → Tm Γ (((Δ , A) , B) , C) A
  *v₂ = *var x₂

  module Examples where
    I : ∀ {Γ Δ A} → Tm Γ Δ (A ⊃ A)
    I = lam v₀

    K : ∀ {Γ Δ A B} → Tm Γ Δ (A ⊃ B ⊃ A)
    K = lam (lam v₁)

    S : ∀ {Γ Δ A B C} → Tm Γ Δ ((A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C)
    S = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

    D : ∀ {Γ Δ A B} → Tm Γ Δ (□ (A ⊃ B) ⊃ □ A ⊃ □ B)
    D = lam (lam (down v₁ (down v₀ (up (app *v₁ *v₀)))))

    T : ∀ {Γ Δ A} → Tm Γ Δ (□ A ⊃ A)
    T = lam (down v₀ *v₀)

    #4 : ∀ {Γ Δ A} → Tm Γ Δ (□ A ⊃ □ □ A)
    #4 = lam (down v₀ (up (up *v₀)))

    E1 : ∀ {Γ Δ A} → Tm Γ Δ (□ (□ A ⊃ A))
    E1 = up T

    E2 : ∀ {Γ Δ A} → Tm Γ Δ (□ (□ A ⊃ □ □ A))
    E2 = up #4

    E3 : ∀ {Γ Δ A B} → Tm Γ Δ (□ □ (A ⊃ B ⊃ A ∧ B))
    E3 = up (up (lam (lam (pair v₁ v₀))))

    E4 : ∀ {Γ Δ A B} → Tm Γ Δ (□ (□ A ⊃ □ B ⊃ □ □ (A ∧ B)))
    E4 = up (lam (lam (down v₁ (down v₀ (up (up (pair *v₁ *v₀)))))))


mutual
  data Ty : Set where
    ⊥  : Ty
    _⊃_ : Ty → Ty → Ty
    _∧_ : Ty → Ty → Ty
    _∴_ : ∀ {Ξ A} → Tm ∅ Ξ A → Ty → Ty

  data Tm (Γ Δ : Cx Ty) : Ty → Set where
    var  : ∀ {A} → Var Ty Γ A → Tm Γ Δ A
    lam  : ∀ {A B} → Tm (Γ , A) Δ B → Tm Γ Δ (A ⊃ B)
    app  : ∀ {A B} → Tm Γ Δ (A ⊃ B) → Tm Γ Δ A → Tm Γ Δ B
    *var : ∀ {A} → Var Ty Δ A → Tm Γ Δ A
    up   : ∀ {A} → (t : Tm ∅ Δ A) → Tm Γ Δ (t ∴ A)
    down : ∀ {Ξ A C} {t : Tm ∅ Ξ A} → Tm Γ Δ (t ∴ A) → Tm Γ (Δ , A) C → Tm Γ Δ C
    pair : ∀ {A B} → Tm Γ Δ A → Tm Γ Δ B → Tm Γ Δ (A ∧ B)
    fst  : ∀ {A B} → Tm Γ Δ (A ∧ B) → Tm Γ Δ A
    snd  : ∀ {A B} → Tm Γ Δ (A ∧ B) → Tm Γ Δ B


syntax lam t      = ƛ t
syntax app t₁ t₂  = t₁ ∙ t₂
syntax up t       = ⇑ t
syntax down t₁ t₂ = ⇓⟨ t₁ ∣ t₂ ⟩
syntax pair t₁ t₂ = p⟨ t₁ , t₂ ⟩
syntax fst t      = π₀ t
syntax snd t      = π₁ t

infixr 5 _⊃_
infixl 10 _∧_
infixl 10 app
infixr 15 _∴_


v₀ : ∀ {Γ Δ A} → Tm (Γ , A) Δ A
v₀ = var x₀

v₁ : ∀ {Γ Δ A B} → Tm ((Γ , A) , B) Δ A
v₁ = var x₁

v₂ : ∀ {Γ Δ A B C} → Tm (((Γ , A) , B) , C) Δ A
v₂ = var x₂

*v₀ : ∀ {Γ Δ A} → Tm Γ (Δ , A) A
*v₀ = *var x₀

*v₁ : ∀ {Γ Δ A B} → Tm Γ ((Δ , A) , B) A
*v₁ = *var x₁

*v₂ : ∀ {Γ Δ A B C} → Tm Γ (((Δ , A) , B) , C) A
*v₂ = *var x₂

[vᵢ]_ : Ty → Ty
[vᵢ] A = _∴_ {Ξ = (∅ , A)} *v₀ A


module Examples where
  I : ∀ {Γ Δ A} → Tm Γ Δ (A ⊃ A)
  I = lam v₀

  K : ∀ {Γ Δ A B} → Tm Γ Δ (A ⊃ B ⊃ A)
  K = lam (lam v₁)

  S : ∀ {Γ Δ A B C} → Tm Γ Δ ((A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C)
  S = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

  D : ∀ {Γ Δ A B} → Tm Γ Δ ([vᵢ] (A ⊃ B) ⊃ [vᵢ] A ⊃ app *v₁ *v₀ ∴ B)
  D = lam (lam (down v₁ (down v₀ (up (app *v₁ *v₀)))))

  T : ∀ {Γ Δ A} → Tm Γ Δ ([vᵢ] A ⊃ A)
  T = lam (down v₀ *v₀)

  #4 : ∀ {Γ Δ A} → Tm Γ Δ ([vᵢ] A ⊃ up *v₀ ∴ *v₀ ∴ A)
  #4 = lam (down v₀ (up (up *v₀)))

  E1 : ∀ {Γ Δ A} → Tm Γ Δ (T ∴ ([vᵢ] A ⊃ A))
  E1 = up T

  E2 : ∀ {Γ Δ A} → Tm Γ Δ (#4 ∴ ([vᵢ] A ⊃ up *v₀ ∴ *v₀ ∴ A))
  E2 = up #4

  E3 : ∀ {Γ Δ A B} →
       Tm Γ Δ (up (lam (lam (pair v₁ v₀))) ∴ lam (lam (pair v₁ v₀)) ∴ (A ⊃ B ⊃ A ∧ B))
  E3 = up (up (lam (lam (pair v₁ v₀))))

  E4 : ∀ {Γ Δ A B} →
       Tm Γ Δ (lam (lam (down v₁ (down v₀ (up (up (pair *v₁ *v₀)))))) ∴
              ([vᵢ] A ⊃ [vᵢ] B ⊃ up (pair *v₁ *v₀) ∴ pair *v₁ *v₀ ∴ (A ∧ B)))
  E4 = up (lam (lam (down v₁ (down v₀ (up (up (pair *v₁ *v₀)))))))


module AltArtemovNotation where
  I : ∀ {Γ Δ A} → Tm Γ Δ (A ⊃ A)
  I = ƛ v₀

  K : ∀ {Γ Δ A B} → Tm Γ Δ (A ⊃ B ⊃ A)
  K = ƛ ƛ v₁

  S : ∀ {Γ Δ A B C} → Tm Γ Δ ((A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C)
  S = ƛ ƛ ƛ ((v₂ ∙ v₀) ∙ (v₁ ∙ v₀))

  D : ∀ {Γ Δ A B} → Tm Γ Δ ([vᵢ] (A ⊃ B) ⊃ [vᵢ] A ⊃ (*v₁ ∙ *v₀) ∴ B)
  D = ƛ ƛ ⇓⟨ v₁ ∣ ⇓⟨ v₀ ∣ ⇑ (*v₁ ∙ *v₀) ⟩ ⟩

  T : ∀ {Γ Δ A} → Tm Γ Δ ([vᵢ] A ⊃ A)
  T = ƛ ⇓⟨ v₀ ∣ *v₀ ⟩

  #4 : ∀ {Γ Δ A} → Tm Γ Δ ([vᵢ] A ⊃ ⇑ *v₀ ∴ *v₀ ∴ A)
  #4 = ƛ ⇓⟨ v₀ ∣ ⇑ ⇑ *v₀ ⟩

  E1 : ∀ {Γ Δ A} → Tm Γ Δ (T ∴ ([vᵢ] A ⊃ A))
  E1 = ⇑ T

  E2 : ∀ {Γ Δ A} → Tm Γ Δ (#4 ∴ ([vᵢ] A ⊃ ⇑ *v₀ ∴ *v₀ ∴ A))
  E2 = ⇑ #4

  E3 : ∀ {Γ Δ A B} →
       Tm Γ Δ (⇑ ƛ ƛ p⟨ v₁ , v₀ ⟩ ∴ ƛ ƛ p⟨ v₁ , v₀ ⟩ ∴ (A ⊃ B ⊃ A ∧ B))
  E3 = ⇑ ⇑ ƛ ƛ p⟨ v₁ , v₀ ⟩

  E4 : ∀ {Γ Δ A B} →
       Tm Γ Δ (ƛ ƛ ⇓⟨ v₁ ∣ ⇓⟨ v₀ ∣ ⇑ ⇑ p⟨ *v₁ , *v₀ ⟩ ⟩ ⟩ ∴
              ([vᵢ] A ⊃ [vᵢ] B ⊃ ⇑ p⟨ *v₁ , *v₀ ⟩ ∴ p⟨ *v₁ , *v₀ ⟩ ∴ (A ∧ B)))
  E4 = ⇑ ƛ ƛ ⇓⟨ v₁ ∣ ⇓⟨ v₀ ∣ ⇑ ⇑ p⟨ *v₁ , *v₀ ⟩ ⟩ ⟩

mutual
  ⟦_⟧ᴬ : Ty → Set
  ⟦ ⊥ ⟧ᴬ    = Empty
  ⟦ A ⊃ B ⟧ᴬ = ⟦ A ⟧ᴬ → ⟦ B ⟧ᴬ
  ⟦ A ∧ B ⟧ᴬ = ⟦ A ⟧ᴬ × ⟦ B ⟧ᴬ
  ⟦ t ∴ A ⟧ᴬ = ⟦ A ⟧ᴬ

  ⟦_⟧ᴳ : Cx Ty → Set
  ⟦ ∅ ⟧ᴳ       = Unit
  ⟦ (Γ , A) ⟧ᴳ = ⟦ Γ ⟧ᴳ × ⟦ A ⟧ᴬ

  ⟦_⟧ˣ : ∀ {Γ A} → Var Ty Γ A → ⟦ Γ ⟧ᴳ → ⟦ A ⟧ᴬ
  ⟦ top ⟧ˣ   (γ , a) = a
  ⟦ pop x ⟧ˣ (γ , b) = ⟦ x ⟧ˣ γ

  ⟦_⟧ : ∀ {Γ Δ A} → Tm Γ Δ A → ⟦ Γ ⟧ᴳ → ⟦ Δ ⟧ᴳ → ⟦ A ⟧ᴬ
  ⟦ var x ⟧      γ δ = ⟦ x ⟧ˣ γ
  ⟦ lam t ⟧      γ δ = λ a → ⟦ t ⟧ (γ , a) δ
  ⟦ app t₁ t₂ ⟧  γ δ = (⟦ t₁ ⟧ γ δ) (⟦ t₂ ⟧ γ δ)
  ⟦ *var x ⟧     γ δ = ⟦ x ⟧ˣ δ
  ⟦ up t ⟧       γ δ = ⟦ t ⟧ unit δ
  ⟦ down t₁ t₂ ⟧ γ δ = ⟦ t₂ ⟧ γ (δ , ⟦ t₁ ⟧ γ δ)
  ⟦ pair t₁ t₂ ⟧ γ δ = (⟦ t₁ ⟧ γ δ , ⟦ t₂ ⟧ γ δ)
  ⟦ fst t ⟧      γ δ = proj₁ (⟦ t ⟧ γ δ)
  ⟦ snd t ⟧      γ δ = proj₂ (⟦ t ⟧ γ δ)

open import Relation.Binary.HeterogeneousEquality as H

hcongprod : ∀ {A B C D : Set} {a : A} {b : B} → (p₁ : A ≅ C) → (p₂ : D ≅ B) →
        b ≡ H.subst (λ x → x) p₂ (proj₂ (H.subst (λ x → x) (H.cong₂ _×_ p₁ (H.sym p₂)) (a , b)))
hcongprod refl refl = refl

congprod₂ : ∀ {A B C D : Set} (a : A) (b : B) → (p₁ : A ≡ C) → (p₂ : B ≡ D) →
        b ≡ P.subst (λ x → x) (P.sym p₂) (proj₂ (P.subst (λ x → x) (P.cong₂ _×_ p₁ p₂) (a , b)))
congprod₂ a b refl refl = refl

module ForgetfulProjection where
  ⌊_⌋ᴬ : Ty → S4.Ty
  ⌊ ⊥ ⌋ᴬ    = S4.⊥
  ⌊ A ⊃ B ⌋ᴬ = ⌊ A ⌋ᴬ S4.⊃ ⌊ B ⌋ᴬ
  ⌊ A ∧ B ⌋ᴬ = ⌊ A ⌋ᴬ S4.∧ ⌊ B ⌋ᴬ
  ⌊ t ∴ A ⌋ᴬ = S4.□ ⌊ A ⌋ᴬ

  ⌊_⌋ᴬ-sound : ∀ t → ⟦ t ⟧ᴬ ≡ S4.⟦ ⌊ t ⌋ᴬ ⟧ᴬ
  ⌊ ⊥ ⌋ᴬ-sound = refl
  ⌊ S ⊃ T ⌋ᴬ-sound = P.cong₂ (λ x y → x → y) ⌊ S ⌋ᴬ-sound ⌊ T ⌋ᴬ-sound
  ⌊ S ∧ T ⌋ᴬ-sound = P.cong₂ _×_ ⌊ S ⌋ᴬ-sound ⌊ T ⌋ᴬ-sound
  ⌊ x ∴ T ⌋ᴬ-sound = ⌊ T ⌋ᴬ-sound

  ⌊_⌋ᴳ : Cx Ty → Cx S4.Ty
  ⌊ ∅ ⌋ᴳ       = ∅
  ⌊ (Γ , A) ⌋ᴳ = (⌊ Γ ⌋ᴳ , ⌊ A ⌋ᴬ)

  ⌊_⌋ᴳ-sound : ∀ Γ → ⟦ Γ ⟧ᴳ ≡ S4.⟦ ⌊ Γ ⌋ᴳ ⟧ᴳ
  ⌊ ∅ ⌋ᴳ-sound = refl
  ⌊ Γ , τ ⌋ᴳ-sound = P.cong₂ _×_ ⌊ Γ ⌋ᴳ-sound ⌊ τ ⌋ᴬ-sound

  ⌊_⌋ˣ : ∀ {Γ A} → Var Ty Γ A → Var S4.Ty ⌊ Γ ⌋ᴳ ⌊ A ⌋ᴬ
  ⌊ top ⌋ˣ   = top
  ⌊ pop x ⌋ˣ = pop ⌊ x ⌋ˣ

  ⌊_⌋ : ∀ {Γ Δ A} → Tm Γ Δ A → S4.Tm ⌊ Γ ⌋ᴳ ⌊ Δ ⌋ᴳ ⌊ A ⌋ᴬ
  ⌊ var x ⌋      = S4.var ⌊ x ⌋ˣ
  ⌊ lam t ⌋      = S4.lam ⌊ t ⌋
  ⌊ app t₁ t₂ ⌋  = S4.app ⌊ t₁ ⌋ ⌊ t₂ ⌋
  ⌊ *var x ⌋     = S4.*var ⌊ x ⌋ˣ
  ⌊ up t ⌋       = S4.up ⌊ t ⌋
  ⌊ down t₁ t₂ ⌋ = S4.down ⌊ t₁ ⌋ ⌊ t₂ ⌋
  ⌊ pair t₁ t₂ ⌋ = S4.pair ⌊ t₁ ⌋ ⌊ t₂ ⌋
  ⌊ fst t ⌋      = S4.fst ⌊ t ⌋
  ⌊ snd t ⌋      = S4.snd ⌊ t ⌋

  -- Further correctness lemmas. Having to use subst is a pain.

  cast : ∀ {t u : Set} → t ≡ u → t → u -- u → t
  cast p = P.subst (λ x → x) p

  cast′ : ∀ {t u : Set} → t ≡ u → u → t
  cast′ t≡u = cast (P.sym t≡u)

  congprod₁ : ∀ {A B C D : Set} (a : A) (b : B) → (p₁ : A ≡ C) → (p₂ : B ≡ D) →
        a ≡ cast′ p₁ (proj₁ (cast (P.cong₂ _×_ p₁ p₂) (a , b)))
  congprod₁ a b refl refl = refl

  congfprod₁ : ∀ {X Y A B C D : Set} (a : X) (b : B) → (p₁ : A ≡ C) → (p₂ : B ≡ D) → (p₃ : X ≡ Y) → (f : X → A) → (g : Y → C) →
        (fgrel : f a ≡ cast′ p₁ (g (cast p₃ a))) →
        cast′ p₁ (proj₁ (cast (P.cong₂ _×_ p₁ p₂) (f a , b))) ≡ cast′ p₁ (g (proj₁ (cast (P.cong₂ _×_ p₃ p₂) (a , b))))
  congfprod₁ a b refl refl refl f g fgrel = fgrel

  ⌊_⌋ˣ-sound : ∀ {Γ A} → (x : Var Ty Γ A) → (γ : ⟦ Γ ⟧ᴳ) → ⟦ x ⟧ˣ γ ≡ cast′ ⌊ A ⌋ᴬ-sound (S4.⟦ ⌊ x ⌋ˣ ⟧ˣ (cast ⌊ Γ ⌋ᴳ-sound γ))
  ⌊_⌋ˣ-sound {Γ , A} top (γ , a) = congprod₂ γ a ⌊ Γ ⌋ᴳ-sound ⌊ A ⌋ᴬ-sound
  ⌊_⌋ˣ-sound {Γ , A} {B} (pop x) (γ , b) =
    P.trans
      (congprod₁ (⟦ x ⟧ˣ γ) b (⌊ B ⌋ᴬ-sound) (⌊ A ⌋ᴬ-sound))
      (congfprod₁ γ b ⌊ B ⌋ᴬ-sound ⌊ A ⌋ᴬ-sound ⌊ Γ ⌋ᴳ-sound (⟦ x ⟧ˣ) (S4.⟦ ⌊ x ⌋ˣ ⟧ˣ) (⌊_⌋ˣ-sound x γ))


  --⌊_⌋-sound : ∀ {Γ Δ A} → (t : Tm Γ Δ A) → (γ : ⟦ Γ ⟧ᴳ) → (δ : ⟦ Δ ⟧ᴳ) → (⟦ t ⟧ γ δ) ≡ S4.⟦ ⌊ t ⌋ ⟧ ? ?
  --⌊_⌋-sound = ?