------------------------------------------------------------------------
-- The Agda standard library
--
-- Concepts from rewriting theory
-- Definitions are based on "Term Rewriting Systems" by J.W. Klop
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Relation.Binary.Rewriting where

open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Data.Product.Base using (_×_ ; ∃ ; -,_; _,_ ; proj₁ ; proj₂)
open import Data.Empty using (⊥-elim)
open import Function.Base using (flip)
open import Induction.WellFounded using (WellFounded; Acc; acc)
open import Relation.Binary.Core using (REL; Rel)
open import Relation.Binary.Construct.Closure.Equivalence using (EqClosure)
open import Relation.Binary.Construct.Closure.Equivalence.Properties
  using (a—↠b&a—↠c⇒b↔c)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star; _◅_; ε; _◅◅_)
open import Relation.Binary.Construct.Closure.Symmetric using (fwd; bwd)
open import Relation.Binary.Construct.Closure.Transitive
  using (Plus; [_]; _∼⁺⟨_⟩_)
open import Relation.Nullary.Negation.Core using (¬_)

-- The following definitions are taken from Klop [5]
module _ {a ℓ} {A : Set a} (_⟶_ : Rel A ℓ) where

  private
    _⟵_  = flip _⟶_
    _—↠_ = Star _⟶_
    _↔_  = EqClosure _⟶_

  IsNormalForm : A → Set _
  IsNormalForm a = ¬ ∃ λ b → (a ⟶ b)

  HasNormalForm : A → Set _
  HasNormalForm b = ∃ λ a → IsNormalForm a × (b —↠ a)

  NormalForm : Set _
  NormalForm = ∀ {a b} → IsNormalForm a → b ↔ a → b —↠ a

  WeaklyNormalizing : Set _
  WeaklyNormalizing = ∀ a → HasNormalForm a

  StronglyNormalizing : Set _
  StronglyNormalizing = WellFounded _⟵_

  UniqueNormalForm : Set _
  UniqueNormalForm = ∀ {a b} → IsNormalForm a → IsNormalForm b → a ↔ b → a ≡ b

  Confluent : Set _
  Confluent = ∀ {A B C} → A —↠ B → A —↠ C → ∃ λ D → (B —↠ D) × (C —↠ D)

  WeaklyConfluent : Set _
  WeaklyConfluent = ∀ {A B C} → A ⟶ B → A ⟶ C → ∃ λ D → (B —↠ D) × (C —↠ D)


Deterministic : ∀ {a b ℓ₁ ℓ₂} → {A : Set a} → {B : Set b} → Rel B ℓ₁ → REL A B ℓ₂ → Set _
Deterministic _≈_ _—→_ = ∀ {x y z} → x —→ y → x —→ z → y ≈ z

module _ {a ℓ} {A : Set a} {_⟶_ : Rel A ℓ} where

  private
    _—↠_ = Star _⟶_
    _↔_  = EqClosure _⟶_
    _⟶₊_ = Plus _⟶_

  det⇒conf : Deterministic _≡_ _⟶_ → Confluent _⟶_
  det⇒conf det ε          rs₂        = -, rs₂ , ε
  det⇒conf det rs₁        ε          = -, ε , rs₁
  det⇒conf det (r₁ ◅ rs₁) (r₂ ◅ rs₂)
    rewrite det r₁ r₂ = det⇒conf det rs₁ rs₂

  conf⇒wcr : Confluent _⟶_ → WeaklyConfluent _⟶_
  conf⇒wcr c fst snd = c (fst ◅ ε) (snd ◅ ε)

  conf⇒nf : Confluent _⟶_ → NormalForm _⟶_
  conf⇒nf c aIsNF ε = ε
  conf⇒nf c aIsNF (fwd x ◅ rest) = x ◅ conf⇒nf c aIsNF rest
  conf⇒nf c aIsNF (bwd y ◅ rest) with c (y ◅ ε) (conf⇒nf c aIsNF rest)
  ... | _ , _    , x ◅ _ = ⊥-elim (aIsNF (_ , x))
  ... | _ , left , ε     = left

  conf⇒unf : Confluent _⟶_ → UniqueNormalForm _⟶_
  conf⇒unf _ _     _     ε           = refl
  conf⇒unf _ aIsNF _     (fwd x ◅ _) = ⊥-elim (aIsNF (_ , x))
  conf⇒unf c aIsNF bIsNF (bwd y ◅ r) with c (y ◅ ε) (conf⇒nf c bIsNF r)
  ... | _ , ε     , x ◅ _ = ⊥-elim (bIsNF (_ , x))
  ... | _ , x ◅ _ , _     = ⊥-elim (aIsNF (_ , x))
  ... | _ , ε     , ε     = refl

  un&wn⇒cr : UniqueNormalForm _⟶_ → WeaklyNormalizing _⟶_ → Confluent _⟶_
  un&wn⇒cr un wn {a} {b} {c} aToB aToC with wn b | wn c
  ... | (d , (d-nf , bToD)) | (e , (e-nf , cToE))
    with un d-nf e-nf (a—↠b&a—↠c⇒b↔c (aToB ◅◅ bToD) (aToC ◅◅ cToE))
  ... | refl = d , bToD , cToE

-- Newman's lemma
  sn&wcr⇒cr : StronglyNormalizing _⟶₊_ → WeaklyConfluent _⟶_ → Confluent _⟶_
  sn&wcr⇒cr sn wcr = helper (sn _) where

    starToPlus : ∀ {a b c} → (a ⟶ b) → b —↠ c → a ⟶₊ c
    starToPlus aToB ε = [ aToB ]
    starToPlus {a} aToB (e ◅ bToC) = a ∼⁺⟨ [ aToB ] ⟩ (starToPlus e bToC)

    helper : ∀ {a b c} → (acc : Acc (flip _⟶₊_) a) →
             a —↠ b → a —↠ c → ∃ λ d → (b —↠ d) × (c —↠ d)
    helper _       ε           snd         = -, snd , ε
    helper _       fst         ε           = -, ε   , fst
    helper (acc g) (toJ ◅ fst) (toK ◅ snd) = result where

        wcrProof = wcr toJ toK
        innerPoint = proj₁ wcrProof
        jToInner = proj₁ (proj₂ wcrProof)
        kToInner = proj₂ (proj₂ wcrProof)

        lhs = helper (g [ toJ ]) fst jToInner
        rhs = helper (g [ toK ]) snd kToInner

        fromAB = proj₁ (proj₂ lhs)
        fromInnerB = proj₂ (proj₂ lhs)

        fromAC = proj₁ (proj₂ rhs)
        fromInnerC = proj₂ (proj₂ rhs)

        aToInner : _ ⟶₊ innerPoint
        aToInner = starToPlus toJ jToInner

        finalRecursion = helper (g aToInner) fromInnerB fromInnerC

        bMidToDest = proj₁ (proj₂ finalRecursion)
        cMidToDest = proj₂ (proj₂ finalRecursion)

        result : ∃ λ d → (_ —↠ d) × (_ —↠ d)
        result = _ , fromAB ◅◅ bMidToDest , fromAC ◅◅ cMidToDest