------------------------------------------------------------------------
-- The two definitions of context extensions are isomorphic
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Context.Extension.Isomorphic
  {i u e} (Uni : IndexedUniverse i u e) where

import deBruijn.Context.Basics          as Basics
import deBruijn.Context.Extension.Left  as Left
import deBruijn.Context.Extension.Right as Right
open import Function.Base
open import Function.Inverse using (_↔_)
import Relation.Binary.PropositionalEquality as P

open Basics Uni
open Left   Uni
open Right  Uni
open P.≡-Reasoning

-- Ctxt₊-s can be turned into Ctxt⁺-s.

₊-to-⁺ : ∀ {Γ} → Ctxt₊ Γ → Ctxt⁺ Γ
₊-to-⁺ ε        = ε
₊-to-⁺ (σ ◅ Γ₊) = ε ▻ σ ⁺++⁺ ₊-to-⁺ Γ₊

abstract

  -- The semantics is preserved.

  ++⁺-₊-to-⁺ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Γ ++₊ Γ₊ ≅-Ctxt Γ ++⁺ ₊-to-⁺ Γ₊
  ++⁺-₊-to-⁺     ε        = P.refl
  ++⁺-₊-to-⁺ {Γ} (σ ◅ Γ₊) = begin
    Γ ▻ σ ++₊ Γ₊                  ≡⟨ ++⁺-₊-to-⁺ Γ₊ ⟩
    Γ ▻ σ ++⁺ ₊-to-⁺ Γ₊           ≡⟨ ++⁺-++⁺ (ε ▻ σ) (₊-to-⁺ Γ₊) ⟩
    Γ ++⁺ (ε ▻ σ ⁺++⁺ ₊-to-⁺ Γ₊)  ∎

mutual

  -- Ctxt⁺-s can be turned into Ctxt₊-s.

  ⁺-to-₊ : ∀ {Γ} → Ctxt⁺ Γ → Ctxt₊ Γ
  ⁺-to-₊ ε        = ε
  ⁺-to-₊ (Γ⁺ ▻ σ) =
    ⁺-to-₊ Γ⁺ ₊++₊ P.subst Ctxt₊ (++₊-⁺-to-₊ Γ⁺) (σ ◅ ε)

  abstract

    -- The semantics is preserved.

    ++₊-⁺-to-₊ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Γ ++⁺ Γ⁺ ≅-Ctxt Γ ++₊ ⁺-to-₊ Γ⁺
    ++₊-⁺-to-₊     ε        = P.refl
    ++₊-⁺-to-₊ {Γ} (Γ⁺ ▻ σ) =
      let σ◅ε = P.subst Ctxt₊ (++₊-⁺-to-₊ Γ⁺) (σ ◅ ε)

      in begin
      Γ ++⁺ Γ⁺ ▻ σ                ≡⟨ P.refl ⟩
      Γ ++⁺ Γ⁺ ++₊ (σ ◅ ε)        ≡⟨ P.sym $ ++₊-cong $ drop-subst-Ctxt₊ id (++₊-⁺-to-₊ Γ⁺) ⟩
      Γ ++₊ ⁺-to-₊ Γ⁺ ++₊ σ◅ε     ≡⟨ ++₊-++₊ (⁺-to-₊ Γ⁺) σ◅ε ⟩
      Γ ++₊ (⁺-to-₊ Γ⁺ ₊++₊ σ◅ε)  ∎

-- Some congruence lemmas.

₊-to-⁺-cong : ∀ {Γ₁} {Γ₊₁ : Ctxt₊ Γ₁}
                {Γ₂} {Γ₊₂ : Ctxt₊ Γ₂} →
              Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ₊-to-⁺ Γ₊₁ ≅-Ctxt⁺ ₊-to-⁺ Γ₊₂
₊-to-⁺-cong P.refl = P.refl

⁺-to-₊-cong : ∀ {Γ₁} {Γ⁺₁ : Ctxt⁺ Γ₁}
                {Γ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} →
              Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ⁺-to-₊ Γ⁺₁ ≅-Ctxt₊ ⁺-to-₊ Γ⁺₂
⁺-to-₊-cong P.refl = P.refl

-- Ctxt⁺ and Ctxt₊ are isomorphic.

Ctxt⁺↔Ctxt₊ : ∀ Γ → Ctxt⁺ Γ ↔ Ctxt₊ Γ
Ctxt⁺↔Ctxt₊ Γ = record
  { to         = P.→-to-⟶ ⁺-to-₊
  ; from       = P.→-to-⟶ ₊-to-⁺
  ; inverse-of = record
    { left-inverse-of  = λ Γ⁺ → ≅-Ctxt⁺-⇒-≡ $ ₊-to-⁺-⁺-to-₊ Γ⁺
    ; right-inverse-of = λ Γ₊ → ≅-Ctxt₊-⇒-≡ $ ⁺-to-₊-₊-to-⁺ Γ₊
    }
  }
  where
  abstract
    ₊-to-⁺-⁺-to-₊ : (Γ⁺ : Ctxt⁺ Γ) → ₊-to-⁺ (⁺-to-₊ Γ⁺) ≅-Ctxt⁺ Γ⁺
    ₊-to-⁺-⁺-to-₊ Γ⁺ = cancel-++⁺-left _ _ (begin
      Γ ++⁺ ₊-to-⁺ (⁺-to-₊ Γ⁺)  ≡⟨ P.sym $ ++⁺-₊-to-⁺ (⁺-to-₊ Γ⁺) ⟩
      Γ ++₊ (⁺-to-₊ Γ⁺)         ≡⟨ P.sym $ ++₊-⁺-to-₊ Γ⁺ ⟩
      Γ ++⁺ Γ⁺                  ∎)

    ⁺-to-₊-₊-to-⁺ : (Γ₊ : Ctxt₊ Γ) → ⁺-to-₊ (₊-to-⁺ Γ₊) ≅-Ctxt₊ Γ₊
    ⁺-to-₊-₊-to-⁺ Γ₊ = cancel-++₊-left _ _ (begin
      Γ ++₊ ⁺-to-₊ (₊-to-⁺ Γ₊)  ≡⟨ P.sym $ ++₊-⁺-to-₊ (₊-to-⁺ Γ₊) ⟩
      Γ ++⁺ (₊-to-⁺ Γ₊)         ≡⟨ P.sym $ ++⁺-₊-to-⁺ Γ₊ ⟩
      Γ ++₊ Γ₊                  ∎)