{-# OPTIONS --without-K --safe #-}

module NonCumulative.Soundness.Weakening where

open import Lib

open import Data.List.Properties as Lₚ

open import NonCumulative.Statics.Ascribed.Full
open import NonCumulative.Statics.Ascribed.CtxEquiv
open import NonCumulative.Statics.Ascribed.Presup
open import NonCumulative.Statics.Ascribed.Refl
open import NonCumulative.Statics.Ascribed.PER
open import NonCumulative.Statics.Ascribed.Simpl

infix 4 _⊢w_∶_

data _⊢w_∶_ : Ctx  Subst  Ctx  Set where
  r-I : Γ ⊢s σ  I  Δ 
        ----------------
        Γ ⊢w σ  Δ
  r-p :  {i} 
        Γ ⊢w τ  (T  i)  Δ 
        Γ ⊢s σ  p τ  Δ 
        -------------------
        Γ ⊢w σ  Δ


-- A weakening is a well-formed substitution.
⊢w⇒⊢s : Γ ⊢w σ  Δ  Γ ⊢s σ  Δ
⊢w⇒⊢s (r-I ⊢σ)   = proj₁ (proj₂ (presup-s-≈ ⊢σ))
⊢w⇒⊢s (r-p _ ⊢σ) = proj₁ (proj₂ (presup-s-≈ ⊢σ))

-- A weakening's equivalent substitution is also a weakening.
s≈-resp-⊢w : Γ ⊢s σ  σ′  Δ  Γ ⊢w σ′  Δ  Γ ⊢w σ  Δ
s≈-resp-⊢w σ≈σ′ (r-I σ′≈)    = r-I (s-≈-trans σ≈σ′ σ′≈)
s≈-resp-⊢w σ≈σ′ (r-p ⊢δ σ′≈) = r-p ⊢δ (s-≈-trans σ≈σ′ σ′≈)

-- A weakenings respects context stack equivalence.
⊢w-resp-⊢≈ˡ : Γ ⊢w σ  Δ 
              Γ  Γ′ 
             --------------
             Γ′ ⊢w σ  Δ
⊢w-resp-⊢≈ˡ (r-I σ≈I) Γ≈Γ′    = r-I (ctxeq-s-≈ Γ≈Γ′ σ≈I)
⊢w-resp-⊢≈ˡ (r-p ⊢τ ≈pτ) Γ≈Γ′ = r-p (⊢w-resp-⊢≈ˡ ⊢τ Γ≈Γ′) (ctxeq-s-≈ Γ≈Γ′ ≈pτ)

⊢w-resp-⊢≈ʳ : Γ ⊢w σ  Δ 
              Δ  Δ′ 
             -------------
             Γ ⊢w σ  Δ′
⊢w-resp-⊢≈ʳ (r-I σ≈) Δ≈Δ′                       = r-I (s-≈-conv σ≈ Δ≈Δ′)
⊢w-resp-⊢≈ʳ (r-p ⊢τ ≈pτ) Δ≈Δ′
  with presup-s (⊢w⇒⊢s ⊢τ)
... | _ , ⊢∷ ⊢Δ ⊢T                              = r-p (⊢w-resp-⊢≈ʳ ⊢τ (∷-cong-simp Δ≈Δ′ (≈-refl ⊢T))) (s-≈-conv ≈pτ Δ≈Δ′)

----------------------------------------
-- Weakenings form a category.

-- Weakenings are closed under composition.
⊢w-∘ : Γ′ ⊢w σ′  Γ″ 
       Γ ⊢w σ  Γ′ 
       -----------------
       Γ ⊢w σ′  σ  Γ″
⊢w-∘ (r-I σ′≈I) ⊢σ
  with presup-s-≈ σ′≈I
...  | _ , _ , ⊢I , ⊢Γ″            = ⊢w-resp-⊢≈ʳ (s≈-resp-⊢w (s-≈-trans (∘-cong (s-≈-refl (⊢w⇒⊢s ⊢σ)) σ′≈I) (s-≈-conv (I-∘ (⊢w⇒⊢s ⊢σ)) Γ′≈Γ″))
                                                             (⊢w-resp-⊢≈ʳ ⊢σ Γ′≈Γ″))
                                                 (≈-Ctx-refl ⊢Γ″)
  where Γ′≈Γ″ = ⊢I-inv ⊢I
⊢w-∘ (r-p ⊢τ ≈pτ) ⊢σ               = r-p (⊢w-∘ ⊢τ ⊢σ)
                                         (s-≈-trans (∘-cong (s-≈-refl (⊢w⇒⊢s ⊢σ)) ≈pτ)
                                                    (∘-assoc (s-wk (proj₂ (presup-s (⊢w⇒⊢s ⊢τ)))) (⊢w⇒⊢s ⊢τ) (⊢w⇒⊢s ⊢σ)))

-- Identity is restricted.
⊢wI :  Γ  Γ ⊢w I  Γ
⊢wI ⊢Γ = r-I (I-≈ ⊢Γ)

⊢wwk :  {i}   (T  i)  Γ  (T  i)  Γ ⊢w wk  Γ
⊢wwk ⊢TΓ = r-p (⊢wI ⊢TΓ) (s-≈-sym (∘-I (s-wk ⊢TΓ)))