{-|
This module proves decidable equality for λ○▷pat
contexts, types, and variables (debruijn indices).
-}

{-# OPTIONS --safe #-}
module Pat.Context.Equality where

open import Axiom.UniquenessOfIdentityProofs using (module Decidable⇒UIP)
open import Data.Nat using (ℕ; suc; zero; _≥‴_; _≤‴_; ≤‴-refl; ≤‴-step)
open import Data.Nat.Properties using (_≟_; <-irrefl; ≤‴⇒≤; <-asym; ≡-irrelevant; _≤‴?_; ≤‴-irrelevant)
open import Function using (_∘_; _∘₂_)
open import Relation.Nullary.Decidable using (Dec; yes; no)
open import Relation.Binary.Definitions using (DecidableEquality; Irrelevant)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; subst)

open import Pat.Context

-- Injectivity of type and context constructors

[⊢]⇒-injective₁ : [ Δ ⊢ A ]⇒ B ≡ [ Δ′ ⊢ A′ ]⇒ B′ → Δ ≡ Δ′
[⊢]⇒-injective₁ refl = refl

[⊢]⇒-injective₂ : [ Δ ⊢ A ]⇒ B ≡ [ Δ′ ⊢ A′ ]⇒ B′ → A ≡ A′
[⊢]⇒-injective₂ refl = refl

[⊢]⇒-injective₃ : [ Δ ⊢ A ]⇒ B ≡ [ Δ′ ⊢ A′ ]⇒ B′ → B ≡ B′
[⊢]⇒-injective₃ refl = refl

▷-injective₁ : Γ ▷ A ≡ Γ′ ▷ A′ → Γ ≡ Γ′
▷-injective₁ refl = refl

▷-injective₂ : Γ ▷ A ≡ Γ′ ▷ A′ → A ≡ A′
▷-injective₂ refl = refl

◯-injective : ◯ A ≡ ◯ B → A ≡ B
◯-injective refl = refl

,[⊢^]-injective₁ : Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → Γ ≡ Γ′
,[⊢^]-injective₁ refl = refl

,[⊢^]-injectiveₘ : ∀ {A : Type m} {A′ : Type m′} → Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → m ≡ m′
,[⊢^]-injectiveₘ refl = refl

,[⊢^]-injective₂ : Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → Δ ≡ Δ′
,[⊢^]-injective₂ = lemma refl where
  lemma : ∀ {A : Type m} {A′ : Type m′} → (eq : m ≡ m′) → Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → subst Context eq Δ ≡ Δ′
  lemma m≡m refl = cong (λ e → subst Context e _) (≡-irrelevant m≡m refl)

,[⊢^]-injective₃ : Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → A ≡ A′
,[⊢^]-injective₃ = lemma refl where
  lemma : ∀ {A : Type m} {A′ : Type m′} → (eq : m ≡ m′) → Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → subst Type eq A ≡ A′
  lemma m≡m refl = cong (λ e → subst Type e _) (≡-irrelevant m≡m refl)

,[⊢^]-injective₄ : Γ ,[ Δ ⊢ A ^ m≥n ] ≡ Γ′ ,[ Δ′ ⊢ A′ ^ m′≥n ] → m≥n ≡ m′≥n
,[⊢^]-injective₄ _ = ≤‴-irrelevant _ _

-- | Decidable equality for types
_≟ᵗ_ : DecidableEquality (Type n)
-- | Decidable equality for contexts
_≟ᶜ_ : DecidableEquality (Context n)

([ Δ ⊢ A ]⇒ B) ≟ᵗ ([ Δ′ ⊢ A′ ]⇒ B′) with Δ ≟ᶜ Δ′ | A ≟ᵗ A′ | B ≟ᵗ B′
... | no Δ≢Δ′ | _ | _ = no (Δ≢Δ′ ∘ [⊢]⇒-injective₁)
... | yes _ | no A≢A′ | _ = no (A≢A′ ∘ [⊢]⇒-injective₂)
... | yes _ | yes _ | no B≢B′ = no (B≢B′ ∘ [⊢]⇒-injective₃)
... | yes refl | yes refl | yes refl = yes refl
(Δ ▷ A) ≟ᵗ (Δ′ ▷ A′) with Δ ≟ᶜ Δ′ | A ≟ᵗ A′
... | no Δ≢Δ′ | _ = no (Δ≢Δ′ ∘ ▷-injective₁)
... | yes _ | no A≢A′ = no (A≢A′ ∘ ▷-injective₂)
... | yes refl | yes refl = yes refl
`Bool ≟ᵗ `Bool = yes refl
◯ A ≟ᵗ ◯ B with A ≟ᵗ B
... | yes A≡B = yes (cong ◯ A≡B)
... | no A≢B = no (A≢B ∘ ◯-injective)
([ Δ ⊢ A ]⇒ B) ≟ᵗ `Bool = no (λ ())
([ Δ ⊢ A ]⇒ B) ≟ᵗ (Δ′ ▷ A′) = no (λ ())
([ Δ ⊢ A ]⇒ B) ≟ᵗ ◯ _ = no (λ ())
(Δ ▷ A) ≟ᵗ ([ Δ′ ⊢ A′ ]⇒ B) = no (λ ())
(Δ ▷ A) ≟ᵗ ◯ A′ = no (λ ())
(Δ ▷ A) ≟ᵗ `Bool = no (λ ())
`Bool ≟ᵗ ([ Δ ⊢ A ]⇒ B) = no (λ ())
`Bool ≟ᵗ (Δ ▷ A) = no (λ ())
`Bool ≟ᵗ ◯ B = no (λ ())
◯ A ≟ᵗ ([ Δ ⊢ A′ ]⇒ B) = no (λ ())
◯ A ≟ᵗ (Δ ▷ A′) = no (λ ())
◯ A ≟ᵗ `Bool = no (λ ())

