Source.Size.Substitution.Canonical

{-# OPTIONS --without-K --safe #-}
module Source.Size.Substitution.Canonical where

open import Source.Size
open import Util.Prelude


infix  0 Sub⊢
infixl 5 _>>_


data Sub (Δ : Ctx) : (Ω : Ctx) → Set where
  [] : Sub Δ []
  Snoc : (σ : Sub Δ Ω) (n : Size Δ) → Sub Δ (Ω ∙ m)


variable
  σ τ σ′ τ′ ι ι′ : Sub Δ Ω


subV : Sub Δ Ω → Var Ω → Size Δ
subV (Snoc σ n) zero = n
subV (Snoc σ n) (suc x) = subV σ x


sub : Sub Δ Ω → Size Ω → Size Δ
sub σ (var x) = subV σ x
sub σ ∞ = ∞
sub σ zero = zero
sub σ (suc n) = suc (sub σ n)


data Sub⊢ Δ : ∀ Ω (σ : Sub Δ Ω) → Set where
  [] : Sub⊢ Δ [] []
  Snoc : (⊢σ : Sub⊢ Δ Ω σ) (n<m : n < sub σ m) → Sub⊢ Δ (Ω ∙ m) (Snoc σ n)


syntax Sub⊢ Δ Ω σ = σ ∶ Δ ⇒ Ω


abstract
  sub-Snoc : ∀ (σ : Sub Δ Ω) n o
    → sub (Snoc {m = m} σ n) (wk o) ≡ sub σ o
  sub-Snoc σ n (var x) = refl
  sub-Snoc σ n ∞ = refl
  sub-Snoc σ n zero = refl
  sub-Snoc σ n (suc o) = cong suc (sub-Snoc σ n o)


  mutual
    subV-resp-< : σ ∶ Δ ⇒ Ω → var x < n → subV σ x < sub σ n
    subV-resp-< {x = zero} (Snoc {σ = σ} {n} {m} ⊢σ n<m) (var refl)
      = subst (n <_) (sym (sub-Snoc σ n m)) n<m
    subV-resp-< {x = suc x} (Snoc {σ = σ} {n} {m} ⊢σ n<m) (var refl)
      = subst (subV σ x <_) (sym (sub-Snoc σ n (bound x)))
          (subV-resp-< ⊢σ (var refl))
    subV-resp-< ⊢σ <suc = <suc
    subV-resp-< ⊢σ (<-trans x<m m<n)
      = <-trans (subV-resp-< ⊢σ x<m) (sub-resp-< ⊢σ m<n)


    sub-resp-< : σ ∶ Δ ⇒ Ω → n < m → sub σ n < sub σ m
    sub-resp-< ⊢σ (var p) = subV-resp-< ⊢σ (var p)
    sub-resp-< ⊢σ zero<suc = zero<suc
    sub-resp-< ⊢σ zero<∞ = zero<∞
    sub-resp-< ⊢σ (suc<suc n<m) = suc<suc (sub-resp-< ⊢σ n<m)
    sub-resp-< ⊢σ (suc<∞ n<∞) = suc<∞ (sub-resp-< ⊢σ n<∞)
    sub-resp-< ⊢σ (<-trans n<o o<m)
      = <-trans (sub-resp-< ⊢σ n<o) (sub-resp-< ⊢σ o<m)
    sub-resp-< ⊢σ <suc = <suc


Weaken : Sub Δ Ω → Sub (Δ ∙ n) Ω
Weaken [] = []
Weaken (Snoc σ m) = Snoc (Weaken σ) (wk m)


abstract
  subV-Weaken : ∀ (σ : Sub Δ Ω) x → subV (Weaken {n = o} σ) x ≡ wk (subV σ x)
  subV-Weaken (Snoc σ n) zero = refl
  subV-Weaken (Snoc σ n) (suc x) = subV-Weaken σ x


  sub-Weaken : ∀ (σ : Sub Δ Ω) n → sub (Weaken {n = o} σ) n ≡ wk (sub σ n)
  sub-Weaken σ (var x) = subV-Weaken σ x
  sub-Weaken σ ∞ = refl
  sub-Weaken σ zero = refl
  sub-Weaken σ (suc n) = cong suc (sub-Weaken σ n)


  Weaken⊢ : σ ∶ Δ ⇒ Ω → Weaken σ ∶ Δ ∙ n ⇒ Ω
  Weaken⊢ [] = []
  Weaken⊢ (Snoc {σ = σ} {n} {m} ⊢σ n<m)
    = Snoc (Weaken⊢ ⊢σ)
        (subst (wk n <_) (sym (sub-Weaken σ m)) (wk-resp-< n<m))


Lift : (σ : Sub Δ Ω) → Sub (Δ ∙ m) (Ω ∙ n)
Lift σ = Snoc (Weaken σ) (var zero)


abstract
  Lift⊢ : σ ∶ Δ ⇒ Ω → m ≡ sub σ n → Lift σ ∶ Δ ∙ m ⇒ Ω ∙ n
  Lift⊢ {Δ} {σ = σ} {n = n} ⊢σ refl
    = Snoc (Weaken⊢ ⊢σ) (var (sub-Weaken σ n))


mutual
  Id : Sub Δ Δ
  Id {[]} = []
  Id {Δ ∙ n} = Lift Id


  abstract
    subV-Id : ∀ x → subV (Id {Δ}) x ≡ var x
    subV-Id zero = refl
    subV-Id (suc x) = trans (subV-Weaken Id x) (cong wk (subV-Id x))


    sub-Id : ∀ n → σ ≡ Id → sub σ n ≡ n
    sub-Id (var x) refl  = subV-Id x
    sub-Id ∞ _ = refl
    sub-Id zero _ = refl
    sub-Id (suc n) p = cong suc (sub-Id n p)


abstract
  Id⊢ : Id ∶ Δ ⇒ Δ
  Id⊢ {[]} = []
  Id⊢ {Δ ∙ n} = Lift⊢ Id⊢ (sym (sub-Id _ refl))


Wk : Sub (Δ ∙ n) Δ
Wk = Weaken Id


abstract
  sub-Wk : ∀ n → sub (Wk {Δ} {o}) n ≡ wk n
  sub-Wk n = trans (sub-Weaken Id n) (cong wk (sub-Id _ refl))


  Wk⊢ : Wk ∶ Δ ∙ n ⇒ Δ
  Wk⊢ = Weaken⊢ Id⊢


Sing : Size Δ → Sub Δ (Δ ∙ m)
Sing n = Snoc Id n


abstract
  Sing⊢ : n < m → Sing n ∶ Δ ⇒ Δ ∙ m
  Sing⊢ {n = n} n<m
    = Snoc Id⊢ (subst (n <_) (sym (sub-Id _ refl)) n<m)


_>>_ : Sub Δ Δ′ → Sub Δ′ Δ″ → Sub Δ Δ″
σ >> [] = []
σ >> Snoc τ n = Snoc (σ >> τ) (sub σ n)


abstract
  subV->> : ∀ (σ : Sub Δ Δ′) (τ : Sub Δ′ Δ″) x
    → subV (σ >> τ) x ≡ sub σ (subV τ x)
  subV->> σ (Snoc τ n) zero = refl
  subV->> σ (Snoc τ n) (suc x) = subV->> σ τ x


  sub->> : ∀ n → ι ≡ σ >> τ
    → sub ι n ≡ sub σ (sub τ n)
  sub->> {σ = σ} {τ} (var x) refl = subV->> σ τ x
  sub->> ∞ _ = refl
  sub->> zero _ = refl
  sub->> (suc n) p = cong suc (sub->> n p)


  sub->>′ : σ >> τ ≡ σ′ >> τ′ → sub σ (sub τ n) ≡ sub σ′ (sub τ′ n)
  sub->>′ {σ = σ} {τ = τ} {σ′ = σ′} {τ′} {n} eq
    = trans (sym (sub->> n refl))
        (trans (cong (λ σ → sub σ n) eq) (sub->> n refl))


  >>⊢ : σ ∶ Δ ⇒ Δ′ → τ ∶ Δ′ ⇒ Δ″ → σ >> τ ∶ Δ ⇒ Δ″
  >>⊢ ⊢σ [] = []
  >>⊢ {σ = σ} ⊢σ (Snoc {σ = τ} {n} {m} ⊢τ n<m)
    = Snoc (>>⊢ ⊢σ ⊢τ)
        (subst (sub σ n <_) (sym (sub->> m refl)) (sub-resp-< ⊢σ n<m))


Skip : Sub (Δ ∙ n ∙ v0) (Δ ∙ n)
Skip = Snoc (Weaken Wk) (var zero)


abstract
  Skip⊢ : Skip ∶ Δ ∙ n ∙ v0 ⇒ Δ ∙ n
  Skip⊢ {n = n}
    = Snoc (Weaken⊢ Wk⊢)
        (<-trans (var refl)
          (var (trans (sub-Weaken Wk n) (cong wk (sub-Wk n)))))


  Weaken>> : Weaken σ >> τ ≡ Weaken {n = n} (σ >> τ)
  Weaken>> {τ = []} = refl
  Weaken>> {σ = σ} {τ = Snoc τ n} = cong₂ Snoc Weaken>>  (sub-Weaken σ n)


  Snoc>>Weaken : Snoc {m = m} σ n >> Weaken τ ≡ σ >> τ
  Snoc>>Weaken {τ = []} = refl
  Snoc>>Weaken {σ = σ} {n = n} {τ = Snoc τ k}
    = cong₂ Snoc Snoc>>Weaken (sub-Snoc σ n k)


  id-l : Id >> σ ≡ σ
  id-l {σ = []} = refl
  id-l {σ = Snoc σ n} = cong₂ Snoc id-l (sub-Id n refl)


  id-r : {σ : Sub Δ Ω} → σ >> Id ≡ σ
  id-r {σ = []} = refl
  id-r {σ = Snoc σ n} = cong₂ Snoc (trans Snoc>>Weaken id-r) refl


  >>-assoc : σ >> (τ >> ι) ≡ σ >> τ >> ι
  >>-assoc {ι = []} = refl
  >>-assoc {σ = σ} {τ = τ} {ι = Snoc ι n}
    = cong₂ Snoc >>-assoc (sym (sub->> n refl))


  Wk>> : Wk >> σ ≡ Weaken {n = n} σ
  Wk>> = trans Weaken>> (cong Weaken id-l)


  Snoc>>Wk : Snoc {m = m} σ n >> Wk ≡ σ
  Snoc>>Wk = trans Snoc>>Weaken id-r


  Lift>>Weaken : Lift {m = m} {n} σ >> Weaken τ ≡ Weaken (σ >> τ)
  Lift>>Weaken = trans Snoc>>Weaken Weaken>>


  Lift>>Wk : Lift {m = m} {n} σ >> Wk ≡ Wk >> σ
  Lift>>Wk = trans Lift>>Weaken (trans (sym Wk>>) (cong (Wk >>_) id-r))


  Sing>>Weaken : Sing {m = m} n >> Weaken σ ≡ σ
  Sing>>Weaken = trans Snoc>>Weaken id-l


  Sing>>Wk : Sing {m = m} n >> Wk ≡ Id
  Sing>>Wk = trans Snoc>>Weaken id-r


  Sing>>Lift : ∀ n → Sing (sub σ n) >> Lift {m = m} {o} σ ≡ σ >> Sing n
  Sing>>Lift n = cong₂ Snoc (trans Sing>>Weaken (sym id-r)) refl


  Lift>>Lift : Lift {m = m} {n} σ >> Lift {n = o} τ ≡ Lift (σ >> τ)
  Lift>>Lift = cong₂ Snoc Lift>>Weaken refl


  Skip>>Weaken : Skip {n = n} >> Weaken σ ≡ Weaken (Weaken σ)
  Skip>>Weaken = trans Snoc>>Weaken (trans Weaken>> (cong Weaken Wk>>))


  Skip>>Lift : Skip >> Lift {m = m} {n} σ ≡ Lift (Lift σ) >> Skip
  Skip>>Lift
    = cong₂ Snoc
        (trans Skip>>Weaken
          (sym (trans Lift>>Weaken (cong Weaken (trans Snoc>>Weaken id-r)))))
      refl


  Lift-Id : Lift {m = m} Id ≡ Id
  Lift-Id = refl


  LiftSing>>Wk>>Wk : Lift {m = o} {m} (Sing n) >> (Wk >> Wk) ≡ Wk
  LiftSing>>Wk>>Wk {n = n} {m} = let open ≡-Reasoning in
    begin
      Lift (Sing n) >> (Wk >> Wk)
    ≡⟨ cong (Lift (Sing n) >>_) Wk>> ⟩
      Lift (Sing n) >> (Weaken Wk)
    ≡⟨ Lift>>Weaken ⟩
      Weaken (Sing n >> Weaken Id)
    ≡⟨ cong Weaken Sing>>Weaken ⟩
      Wk
    ∎


  LiftSing>>Skip
    : Lift {m = m} (Sing {m = m} n) >> Skip ≡ Sing {m = o} (var zero) >> Lift Wk
  LiftSing>>Skip {n = n} = cong₂ Snoc go refl
    where
      go : Lift (Sing n) >> Weaken Wk ≡ Sing (var zero) >> Weaken Wk
      go = let open ≡-Reasoning in
        begin
          Lift (Sing n) >> Weaken Wk
        ≡⟨ Lift>>Weaken ⟩
          Weaken (Sing n >> Weaken Id)
        ≡⟨ cong Weaken Sing>>Wk ⟩
          Wk
        ≡⟨ sym Sing>>Weaken ⟩
          Sing (var zero) >> Weaken Wk
        ∎


  LiftLift>>Skip : Lift (Lift {m = m} {n} σ) >> Skip ≡ Skip >> Lift σ
  LiftLift>>Skip
    = cong₂ Snoc (trans Lift>>Weaken
        (sym (trans Skip>>Weaken (cong Weaken (sym Snoc>>Wk))))) refl