module univTypes.SubjectReduction.Inversion where

open import Data.Product renaming (_,_ to ⟨_,_⟩)
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.SubjectReduction.ConversionProperties using (≈-refl; ≈-trans; ≈-sym; ≈-sub)

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

-- Inversion for lambda terms

↪-∀-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} →
  ∀[x⦂ t₁ ] t₂ ↪ t → 
  ∃[ t₁' ] ∃[ t₂' ] t ≡ ∀[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂')
↪-∀-shape (ξ-∀₁ ↪₁) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-step ↪₁ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
↪-∀-shape (ξ-∀₂ ↪₂) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-step ↪₂ ↪*-refl ⟩ ⟩ ⟩ ⟩

↪*-∀-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} →
  (∀[x⦂ t₁ ] t₂) ↪* t → 
  ∃[ t₁' ] ∃[ t₂' ] t ≡ ∀[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂')
↪*-∀-shape ↪*-refl = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
↪*-∀-shape (↪*-step ∀↪z z↪*t) with ↪-∀-shape ∀↪z
... | ⟨ x₁ , ⟨ x₂ , ⟨ refl , ⟨ t₁↪*x₁ , t₂↪*x₂ ⟩ ⟩ ⟩ ⟩ with ↪*-∀-shape z↪*t 
... | ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ x₁↪*y₁ , x₂↪*y₂ ⟩ ⟩ ⟩ ⟩ 
    = ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ ↪*-trans t₁↪*x₁ x₁↪*y₁ , ↪*-trans t₂↪*x₂ x₂↪*y₂ ⟩ ⟩ ⟩ ⟩

invert-≈-∀ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} →
  (∀[x⦂ t₁ ] t₂) ≈ (∀[x⦂ t₁' ] t₂') →
  t₁ ≈ t₁' × t₂ ≈ t₂'
invert-≈-∀ (mk-≈ x ∀₁↪*x ∀₂↪*x) with ↪*-∀-shape ∀₁↪*x | ↪*-∀-shape ∀₂↪*x
... | ⟨ a₁ , ⟨ a₂ , ⟨ refl , ⟨ t₁↪*a₁ , t₂↪*a₁ ⟩ ⟩ ⟩ ⟩ 
    | ⟨ b₁ , ⟨ b₂ , ⟨ refl , ⟨ t₁'↪*b₁ , t₂'↪*b₂ ⟩ ⟩ ⟩ ⟩ 
    = ⟨ mk-≈ a₁ t₁↪*a₁ t₁'↪*b₁ , mk-≈ a₂ t₂↪*a₁ t₂'↪*b₂ ⟩

invert-⊢λ' : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t : Term n} →
  Γ ⊢ `λ e ⦂ t →
  ∃[ t₁ ] ∃[ t₂ ]
    t ≈ (∀[x⦂ t₁ ] t₂) ×
    Γ ⊢ t₁ ⦂ `Set ×
    Γ , t₁ ⊢ e ⦂ t₂
invert-⊢λ' (⊢-λ ⊢λ ⊢e) = ⟨ _ , ⟨ _ , ⟨ ≈-refl , ⟨ ⊢λ , ⊢e ⟩ ⟩ ⟩ ⟩
invert-⊢λ' (⊢-≈ t₁≈t ⊢λ⦂t₁) with invert-⊢λ' ⊢λ⦂t₁
... | ⟨ X , ⟨ E , ⟨ t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩
    = ⟨ X , ⟨ E , ⟨ ≈-trans (≈-sym t₁≈t) t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩

invert-⊢λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ : Term n} {t₂ : Term (suc n)}
  → Γ ⊢ `λ e ⦂ ∀[x⦂ t₁ ] t₂
  → ∃[ t₁' ] ∃[ t₂' ]
      t₁ ≈ t₁' ×
      t₂ ≈ t₂' ×
      Γ ⊢ t₁' ⦂ `Set ×
      Γ , t₁' ⊢ e ⦂ t₂'
invert-⊢λ (⊢-λ ⊢λ ⊢λ₁) = ⟨ _ , ⟨ _ , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ ⊢λ , ⊢λ₁ ⟩ ⟩ ⟩ ⟩ ⟩
invert-⊢λ (⊢-≈ t≈∀ ⊢λ) with invert-⊢λ' ⊢λ 
... | ⟨ X , ⟨ E , ⟨ t≈∀' , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ with invert-≈-∀ (≈-trans (≈-sym t≈∀) t≈∀')
... | ⟨ ≈₁ , ≈₂ ⟩ 
    = ⟨ X , ⟨ E , ⟨ ≈₁ , ⟨ ≈₂ , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ ⟩


