module univTypes.SubjectReduction.Composition where

open import Data.Product
open import Data.Sum
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning)
open import Data.Fin using (zero; suc) renaming (Fin to 𝔽)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥; ⊥-elim)

open import univTypes.SubjectReduction.Specification
open import univTypes.Util.Fin

--------------------------------------------------------------------------------

-- Composition of two renamings

_∘ᵣᵣ_ : ∀ {n₁ n₂ n₃} → Ren n₂ n₃ → Ren n₁ n₂ → Ren n₁ n₃
(ρ₁ ∘ᵣᵣ ρ₂) x = ρ₁ (ρ₂ x)

ext-dist-∘ᵣᵣ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (ρ₂ : Ren n₁ n₂)
  → extᵣ (ρ₁ ∘ᵣᵣ ρ₂) ≡ (extᵣ ρ₁) ∘ᵣᵣ (extᵣ ρ₂)
ext-dist-∘ᵣᵣ ρ₁ ρ₂ = fun-ext eq
  where
    eq : ∀ {n₁ n₂ n₃} {ρ₁ : Ren n₂ n₃} {ρ₂ : Ren n₁ n₂}
      → (x : Fin (suc n₁)) → extᵣ (ρ₁ ∘ᵣᵣ ρ₂) x ≡ (extᵣ ρ₁ ∘ᵣᵣ extᵣ ρ₂) x
    eq zero = refl
    eq (suc x) = refl


fusion-∘ᵣᵣ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (ρ₂ : Ren n₁ n₂) (e : Term n₁)
  → ren ρ₁ (ren ρ₂ e) ≡ ren (ρ₁ ∘ᵣᵣ ρ₂) e
fusion-∘ᵣᵣ ρ₁ ρ₂ (` x) = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ `Set = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ `refl = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ (∀[x⦂ x ] e) 
  rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ x | (fusion-∘ᵣᵣ (extᵣ ρ₁) (extᵣ ρ₂) e) | ext-dist-∘ᵣᵣ ρ₁ ρ₂ = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ (l · r) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ l | fusion-∘ᵣᵣ ρ₁ ρ₂ r = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ (`λ e) rewrite fusion-∘ᵣᵣ (extᵣ ρ₁) (extᵣ ρ₂) e | ext-dist-∘ᵣᵣ ρ₁ ρ₂ = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ (∃[x⦂ x ] e) 
  rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ x | fusion-∘ᵣᵣ (extᵣ ρ₁) (extᵣ ρ₂) e | ext-dist-∘ᵣᵣ ρ₁ ρ₂ = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ (l `, r) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ l | fusion-∘ᵣᵣ ρ₁ ρ₂ r = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ (`proj₁ e) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ e = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ (`proj₂ e) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ e = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ (l `≡ r) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ l | fusion-∘ᵣᵣ ρ₁ ρ₂ r = refl
