open import Data.Empty
open import Data.Product
open import Relation.Binary.Construct.Closure.ReflexiveTransitive hiding (_⋆)
open import Relation.Nullary
open import Data.Sum

open import Stoughton.Var

module ChurchRosser (𝒞 : Set) {𝒱 : Set} (var : Enum 𝒱) where

  open Enum
  
  open import Stoughton.Syntax 𝒞 𝒱 (_≟_ var)
  open import Stoughton.Alpha 𝒞 var
  open import Stoughton.Substitution 𝒞 var      
  open import Stoughton.SubstitutionLemmas 𝒞 var
  open import BetaReduction 𝒞 var
  open import BetaConversion 𝒞 var  
  open import Relation 𝒞 var
  open import ParallelReduction 𝒞 var
  open import ParallelReduction.Properties 𝒞 var 

  compatAlphaUnary : ∀ {M M' N N' x} → M ∼α M' → N ∼α N' → M [ x := N ] ∼α M' [ x := N' ]
  compatAlphaUnary M∼M' N∼N' = lemma-subst M∼M' (lemma≺+∼α⇂ lemmaι∼α⇂ N∼N')

  compatParSubUnary : ∀ {M M' N N' x} → M ⇉ M' → N ⇉ N' → ∃ λ P → M [ x := N ] ⇉ P × P ∼α M' [ x := N' ]
  compatParSubUnary {x = x} M⇉M' N⇉N' = compatParSub M⇉M' (corollary⇉ₛ≺+ x N⇉N')
  
  data IsAbs : Λ → Set where
    isAbs : ∀ {x A M} → IsAbs (λ[ x ∶ A ] M)

  isAbs? : ∀ M → Dec (IsAbs M)
  isAbs? (c x) = no (λ ())
  isAbs? (v x) = no (λ ())
  isAbs? (λ[ x ∶ A ] M) = yes isAbs
  isAbs? (Π[ x ∶ A ] B) = no (λ ())
  isAbs? (M · N) = no (λ ())

  infix  _⋆
  _⋆ : Λ → Λ
  (v x)⋆ = v x
  (c k)⋆ = c k
  (λ[ x ∶ A ] M)⋆ = λ[ x ∶ A ⋆ ](M ⋆)
  (Π[ x ∶ A ] B)⋆ = Π[ x ∶ A ⋆ ](B ⋆)
  (M · N)⋆ with isAbs? M
  ... | yes (isAbs {x} {A} {M}) = (M ⋆)[ x := N ⋆ ]  
  ... | no _ = (M ⋆) · (N ⋆)

  takahashi : ∀ {M N} → M ⇉ N → ∃ λ P → N ⇉ P × P ∼α M ⋆ 
  takahashi {c k} ⇉c = c k , ⇉c , ∼ρ
  takahashi {v x} ⇉v = v x , ⇉v , ∼ρ
  takahashi {λ[ x ∶ A ] M} (⇉λ A⇉A' M⇉M') with takahashi A⇉A' | takahashi M⇉M'
  ... | P₁ , A⇉P₁ , P₁∼A* | P₂ , M⇉P₂ , P₂∼M* = λ[ x ∶ P₁ ] P₂ , ⇉λ A⇉P₁ M⇉P₂ , lemma∼λ P₁∼A* P₂∼M* 
  takahashi {Π[ x ∶ A ] B} (⇉Π A⇉A' B⇉B') with takahashi A⇉A' | takahashi B⇉B'
  ... | P₁ , A⇉P₁ , P₁∼A* | P₂ , B⇉P₂ , P₂∼B* = Π[ x ∶ P₁ ] P₂ , ⇉Π A⇉P₁ B⇉P₂ , lemma∼Π P₁∼A* P₂∼B* 
  takahashi {M' · _} _ with isAbs? M'
  -- 1ˢᵗ (sub-)case of redex:
  takahashi {M = .((λ[ x ∶ A ] M₀) · M₁)} {N = .((λ[ x ∶ B ] N₀) · N₁)} (⇉· {N = M₁} {N₁} (⇉λ {A' = B} {M' = N₀} _ M₀⇉N₀) M₁⇉N₁) 
    | yes (isAbs {x} {A} {M₀}) with takahashi M₀⇉N₀ | takahashi M₁⇉N₁
  ... | P₁ , N₀⇉P₁ , P₁∼M₀* | P₂ , N₁⇉P₂ , P₂∼M₁* = P₁ [ x := P₂ ] , ⇉β N₀⇉P₁ N₁⇉P₂ , compatAlphaUnary P₁∼M₀* P₂∼M₁*
  -- 2ⁿᵈ (sub-)case of redex:
  takahashi {M = .((λ[ x ∶ A ] M₀) · M₁)} {N = .(N₀ [ x := N₁ ])} (⇉β {M' = N₀} {M₁} {N₁} M₀⇉N₀ M₁⇉N₁)
    | yes (isAbs {x} {A} {M₀}) with takahashi M₀⇉N₀ | takahashi M₁⇉N₁ 
  ... | P₁ , N₀⇉P₁ , P₁∼M₀* | P₂ , N₁⇉P₂ , P₂∼M₁* with compatParSubUnary N₀⇉P₁ N₁⇉P₂
  ... | Q , N₀[x=N₁]⇉Q , Q∼P₁[x=P₂] = Q , N₀[x=N₁]⇉Q , ∼τ Q∼P₁[x=P₂] (compatAlphaUnary P₁∼M₀* P₂∼M₁*)
  takahashi {M · N} (⇉· M⇉M' N⇉N') | no _ with takahashi M⇉M' | takahashi N⇉N'
  ... | P₁ , M'⇉P₁ , P₁∼M* | P₂ , N'⇉P₂ , P₂∼N* = P₁ · P₂ , ⇉· M'⇉P₁ N'⇉P₂ , ∼· P₁∼M* P₂∼N* 
  takahashi {.(λ[ x ∶ A ] M) · N} (⇉β {x} {A} {M} _ _) | no isAbsλ[x:A]M→⊥ = ⊥-elim (isAbsλ[x:A]M→⊥ (isAbs {x} {A} {M}))

  parPent : Pent _⇉_
  parPent M⇉N M⇉P with takahashi M⇉N | takahashi M⇉P
  ... | Q₁ , N⇉Q₁ , Q₁∼M* | Q₂ , P⇉Q₂ , Q₂∼M* = Q₁ , Q₂ , N⇉Q₁ , P⇉Q₂ , ∼τ Q₁∼M* (∼σ Q₂∼M*) 

  pentParStar : Pent (Star _⇉_)
  pentParStar = PentClosStar parComm parPent

  CR1 : Pent _→β*₀_
  CR1 M→*N M→*P with pentParStar (starParContainsManyStep M→*N) (starParContainsManyStep M→*P)
  ... | Q₁ , Q₂ , N⇉*Q₁ , P⇉*Q₂ , Q₁∼Q₂ = Q₁ , Q₂ , manyStepBetaContainsStarPar N⇉*Q₁ , manyStepBetaContainsStarPar P⇉*Q₂ , Q₁∼Q₂

  CR2 : ∀ {M N} → M ≃β N → ∃₂ λ P₁ P₂ → M →β*₀ P₁ × N →β*₀ P₂ × P₁ ∼α P₂
  CR2 {M} ε = M , M , ε , ε , ∼ρ
  CR2 {M} {N} (r ◅ P≃N) with CR2 P≃N
  CR2 {M} {N} (inj₁ (inj₁ M∼P) ◅ P≃N) | Q₁ , Q₂ , P→*Q₁ , N→*Q₂ , Q₁∼Q₂ with manyStepCommutesAlpha M∼P P→*Q₁
  ... | R , M→*R , R∼Q₁ = R , Q₂ , M→*R , N→*Q₂ , ∼τ R∼Q₁ Q₁∼Q₂
  CR2 {M} {N} (inj₁ (inj₂ M→P) ◅ P≃N) | Q₁ , Q₂ , P→*Q₁ , N→*Q₂ , Q₁∼Q₂ = Q₁ , Q₂ , M→P ◅ P→*Q₁ , N→*Q₂ , Q₁∼Q₂
  CR2 {M} {N} (inj₂ (inj₁ P∼M) ◅ P≃N) | Q₁ , Q₂ , P→*Q₁ , N→*Q₂ , Q₁∼Q₂ with manyStepCommutesAlpha (∼σ P∼M) P→*Q₁
  ... | R , M→*R , R∼Q₁ = R , Q₂ , M→*R , N→*Q₂ , ∼τ R∼Q₁ Q₁∼Q₂ 
  CR2 {M} {N} (inj₂ (inj₂ P→M) ◅ P≃N) | Q₁ , Q₂ , P→*Q₁ , N→*Q₂ , Q₁∼Q₂ with CR1 (P→M ◅ ε) P→*Q₁
  ... | R₁ , R₂ , M→*R₁ , Q₁→*R₂ , R₁∼R₂ with manyStepCommutesAlpha (∼σ Q₁∼Q₂) Q₁→*R₂
  ... | S , Q₂→*S , S∼R₂ = R₁ , S , M→*R₁ , Q₂→*S ▻▻ N→*Q₂ , ∼τ R₁∼R₂ (∼σ S∼R₂)