ILP9.agda

{-# OPTIONS --rewriting #-}

module ILP9 where

open import PreludeList public


id≟Nat : (n : Nat) → n ≟Nat n ≡ yes refl
id≟Nat n with n ≟Nat n
...      | yes refl = refl
...      | no n≢n   = refl ↯ n≢n
{-# REWRITE id≟Nat #-}


data Tm : Set where
  instance
    VAR   : Nat → Tm
    MVAR  : Nat → Tm
    LAM   : Nat → Tm → Tm
    APP   : Tm → Tm → Tm
    BOX   : Tm → Tm
    UNBOX : Tm → Nat → Tm → Tm

_[_≔_]ᵀᵐ : Tm → Nat → Tm → Tm
VAR y       [ x ≔ S ]ᵀᵐ with x ≟Nat y
...                     | yes refl = S
...                     | no x≢y   = VAR y
MVAR y      [ x ≔ S ]ᵀᵐ with x ≟Nat y
...                     | yes refl = S
...                     | no x≢y   = MVAR y
LAM y M     [ x ≔ S ]ᵀᵐ with x ≟Nat y
...                     | yes refl = LAM x M
...                     | no x≢y   = LAM y (M [ x ≔ S ]ᵀᵐ)
APP M N     [ x ≔ S ]ᵀᵐ = APP (M [ x ≔ S ]ᵀᵐ) (N [ x ≔ S ]ᵀᵐ)
BOX M       [ x ≔ S ]ᵀᵐ = BOX (M [ x ≔ S ]ᵀᵐ)
UNBOX M y N [ x ≔ S ]ᵀᵐ with x ≟Nat y
...                     | yes refl = UNBOX (M [ x ≔ S ]ᵀᵐ) x N
...                     | no x≢y   = UNBOX (M [ x ≔ S ]ᵀᵐ) y (N [ x ≔ S ]ᵀᵐ)

data _∥ᵀᵐ_ : Nat → Tm → Set where
  instance
    x∥VAR   : ∀ {x y}     → {{_ : x ≢ y}} → x ∥ᵀᵐ VAR y
    x∥MVAR  : ∀ {x y}     → {{_ : x ≢ y}} → x ∥ᵀᵐ MVAR y
    x∥LAM   : ∀ {x y M}   → {{_ : x ≢ y}} → {{_ : x ∥ᵀᵐ M}} → x ∥ᵀᵐ LAM y M
    x∥APP   : ∀ {x M N}   → {{_ : x ∥ᵀᵐ M}} {{_ : x ∥ᵀᵐ N}} → x ∥ᵀᵐ APP M N
    x∥BOX   : ∀ {x M}     → {{_ : x ∥ᵀᵐ M}} → x ∥ᵀᵐ BOX M
    x∥UNBOX : ∀ {x y M N} → {{_ : x ≢ y}} → {{_ : x ∥ᵀᵐ M}} {{_ : x ∥ᵀᵐ N}} → x ∥ᵀᵐ UNBOX M y N

instance
  idsubTm : ∀ {M S x} {{_ : x ∥ᵀᵐ M}} → M [ x ≔ S ]ᵀᵐ ≡ M
  idsubTm {{x∥VAR {x} {y} {{x≢y}}}}   with x ≟Nat y
  ...                                 | yes refl = refl ↯ x≢y
  ...                                 | no _     = refl
  idsubTm {{x∥MVAR {x} {y} {{x≢y}}}}  with x ≟Nat y
  ...                                 | yes refl = refl ↯ x≢y
  ...                                 | no _     = refl
  idsubTm {{x∥LAM {x} {y} {{x≢y}}}}   with x ≟Nat y
  ...                                 | yes refl = refl ↯ x≢y
  ...                                 | no _     = cong (LAM y) idsubTm
  idsubTm {{x∥APP}}                   = cong² APP idsubTm idsubTm
  idsubTm {{x∥BOX}}                   = cong BOX idsubTm
  idsubTm {{x∥UNBOX {x} {y} {{x≢y}}}} with x ≟Nat y
  ...                                 | yes refl = refl ↯ x≢y
  ...                                 | no _     = cong² (λ M → UNBOX M y) idsubTm idsubTm


infixr 7 _⇒_
data Ty : Set where
  instance
    •    : Ty
    _⇒_ : Ty → Ty → Ty
    [_]_ : Tm → Ty → Ty

_[_≔_]ᵀʸ : Ty → Nat → Tm → Ty
•         [ x ≔ S ]ᵀʸ = •
(A ⇒ B)  [ x ≔ S ]ᵀʸ = (A [ x ≔ S ]ᵀʸ) ⇒ (B [ x ≔ S ]ᵀʸ)
([ M ] A) [ x ≔ S ]ᵀʸ = [ (M [ x ≔ S ]ᵀᵐ) ] (A [ x ≔ S ]ᵀʸ)

data _∥ᵀʸ_ : Nat → Ty → Set where
  instance
    x∥•  : ∀ {x}     → x ∥ᵀʸ •
    x∥⇒ : ∀ {x A B} → {{_ : x ∥ᵀʸ A}} {{_ : x ∥ᵀʸ B}} → x ∥ᵀʸ (A ⇒ B)
    x∥□  : ∀ {x M A} → {{_ : x ∥ᵀᵐ M}} {{_ : x ∥ᵀʸ A}} → x ∥ᵀʸ ([ M ] A)

instance
  idsubTy : ∀ {A S x} {{_ : x ∥ᵀʸ A}} → A [ x ≔ S ]ᵀʸ ≡ A
  idsubTy {{x∥•}}  = refl
  idsubTy {{x∥⇒}} = cong² _⇒_ idsubTy idsubTy
  idsubTy {{x∥□}}  = cong² [_]_ idsubTm idsubTy


Cx : Set
Cx = List (Nat ∧ Ty) ∧ List (Nat ∧ Ty)


infix 3 _⊢_∷_
data _⊢_∷_ : Cx → Tm → Ty → Set where
  var : ∀ {Δ Γ A x} →
    Γ ∋ (x , A) →
    Δ ⁏ Γ ⊢ VAR x ∷ A

  mvar : ∀ {Δ Γ A x} →
    Δ ∋ (x , A) →
    Δ ⁏ Γ ⊢ MVAR x ∷ A

  lam : ∀ {Δ Γ M A B x} →
    Δ ⁏ Γ , (x , A) ⊢ M ∷ B →
    Δ ⁏ Γ ⊢ LAM x M ∷ A ⇒ B

  app : ∀ {Δ Γ M N A B} →
    Δ ⁏ Γ ⊢ M ∷ A ⇒ B → Δ ⁏ Γ ⊢ N ∷ A →
    Δ ⁏ Γ ⊢ APP M N ∷ B

  box : ∀ {Δ Γ M A} →
    Δ ⁏ ∅ ⊢ M ∷ A →
    Δ ⁏ Γ ⊢ BOX M ∷ [ M ] A

  unbox : ∀ {Δ Γ M N S A C C′ x} {{_ : C [ x ≔ S ]ᵀʸ ≡ C′}} →
    Δ ⁏ Γ ⊢ M ∷ [ S ] A → Δ , (x , A) ⁏ Γ ⊢ N ∷ C →
    Δ ⁏ Γ ⊢ UNBOX M x N ∷ C′

mono⊢ : ∀ {Δ Δ′ Γ Γ′ M A} → Δ′ ⊇ Δ → Γ′ ⊇ Γ → Δ ⁏ Γ ⊢ M ∷ A →
           Δ′ ⁏ Γ′ ⊢ M ∷ A
mono⊢ ζ η (var 𝒾)     = var (mono∋ η 𝒾)
mono⊢ ζ η (mvar 𝒾)    = mvar (mono∋ ζ 𝒾)
mono⊢ ζ η (lam 𝒟)     = lam (mono⊢ ζ (lift η) 𝒟)
mono⊢ ζ η (app 𝒟 ℰ)   = app (mono⊢ ζ η 𝒟) (mono⊢ ζ η ℰ)
mono⊢ ζ η (box 𝒟)     = box (mono⊢ ζ done 𝒟)
mono⊢ ζ η (unbox 𝒟 ℰ) = unbox (mono⊢ ζ η 𝒟) (mono⊢ (lift ζ) η ℰ)


v₀ : ∀ {Δ Γ A x} →
       Δ ⁏ Γ , (x , A) ⊢ VAR x ∷ A
v₀ = var zero

v₁ : ∀ {Δ Γ A B x y} →
       Δ ⁏ Γ , (x , A) , (y , B) ⊢ VAR x ∷ A
v₁ = var (suc zero)

v₂ : ∀ {Δ Γ A B C x y z} →
       Δ ⁏ Γ , (x , A) , (y , B) , (z , C) ⊢ VAR x ∷ A
v₂ = var (suc (suc zero))


axI : ∀ {Δ Γ A x} →
        Δ ⁏ Γ ⊢ LAM x (VAR x)
              ∷ A ⇒ A
axI = lam v₀

axK : ∀ {Δ Γ A B x y} →
        Δ ⁏ Γ ⊢ LAM x (LAM y (VAR x))
              ∷ A ⇒ B ⇒ A
axK = lam (lam v₁)

axS : ∀ {Δ Γ A B C f g x} →
        Δ ⁏ Γ ⊢ LAM f (LAM g (LAM x (APP (APP (VAR f) (VAR x)) (APP (VAR g) (VAR x)))))
              ∷ (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C
axS = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))


mv₀ : ∀ {Δ Γ A x} →
        Δ , (x , A) ⁏ Γ ⊢ MVAR x ∷ A
mv₀ = mvar zero

mv₁ : ∀ {Δ Γ A B x y} →
        Δ , (x , A) , (y , B) ⁏ Γ ⊢ MVAR x ∷ A
mv₁ = mvar (suc zero)

mv₂ : ∀ {Δ Γ A B C x y z} →
        Δ , (x , A) , (y , B) , (z , C) ⁏ Γ ⊢ MVAR x ∷ A
mv₂ = mvar (suc (suc zero))


instance
  helpD₁ : ∀ {M N S B f} {{_ : f ∥ᵀᵐ N}} {{_ : f ∥ᵀʸ B}} →
             [ APP M (N [ f ≔ S ]ᵀᵐ) ] (B [ f ≔ S ]ᵀʸ) ≡ [ APP M N ] B
  helpD₁ {M} = cong² [_]_ (cong (APP M) idsubTm) idsubTy

instance
  helpD₂ : ∀ {N M S B x} {{_ : x ∥ᵀᵐ M}} {{_ : x ∥ᵀʸ B}} →
             [ APP (M [ x ≔ S ]ᵀᵐ) N ] (B [ x ≔ S ]ᵀʸ) ≡ [ APP M N ] B
  helpD₂ {N} = cong² [_]_ (cong (λ M → APP M N) idsubTm) idsubTy

instance
  help4 : ∀ {M A S x} {{_ : x ∥ᵀʸ A}} →
            [ BOX M ] [ M ] (A [ x ≔ S ]ᵀʸ) ≡ [ BOX M ] [ M ] A
  help4 {M} = cong (λ A → [ BOX M ] [ M ] A) idsubTy


-- TODO: Can we automatically get x ∥ᵀᵐ MVAR f from x ≢ f?
-- TODO: Can we avoid having to explicitly declare C?
-- NOTE: Needs {-# REWRITE id≟Nat #-}.
axD : ∀ {Δ Γ M A N B f x `f `x} →
        {{_ : f ∥ᵀᵐ N}} {{_ : f ∥ᵀʸ B}} →
        {{_ : x ∥ᵀᵐ MVAR f}} {{_ : x ∥ᵀʸ B}} →
        Δ ⁏ Γ ⊢ LAM `f (LAM `x (UNBOX (VAR `f) f (UNBOX (VAR `x) x (BOX (APP (MVAR f) (MVAR x))))))
              ∷ [ M ] (A ⇒ B) ⇒ [ N ] A ⇒ [ APP M N ] B
axD {N = N} {B} {f} {x} =
      lam (lam
        (unbox {C = [ APP (MVAR f) N ] B} v₁
          (unbox {C = [ APP (MVAR f) (MVAR x) ] B} v₀
            (box (app mv₁ mv₀)))))

axT : ∀ {Δ Γ M A x `x} →
        {{_ : x ∥ᵀʸ A}} →
        Δ ⁏ Γ ⊢ LAM `x (UNBOX (VAR `x) x (MVAR x))
              ∷ [ M ] A ⇒ A
axT = lam (unbox v₀ mv₀)

-- NOTE: Needs {-# REWRITE id≟Nat #-}.
ax4 : ∀ {Δ Γ M A x `x} →
        {{_ : x ∥ᵀʸ A}} →
        Δ ⁏ Γ ⊢ LAM `x (UNBOX (VAR `x) x (BOX (BOX (MVAR x))))
              ∷ [ M ] A ⇒ [ BOX M ] [ M ] A
ax4 = lam (unbox v₀ (box (box mv₀)))