open import Data.Product
open import Data.Sum
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (cong)
open import Relation.Binary.Construct.Union

open import Stoughton.Var

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

  open import Stoughton.Syntax 𝒞 𝒱 (Enum._≟_ var)
  open import Stoughton.Alpha 𝒞 var
  open import Stoughton.Substitution 𝒞 var      
  open import Stoughton.SubstitutionLemmas 𝒞 var

  Diam : (Λ → Λ → Set) → Set
  Diam _𝒮_ = ∀ {M N P} → M 𝒮 N → M 𝒮 P → ∃ λ Q → N 𝒮 Q × P 𝒮 Q
  
  Pent : (Λ → Λ → Set) → Set
  Pent _𝒮_ = ∀ {M N P} → M 𝒮 N → M 𝒮 P → ∃₂ λ Q₁ Q₂ → N 𝒮 Q₁ × P 𝒮 Q₂ × Q₁ ∼α Q₂

  starInStarAlpha : ∀ {t 𝒮} → Star {t = t} 𝒮 ⇒ Star (𝒮 ∪ _∼α_)
  starInStarAlpha ε = ε
  starInStarAlpha (M→N ◅ M↠N) = inj₁ M→N ◅ starInStarAlpha M↠N

  alphaInStarAlpha : ∀ {t 𝒮 M N} → M ∼α N → Star {t = t} (𝒮 ∪ _∼α_) M N
  alphaInStarAlpha M∼N = inj₂ M∼N ◅ ε

  Strip : (Λ → Λ → Set) → Set
  Strip 𝒮 = ∀ {M N R} → (Star 𝒮) M N → 𝒮 M R → ∃₂ λ T₁ T₂ → 𝒮 N T₁ × (Star 𝒮) R T₂ × T₁ ∼α T₂
    
  module _ {𝒮} (comm : CommAlpha 𝒮) where

    CommClosStar : CommAlpha (Star 𝒮)
    CommClosStar {M} {N} {.N} M∼N ε = M , ε , M∼N
    CommClosStar M∼N (N→P' ◅ P'↠P) with comm M∼N N→P'
    ... | Q' , M→Q' , Q'∼P' with CommClosStar Q'∼P' P'↠P
    ... | Q″ , Q'↠Q″ , Q″∼P = Q″ , M→Q' ◅ Q'↠Q″ , Q″∼P

    postponement : ∀ {M N} → Star (𝒮 ∪ _∼α_) M N → ∃ λ P → Star 𝒮 M P × P ∼α N 
    postponement {M} {.M} ε = M , ε , ∼ρ
    postponement (_◅_ {M} {Q} {N} (inj₁ M→Q) Q↠N) with postponement Q↠N
    ... | P' , Q↠P' , P'∼N = P' , M→Q ◅ Q↠P' , P'∼N
    postponement (_◅_ {M} {Q} {N} (inj₂ M∼Q) Q↠N) with postponement Q↠N
    ... | P' , Q↠P' , P'∼N with CommClosStar M∼Q Q↠P'
    ... | P″ , Q↠P″ , P″∼P' = P″ , Q↠P″ , ∼τ P″∼P' P'∼N

    PentDiam : Pent (Star 𝒮) → Diam (Star (𝒮 ∪ _∼α_))
    PentDiam pent M↠N M↠P with postponement M↠N | postponement M↠P
    ... | N′ , M↠N′ , N′∼N | P′ , M↠P′ , P′∼P with pent M↠N′ M↠P′
    ... | N″ , P″ , N′↠N″ , P′↠P″ , N″∼P″ with CommClosStar (∼σ N′∼N) N′↠N″ | CommClosStar (∼σ P′∼P) P′↠P″
    ... | N‴ , N↠N‴ , N‴∼N″ | P‴ , P↠P‴ , P‴∼P″ =
      N″ , starInStarAlpha N↠N‴ ◅◅ alphaInStarAlpha N‴∼N″
         , starInStarAlpha P↠P‴ ◅◅ alphaInStarAlpha (∼τ P‴∼P″ (∼σ N″∼P″))

    strip : Pent 𝒮 → Strip 𝒮
    strip _ {M} {.M} {R} ε M→R = R , R , M→R , ε , ∼ρ  
    strip pent {M} {N} {R} (M→N' ◅ N'↠N) M→R with pent M→N' M→R
    ... | Q' , R' , N'→Q' , R→R' , Q'∼R' with strip pent N'↠N N'→Q'
    ... | T₁ , Q″ , N→T₁ , Q'↠Q″ , T₁∼Q″ with CommClosStar (∼σ Q'∼R') Q'↠Q″
    ... | T₂ , R'↠T₂ , T₂∼Q″  = 
      T₁ , T₂ , N→T₁ , R→R' ◅ R'↠T₂ , ∼τ T₁∼Q″ (∼σ T₂∼Q″)

    PentClosStar : Pent 𝒮 → Pent (Star 𝒮)
    PentClosStar _ {M} {.M} {R} ε M→*R = R , R , M→*R , ε , ∼ρ
    PentClosStar _ {M} {N} {.M} M↠N@(_ ◅ _) ε = N , N , ε , M↠N , ∼ρ
    PentClosStar pent {M} {N} {R} (M→N' ◅ N'↠N) (M→R ◅ R↠P) with pent M→N' M→R
    ... | Q' , R' , N'→Q' , R→R' , Q'∼R' with strip pent N'↠N N'→Q'
    ... | T₁ , Q″ , N→T₁ , Q'↠Q″ , T₁∼Q″ with CommClosStar (∼σ Q'∼R') Q'↠Q″
    ... | T₂ , R'↠T₂ , T₂∼Q″ with PentClosStar pent (R→R' ◅ R'↠T₂) R↠P
    ... | Q'₁ , Q₂ , T₂↠Q'₁ , P↠Q₂ , Q'₁∼Q₂ with CommClosStar (∼τ T₁∼Q″ (∼σ T₂∼Q″)) T₂↠Q'₁
    ... | Q₁ , T₁↠Q₁ , Q₁∼Q'₁ = Q₁ , Q₂ , N→T₁ ◅ T₁↠Q₁ , P↠Q₂ , ∼τ Q₁∼Q'₁ Q'₁∼Q₂