∅ ≟ᶜ ∅ = yes refl 
(_,[_^_] {m = m} Γ (Δ ⊢ A) m≥n) ≟ᶜ (_,[_^_] {m = m′} Γ′ (Δ′ ⊢ A′) m′≥n) with Γ ≟ᶜ Γ′ | m ≟ m′
... | no Γ≢Γ′ | _ = no (Γ≢Γ′ ∘ ,[⊢^]-injective₁)
... | yes _ | no m≢m′ = no (m≢m′ ∘ ,[⊢^]-injectiveₘ)
... | yes refl | yes refl with Δ ≟ᶜ  Δ′ | A ≟ᵗ A′
...   | no Δ≢Δ′ | _ = no (Δ≢Δ′ ∘ ,[⊢^]-injective₂)
...   | yes _ | no A≢A′ = no (A≢A′ ∘ ,[⊢^]-injective₃)
...   | yes refl | yes refl with refl ← ≤‴-irrelevant m≥n m′≥n = yes refl
(Γ₁ ++ Γ₂) ≟ᶜ (Γ′₁ ++ Γ′₂) with Γ₁ ≟ᶜ Γ′₁ | Γ₂ ≟ᶜ Γ′₂
... | no Γ₁≢Γ′₁ | _ = no (Γ₁≢Γ′₁ ∘ λ { refl → refl })
... | yes _ | no Γ₂≢Γ′₂ = no (Γ₂≢Γ′₂ ∘ λ { refl → refl })
... | yes refl | yes refl = yes refl
∅ ≟ᶜ (Γ′ ,[ _ ⊢ _ ^ _ ]) = no (λ ())
∅ ≟ᶜ (Γ₁ ++ Γ₂) = no (λ ())
(Γ ,[ _ ⊢ _ ^ _ ]) ≟ᶜ ∅ =  no (λ ())
(Γ ,[ _ ⊢ _ ^ _ ]) ≟ᶜ (Γ′₁ ++ Γ′₂) = no (λ ())
(Γ₁ ++ Γ₂) ≟ᶜ (Γ′ ,[ _ ⊢ _ ^ _ ]) = no (λ ())
(Γ₁ ++ Γ₂) ≟ᶜ ∅ = no (λ ())

-- | ≤‴ has irrelevant equality
≡≤‴-irrelevant : Irrelevant {A = m ≥‴ n} _≡_
≡≤‴-irrelevant = Decidable⇒UIP.≡-irrelevant (yes ∘₂ ≤‴-irrelevant)

-- | Context has irrelevant equality
≡ᶜ-irrelevant : Irrelevant {A = Context n} _≡_
≡ᶜ-irrelevant = Decidable⇒UIP.≡-irrelevant (_≟ᶜ_)

-- | Type has irrelevant equality
≡ᵗ-irrelevant : Irrelevant {A = Type n} _≡_
≡ᵗ-irrelevant = Decidable⇒UIP.≡-irrelevant (_≟ᵗ_)

-- | Decidable equality for variables
_≟ˣ_ : DecidableEquality (Γ ∋[ Δ ⊢ A ^ m≥n ])
Z ≟ˣ y = lemma refl refl refl refl y where
  subst₄ : (eq : m ≡ m′) (eq₁ : subst Context eq Δ ≡ Δ′) (eq₂ : subst Type eq A ≡ A′) (eq₃ : subst (_≥‴ n) eq m≥n ≡ m′≥n)
         → Γ ,[ Δ ⊢ A ^ m≥n ] ∋[ Δ ⊢ A ^ m≥n ] → Γ ,[ Δ ⊢ A ^ m≥n ] ∋[ Δ′ ⊢ A′ ^ m′≥n ]
  subst₄ refl refl refl refl y = y
  cong₃ : ∀ {ℓ} {A B C D : Set ℓ} {x₁ x₂ y₁ y₂ z₁ z₂} (f : A → B → C → D) → x₁ ≡ x₂ → y₁ ≡ y₂ → z₁ ≡ z₂ → f x₁ y₁ z₁ ≡ f x₂ y₂ z₂
  cong₃ f refl refl refl = refl
  lemma : (eq : m ≡ m′) (eq₁ : subst Context eq Δ ≡ Δ′) (eq₂ : subst Type eq A ≡ A′) (eq₃ : subst (_≥‴ n) eq m≥n ≡ m′≥n)
        → (y : Γ ,[ Δ ⊢ A ^ m≥n ] ∋[ Δ′ ⊢ A′ ^ m′≥n ]) → Dec (subst₄ eq eq₁ eq₂ eq₃ Z ≡ y)
  lemma eq eq₁ eq₂ eq₃ Z
    rewrite ≡-irrelevant eq refl
    rewrite ≡ᶜ-irrelevant eq₁ refl | ≡ᵗ-irrelevant eq₂ refl | ≡≤‴-irrelevant eq₃ refl = yes refl
  lemma refl refl refl refl (S y) = no λ ()
S x ≟ˣ Z = no (λ ())
S x ≟ˣ S y with x ≟ˣ y
... | yes refl = yes refl
... | no x≢y = no (λ { refl → x≢y refl })
L x ≟ˣ L y with x ≟ˣ y
... | yes refl = yes refl
... | no x≢y = no (λ { refl → x≢y refl })
R x ≟ˣ R y with x ≟ˣ y
... | yes refl = yes refl
... | no x≢y = no (λ { refl → x≢y refl })
L x ≟ˣ R y = no (λ ())
R x ≟ˣ L y = no (λ ())