```------------------------------------------------------------------------
-- 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₊ Γ₊       ]  ∎
```