Subst.agda

module Subst where

open import Prelude
open import Lambda

infix 100 _[_] _[_:=_] _↑
infixl 100 _↑_ _↑ˢ_ _↑ˣ_ _↓ˣ_
infixl 60 _-_

{-
_-_ : {τ : Type}(Γ : Ctx) -> Var Γ τ -> Ctx
ε     - ()
Γ , τ - vz   = Γ
Γ , τ - vs x = (Γ - x) , τ

wkˣ : {Γ : Ctx}{σ τ : Type}
      (x : Var Γ σ) -> Var (Γ - x) τ -> Var Γ τ
wkˣ vz     y      = vs y
wkˣ (vs x) vz     = vz
wkˣ (vs x) (vs y) = vs (wkˣ x y)

wk : {Γ : Ctx}{σ τ : Type}
     (x : Var Γ σ) -> Term (Γ - x) τ -> Term Γ τ
wk x (var y) = var (wkˣ x y)
wk x (s • t) = wk x s • wk x t
wk x (ƛ t)   = ƛ wk (vs x) t

_↑ : {Γ : Ctx}{σ τ : Type} -> Term Γ τ -> Term (Γ , σ) τ
t ↑ = wk vz t

_↑_ : {Γ : Ctx}{τ : Type} -> Term Γ τ -> (Δ : Ctx) -> Term (Γ ++ Δ) τ
t ↑ ε       = t
t ↑ (Δ , σ) = (t ↑ Δ) ↑

data Cmpˣ {Γ : Ctx}{τ : Type}(x : Var Γ τ) :
          {σ : Type} -> Var Γ σ -> Set where
  same : Cmpˣ x x
  diff : {σ : Type}(y : Var (Γ - x) σ) -> Cmpˣ x (wkˣ x y)

_≟_ : {Γ : Ctx}{σ τ : Type}(x : Var Γ σ)(y : Var Γ τ) -> Cmpˣ x y
vz   ≟ vz   = same
vz   ≟ vs y = diff y
vs x ≟ vz   = diff vz
vs x ≟ vs y with x ≟ y
vs x ≟ vs .x         | same   = same
vs x ≟ vs .(wkˣ x y) | diff y = diff (vs y)

_[_:=_] : {Γ : Ctx}{σ τ : Type} ->
         Term Γ σ -> (x : Var Γ τ) -> Term (Γ - x) τ ->
         Term (Γ - x) σ
var y   [ x := u ] with x ≟ y
var .x         [ x := u ] | same = u
var .(wkˣ x y) [ x := u ] | diff y = var y
(s • t) [ x := u ] = s [ x := u ] • t [ x := u ]
(ƛ t)   [ x := u ] = ƛ t [ vs x := u ↑ ]
-}

infix 30 _─⟶_
infixl 90 _/_

_─⟶_ : Ctx -> Ctx -> Set
Γ ─⟶ Δ = Terms Γ Δ

idS : forall {Γ} -> Γ ─⟶ Γ
idS = tabulate var

infixr 80 _∘ˢ_

[_] : forall {Γ σ  } -> Term Γ σ -> Γ ─⟶ Γ , σ
[ t ] = idS ◄ t

wkS : forall {Γ Δ τ} -> Γ ─⟶ Δ -> Γ , τ ─⟶ Δ
wkS ∅       = ∅
wkS (θ ◄ t) = wkS θ ◄ wk t

_↑ : forall {Γ Δ τ} -> (Γ ─⟶ Δ) -> Γ , τ ─⟶ Δ , τ
θ ↑ = wkS θ ◄ vz

_/_ : forall {Γ Δ τ} -> Term Δ τ -> Γ ─⟶ Δ -> Term Γ τ
vz      / (θ ◄ u) = u
wk t    / (θ ◄ u) = t / θ
(s • t) / θ       = s / θ • t / θ
(ƛ t)   / θ       = ƛ t / θ ↑

_∘ˢ_ : forall {Γ Δ Θ} -> Δ ─⟶ Θ -> Γ ─⟶ Δ -> Γ ─⟶ Θ
∅       ∘ˢ θ = ∅
(δ ◄ t) ∘ˢ θ = δ ∘ˢ θ ◄ t / θ

inj : forall {Γ Δ τ} Θ -> Term Γ τ -> Γ ─⟶ Δ ++ Θ -> Γ ─⟶ Δ , τ ++ Θ
inj ε       t θ       = θ ◄ t
inj (Θ , σ) t (θ ◄ u) = inj Θ t θ ◄ u

[_⟵_] : forall {Γ τ} Δ -> Term (Γ ++ Δ) τ -> Γ ++ Δ ─⟶ Γ , τ ++ Δ
[ Δ ⟵ t ] = inj Δ t idS

