{-# OPTIONS --safe #-}

module CBPV.Equality where

open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (All; _∷_; []; lookup)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product using () renaming (_×_ to _×′_; _,_ to _,′_)
open import Level using (0ℓ)
open import Relation.Binary using (Rel; _⇒_; _=[_]⇒_; Reflexive; Symmetric; Transitive; Setoid)
open import Relation.Binary.PropositionalEquality using (refl)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

open import CBPV.Axiom
open import CBPV.Family
open import CBPV.Term
open import CBPV.Type

private
  variable
    Vs Vs′ : List (Context ×′ ValType)
    Cs Cs′ : List (Context ×′ CompType)
    Γ Δ : Context
    A A′ : ValType
    B B′ : CompType

infix 0 _⨾_▹_⊢ᵛ_≈_ _⨾_▹_⊢ᶜ_≈_

data _⨾_▹_⊢ᵛ_≈_ : ∀ Vs Cs Γ {A} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A) 0ℓ
data _⨾_▹_⊢ᶜ_≈_ : ∀ Vs Cs Γ {B} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B) 0ℓ

data _⨾_▹_⊢ᵛ_≈_ where
  refl  : Reflexive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_)
  sym   : Symmetric {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_)
  trans : Transitive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_)
  axiom : (_⨾_▹⊢ᵛ_≋_ Vs Cs {A}) ⇒ (Vs ⨾ Cs ▹ [] ⊢ᵛ_≈_)
  ren   : (ρ : Γ ~[ I ]↝ᵛ Δ) → (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_) =[ renᵛ {A = A} ρ ]⇒ (Vs ⨾ Cs ▹ Δ ⊢ᵛ_≈_)
  msub  :
    {val₁ val₂ : ⌞ Vs ⌟ᵛ ⇒ᵛ δᵛ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᵛ_)}
    {comp₁ comp₂ : ⌞ Cs ⌟ᶜ ⇒ᶜ δᶜ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᶜ_)}
    {t u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} →
    (∀ {A Δ} → (m : (Δ ,′ A) ∈ Vs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᵛ val₁ m ≈ val₂ m) →
    (∀ {B Δ} → (m : (Δ ,′ B) ∈ Cs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᶜ comp₁ m ≈ comp₂ m) →
    Vs ⨾ Cs ▹ Γ ⊢ᵛ t ≈ u →
    Vs′ ⨾ Cs′ ▹ Γ ⊢ᵛ msubᵛ val₁ comp₁ t ≈ msubᵛ val₂ comp₂ u

data _⨾_▹_⊢ᶜ_≈_ where
  refl  : Reflexive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_)
  sym   : Symmetric {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_)
  trans : Transitive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_)
  axiom : (_⨾_▹⊢ᶜ_≋_ Vs Cs {B}) ⇒ (Vs ⨾ Cs ▹ [] ⊢ᶜ_≈_)
  ren   : (ρ : Γ ~[ I ]↝ᵛ Δ) → (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_) =[ renᶜ {B = B} ρ ]⇒ (Vs ⨾ Cs ▹ Δ ⊢ᶜ_≈_)
  msub  :
    {val₁ val₂ : ⌞ Vs ⌟ᵛ ⇒ᵛ δᵛ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᵛ_)}
    {comp₁ comp₂ : ⌞ Cs ⌟ᶜ ⇒ᶜ δᶜ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᶜ_)}
    {t u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} →
    (∀ {A Δ} → (m : (Δ ,′ A) ∈ Vs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᵛ val₁ m ≈ val₂ m) →
    (∀ {B Δ} → (m : (Δ ,′ B) ∈ Cs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᶜ comp₁ m ≈ comp₂ m) →
    Vs ⨾ Cs ▹ Γ ⊢ᶜ t ≈ u →
    Vs′ ⨾ Cs′ ▹ Γ ⊢ᶜ msubᶜ val₁ comp₁ t ≈ msubᶜ val₂ comp₂ u

≈ᵛ-setoid :
  (Vs : List (Context ×′ ValType)) (Cs : List (Context ×′ CompType)) (Γ : Context) (A : ValType) →
  Setoid 0ℓ 0ℓ
≈ᵛ-setoid Vs Cs Γ A = record
  { Carrier = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A
  ; _≈_ = Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_
  ; isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
  }

≈ᶜ-setoid :
  (Vs : List (Context ×′ ValType)) (Cs : List (Context ×′ CompType)) (Γ : Context) (B : CompType) →
  Setoid 0ℓ 0ℓ
≈ᶜ-setoid Vs Cs Γ B = record
  { Carrier = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B
  ; _≈_ = Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_
  ; isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
  }

module ValReasoning {Vs} {Cs} {Γ} {A} = SetoidReasoning (≈ᵛ-setoid Vs Cs Γ A)
module CompReasoning {Vs} {Cs} {Γ} {B} = SetoidReasoning (≈ᶜ-setoid Vs Cs Γ B)

-- Congruence

val-congᵛ :
  (t : ⌞ (Δ ,′ A′) ∷ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A)
  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A′} →
  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᵛ s ≈ u →
  Vs ⨾ Cs ▹ Γ ⊢ᵛ val-instᵛ s t ≈ val-instᵛ u t
val-congᵛ t s≈u =
  msub {t = t}
    (λ
      { (here refl) → s≈u
      ; (there m)   → refl
      })
    (λ m → refl)
    refl

val-congᶜ :
  (t : ⌞ (Δ ,′ A) ∷ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B)
  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A} →
  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᵛ s ≈ u →
  Vs ⨾ Cs ▹ Γ ⊢ᶜ val-instᶜ s t ≈ val-instᶜ u t
