------------------------------------------------------------------------
-- Operations and lemmas related to application of substitutions
------------------------------------------------------------------------

open import Universe

module deBruijn.Substitution.Data.Application.Application1
  {i u e} {Uni : Indexed-universe i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Application.Application22
open import deBruijn.Substitution.Data.Basics
open import deBruijn.Substitution.Data.Map
open import deBruijn.Substitution.Data.Simple
open import Function using (_$_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open P.≡-Reasoning

-- More operations and lemmas related to application. In this module
-- the application operator is assumed to be homogeneous, so some
-- previously proved lemmas can be stated in a less complicated way.

record Application₁ {t} (T : Term-like t) : Set (i  u  e  t) where

  open Term-like T

  field
    -- Simple substitutions.
    simple : Simple T

    -- The homogeneous variant is defined in terms of the
    -- heterogeneous one.
    application₂₂ : Application₂₂ simple simple ([id] {T = T})

  open Simple simple public
  open Application₂₂ application₂₂ public
    hiding ( ∘⋆; ∘⋆-cong; /∋-∘⋆
           ; trans-cong; id-∘; map-trans-wk-subst; map-trans-↑; wk-∘-↑
           )

  -- Composition of multiple substitutions.
  --
  -- Note that singleton sequences are handled specially, to avoid the
  -- introduction of unnecessary identity substitutions.

  ∘⋆ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}  Subs T ρ̂  Sub T ρ̂
  ∘⋆ ε        = id
  ∘⋆ (ε   ρ) = ρ
  ∘⋆ (ρs  ρ) = ∘⋆ ρs  ρ

  -- A congruence lemma.

  ∘⋆-cong :  {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T ρ̂₁}
              {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T ρ̂₂} 
            ρs₁ ≅-⇨⋆ ρs₂  ∘⋆ ρs₁ ≅-⇨ ∘⋆ ρs₂
  ∘⋆-cong P.refl = P.refl

  abstract

    -- Applying a composed substitution to a variable is equivalent to
    -- applying all the substitutions one after another.

    /∋-∘⋆ :  {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ  σ) (ρs : Subs T ρ̂) 
            x /∋ ∘⋆ ρs ≅-⊢ var · x /⊢⋆ ρs
    /∋-∘⋆ x ε = begin
      [ x /∋ id ]  ≡⟨ /∋-id x 
      [ var · x ]  
    /∋-∘⋆ x (ε  ρ) = begin
      [ x /∋ ρ       ]  ≡⟨ P.sym $ var-/⊢ x ρ 
      [ var · x /⊢ ρ ]  
    /∋-∘⋆ x (ρs  ρ₁  ρ₂) = begin
      [ x /∋ ∘⋆ (ρs  ρ₁)  ρ₂      ]  ≡⟨ /∋-∘ x (∘⋆ (ρs  ρ₁)) ρ₂ 
      [ x /∋ ∘⋆ (ρs  ρ₁) /⊢ ρ₂     ]  ≡⟨ /⊢-cong (/∋-∘⋆ x (ρs  ρ₁)) P.refl 
      [ var · x /⊢⋆ (ρs  ρ₁) /⊢ ρ₂ ]  

    -- Yet another variant of var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆.

    ∘⋆-⇒-/⊢⋆ :
       {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρs₁ : Subs T ρ̂) (ρs₂ : Subs T ρ̂) 
      ∘⋆ ρs₁ ≅-⇨ ∘⋆ ρs₂   {σ} (t : Γ  σ)  t /⊢⋆ ρs₁ ≅-⊢ t /⊢⋆ ρs₂
    ∘⋆-⇒-/⊢⋆ ρs₁ ρs₂ hyp = var-/⊢⋆-⇒-/⊢⋆ ρs₁ ρs₂  x  begin
      [ var · x /⊢⋆ ρs₁ ]  ≡⟨ P.sym $ /∋-∘⋆ x ρs₁ 
      [ x /∋ ∘⋆ ρs₁     ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) hyp 
      [ x /∋ ∘⋆ ρs₂     ]  ≡⟨ /∋-∘⋆ x ρs₂ 
      [ var · x /⊢⋆ ρs₂ ]  )

    -- id is a left identity of _∘_.

    id-∘ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂)  id  ρ ≅-⇨ ρ
    id-∘ ρ = begin
      [ id  ρ     ]  ≡⟨ Application₂₂.id-∘ application₂₂ ρ 
      [ map [id] ρ ]  ≡⟨ map-[id] ρ 
      [ ρ          ]  

    -- The wk substitution commutes with any other (modulo lifting
    -- etc.).

    wk-∘-↑ :  {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) 
             ρ  wk {σ = σ / ρ} ≅-⇨ wk {σ = σ}  ρ 
    wk-∘-↑ σ ρ = begin
      [ ρ  wk           ]  ≡⟨ ∘-cong (P.sym $ map-[id] ρ) P.refl 
      [ map [id] ρ  wk  ]  ≡⟨ Application₂₂.wk-∘-↑ application₂₂ σ ρ 
      [ wk {σ = σ}  ρ  ]  

    -- Applying a composed substitution is equivalent to applying one
    -- substitution and then the other.

    /⊢-∘ :  {Γ Δ Ε σ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε}
           (t : Γ  σ) (ρ₁ : Sub T ρ̂₁) (ρ₂ : Sub T ρ̂₂) 
           t /⊢ ρ₁  ρ₂ ≅-⊢ t /⊢ ρ₁ /⊢ ρ₂
    /⊢-∘ t ρ₁ ρ₂ = ∘⋆-⇒-/⊢⋆ (ε  ρ₁  ρ₂) (ε  ρ₁  ρ₂) P.refl t

    -- _∘_ is associative.

    ∘-∘ :  {Γ Δ Ε Ζ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {ρ̂₃ : Ε ⇨̂ Ζ}
          (ρ₁ : Sub T ρ̂₁) (ρ₂ : Sub T ρ̂₂) (ρ₃ : Sub T ρ̂₃) 
          ρ₁  (ρ₂  ρ₃) ≅-⇨ (ρ₁  ρ₂)  ρ₃
    ∘-∘ ρ₁ ρ₂ ρ₃ = extensionality P.refl λ x  begin
      [ x /∋ ρ₁  (ρ₂  ρ₃) ]  ≡⟨ /∋-∘ x ρ₁ (ρ₂  ρ₃) 
      [ x /∋ ρ₁ /⊢ ρ₂  ρ₃  ]  ≡⟨ /⊢-∘ (x /∋ ρ₁) ρ₂ ρ₃ 
      [ x /∋ ρ₁ /⊢ ρ₂ /⊢ ρ₃ ]  ≡⟨ /⊢-cong (P.sym $ /∋-∘ x ρ₁ ρ₂) (P.refl {x = [ ρ₃ ]}) 
      [ x /∋ ρ₁  ρ₂ /⊢ ρ₃  ]  ≡⟨ P.sym $ /∋-∘ x (ρ₁  ρ₂) ρ₃ 
      [ x /∋ (ρ₁  ρ₂)  ρ₃ ]  

    -- If sub t is applied to variable zero then t is returned.

    zero-/⊢-sub :  {Γ σ} (t : Γ  σ)  var · zero /⊢ sub t ≅-⊢ t
    zero-/⊢-sub t = begin
      [ var · zero /⊢ sub t ]  ≡⟨ var-/⊢ zero (sub t) 
      [ zero /∋ sub t       ]  ≡⟨ P.refl 
      [ t                   ]  

    -- The sub substitution commutes with any other (modulo lifting
    -- etc.).

    ↑-∘-sub :  {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (t : Γ  σ) (ρ : Sub T ρ̂) 
              sub t  ρ ≅-⇨ ρ  σ  sub (t /⊢ ρ)
    ↑-∘-sub t ρ =
      let lemma = begin
            [ id  ρ                    ]  ≡⟨ id-∘ ρ 
            [ ρ                         ]  ≡⟨ P.sym $ wk-subst-∘-sub ρ (t /⊢ ρ) 
            [ wk-subst ρ  sub (t /⊢ ρ) ]  

      in begin
        [ sub t  ρ                                              ]  ≡⟨ P.refl 
        [ (id  t)  ρ                                           ]  ≡⟨ ▻-∘ id t ρ 
        [ id  ρ  t /⊢ ρ                                        ]  ≡⟨ ▻⇨-cong P.refl lemma (P.sym $ zero-/⊢-sub (t /⊢ ρ)) 
        [ wk-subst ρ  sub (t /⊢ ρ)  var · zero /⊢ sub (t /⊢ ρ) ]  ≡⟨ P.sym $ ▻-∘ (wk-subst ρ) (var · zero) (sub (t /⊢ ρ)) 
        [ (wk-subst ρ  var · zero)  sub (t /⊢ ρ)               ]  ≡⟨ ∘-cong (P.sym $ unfold-↑ ρ) P.refl 
        [ ρ   sub (t /⊢ ρ)                                     ]  

  -- wk-subst⁺ can be expressed using composition and wk⁺.

  ∘-wk⁺ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) (Δ⁺ : Ctxt⁺ Δ) 
          ρ  wk⁺ Δ⁺ ≅-⇨ wk-subst⁺ Δ⁺ ρ
  ∘-wk⁺ ρ ε = begin
    [ ρ  wk⁺ ε     ]  ≡⟨ P.refl 
    [ ρ  id        ]  ≡⟨ ∘-id ρ 
    [ ρ             ]  ≡⟨ P.refl 
    [ wk-subst⁺ ε ρ ]  
  ∘-wk⁺ ρ (Δ⁺  σ) = begin
    [ ρ  wk⁺ (Δ⁺  σ)          ]  ≡⟨ ∘-cong (P.refl {x = [ ρ ]}) (wk⁺-▻ Δ⁺) 
    [ ρ  (wk⁺ Δ⁺  wk)         ]  ≡⟨ ∘-∘ ρ (wk⁺ Δ⁺) wk 
    [ (ρ  wk⁺ Δ⁺)  wk         ]  ≡⟨ ∘-cong (∘-wk⁺ ρ Δ⁺) P.refl 
    [ wk-subst⁺ Δ⁺ ρ  wk       ]  ≡⟨ ∘-wk (wk-subst⁺ Δ⁺ ρ) 
    [ wk-subst (wk-subst⁺ Δ⁺ ρ) ]  ≡⟨ P.refl 
    [ wk-subst⁺ (Δ⁺  σ) ρ      ]  

  mutual

    -- wk-subst₊ can be expressed using composition and wk₊.

    ∘-wk₊ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) (Δ₊ : Ctxt₊ Δ) 
            ρ  wk₊ Δ₊ ≅-⇨ wk-subst₊ Δ₊ ρ
    ∘-wk₊ ρ ε = begin
      [ ρ  wk₊ ε     ]  ≡⟨ P.refl 
      [ ρ  id        ]  ≡⟨ ∘-id ρ 
      [ ρ             ]  ≡⟨ P.refl 
      [ wk-subst₊ ε ρ ]  
    ∘-wk₊ ρ (σ  Δ₊) = begin
      [ ρ  wk₊ (σ  Δ₊)          ]  ≡⟨ ∘-cong (P.refl {x = [ ρ ]}) (wk₊-◅ Δ₊) 
      [ ρ  (wk  wk₊ Δ₊)         ]  ≡⟨ ∘-∘ ρ wk (wk₊ Δ₊) 
      [ (ρ  wk)  wk₊ Δ₊         ]  ≡⟨ ∘-cong (∘-wk ρ) P.refl 
      [ wk-subst ρ  wk₊ Δ₊       ]  ≡⟨ ∘-wk₊ (wk-subst ρ) Δ₊ 
      [ wk-subst₊ Δ₊ (wk-subst ρ) ]  ≡⟨ P.refl 
      [ wk-subst₊ (σ  Δ₊) ρ      ]  

    -- Unfolding lemma for wk₊.

    wk₊-◅ :  {Γ σ} (Γ₊ : Ctxt₊ (Γ  σ)) 
            wk₊ (σ  Γ₊) ≅-⇨ wk  wk₊ Γ₊
    wk₊-◅ {σ = σ} Γ₊ = begin
      [ wk₊ (σ  Γ₊)    ]  ≡⟨ P.refl 
      [ wk-subst₊ Γ₊ wk ]  ≡⟨ P.sym $ ∘-wk₊ wk Γ₊ 
      [ wk  wk₊ Γ₊     ]  

  -- A consequence of wk₊-◅.

  /∋-wk₊-◅ :  {Γ τ σ} (x : Γ  τ) (Γ₊ : Ctxt₊ (Γ  σ)) 
             x /∋ wk₊ (σ  Γ₊) ≅-⊢ suc x /∋ wk₊ Γ₊
  /∋-wk₊-◅ {σ = σ} x Γ₊ = begin
    [ x /∋ wk₊ (σ  Γ₊)     ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) (wk₊-◅ Γ₊) 
    [ x /∋ wk  wk₊ Γ₊      ]  ≡⟨ /∋-∘ x wk (wk₊ Γ₊) 
    [ x /∋ wk /⊢ wk₊ Γ₊     ]  ≡⟨ /⊢-cong (/∋-wk x) P.refl 
    [ var · suc x /⊢ wk₊ Γ₊ ]  ≡⟨ var-/⊢ (suc x) (wk₊ Γ₊) 
    [ suc x /∋ wk₊ Γ₊       ]