_↑_ : forall {Γ σ} -> Term Γ σ -> (Δ : Ctx) -> Term (Γ ++ Δ) σ
t ↑ ε       = t
t ↑ (Δ , τ) = wk (t ↑ Δ)

_↑ˢ_ : forall {Γ Δ} -> Terms Γ Δ -> (Θ : Ctx) -> Terms (Γ ++ Θ) Δ
∅        ↑ˢ Θ = ∅
(ts ◄ t) ↑ˢ Θ = ts ↑ˢ Θ ◄ t ↑ Θ

_↑ˣ_ : forall {Γ τ} -> Var Γ τ -> (Δ : Ctx) -> Var (Γ ++ Δ) τ
x ↑ˣ ε       = x
x ↑ˣ (Δ , σ) = vsuc (x ↑ˣ Δ)

lem-var-↑ˣ : forall {Γ τ}(x : Var Γ τ)(Δ : Ctx) ->
             var (x ↑ˣ Δ) ≡ var x ↑ Δ
lem-var-↑ˣ x ε       = refl
lem-var-↑ˣ x (Δ , σ) = cong wk (lem-var-↑ˣ x Δ)

{- Not true!
lem-•-↑ : forall {Γ σ τ}(t : Term Γ (σ ⟶ τ))(u : Term Γ σ) Δ ->
          (t ↑ Δ) • (u ↑ Δ) ≡ (t • u) ↑ Δ
lem-•-↑ t u ε       = refl
lem-•-↑ t u (Δ , δ) = {! !}

lem-•ˢ-↑ : forall {Γ Θ τ}(t : Term Γ (Θ ⇒ τ))(ts : Terms Γ Θ) Δ ->
           (t ↑ Δ) •ˢ (ts ↑ˢ Δ) ≡ (t •ˢ ts) ↑ Δ
lem-•ˢ-↑ t ∅        Δ = refl
lem-•ˢ-↑ t (u ◄ us) Δ = {! !}
-}

{-
_[_] : {Γ : Ctx}{σ τ : Type} ->
       Term (Γ , τ) σ -> Term Γ τ -> Term Γ σ
t [ u ] = t / [ u ]
-}

{-
vz      [ u ] = u
wk t    [ u ] = {! !}
(s • t) [ u ] = {! !}
(ƛ_ {τ = ρ} t)   [ u ] = ƛ {! !}
-}

{-
_↓ˣ_ : {Γ : Ctx}{σ τ : Type}
       (y : Var Γ σ)(x : Var (Γ - y) τ) -> Var (Γ - wkˣ y x) σ
vz   ↓ˣ x    = vz
vs y ↓ˣ vz   = y
vs y ↓ˣ vs x = vs (y ↓ˣ x)

lem-commute-minus :
  {Γ : Ctx}{σ τ : Type}(y : Var Γ σ)(x : Var (Γ - y) τ) ->
  Γ - y - x ≡ Γ - wkˣ y x - (y ↓ˣ x)
lem-commute-minus vz     x      = refl
lem-commute-minus (vs y) vz     = refl
lem-commute-minus (vs {Γ} y) (vs x) with Γ - y - x | lem-commute-minus y x
... | ._ | refl = refl


Lem-wk-[] :
      {Γ : Ctx}{τ σ ρ : Type}
      (y : Var Γ τ)
      (x : Var (Γ - y) σ)
      (t : Term (Γ - wkˣ y x) ρ)
      (u : Term (Γ - y - x) τ) -> Set
Lem-wk-[] {Γ}{τ}{σ}{ρ} y x t u =
    wk (wkˣ y x) t [ y := wk x u ]
    ≡ wk x t[u']'
  where
    u' : Term (Γ - wkˣ y x - y ↓ˣ x) τ
    u' = subst (\Δ -> Term Δ τ) (sym (lem-commute-minus y x)) u

    t[u']' : Term (Γ - y - x) ρ
    t[u']' = subst (\Δ -> Term Δ ρ) (lem-commute-minus y x)
             (t [ y ↓ˣ x := u' ])

postulate
 lem-wk-[] : {Γ : Ctx}{σ τ ρ : Type}
             (y : Var Γ τ)(x : Var (Γ - y) σ)
             (t : Term (Γ - wkˣ y x) ρ){u : Term (Γ - y - x) τ} ->
             Lem-wk-[] y x t u
{-
lem-wk-[] y x (var z) = {! !}
lem-wk-[] y x (t • u) = {! !}
lem-wk-[] y x (ƛ t)   = {! !}
-}

lem-wk-[]' : {Γ : Ctx}{σ τ ρ : Type}
            (x : Var Γ σ)(t : Term (Γ - x , ρ) τ){u : Term (Γ - x) ρ} ->
            wk x (t [ vz := u ]) ≡ wk (vs x) t [ vz := wk x u ]
lem-wk-[]' x t = sym (lem-wk-[] vz x t)

-}