-- Inversion for pairs

↪-∃-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} →
  ∃[x⦂ t₁ ] t₂ ↪ t → 
  ∃[ t₁' ] ∃[ t₂' ] t ≡ ∃[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂')
↪-∃-shape (ξ-∃₁ ↪₁) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-step ↪₁ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
↪-∃-shape (ξ-∃₂ ↪₂) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-step ↪₂ ↪*-refl ⟩ ⟩ ⟩ ⟩

↪*-∃-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} →
  (∃[x⦂ t₁ ] t₂) ↪* t → 
  ∃[ t₁' ] ∃[ t₂' ] t ≡ ∃[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂')
↪*-∃-shape ↪*-refl = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
↪*-∃-shape (↪*-step ∀↪z z↪*t) with ↪-∃-shape ∀↪z
... | ⟨ x₁ , ⟨ x₂ , ⟨ refl , ⟨ t₁↪*x₁ , t₂↪*x₂ ⟩ ⟩ ⟩ ⟩ with ↪*-∃-shape z↪*t 
... | ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ x₁↪*y₁ , x₂↪*y₂ ⟩ ⟩ ⟩ ⟩ 
    = ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ ↪*-trans t₁↪*x₁ x₁↪*y₁ , ↪*-trans t₂↪*x₂ x₂↪*y₂ ⟩ ⟩ ⟩ ⟩

invert-≈-∃ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} →
  (∃[x⦂ t₁ ] t₂) ≈ (∃[x⦂ t₁' ] t₂') →
  t₁ ≈ t₁' × t₂ ≈ t₂'
invert-≈-∃ (mk-≈ x ∃₁↪*x ∃₂↪*x) with ↪*-∃-shape ∃₁↪*x | ↪*-∃-shape ∃₂↪*x
... | ⟨ a₁ , ⟨ a₂ , ⟨ refl , ⟨ t₁↪*a₁ , t₂↪*a₁ ⟩ ⟩ ⟩ ⟩ 
    | ⟨ b₁ , ⟨ b₂ , ⟨ refl , ⟨ t₁'↪*b₁ , t₂'↪*b₂ ⟩ ⟩ ⟩ ⟩ 
    = ⟨ mk-≈ a₁ t₁↪*a₁ t₁'↪*b₁ , mk-≈ a₂ t₂↪*a₁ t₂'↪*b₂ ⟩

invert-⊢,' : ∀ {n} {Γ : Context n} {l r t : Term n} →
  Γ ⊢ l `, r ⦂ t →
  ∃[ t₁ ] ∃[ t₂ ]
    t ≈ (∃[x⦂ t₁ ] t₂) ×
    Γ ⊢ l ⦂ t₁ ×
    Γ ⊢ r ⦂ t₂ [ l ]
invert-⊢,' (⊢-≈ t₁≈t ⊢lr) with invert-⊢,' ⊢lr 
... | ⟨ x₁ , ⟨ x₂ , ⟨ t≈∃ , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ 
  = ⟨ x₁ , ⟨ x₂ , ⟨ ≈-sym (≈-trans (≈-sym t≈∃) t₁≈t) , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ 
invert-⊢,' (⊢-, {n} {Γ} {e₁} {e₂} {t₁} {t₂} ⊢l ⊢r) = ⟨ t₁ , ⟨ t₂ , ⟨  ≈-refl , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩

invert-⊢, : ∀ {n} {Γ : Context n} {l r : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
  → Γ ⊢ l `, r ⦂ ∃[x⦂ t₁ ] t₂
  → ∃[ t₁' ] ∃[ t₂' ]
      t₁ ≈ t₁' ×
      t₂ ≈ t₂' ×
      Γ ⊢ l ⦂ t₁ ×
      Γ ⊢ r ⦂ t₂ [ l ]
invert-⊢, (⊢-≈ t≈∃ ⊢lr) with invert-⊢,' ⊢lr
... | ⟨ x₁ , ⟨ x₂ , ⟨ t≈∃' , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ with invert-≈-∃ (≈-trans (≈-sym t≈∃) t≈∃')
... | ⟨ ≈₁ , ≈₂ ⟩
  = ⟨ x₁ , ⟨ x₂ , ⟨ ≈₁ , ⟨ ≈₂ , ⟨ ⊢-≈ (≈-sym ≈₁) ⊢l , ⊢-≈ (≈-sub _ (≈-sym ≈₂)) ⊢r ⟩ ⟩ ⟩ ⟩ ⟩