fusion-∘ᵣᵣ ρ₁ ρ₂ (`subst t e₁ e₂) 
  rewrite fusion-∘ᵣᵣ (extᵣ ρ₁) (extᵣ ρ₂) t | fusion-∘ᵣᵣ ρ₁ ρ₂ e₁ | fusion-∘ᵣᵣ ρ₁ ρ₂ e₂ | ext-dist-∘ᵣᵣ ρ₁ ρ₂
    = refl

wk-extᵣ : ∀ {m n} (ρ : Ren m n)
  → wk ∘ᵣᵣ ρ ≡ extᵣ ρ ∘ᵣᵣ wk
wk-extᵣ ρ = refl
open import Relation.Binary.PropositionalEquality using (trans)
wk-extᵣ-fusion : ∀ {m n} (ρ : Ren m n) (e : Term m)
  → ren wk (ren ρ e) ≡ ren (extᵣ ρ) (ren wk e)
wk-extᵣ-fusion ρ e = trans (fusion-∘ᵣᵣ wk ρ e) (trans (cong (λ x → ren x e ) (wk-extᵣ ρ))  (sym (fusion-∘ᵣᵣ (extᵣ ρ) wk e)))

--------------------------------------------------------------------------------

-- Composition of a substitution and a renaming

_∘ₛᵣ_ : ∀ {n₁ n₂ n₃} → Sub n₂ n₃ → Ren n₁ n₂ → Sub n₁ n₃
(σ₁ ∘ₛᵣ ρ₂) x = σ₁ (ρ₂ x)

ext-dist-∘ₛᵣ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (ρ₂ : Ren n₁ n₂)
  → extₛ (σ₁ ∘ₛᵣ ρ₂) ≡ (extₛ σ₁) ∘ₛᵣ (extᵣ ρ₂)
ext-dist-∘ₛᵣ _ _ = fun-ext λ{zero → refl; (suc x) → refl }

fusion-∘ₛᵣ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (ρ₂ : Ren n₁ n₂) (e : Term n₁)
  → sub σ₁ (ren ρ₂ e) ≡ sub (σ₁ ∘ₛᵣ ρ₂) e
fusion-∘ₛᵣ σ ρ (` x)                                                            = refl
fusion-∘ₛᵣ σ ρ `Set                                                             = refl
fusion-∘ₛᵣ σ ρ `refl = refl
fusion-∘ₛᵣ σ ρ (`λ e) rewrite fusion-∘ₛᵣ (extₛ σ) (extᵣ ρ) e | ext-dist-∘ₛᵣ σ ρ = refl
fusion-∘ₛᵣ σ ρ (l · r) rewrite fusion-∘ₛᵣ σ ρ l |  fusion-∘ₛᵣ σ ρ r             = refl
fusion-∘ₛᵣ σ ρ (∀[x⦂ x ] e) rewrite fusion-∘ₛᵣ σ ρ x 
                                  | fusion-∘ₛᵣ (extₛ σ) (extᵣ ρ) e 
                                  | ext-dist-∘ₛᵣ σ ρ                            = refl
fusion-∘ₛᵣ σ ρ (∃[x⦂ x ] e) rewrite fusion-∘ₛᵣ σ ρ x 
                                  | fusion-∘ₛᵣ (extₛ σ) (extᵣ ρ) e 
                                  | ext-dist-∘ₛᵣ σ ρ                            = refl
fusion-∘ₛᵣ σ ρ (l `, r) rewrite fusion-∘ₛᵣ σ ρ l |  fusion-∘ₛᵣ σ ρ r            = refl
fusion-∘ₛᵣ σ ρ (l `≡ r) rewrite fusion-∘ₛᵣ σ ρ l |  fusion-∘ₛᵣ σ ρ r            = refl
fusion-∘ₛᵣ σ ρ (`proj₁ e) rewrite fusion-∘ₛᵣ σ ρ e = refl
fusion-∘ₛᵣ σ ρ (`proj₂ e) rewrite fusion-∘ₛᵣ σ ρ e = refl
fusion-∘ₛᵣ σ ρ (`subst t e₁ e₂) 
  rewrite fusion-∘ₛᵣ (extₛ σ) (extᵣ ρ) t  | fusion-∘ₛᵣ σ ρ e₁
        | fusion-∘ₛᵣ σ ρ e₂               | ext-dist-∘ₛᵣ σ ρ
                                                                                = refl
--------------------------------------------------------------------------------

-- Composition of a renaming and a substitution

_∘ᵣₛ_ : ∀ {n₁ n₂ n₃} → Ren n₂ n₃ → Sub n₁ n₂ → Sub n₁ n₃
(ρ₁ ∘ᵣₛ σ₂) x = ren ρ₁ (σ₂ x)

suc' : ∀ {n} → (x : Fin n) → Fin (suc n)
suc' x = suc x

