open import Data.Product
open import Data.Sum
open import Data.List.Membership.Propositional
open import Relation.Binary.PropositionalEquality as PEq
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.Construct.Closure.Equivalence as Eq
open import Relation.Binary.Construct.Union
open import Relation.Binary
open import Data.List.Relation.Binary.Pointwise as Pw
open import Data.List
open import Data.Empty
open import Relation.Nullary
import Relation.Binary.Reasoning.Preorder as PreR
open import Data.List.Relation.Unary.Any as Any
open import Data.List.Relation.Binary.Subset.Propositional.Properties

open import Stoughton.Var

module SubjectReduction {𝒞 𝒱 : Set} (isVar : Enum 𝒱) (𝒜 : 𝒞 → 𝒞 → Set) (ℛ : 𝒞 → 𝒞 → 𝒞 → Set) where

  private
    _≟_ = Enum._≟_ isVar

  open import Stoughton.Chi (Enum.encode isVar) (Enum.decode isVar) (Enum.inverse isVar)
  open import Stoughton.Alpha 𝒞 isVar
  open import Stoughton.Syntax 𝒞 𝒱 _≟_
  open import Stoughton.Substitution 𝒞 isVar
  open import Stoughton.SubstitutionLemmas 𝒞 isVar
  
  open import Beta 𝒞 isVar
  open import BetaReduction 𝒞 isVar
  open import BetaConversion 𝒞 isVar
  open import Context 𝒱 Λ _≟_
  open import Context.Properties 𝒞 isVar
  open import ChurchRosser 𝒞 isVar
  open import PTSs isVar 𝒜 ℛ
  open import PTSs.Metatheory isVar 𝒜 ℛ
  open import CxtClosure 𝒞 isVar _▹β_ as OneStepBeta using ()

  open import ParallelReduction 𝒞 isVar
  open import ParallelReduction.Properties 𝒞 isVar  
  open import InjectivityProducts 𝒞 isVar

  open OneStepBeta.PreservesFreshness βpreserves# using (∉→C-)

  infix  _→β₌_
  _→β₌_ : Λ → Λ → Set
  _→β₌_ = _≡_ ∪ _→β_

  infix  _→→β₌_
  _→→β₌_ : Cxt → Cxt → Set
  _→→β₌_ = Pointwise (λ (x , A) (y , B) → x ≡ y × A →β₌ B)

  oneStepCxtRefl : Reflexive _→→β₌_
  oneStepCxtRefl {[]} = []
  oneStepCxtRefl {(x , A) ∷ Γ} = (PEq.refl , inj₁ PEq.refl) ∷ oneStepCxtRefl {Γ}

  dom→→β₌ : ∀ {y Γ Δ} → y ∉ dom Δ → Γ →→β₌ Δ → y ∉ dom Γ
  dom→→β₌ y∉Γ′ [] = λ ()
  dom→→β₌ {y} y∉Γ′,x (_∷_ {(x , _)} {(.x , _)} (refl , _) Γ∼Γ′) with y ≟ x
  dom→→β₌ {y} y∉Γ′,y (_∷_ {(.y , _)} {(.y , _)} (refl , _) Γ∼Γ′) | yes refl = ⊥-elim (y∉Γ′,y (here PEq.refl))
  dom→→β₌ {y} y∉Γ′,x (_∷_ {(x , A)} _ Γ∼Γ′) | no y≢x = ∉≢, y≢x (dom→→β₌ (lemma∉‚ y∉Γ′,x) Γ∼Γ′)

  dom←←β₌ : ∀ {y Γ Δ} → y ∉ dom Γ → Γ →→β₌ Δ → y ∉ dom Δ
  dom←←β₌ y∉Γ′ [] = λ ()
  dom←←β₌ {y} y∉Γ′,x (_∷_ {(x , _)} {(.x , _)} (refl , _) Γ∼Γ′) with y ≟ x
  dom←←β₌ {y} y∉Γ′,y (_∷_ {(.y , _)} {(.y , _)} (refl , _) Γ∼Γ′) | yes refl = ⊥-elim (y∉Γ′,y (here PEq.refl))
  dom←←β₌ {y} y∉Γ′,x (_∷_ {(x , A)} _ Γ∼Γ′) | no y≢x = ∉≢, y≢x (dom←←β₌ (lemma∉‚ y∉Γ′,x) Γ∼Γ′)
  
  declRedCxt : ∀ {x A Γ Δ} → Γ →→β₌ Δ → (x , A) ∈ Γ → ∃ λ B → (x , B) ∈ Δ × A →β₌ B
  declRedCxt {x} {A} (_∷_ .{(x , A)} {(.x , B)} (refl , A→₌B) _) (here refl) = B , here PEq.refl , A→₌B
  declRedCxt (_∷_ (refl , _) Γ∼Δ) (there x∈Γ) with declRedCxt Γ∼Δ x∈Γ
  ... | B , x,B∈Γ' , A→₌B  = B , there x,B∈Γ' , A→₌B

  convContainsPar : _⇉_ ⇒ _≃β_
  convContainsPar M⇉N = rednInConv (manyStepBetaContainsPar M⇉N)

  mutual
    cxtRed : ∀ {Γ Δ} → Γ okₛ → Γ →→β₌ Δ → Δ okₛ
    cxtRed ⊢nil [] = ⊢nil
    cxtRed (⊢cons Γok x∉domΓ Γ⊢A:s) (_∷_ {(x , A)} {(.x , B)} (refl , A→₌B) Γ→Δ) =
      ⊢cons (cxtRed Γok Γ→Δ) (dom←←β₌ x∉domΓ Γ→Δ) (subRed Γ⊢A:s Γ→Δ A→₌B)  

    subRed : ∀ {Γ Δ M N A} → Γ ⊢ₛ M ∶ A → Γ →→β₌ Δ → M →β₌ N → Δ ⊢ₛ N ∶ A
    subRed (⊢var {_} {A} Γok x,A∈Γ) Γ→Δ (inj₁ refl) with declRedCxt Γ→Δ x,A∈Γ | cxtRed Γok Γ→Δ
    ... | .A , x,A∈Δ , inj₁ refl | Δok = ⊢var Δok x,A∈Δ
    ... | B , x,B∈Δ , inj₂ A→B | Δok = ⊢conv (⊢var Δok x,B∈Δ) (inj₂ (inj₂ A→B) ◅ ε) (proj₂ (lemma Γok Δok x,A∈Γ Γ→Δ))
      where
      lemma : ∀ {Γ Δ x A} → Γ okₛ → Δ okₛ → (x , A) ∈ Γ → Γ →→β₌ Δ → ∃ λ s → Δ ⊢ₛ A ∶ c s
      lemma ⊢nil _ ()
      lemma (⊢cons {.Γ'} {.x} {s} {.A} _ _ Γ'⊢A:s) Δ',x:Bok (here refl) (_∷_ {(x , A)} {(.x , B)} {Γ'} {Δ'} (refl , _) Γ'→Δ') =
        s , thinning (xs⊆x∷xs Δ' (x , B)) Δ',x:Bok (subRed Γ'⊢A:s Γ'→Δ' (inj₁ PEq.refl))
      lemma (⊢cons Γok _ _) Δ,y:Bok@(⊢cons {Δ} {y} {_} {B} Δok y∉Δ Δ⊢C:𝒰) (there x,A∈Γ) (_∷_ (refl , _) Γ→Δ) with lemma Γok Δok x,A∈Γ Γ→Δ
      ... | s , Δ⊢A:s = s , thinning (xs⊆x∷xs Δ (y , B)) Δ,y:Bok Δ⊢A:s
    subRed (⊢var _ _) Γ→Δ (inj₂ (→cxt ()))
    subRed (⊢sort Γok As₁s₂) Γ→Δ (inj₁ refl) = ⊢sort (cxtRed Γok Γ→Δ) As₁s₂
    subRed (⊢sort _ _) Γ→Δ (inj₂ (→cxt ()))
    subRed (⊢prod Rs₁s₂s₃ Γ⊢A:s₁ z∉fvB-y Γ,z:A⊢B[y=z]:s₂) Γ→Δ (inj₁ refl) =
      ⊢prod
        Rs₁s₂s₃
        (subRed Γ⊢A:s₁ Γ→Δ (inj₁ PEq.refl))
        z∉fvB-y
        (subRed Γ,z:A⊢B[y=z]:s₂ ((PEq.refl , inj₁ PEq.refl) ∷ Γ→Δ) (inj₁ PEq.refl))        
    subRed (⊢prod Rs₁s₂s₃ Γ⊢A:s₁ z∉fvB-y Γ,z:A⊢B[y=z]:s₂) Γ→Δ (inj₂ (→ΠL A→A')) =
      ⊢prod Rs₁s₂s₃ (subRed Γ⊢A:s₁ Γ→Δ (inj₂ A→A')) z∉fvB-y (subRed Γ,z:A⊢B[y=z]:s₂ ((PEq.refl , inj₂ A→A') ∷ Γ→Δ) (inj₁ PEq.refl))
    subRed {Γ} {Δ} (⊢prod {y} {z} {s₁} {s₂} {s₃} {A} {B} Rs₁s₂s₃ Γ⊢A:s₁ z∉fvB-y Γ,z:A⊢B[y=z]:s₂) Γ→Δ (inj₂ (→ΠR {_} {_} {_} {B'} B→B')) =
      ⊢prod Rs₁s₂s₃ (subRed Γ⊢A:s₁ Γ→Δ (inj₁ PEq.refl)) z∉fvB'-y goal
      where
      z∉fvB'-y : z ∉ fv B' - y
      z∉fvB'-y = ∉→C- z∉fvB-y B→B'
      goal : Δ ‚ z ∶ A ⊢ₛ B' [ y := v z ] ∶ c s₂
      goal with compatRedSub {σ = ι ‚ y := v z} B→B'
      ... | C , B[y=z]→C , C∼B'[y=z] =
        closAlpha C∼B'[y=z] (subRed Γ,z:A⊢B[y=z]:s₂ ((PEq.refl , inj₁ PEq.refl) ∷ Γ→Δ) (inj₂ B[y=z]→C))
    subRed (⊢abs ℛs₁s₂₃ z∉fvM-x z∉fvB-y Γ⊢A:s₁ Γ,z:A⊢M[x=z]:B[y=z] Γ,z:A⊢B[y=z]:s₂) Γ→Δ (inj₁ refl) = 
      ⊢abs ℛs₁s₂₃ z∉fvM-x z∉fvB-y
           (subRed Γ⊢A:s₁ Γ→Δ (inj₁ PEq.refl))
           (subRed Γ,z:A⊢M[x=z]:B[y=z] ((PEq.refl , inj₁ PEq.refl) ∷ Γ→Δ) (inj₁ PEq.refl))
           (subRed Γ,z:A⊢B[y=z]:s₂ ((PEq.refl , inj₁ PEq.refl) ∷ Γ→Δ) (inj₁ PEq.refl))
    subRed (⊢abs ℛs₁s₂₃ z∉fvM-x z∉fvB-y Γ⊢A:s₁ Γ,z:A⊢M[x=z]:B[y=z] Γ,z:A⊢B[y=z]:s₂) Γ→Δ (inj₂ (→λL A→A')) =
      ⊢conv (⊢abs ℛs₁s₂₃ z∉fvM-x z∉fvB-y
                  (subRed Γ⊢A:s₁ Γ→Δ (inj₂ A→A'))
                  (subRed Γ,z:A⊢M[x=z]:B[y=z] ((PEq.refl , inj₂ A→A') ∷ Γ→Δ) (inj₁ PEq.refl))
                  (subRed Γ,z:A⊢B[y=z]:s₂ ((PEq.refl , inj₂ A→A') ∷ Γ→Δ) (inj₁ PEq.refl)))
            (inj₂ (inj₂ (→ΠL A→A')) ◅ ε)
            (⊢prod ℛs₁s₂₃
                   (subRed Γ⊢A:s₁ Γ→Δ (inj₁ PEq.refl))
                   z∉fvB-y
                   (subRed Γ,z:A⊢B[y=z]:s₂ ((PEq.refl , inj₁ PEq.refl) ∷ Γ→Δ) (inj₁ PEq.refl))) 
    subRed {Γ} {Δ} (⊢abs {x} {y} {z} {s} {A = A} {B} ℛs₁s₂₃ z∉fvM-x z∉fvB-y Γ⊢A:s₁ Γ,z:A⊢M[x=z]:B[y=z] Γ,z:A⊢B[y=z]:s₂) Γ→Δ
      (inj₂ (→λR {M' = M'} M→M')) =
      ⊢abs ℛs₁s₂₃ z∉fvM'-x z∉fvB-y
           (subRed Γ⊢A:s₁ Γ→Δ (inj₁ PEq.refl))
           goal
           (subRed Γ,z:A⊢B[y=z]:s₂ ((PEq.refl , inj₁ PEq.refl) ∷ Γ→Δ) (inj₁ PEq.refl))
      where
      z∉fvM'-x : z ∉ fv M' - x
      z∉fvM'-x = ∉→C- z∉fvM-x M→M'    
      goal : Δ ‚ z ∶ A ⊢ₛ M' [ x := v z ] ∶ B [ y := v z ]
      goal with compatRedSub {σ = ι ‚ x := v z} M→M'
      ... | N , M[x=z]→N , N∼M'[x=z] =
        closAlpha N∼M'[x=z] (subRed Γ,z:A⊢M[x=z]:B[y=z] ((PEq.refl , inj₁ PEq.refl) ∷ Γ→Δ) (inj₂ M[x=z]→N))
    subRed (⊢app Γ⊢M:Π[y:A]B Γ⊢N:A) Γ→Δ (inj₁ refl) = ⊢app (subRed Γ⊢M:Π[y:A]B Γ→Δ (inj₁ PEq.refl)) (subRed Γ⊢N:A Γ→Δ (inj₁ PEq.refl))
    subRed (⊢app Γ⊢M:Π[y:A]B Γ⊢N:A) Γ→Δ (inj₂ (→·L M→M')) = ⊢app (subRed Γ⊢M:Π[y:A]B Γ→Δ (inj₂ M→M')) (subRed Γ⊢N:A Γ→Δ (inj₁ PEq.refl))
    subRed {Γ} {Δ} (⊢app {x} {M} {N} {A} {B} Γ⊢M:Π[x:A]B Γ⊢N:A) Γ→Δ (inj₂ (→·R {_} {N'} N→N'))
      with (subRed Γ⊢M:Π[x:A]B Γ→Δ (inj₁ PEq.refl))
    ... | Δ⊢M:Π[x:A]B with syntacticValidity Δ⊢M:Π[x:A]B
    ... | _ , inj₁ ()
    ... | s' , inj₂ Δ⊢Π[x:A]B:s' with genProd Δ⊢Π[x:A]B:s'
    ... | s₁ , s₂ , s₃ , y , Rs₁s₂s₃ , Δ⊢A:s₁ , y∉fvB-x , Δ,y:A⊢B[x=y]:s₂ , _ =
      ⊢conv (⊢app Δ⊢M:Π[x:A]B Δ⊢N':A) B[x=N']≃B[x=N] Δ⊢B[x=N]:s₂
      where
      Δ⊢N':A : Δ ⊢ₛ N' ∶ A
      Δ⊢N':A = subRed Γ⊢N:A Γ→Δ (inj₂ N→N')
      Δ⊢B[x=y][y=N']:s₂ : Δ ⊢ₛ B [ x := v y ] [ y := N' ] ∶ c s₂
      Δ⊢B[x=y][y=N']:s₂ = cut Δ,y:A⊢B[x=y]:s₂ Δ⊢N':A 
      Δ⊢B[x=N']:s₂ : Δ ⊢ₛ B [ x := N' ] ∶ c s₂
      Δ⊢B[x=N']:s₂ = subst (λ C → Δ ⊢ₛ C ∶ c s₂) (sym (composRenUpd {x} {y} {B} y∉fvB-x)) Δ⊢B[x=y][y=N']:s₂
      Δ⊢N:A : Δ ⊢ₛ N ∶ A
      Δ⊢N:A = subRed Γ⊢N:A Γ→Δ (inj₁ PEq.refl)
      Δ⊢B[x=y][y=N]:s₂ : Δ ⊢ₛ B [ x := v y ] [ y := N ] ∶ c s₂
      Δ⊢B[x=y][y=N]:s₂ = cut Δ,y:A⊢B[x=y]:s₂ Δ⊢N:A 
      Δ⊢B[x=N]:s₂ : Δ ⊢ₛ B [ x := N ] ∶ c s₂
      Δ⊢B[x=N]:s₂ = subst (λ C → Δ ⊢ₛ C ∶ c s₂) (sym (composRenUpd {x} {y} {B} y∉fvB-x)) Δ⊢B[x=y][y=N]:s₂    
      N⇉N' : N ⇉ N'
      N⇉N' = parContainsOneStep N→N'
      B[x=N]⇉C×C∼B[x=N']  : ∃ λ C → B [ x := N ] ⇉ C × C ∼α B [ x := N' ]
      B[x=N]⇉C×C∼B[x=N'] = compatParSub {B} ⇉ρ (lemma⇉ₛ≺+ x {σ = ι} N⇉N' lemma⇉ₛρ)
      B[x=N]≃B[x=N'] : B [ x := N ] ≃β B [ x := N' ]
      B[x=N]≃B[x=N'] with B[x=N]⇉C×C∼B[x=N']
      ... | _ , B[x=N]⇉C , C∼B[x=N'] = Eq.transitive (_∼α_ ∪ _→β_) (convContainsPar B[x=N]⇉C) (inj₁ (inj₁ C∼B[x=N']) ◅ ε)
      B[x=N']≃B[x=N] : B [ x := N' ] ≃β B [ x := N ] 
      B[x=N']≃B[x=N] = Eq.symmetric (_∼α_ ∪ _→β_) B[x=N]≃B[x=N']
    ---------------------------------------------------------------------------------------------
    --  (possibly) the most complex case, i.e., when M is a redex and it is being contracted:  --
    ---------------------------------------------------------------------------------------------   
    subRed {Γ} {Δ} .{(λ[ x ∶ A₁ ] M₁) · M₂} .{M₁ [ x := M₂ ]}
      (⊢app {y} {A = B₁} {B₂} Γ⊢λ[x:A₁]M₁:Π[y:B₁]B₂ Γ⊢M₂:B₁) Γ→Δ (inj₂ (→cxt (β {x} {M₁} {M₂} {A₁}))) 
      with subRed Γ⊢λ[x:A₁]M₁:Π[y:B₁]B₂ Γ→Δ (inj₁ PEq.refl) | subRed Γ⊢M₂:B₁ Γ→Δ (inj₁ PEq.refl) ------------------------------------> (1)
    ... | Δ⊢λ[x:A₁]M₁:Π[y:B₁]B₂ | Δ⊢M₂:B₁ with genLam Δ⊢λ[x:A₁]M₁:Π[y:B₁]B₂ ---------------------------------------------------------> (2)
    ... | s₁ , s₂ , _ , y' , z , B₂' , _ , z∉fvM₁-x , z∉fvB₂'-y' , Δ⊢A₁:s₁ , Δ,z:A₁⊢M₁[x=z]:B₂'[y'=z] , _ , Π[y:B₁]B₂≃Π[y':A₁]B₂'
      with injProdGen Π[y:B₁]B₂≃Π[y':A₁]B₂' -----------------------------------------------------------------------------------------> (3)
    ... | B₁≃A₁ , ∀w→B₂[y=w]≃B₂'[y'=w] with syntacticValidity Δ⊢λ[x:A₁]M₁:Π[y:B₁]B₂ -------------------------------------------------> (4)
    ... | _ , inj₁ ()
    ... | s , inj₂ Δ⊢Π[y:B₁]B₂:s with genProd Δ⊢Π[y:B₁]B₂:s -------------------------------------------------------------------------> (5)
    ... | s₁' , s₂' , _ , z' , _ , Δ⊢B₁:s₁' , z'∉fvB₂-y , Δ,z':B₁⊢B₂[y=z']:s₂' , _ =
      ⊢conv Δ⊢M₁[x=M₂]:B₂'[y'=M₂] B₂'[y'=M₂]≃B₂[y=M₂] Δ⊢B₂[y=M₂]:s₂
      where
      Δ⊢M₂:A₁ : Δ ⊢ₛ M₂ ∶ A₁ ---------------------------------------------------------------------------------------------------------> (6)
      Δ⊢M₂:A₁ = ⊢conv Δ⊢M₂:B₁ B₁≃A₁ Δ⊢A₁:s₁     
      Δ⊢M₁[x=z][z=M₂]:B₂'[y'=z][z=M₂] : Δ ⊢ₛ M₁ [ x := v z ] [ z := M₂ ] ∶ B₂' [ y' := v z ] [ z := M₂ ] -----------------------------> (7)
      Δ⊢M₁[x=z][z=M₂]:B₂'[y'=z][z=M₂] = cut Δ,z:A₁⊢M₁[x=z]:B₂'[y'=z] Δ⊢M₂:A₁ 
      Δ⊢M₁[x=M₂]:B₂'[y'=M₂] : Δ ⊢ₛ M₁ [ x := M₂ ] ∶ B₂' [ y' := M₂ ] 
      Δ⊢M₁[x=M₂]:B₂'[y'=M₂] =
        subst₂ (λ P C → Δ ⊢ₛ P ∶ C)
               (sym (composRenUpd {x} {z} {M₁} z∉fvM₁-x))
               (sym (composRenUpd {y'} {z} {B₂'} z∉fvB₂'-y'))
               Δ⊢M₁[x=z][z=M₂]:B₂'[y'=z][z=M₂]
      B₂'[y'=M₂]≃B₂[y=M₂] : B₂' [ y' := M₂ ] ≃β B₂ [ y := M₂ ] ----------------------------------------------------------------------> (8)
      B₂'[y'=M₂]≃B₂[y=M₂] =
        subst₂ (λ C D → C ≃β D)
               (sym (composRenUpd {y'} {z″} {B₂'} z″∉fvB₂'-y'))
               (sym (composRenUpd {y} {z″} {B₂} z″∉fvB₂-y))
               (Eq.symmetric (_∼α_ ∪ _→β_) (compatConvSub (∀w→B₂[y=w]≃B₂'[y'=w] z″)))
         where
         z″ : 𝒱
         z″ = X' (fv B₂' - y' ++ fv B₂ - y)
         z″∉fvB₂'-y' : z″ ∉ fv B₂' - y'
         z″∉fvB₂'-y' = c∉xs++ys→c∉xs (Xpfresh (fv B₂' - y' ++ fv B₂ - y))
         z″∉fvB₂-y : z″ ∉ fv B₂ - y
         z″∉fvB₂-y = c∉xs++ys→c∉ys (Xpfresh (fv B₂' - y' ++ fv B₂ - y))
      Δ⊢B₂[y=z'][z'=M₂]:s₂ : Δ ⊢ₛ B₂ [ y := v z' ] [ z' := M₂ ] ∶ c s₂' --------------------------------------------------------------> (9)
      Δ⊢B₂[y=z'][z'=M₂]:s₂ = cut Δ,z':B₁⊢B₂[y=z']:s₂' Δ⊢M₂:B₁
      Δ⊢B₂[y=M₂]:s₂ : Δ ⊢ₛ B₂ [ y := M₂ ] ∶ c s₂'
      Δ⊢B₂[y=M₂]:s₂ = subst (λ P → Δ ⊢ₛ P ∶ c s₂') (sym (composRenUpd {y} {z'} {B₂} z'∉fvB₂-y)) Δ⊢B₂[y=z'][z'=M₂]:s₂          
    subRed (⊢conv Γ⊢M:A A≃B Γ⊢B:s) Γ→Δ M→M' = ⊢conv (subRed Γ⊢M:A Γ→Δ M→M') A≃B (subRed Γ⊢B:s Γ→Δ (inj₁ PEq.refl))

    -- Standard statement of the subject redution theorem:

    SR : ∀ {Γ M N A} → Γ ⊢ₛ M ∶ A → M →β N → Γ ⊢ₛ N ∶ A
    SR d r  = subRed d oneStepCxtRefl (inj₂ r) 

    manyStepSR : ∀ {Γ M N A} → Γ ⊢ₛ M ∶ A → M →β*₀ N → Γ ⊢ₛ N ∶ A
    manyStepSR 𝒟 ε = 𝒟
    manyStepSR 𝒟 (M→P ◅ P→*N) = manyStepSR (SR 𝒟 M→P) P→*N