invert-⊢, (⊢-, ⊢l ⊢r) 
  = ⟨ _ , ⟨ _ , ⟨ ≈-refl , ⟨ ≈-refl , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ ⟩

↪-≡-shape : ∀ {n} {t u₁ u₂ : Term n} → 
  u₁ `≡ u₂ ↪ t → 
  ∃[ u₁' ] ∃[ u₂' ] t ≡ u₁' `≡ u₂' × (u₁ ↪* u₁') × (u₂ ↪* u₂')
↪-≡-shape (ξ-≡₁ ↪₁) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-step ↪₁ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
↪-≡-shape (ξ-≡₂ ↪₂) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-step ↪₂ ↪*-refl ⟩ ⟩ ⟩ ⟩

↪*-≡-shape : ∀ {n} {t u₁ u₂ : Term n} →
  (u₁ `≡ u₂) ↪* t → 
  ∃[ u₁' ] ∃[ u₂' ] t ≡ u₁' `≡ u₂' × (u₁ ↪* u₁') × (u₂ ↪* u₂')
↪*-≡-shape ↪*-refl = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
↪*-≡-shape (↪*-step ≡↪x x↪*t) with ↪-≡-shape ≡↪x
... | ⟨ a , ⟨ b , ⟨ refl , ⟨  u₁↪*a , u₂↪*b ⟩ ⟩ ⟩ ⟩ with ↪*-≡-shape x↪*t
... | ⟨ x , ⟨ y , ⟨ refl , ⟨  a↪*x , b↪*y ⟩ ⟩ ⟩ ⟩
    = ⟨ x , ⟨ y , ⟨ refl , ⟨ ↪*-trans u₁↪*a a↪*x , ↪*-trans u₂↪*b b↪*y ⟩ ⟩ ⟩ ⟩

invert-≈-≡ : ∀ {n} {u₁ u₁' u₂ u₂' : Term n} →
  (u₁ `≡ u₂) ≈ (u₁' `≡ u₂') →
  u₁ ≈ u₁' × u₂ ≈ u₂'
invert-≈-≡ (mk-≈ x ≡↪*x ≡'↪*x) with ↪*-≡-shape ≡↪*x
... | ⟨ a , ⟨ b , ⟨ refl , ⟨  u₁↪*a , u₂↪*b ⟩ ⟩ ⟩ ⟩ with ↪*-≡-shape ≡'↪*x
... | ⟨ _ , ⟨ _ , ⟨ refl , ⟨  u₁'↪*a , u₂'↪*b ⟩ ⟩ ⟩ ⟩
    = ⟨ mk-≈ a u₁↪*a u₁'↪*a , mk-≈ b u₂↪*b u₂'↪*b ⟩

invert-⊢refl' : ∀ {n} {Γ : Context n} {t : Term n}
  → Γ ⊢ `refl ⦂ t
  → ∃[ u₁ ] ∃[ u₂ ]
    t ≈ u₁ `≡ u₂ ×
    u₁ ≈ u₂
invert-⊢refl' (⊢-≈ t₁≈t ⊢refl) with invert-⊢refl' ⊢refl 
... | ⟨ u₁ , ⟨ u₂ , ⟨ t₁≈≡ ,  u₁≈u₂ ⟩ ⟩ ⟩  
    = ⟨ _ , ⟨ _ , ⟨ ≈-trans (≈-sym t₁≈t) t₁≈≡ , u₁≈u₂ ⟩ ⟩ ⟩ 
invert-⊢refl' (⊢-refl ⊢refl) = ⟨ _ , ⟨ _ , ⟨ ≈-refl , ≈-refl ⟩ ⟩ ⟩

invert-⊢refl : ∀ {n} {Γ : Context n} {u₁ u₂ : Term n}
  → Γ ⊢ `refl ⦂ u₁ `≡ u₂
  → u₁ ≈ u₂
invert-⊢refl (⊢-refl ⊢refl) = ≈-refl
invert-⊢refl (⊢-≈ t≈≡ ⊢refl) with invert-⊢refl' ⊢refl
... | ⟨ u₁' , ⟨ u₂' ,  ⟨ t≈≡' , ≈' ⟩ ⟩ ⟩ with invert-≈-≡ (≈-trans (≈-sym t≈≡') t≈≡)
... | ⟨ ≈₁ , ≈₂ ⟩ 
    = ≈-trans (≈-trans (≈-sym ≈₁) ≈') ≈₂