fun-ext-aux₁ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (σ₂ : Sub n₁ n₂) (x : Fin (suc n₁))

  → extₛ (ρ₁ ∘ᵣₛ σ₂) x ≡ (extᵣ ρ₁ ∘ᵣₛ extₛ σ₂) x
fun-ext-aux₁ ρ σ zero = refl
fun-ext-aux₁ ρ σ (suc x) = 
                  extₛ (ρ ∘ᵣₛ σ) (suc x)
                    ≡⟨ refl  ⟩
                  ren suc' (ren ρ (σ x))
                    ≡⟨ fusion-∘ᵣᵣ suc' ρ (σ x)  ⟩
                  ren (suc' ∘ᵣᵣ ρ) (σ x)
                    ≡⟨ refl  ⟩
                  ren (extᵣ ρ ∘ᵣᵣ suc') (σ x)
                    ≡⟨ sym (fusion-∘ᵣᵣ (extᵣ ρ) suc' (σ x))  ⟩
                  ren (extᵣ ρ) (ren suc' (σ x))
                    ≡⟨ refl  ⟩
                  ((extᵣ ρ ∘ᵣₛ extₛ σ) (suc x)) ∎
  where open ≡-Reasoning

ext-dist-∘ᵣₛ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (σ₂ : Sub n₁ n₂)
  → extₛ (ρ₁ ∘ᵣₛ σ₂) ≡ (extᵣ ρ₁) ∘ᵣₛ (extₛ σ₂)
ext-dist-∘ᵣₛ ρ σ = fun-ext (fun-ext-aux₁ ρ σ) 

fusion-∘ᵣₛ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (σ₂ : Sub n₁ n₂) (e : Term n₁)
  → ren ρ₁ (sub σ₂ e) ≡ sub (ρ₁ ∘ᵣₛ σ₂) e
fusion-∘ᵣₛ ρ σ (` x)                                          = refl
fusion-∘ᵣₛ ρ σ `Set                                           = refl
fusion-∘ᵣₛ ρ σ `refl = refl
fusion-∘ᵣₛ ρ σ (`λ e) rewrite fusion-∘ᵣₛ (extᵣ ρ) (extₛ σ) e 
                            | ext-dist-∘ᵣₛ ρ σ                = refl
fusion-∘ᵣₛ ρ σ (l · r) rewrite fusion-∘ᵣₛ ρ σ l
                            | fusion-∘ᵣₛ ρ σ r                = refl
fusion-∘ᵣₛ ρ σ (∀[x⦂ x ] e) rewrite fusion-∘ᵣₛ ρ σ x
                            | fusion-∘ᵣₛ (extᵣ ρ) (extₛ σ) e
                            |  ext-dist-∘ᵣₛ ρ σ               = refl
fusion-∘ᵣₛ ρ σ (∃[x⦂ x ] e) rewrite fusion-∘ᵣₛ ρ σ x
                            | fusion-∘ᵣₛ (extᵣ ρ) (extₛ σ) e
                            |  ext-dist-∘ᵣₛ ρ σ               = refl
fusion-∘ᵣₛ ρ σ (l `, r) rewrite fusion-∘ᵣₛ ρ σ l
                            | fusion-∘ᵣₛ ρ σ r                = refl
fusion-∘ᵣₛ ρ σ (l `≡ r) rewrite fusion-∘ᵣₛ ρ σ l
                            | fusion-∘ᵣₛ ρ σ r                = refl
fusion-∘ᵣₛ ρ σ (`proj₁ e) rewrite fusion-∘ᵣₛ ρ σ e = refl
fusion-∘ᵣₛ ρ σ (`proj₂ e) rewrite fusion-∘ᵣₛ ρ σ e = refl
fusion-∘ᵣₛ ρ σ (`subst t e₁ e₂) rewrite fusion-∘ᵣₛ (extᵣ ρ) (extₛ σ) t 
                            | fusion-∘ᵣₛ ρ σ e₁ | fusion-∘ᵣₛ ρ σ e₂
                            |  ext-dist-∘ᵣₛ ρ σ               = refl

wk-extₛ : ∀ {m n} (σ : Sub m n)
  → wk ∘ᵣₛ σ ≡ extₛ σ ∘ₛᵣ wk
wk-extₛ σ = refl

wk-extₛ-fusion : ∀ {m n} (σ : Sub m n) (e : Term m)
  → ren wk (sub σ e) ≡ sub (extₛ σ) (ren wk e)
wk-extₛ-fusion σ e = trans (fusion-∘ᵣₛ wk σ e) (trans (cong (λ x → sub x e) (wk-extₛ σ)) (sym (fusion-∘ₛᵣ (extₛ σ) wk e))) 
--------------------------------------------------------------------------------

-- Composition of two substitutions

_∘ₛₛ_ : ∀ {n₁ n₂ n₃} → Sub n₂ n₃ → Sub n₁ n₂ → Sub n₁ n₃
(σ₁ ∘ₛₛ σ₂) x = sub σ₁ (σ₂ x)


fun-ext-aux₂ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (σ₂ : Sub n₁ n₂) (x : Fin (suc n₁)) 
  → extₛ (σ₁ ∘ₛₛ σ₂) x ≡ (extₛ σ₁ ∘ₛₛ extₛ σ₂) x
fun-ext-aux₂ _ _ zero = refl
fun-ext-aux₂ σ₁ σ₂ (suc x) = 
                ren suc' (sub σ₁ (σ₂ x))
                  ≡⟨ fusion-∘ᵣₛ suc' σ₁ (σ₂ x) ⟩
                sub (suc' ∘ᵣₛ σ₁) (σ₂ x)
                  ≡⟨ sym (fusion-∘ᵣₛ suc'  σ₁ (σ₂ x)) ⟩
                ren wk (sub σ₁ (σ₂ x))
                  ≡⟨ wk-extₛ-fusion σ₁ (σ₂ x) ⟩
                sub (extₛ σ₁) (ren wk (σ₂ x)) ≡⟨ refl ⟩
                (sub (extₛ σ₁) (ren suc' (σ₂ x))) ∎ 
  where open ≡-Reasoning

ext-dist-∘ₛₛ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (σ₂ : Sub n₁ n₂)
  → extₛ (σ₁ ∘ₛₛ σ₂) ≡ (extₛ σ₁) ∘ₛₛ (extₛ σ₂)
ext-dist-∘ₛₛ σ₁ σ₂ = fun-ext  (fun-ext-aux₂ σ₁ σ₂)

fusion-∘ₛₛ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (σ₂ : Sub n₁ n₂) (e : Term n₁)
  → sub σ₁ (sub σ₂ e) ≡ sub (σ₁ ∘ₛₛ σ₂) e
fusion-∘ₛₛ σ₁ σ₂ (` x) = refl
fusion-∘ₛₛ σ₁ σ₂ `Set = refl
fusion-∘ₛₛ σ₁ σ₂ `refl = refl
fusion-∘ₛₛ σ₁ σ₂ (`λ e) rewrite fusion-∘ₛₛ (extₛ σ₁) (extₛ σ₂) e | ext-dist-∘ₛₛ σ₁ σ₂ = refl
fusion-∘ₛₛ σ₁ σ₂ (l · r) rewrite fusion-∘ₛₛ σ₁ σ₂ l | fusion-∘ₛₛ σ₁ σ₂ r = refl
fusion-∘ₛₛ σ₁ σ₂ (l `≡ r) rewrite fusion-∘ₛₛ σ₁ σ₂ l | fusion-∘ₛₛ σ₁ σ₂ r = refl
fusion-∘ₛₛ σ₁ σ₂ (l `, r) rewrite fusion-∘ₛₛ σ₁ σ₂ l | fusion-∘ₛₛ σ₁ σ₂ r = refl
fusion-∘ₛₛ σ₁ σ₂ (∀[x⦂ x ] t) rewrite fusion-∘ₛₛ σ₁ σ₂ x | fusion-∘ₛₛ (extₛ σ₁) (extₛ σ₂) t | ext-dist-∘ₛₛ σ₁ σ₂ = refl
fusion-∘ₛₛ σ₁ σ₂ (∃[x⦂ x ] t) rewrite fusion-∘ₛₛ σ₁ σ₂ x | fusion-∘ₛₛ (extₛ σ₁) (extₛ σ₂) t | ext-dist-∘ₛₛ σ₁ σ₂ = refl
fusion-∘ₛₛ σ₁ σ₂ (`proj₁ e) rewrite fusion-∘ₛₛ σ₁ σ₂ e = refl
fusion-∘ₛₛ σ₁ σ₂ (`proj₂ e) rewrite fusion-∘ₛₛ σ₁ σ₂ e = refl
fusion-∘ₛₛ σ₁ σ₂ (`subst t e₁ e₂) rewrite fusion-∘ₛₛ (extₛ σ₁) (extₛ σ₂) t 
                                          | fusion-∘ₛₛ σ₁ σ₂ e₁
                                          | fusion-∘ₛₛ σ₁ σ₂ e₂
                                          | ext-dist-∘ₛₛ σ₁ σ₂ = refl

-----{!   !}--------------------------------------------------------------------------

-- Identity substitution does nothing

idₛ : ∀ {n} → Sub n n
idₛ x = ` x

extₛ-idₛ : ∀ {n} →
  extₛ (idₛ {n}) ≡ idₛ {suc n}
extₛ-idₛ {n} = fun-ext λ{zero → refl; (suc x) → refl}

sub-id : ∀ {n} (e : Term n)
  → sub idₛ e ≡ e
sub-id (` x) = refl
sub-id `Set = refl
sub-id `refl = refl
sub-id (`λ e) = cong (λ a → `λ a) (trans (cong (λ a → sub a e) extₛ-idₛ) (sub-id e))
sub-id (`proj₁ e) = cong (λ a → `proj₁ a) (trans (cong (λ a → sub a e) refl) (sub-id e))
sub-id (`proj₂ e) = cong (λ a → `proj₂ a) (trans (cong (λ a → sub a e) refl) (sub-id e))
sub-id (l · r) rewrite sub-id l | sub-id r = refl
sub-id (l `≡ r) rewrite sub-id l | sub-id r = refl
sub-id (l `, r) rewrite sub-id l | sub-id r = refl
sub-id (∀[x⦂ x ] e) rewrite sub-id x = cong (λ a → ∀[x⦂ x ] a) (trans (cong (λ a → sub a e) extₛ-idₛ) (sub-id e))
sub-id (∃[x⦂ x ] e) rewrite sub-id x = cong (λ a → ∃[x⦂ x ] a) (trans (cong (λ a → sub a e) extₛ-idₛ) (sub-id e))
sub-id (`subst t e₁ e₂) rewrite sub-id e₁ | sub-id e₂ 
                                     = cong (λ a → `subst a e₁ e₂) (trans (cong (λ a → sub a t) extₛ-idₛ) (sub-id t))

--------------------------------------------------------------------------------

-- Weakening cancels singleton-substitution

wk-0↦ : ∀ {n} (e : Term n)
  → 0↦ e ∘ₛᵣ wk ≡ idₛ
wk-0↦ e = refl

wk-0↦-fusion : ∀ {n} (e : Term n) (e' : Term n)
  → sub (0↦ e) (ren wk e') ≡ e'
wk-0↦-fusion e e' = trans (fusion-∘ₛᵣ (0↦ e) wk e') (trans (cong (λ a → sub a e') (wk-0↦  e)) (sub-id e')) 

--------------------------------------------------------------------------------

-- Swap singleton-substitution with renaming

swap-0↦-extᵣ : ∀ {m n} (ρ : Ren m n) (e : Term m)
  → (0↦ (ren ρ e)) ∘ₛᵣ (extᵣ ρ)  ≡ ρ ∘ᵣₛ (0↦ e)
swap-0↦-extᵣ ρ e = fun-ext λ{zero → refl; (suc x) → refl}

swap-0↦-extᵣ-fusion : ∀ {m n} (ρ : Ren m n) (e : Term m) (e' : Term (suc m)) 
  → sub (0↦ (ren ρ e)) (ren (extᵣ ρ) e') ≡ ren ρ (sub (0↦ e) e')
swap-0↦-extᵣ-fusion ρ e e' = trans          (fusion-∘ₛᵣ (0↦ (ren ρ e)) (extᵣ ρ) e') 
                                    (trans  (cong (λ a → sub a e') (swap-0↦-extᵣ ρ e))
                                            (sym (fusion-∘ᵣₛ ρ (0↦  e) e')))

-- Swap singleton-substitution with substitution

fun-ext-aux₃ : ∀ {m n} (σ : Sub m n) (e : Term m) (x : _)
  → ((0↦ (sub σ e)) ∘ₛₛ (extₛ σ)) x  ≡ (σ ∘ₛₛ (0↦ e)) x 
fun-ext-aux₃ σ e zero = refl
fun-ext-aux₃ σ e (suc x) = 
                sub (0↦ (sub σ e)) (ren suc' (σ x)) 
                  ≡⟨ cong (sub (0↦ (sub σ e))) (sym (sub-id (ren suc' (σ x)))) ⟩ 
                sub (0↦ (sub σ e)) (sub idₛ (ren suc' (σ x))) 
                  ≡⟨ fusion-∘ₛₛ (0↦ (sub σ e)) idₛ (ren suc' (σ x)) ⟩ 
                sub (0↦ (sub σ e) ∘ₛₛ idₛ) (ren suc' (σ x))
                  ≡⟨ refl ⟩ 
                sub (0↦ (sub σ e)) (ren suc' (σ x))
                  ≡⟨ fusion-∘ₛᵣ (0↦ (sub σ e)) suc' (σ x) ⟩
                sub ((0↦ (sub σ e)) ∘ₛᵣ suc') (σ x)
                  ≡⟨ refl ⟩ 
                sub idₛ (σ x)
                  ≡⟨ sub-id _ ⟩ 
                (σ x) ∎
  where open ≡-Reasoning

swap-0↦-extₛ : ∀ {m n} (σ : Sub m n) (e : Term m)
  → (0↦ (sub σ e)) ∘ₛₛ (extₛ σ)  ≡ σ ∘ₛₛ (0↦ e)
swap-0↦-extₛ σ e = fun-ext (fun-ext-aux₃ σ e)

swap-0↦-extₛ-fusion : ∀ {m n} (σ : Sub m n) (e : Term m) (e' : Term (suc m)) 
  → sub (0↦ (sub σ e)) (sub (extₛ σ) e') ≡ sub σ (sub (0↦ e) e')
swap-0↦-extₛ-fusion σ e e' = 
                      sub (0↦ (sub σ e)) (sub (extₛ σ) e')   
                        ≡⟨ fusion-∘ₛₛ (0↦ (sub σ e)) (extₛ σ) e' ⟩
                      sub (0↦ (sub σ e) ∘ₛₛ extₛ σ) e'
                        ≡⟨ cong (λ a → sub a e') (swap-0↦-extₛ σ e) ⟩
                      sub (σ ∘ₛₛ 0↦ e) e' 
                        ≡⟨ sym (fusion-∘ₛₛ σ (0↦ e) e') ⟩
                      sub σ (sub (0↦ e) e') ∎ 
  where open ≡-Reasoning