------------------------------------------------------------------------
-- Parallel substitutions (defined as functions)
------------------------------------------------------------------------

open import Universe

module deBruijn.Substitution.Function.Basics
  {i u e} {Uni : Indexed-universe i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import Function using (id; _∘_; _$_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open P.≡-Reasoning

-- Substitutions, represented as functions from variables to terms.

Sub :  {t} (T : Term-like t) {Γ Δ : Ctxt}  Γ ⇨̂ Δ  Set _
Sub T = [ Var  T ]

private
 module Dummy {t} {T : Term-like t} where

  open Term-like T

  -- Interpretation of substitutions: context morphisms.

  ⟦_⟧⇨ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}  Sub T ρ̂  Γ ⇨̂ Δ
  ⟦_⟧⇨ {ρ̂ = ρ̂} _ = ρ̂

  -- Application of substitutions to types.

  infixl 8 _/I_ _/_

  _/I_ :  {Γ Δ i} {ρ̂ : Γ ⇨̂ Δ}  IType Γ i  Sub T ρ̂  IType Δ i
  σ /I ρ = σ /̂I  ρ ⟧⇨

  _/_ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}  Type Γ  Sub T ρ̂  Type Δ
  σ / ρ = σ   ρ ⟧⇨

  -- Application of substitutions to values.

  infixl 8 _/Val_

  _/Val_ :  {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} 
           Value Γ σ  Sub T ρ̂  Value Δ (σ  ρ̂)
  v /Val ρ = v /̂Val  ρ ⟧⇨

  -- Application of substitutions to context extensions.

  infixl 8 _/⁺_ _/₊_

  _/⁺_ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}  Ctxt⁺ Γ  Sub T ρ̂  Ctxt⁺ Δ
  Γ⁺ /⁺ ρ = Γ⁺ /̂⁺  ρ ⟧⇨

  _/₊_ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}  Ctxt₊ Γ  Sub T ρ̂  Ctxt₊ Δ
  Γ₊ /₊ ρ = Γ₊ /̂₊  ρ ⟧⇨

  -- Application of substitutions to variables.

  infixl 8 _/∋_ _/∋-lemma_

  _/∋_ :  {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ}  Γ  σ  (ρ : Sub T ρ̂)  Δ  σ / ρ
  x /∋ ρ = ρ · x

  _/∋-lemma_ :  {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ  σ) (ρ : Sub T ρ̂) 
               x /̂∋  ρ ⟧⇨ ≅-Value  x /∋ ρ 
  x /∋-lemma ρ = corresponds ρ x

  app∋ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}  Sub T ρ̂  [ Var  T ] ρ̂
  app∋ ρ = record
    { function    = λ _ x  x /∋       ρ
    ; corresponds = λ _ x  x /∋-lemma ρ
    }

  -- Empty substitution.

  ε⇨ :  {Δ}  Sub T ε̂[ Δ ]
  ε⇨ = record { function = λ _ (); corresponds = λ _ () }

  ε⇨[_] :  Δ  Sub T ε̂[ Δ ]
  ε⇨[ _ ] = ε⇨

  -- Extends a substitution with another term.

  private

    -- This function is not local to _▻⇨[_]_ because a proof below
    -- fails to type check if the function depends on the proof
    -- component of the substitution.

    fun :  {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} 
          (∀ {τ}  Γ  τ  Δ  τ  ρ̂) 
          (t : Δ  σ  ρ̂) 
           {τ}  Γ  σ  τ  Δ  τ  (ρ̂ ▻̂  t )
    fun f t zero    = t
    fun f t (suc x) = f x

  infixl 5 _▻⇨_ _▻⇨[_]_

  _▻⇨[_]_ :  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
            (ρ : Sub T ρ̂) σ (t : Δ  σ / ρ)  Sub T (ρ̂ ▻̂[ σ ]  t )
  _▻⇨[_]_ {Γ} {Δ} {ρ̂} ρ σ t =
    record { function = λ _  fun (_·_ ρ) t; corresponds = λ _  corr }
    where
    abstract
      corr :  {τ} (x : Γ  σ  τ) 
             x /̂∋ (ρ̂ ▻̂  t ) ≅-Value  fun (_·_ ρ) t x 
      corr zero    = P.refl
      corr (suc x) = x /∋-lemma ρ

  _▻⇨_ :  {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ}
         (ρ : Sub T ρ̂) (t : Δ  σ / ρ)  Sub T (ρ̂ ▻̂[ σ ]  t )
  ρ ▻⇨ t = ρ ▻⇨[ _ ] t

  -- The tail of a nonempty substitution.

  tail :  {Γ Δ σ} {ρ̂ : Γ  σ ⇨̂ Δ}  Sub T ρ̂  Sub T (t̂ail ρ̂)
  tail ρ = ρ [∘] weaken∋

  -- The head of a nonempty substitution.

  head :  {Γ Δ σ} {ρ̂ : Γ  σ ⇨̂ Δ} (ρ : Sub T ρ̂)  Δ  σ / tail ρ
  head ρ = zero /∋ ρ

  head-lemma :  {Γ Δ σ} {ρ̂ : Γ  σ ⇨̂ Δ} (ρ : Sub T ρ̂) 
               ĥead  ρ ⟧⇨ ≅-Value  head ρ 
  head-lemma ρ = zero /∋-lemma ρ

  -- Equality of substitutions.

  infix 4 _≅-⇨_

  _≅-⇨_ :  {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} (ρ₁ : Sub T ρ̂₁)
            {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} (ρ₂ : Sub T ρ̂₂)  Set _
  _≅-⇨_ = _≅-⟶_

  -- Certain uses of substitutivity can be removed.

  drop-subst-Sub :
     {a} {A : Set a} {x₁ x₂ : A} {Γ Δ}
    (f : A  Γ ⇨̂ Δ) {ρ} (eq : x₁  x₂) 
    P.subst  x  Sub T (f x)) eq ρ ≅-⇨ ρ
  drop-subst-Sub f P.refl = [ P.refl ]

  -- Some congruence lemmas.

  ε⇨-cong :  {Δ₁ Δ₂}  Δ₁ ≅-Ctxt Δ₂  ε⇨[ Δ₁ ] ≅-⇨ ε⇨[ Δ₂ ]
  ε⇨-cong P.refl = [ P.refl ]

  ▻⇨-cong :
     {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {t₁ : Δ₁  σ₁ / ρ₁}
      {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {t₂ : Δ₂  σ₂ / ρ₂} 
    σ₁ ≅-Type σ₂  ρ₁ ≅-⇨ ρ₂  t₁ ≅-⊢ t₂ 
    ρ₁ ▻⇨[ σ₁ ] t₁ ≅-⇨ ρ₂ ▻⇨[ σ₂ ] t₂
  ▻⇨-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] P.refl =
    [ P.refl ]

  ⟦⟧⇨-cong :  {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
               {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} 
             ρ₁ ≅-⇨ ρ₂   ρ₁ ⟧⇨ ≅-⇨̂  ρ₂ ⟧⇨
  ⟦⟧⇨-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} [ P.refl ] = P.refl

  /I-cong :
     {i}
      {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {σ₁ : IType Γ₁ i} {ρ₁ : Sub T ρ̂₁}
      {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {σ₂ : IType Γ₂ i} {ρ₂ : Sub T ρ̂₂} 
    σ₁ ≅-IType σ₂  ρ₁ ≅-⇨ ρ₂  σ₁ /I ρ₁ ≅-IType σ₂ /I ρ₂
  /I-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  /-cong :  {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
             {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} 
           σ₁ ≅-Type σ₂  ρ₁ ≅-⇨ ρ₂  σ₁ / ρ₁ ≅-Type σ₂ / ρ₂
  /-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  /⁺-cong :  {Γ₁ Δ₁ Γ⁺₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
              {Γ₂ Δ₂ Γ⁺₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} 
            Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂  ρ₁ ≅-⇨ ρ₂  Γ⁺₁ /⁺ ρ₁ ≅-Ctxt⁺ Γ⁺₂ /⁺ ρ₂
  /⁺-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  /₊-cong :  {Γ₁ Δ₁ Γ₊₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
              {Γ₂ Δ₂ Γ₊₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} 
            Γ₊₁ ≅-Ctxt₊ Γ₊₂  ρ₁ ≅-⇨ ρ₂  Γ₊₁ /₊ ρ₁ ≅-Ctxt₊ Γ₊₂ /₊ ρ₂
  /₊-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  /∋-cong :  {Γ₁ Δ₁ σ₁} {x₁ : Γ₁  σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
              {Γ₂ Δ₂ σ₂} {x₂ : Γ₂  σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} 
            x₁ ≅-∋ x₂  ρ₁ ≅-⇨ ρ₂  x₁ /∋ ρ₁ ≅-⊢ x₂ /∋ ρ₂
  /∋-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

  tail-cong :  {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁  σ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂  σ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} 
              ρ₁ ≅-⇨ ρ₂  tail ρ₁ ≅-⇨ tail ρ₂
  tail-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} [ P.refl ] = [ P.refl ]

  head-cong :  {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁  σ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂  σ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} 
              ρ₁ ≅-⇨ ρ₂  head ρ₁ ≅-⊢ head ρ₂
  head-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} [ P.refl ] = P.refl

  abstract

    -- Some eta-laws, based on the assumption of extensionality.

    -- Eta in empty contexts.

    ηε : P.Extensionality (i  u  e) (i  u  e  t) 
          {Δ} {ρ̂ : ε ⇨̂ Δ} (ρ : Sub T ρ̂)  ρ ≅-⇨ ε⇨[ Δ ]
    ηε ext ρ = extensional-equality₁ ext P.refl  ())

    -- Eta in non-empty contexts.

    η▻ : P.Extensionality (i  u  e) (i  u  e  t) 
          {Γ Δ σ} {ρ̂ : Γ  σ ⇨̂ Δ} (ρ : Sub T ρ̂) 
         ρ ≅-⇨ tail ρ ▻⇨[ σ ] head ρ
    η▻ ext {Γ} {σ = σ} {ρ̂} ρ = extensional-equality₂ ext lemma₁ lemma₂
      where
      open Term-like Var using () renaming (_≅-⊢_ to _≅-∋′_)

      lemma₁ : ρ̂ ≅-⇨̂ t̂ail ρ̂ ▻̂[ σ ]  head ρ 
      lemma₁ = begin
        [ ρ̂                   ]  ≡⟨ P.refl 
        [ t̂ail ρ̂ ▻̂ ĥead ρ̂     ]  ≡⟨ ▻̂-cong P.refl P.refl (head-lemma ρ) 
        [ t̂ail ρ̂ ▻̂  head ρ  ]  

      lemma₂′ :  {τ} (x : Γ  σ  τ) 
                x /∋ ρ ≅-⊢ x /∋ (tail ρ ▻⇨[ σ ] head ρ)
      lemma₂′ zero    = P.refl
      lemma₂′ (suc x) = P.refl

      lemma₂ :  {τ₁} {x₁ : Γ  σ  τ₁}
                 {τ₂} {x₂ : Γ  σ  τ₂} 
               x₁ ≅-∋′ x₂  x₁ /∋ ρ ≅-⊢ x₂ /∋ (tail ρ ▻⇨[ σ ] head ρ)
      lemma₂ {x₁ = x} P.refl = lemma₂′ x

    -- Two substitutions are equal if their indices are equal and
    -- their projections are pairwise equal (assuming extensionality).

    extensionality :
      P.Extensionality (i  u  e) (i  u  e  t) 
       {Γ Δ₁} {ρ̂₁ : Γ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
          {Δ₂} {ρ̂₂ : Γ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} 
      Δ₁ ≅-Ctxt Δ₂  (∀ {σ} (x : Γ  σ)  x /∋ ρ₁ ≅-⊢ x /∋ ρ₂) 
      ρ₁ ≅-⇨ ρ₂
    extensionality ext {ε} {ρ₁ = ρ₁} {ρ₂ = ρ₂} P.refl hyp =
      ρ₁  ≅-⟶⟨ ηε ext ρ₁ 
      ε⇨  ≅-⟶⟨ sym-⟶ $ ηε ext ρ₂ 
      ρ₂  ∎-⟶
    extensionality ext {Γ  σ} {ρ₁ = ρ₁} {ρ₂ = ρ₂} P.refl hyp =
      ρ₁                  ≅-⟶⟨ η▻ ext ρ₁ 
      tail ρ₁ ▻⇨ head ρ₁  ≅-⟶⟨ ▻⇨-cong P.refl
                                       (extensionality ext P.refl (hyp  suc))
                                       (hyp zero) 
      tail ρ₂ ▻⇨ head ρ₂  ≅-⟶⟨ sym-⟶ $ η▻ ext ρ₂ 
      ρ₂                  ∎-⟶

open Dummy public