val-congᶜ t s≈u =
  msub {t = t}
    (λ
      { (here refl) → s≈u
      ; (there m)   → refl
      })
    (λ m → refl)
    refl

comp-congᵛ :
  (t : ⌞ Vs ⌟ᵛ ⨾ ⌞ (Δ ,′ B) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A)
  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B} →
  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᶜ s ≈ u →
  Vs ⨾ Cs ▹ Γ ⊢ᵛ comp-instᵛ s t ≈ comp-instᵛ u t
comp-congᵛ t s≈u =
  msub {t = t}
    (λ m → refl)
    (λ
      { (here refl) → s≈u
      ; (there m)   → refl
      })
    refl

comp-congᶜ :
  (t : ⌞ Vs ⌟ᵛ ⨾ ⌞ (Δ ,′ B′) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B)
  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B′} →
  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᶜ s ≈ u →
  Vs ⨾ Cs ▹ Γ ⊢ᶜ comp-instᶜ s t ≈ comp-instᶜ u t
comp-congᶜ t s≈u =
  msub {t = t}
    (λ m → refl)
    (λ
      { (here refl) → s≈u
      ; (there m)   → refl
      })
    refl

thmᵛ≈ :
  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A}
  (thm : Vs ⨾ Cs ▹ Γ ⊢ᵛ t ≈ s)
  (ρ : All (I Δ) Γ)
  (ζ : All (λ (Θ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᵛ A) Vs)
  (ξ : All (λ (Θ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᶜ B) Cs) →
  Vs′ ⨾ Cs′ ▹ Δ ⊢ᵛ msub′ᵛ ζ ξ (ren′ᵛ ρ t) ≈ msub′ᵛ ζ ξ (ren′ᵛ ρ s)
thmᵛ≈ thm ρ ζ ξ = msub (λ _ → refl) (λ _ → refl) (ren (lookup ρ) thm)

thmᶜ≈ :
  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B}
  (thm : Vs ⨾ Cs ▹ Γ ⊢ᶜ t ≈ s)
  (ρ : All (I Δ) Γ)
  (ζ : All (λ (Θ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᵛ A) Vs)
  (ξ : All (λ (Θ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᶜ B) Cs) →
  Vs′ ⨾ Cs′ ▹ Δ ⊢ᶜ msub′ᶜ ζ ξ (ren′ᶜ ρ t) ≈ msub′ᶜ ζ ξ (ren′ᶜ ρ s)
thmᶜ≈ thm ρ ζ ξ = msub (λ _ → refl) (λ _ → refl) (ren (lookup ρ) thm)

axᵛ≈ :
  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᵛ A}
  (ax : Vs ⨾ Cs ▹⊢ᵛ t ≋ s)
  (ζ : All (λ (Δ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A) Vs)
  (ξ : All (λ (Δ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B) Cs) →
  Vs′ ⨾ Cs′ ▹ Γ ⊢ᵛ msub′ᵛ ζ ξ (ren′ᵛ [] t) ≈ msub′ᵛ ζ ξ (ren′ᵛ [] s)
axᵛ≈ ax = thmᵛ≈ (axiom ax) []

axᶜ≈ :
  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᶜ B}
  (ax : Vs ⨾ Cs ▹⊢ᶜ t ≋ s)
  (ζ : All (λ (Δ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A) Vs)
  (ξ : All (λ (Δ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B) Cs) →
  Vs′ ⨾ Cs′ ▹ Γ ⊢ᶜ msub′ᶜ ζ ξ (ren′ᶜ [] t) ≈ msub′ᶜ ζ ξ (ren′ᶜ [] s)
axᶜ≈ ax = thmᶜ≈ (axiom ax) []