Proof of the open problem in section 7 of "Pure Subtype Systems" by DeLesley S. Hutchins.

2013-11-13-confluence-problem.agda

module 2013-11-13-confluence-problem where

open import 2013-11-13-relations
open import Function
open import Data.Unit using (⊤;tt)
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Product as P hiding (map;zip;swap)
open import Data.Nat as Nat hiding (fold)
open import Data.Nat.Properties as NatP
open import Relation.Nullary
open import Induction.WellFounded
open import Induction.Nat
open ≡-Reasoning
open import Algebra.Structures

open IsDistributiveLattice isDistributiveLattice using () renaming (∧-comm to ⊔-comm)
open IsCommutativeSemiring isCommutativeSemiring using (+-comm;+-assoc)
open DecTotalOrder Nat.decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)

--------------------------------------------------------------------------------
-- Utility
--------------------------------------------------------------------------------

n≤m⊔n : ∀ m n → n ≤ m ⊔ n
n≤m⊔n m n rewrite ⊔-comm m n = m≤m⊔n n m

⊔≤ : ∀ {m n o} → m ≤ o → n ≤ o → m ⊔ n ≤ o
⊔≤ z≤n n≤o = n≤o
⊔≤ (s≤s m≤o) z≤n = s≤s m≤o
⊔≤ (s≤s m≤o) (s≤s n≤o) = s≤s (⊔≤ m≤o n≤o)

≤⊔≤ : ∀ {a b c d} → a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ d
≤⊔≤ {a} {b} {c} {d} a≤b c≤d = ⊔≤ (≤-trans a≤b (m≤m⊔n b d)) (≤-trans c≤d (n≤m⊔n b d))

--------------------------------------------------------------------------------------------------
-- The problem
--------------------------------------------------------------------------------------------------

data V : Set where
  `A : V
  `C : V → V
  `D : V → V → V

_==_ : Rel₀ V
data _⟶_ : Rel₀ V where
  aca : `A ⟶ `C `A
  d₁ : ∀ {a b} → (eq : a == b) → `D a b ⟶ a
  d₂ : ∀ {a b} → (eq : a == b) → `D a b ⟶ b
  -- Do we also have these? It was not entirely clear from the paper.
  -- But I assume so, since otherwise the relation is strongly normalizing and we could prove confluence that way
  under-c  : ∀ {a a'} → (x : a ⟶ a') → `C a ⟶ `C a'
  under-d₁ : ∀ {a a' b} → (x : a ⟶ a') → `D a b ⟶ `D a' b
  under-d₂ : ∀ {a b b'} → (y : b ⟶ b') → `D a b ⟶ `D a b'
_==_ = Star (Sym _⟶_)

-- we want to prove confluence of _⟶_
-- but to do that we need to expand _==_, which needs confluence

--------------------------------------------------------------------------------------------------
-- Depth based solution
--------------------------------------------------------------------------------------------------

module DepthBased where
  -- depth of a term
  depth : V → ℕ
  depth `A = zero
  depth (`C x) = depth x
  depth (`D x y) = suc (depth x ⊔ depth y)

  -- steps of bounded depth
  -- `Step n` works under at most n `Ds, and also produces terms no more than n deep
  data Step : (n : ℕ) → Rel₀ V where
    aca     : ∀ {n} → Step n (`A) (`C `A)
    d₁      : ∀ {n a b} → (da : depth a ≤ n) → StarSym (Step n) a b → Step (suc n) (`D a b) a
    d₂      : ∀ {n a b} → (db : depth b ≤ n) → StarSym (Step n) a b → Step (suc n) (`D a b) b
    under-c : ∀ {n a a'} → (x : Step n a a') → Step n (`C a) (`C a')
    under-d : ∀ {n a b a' b'} → (x : Star (Step n) a a') → (y : Star (Step n) b b') → Step (suc n) (`D a b) (`D a' b')
    -- we can do many steps at a lower level
    many    : ∀ {n a b} → (da : depth a ≤ n) → (xs : Star (Step n) a b) → Step (suc n) a b
    -- for convenience in confluence proof there is an 'empty' step
    ε       : ∀ {n a} → Step n a a
  
  lift-step : ∀ {m n} → m ≤ n → Step m ⇒ Step n
  lift-step m≤n       aca = aca
  lift-step (s≤s m≤n) (d₁ da x) = d₁ (≤-trans da m≤n) (StarSym.map (lift-step m≤n) x)
  lift-step (s≤s m≤n) (d₂ db x) = d₂ (≤-trans db m≤n) (StarSym.map (lift-step m≤n) x)
  lift-step m≤n       (under-c x) = under-c (lift-step m≤n x)
  lift-step (s≤s m≤n) (under-d x y) = under-d (Star.map (lift-step m≤n) x) (Star.map (lift-step m≤n) y)
  lift-step (s≤s m≤n) (many da xs) = many (≤-trans da m≤n) (Star.map (lift-step m≤n) xs)
  lift-step m≤n       ε = ε

  -- depth of output is ≤ depth of input
  step-depth : ∀ {n} → Step n =[ depth ]⇒ _≥_
  steps-depth : ∀ {n} → Star (Step n) =[ depth ]⇒ _≥_
  step-depth aca = ≤-refl
  step-depth (d₁ {a = a} {b = b} _ _) = ≤-step (m≤m⊔n (depth a) (depth b))
  step-depth (d₂ {a = a} {b = b} _ _) = ≤-step (n≤m⊔n (depth a) (depth b))
  step-depth (under-c x) = step-depth x
  step-depth (under-d x y) = s≤s (≤⊔≤ (steps-depth x) (steps-depth y))
  step-depth (many _ x) = steps-depth x
  step-depth ε = ≤-refl
  steps-depth xs = Star.foldMap _≥_ (flip ≤-trans) ≤-refl step-depth xs
  
  -- Conversion from Step to ⟶ is easy
  from-step : ∀ {n} → Step n ⇒ Star _⟶_
  from-step aca = aca ◅ ε
  from-step (d₁ _ x) = d₁ (StarSym.concatMap' from-step x) ◅ ε
  from-step (d₂ _ x) = d₂ (StarSym.concatMap' from-step x) ◅ ε
  from-step (under-c x) = Star.map under-c (from-step x)
  from-step (under-d x y) = Star.map under-d₁ (Star.concatMap from-step x)
                         ◅◅ Star.map under-d₂ (Star.concatMap from-step y)
  from-step (many _ xs) = Star.concatMap from-step xs
  from-step ε = ε

  -- Now we can convert from ⟶ to Step
  module Any where
    Any : ∀ {A B : Set} → (A → Rel₀ B) → Rel₀ B
    Any R b c = ∃ \a → R a b c
  open Any using (Any)
  
  to-step  : _⟶_ ⇒ Any Step
  to-steps : Star _⟶_ ⇒ Any (Star ∘ Step)
  to-eq : _==_ ⇒ Any (StarSym ∘ Step)
  to-step aca = zero , aca
  to-step (d₁ {a = a} {b = b} eq) with to-eq eq
  ... | n , eq' = suc (n ⊔ (depth a ⊔ depth b))
                , d₁ (≤-trans (m≤m⊔n (depth a) (depth b)) (n≤m⊔n n _))
                     (StarSym.map (lift-step (m≤m⊔n _ _)) eq')
  to-step (d₂ {a = a} {b = b} eq) with to-eq eq
  ... | n , eq' = suc (n ⊔ (depth a ⊔ depth b))
                , d₂ (≤-trans (n≤m⊔n (depth a) (depth b)) (n≤m⊔n n _))
                     (StarSym.map (lift-step (m≤m⊔n _ _)) eq')
  to-step (under-c x) = P.map id under-c (to-step x)
  to-step (under-d₁ x) = P.map suc (\x' → under-d (x' ◅ ε) ε) (to-step x)
  to-step (under-d₂ y) = P.map suc (\y' → under-d ε (y' ◅ ε)) (to-step y)
  to-symstep : Sym _⟶_ ⇒ Any (Sym ∘ Step)
  to-symstep (fwd x) = P.map id fwd (to-step x)
  to-symstep (bwd x) = P.map id bwd (to-step x)
  to-steps ε = zero , ε
  to-steps (x ◅ xs) with to-step x | to-steps xs
  ... | m , x' | n , xs' = (m ⊔ n) , lift-step (m≤m⊔n m n) x' ◅ Star.map (lift-step (n≤m⊔n m n)) xs'
  to-eq ε = zero , ε
  to-eq (x ◅ xs) with to-symstep x | to-eq xs
  ... | m , x' | n , xs' = (m ⊔ n) , Sym.map (lift-step (m≤m⊔n m n)) x'
                                     ◅ StarSym.map (lift-step (n≤m⊔n m n)) xs'

  -- if x has depth ≤ n, then all steps out of it also have depth ≤ n
  -- This depends on confluence, we pass in confluence explicitly, to help the termination checker.
  lower-step  : ∀ {n a b} → (∀ {m} → m ≤′ n → GlobalConfluent (Step m)) → Step (suc n) a b → depth a ≤ n → Star (Step n) a b
  lower-steps : ∀ {n a b} → (∀ {m} → m ≤′ suc n → GlobalConfluent (Step m)) → Star (Step (suc n)) a b → depth a ≤ n → Star (Step n) a b
  lower-eq    : ∀ {n a b} → (∀ {m} → m ≤′ suc n → GlobalConfluent (Step m)) → StarSym (Step (suc n)) a b → depth a ≤ n → depth b ≤ n → StarSym (Step n) a b
  lower-step conf aca da = aca ◅ ε
  lower-step conf (d₁ {a = a} {b = b} _ eq) (s≤s da) =
    d₁ (≤-trans (m≤m⊔n (depth a) (depth b)) da)
       (lower-eq conf eq (≤-trans (m≤m⊔n (depth a) (depth b)) da)
                         (≤-trans (n≤m⊔n (depth a) (depth b)) da)) ◅ ε
  lower-step conf (d₂ {a = a} {b = b} _ eq) (s≤s da) =
    d₂ (≤-trans (n≤m⊔n (depth a) (depth b)) da)
       (lower-eq conf eq (≤-trans (m≤m⊔n (depth a) (depth b)) da)
                         (≤-trans (n≤m⊔n (depth a) (depth b)) da)) ◅ ε
  lower-step conf (under-c x) da = Star.map under-c (lower-step conf x da)
  lower-step conf (under-d {a = a} {b = b} x y) (s≤s da) =
    under-d (lower-steps conf x (≤-trans (m≤m⊔n (depth a) (depth b)) da))
            (lower-steps conf y (≤-trans (n≤m⊔n (depth a) (depth b)) da)) ◅ ε
  lower-step conf (many _ xs) da = xs
  lower-step conf ε da = ε
  lower-steps conf ε da = ε
  lower-steps conf (x ◅ xs) da = lower-step (conf ∘ ≤′-step) x da ◅◅ lower-steps conf xs (≤-trans (step-depth x) da)
  lower-eq {n} conf xs da db with from-StarSym (conf ≤′-refl) xs
  ... | us || vs = Star.map fwd (lower-steps conf us da)
                ◅◅ Star.reverse bwd (lower-steps conf vs db)

  -- It's confluence time
  confluent : ∀ {n} → Confluent (Step n)
  gconfluent : ∀ {n} → GlobalConfluent (Step n)
  gconfluent-upto : ∀ {m n} → m ≤′ n → GlobalConfluent (Step m)

  confluent x ε = ε || x
  confluent ε y = y || ε
  confluent {n = suc n} (many da xs) y with gconfluent {n} xs (lower-step {n} gconfluent-upto y da)
  ... | u || v = many (≤-trans (steps-depth xs) da) u || many (≤-trans (step-depth y) da) v
  confluent {n = suc n} x (many da ys) with gconfluent {n} (lower-step {n} gconfluent-upto x da) ys
  ... | u || v = many (≤-trans (step-depth x) da) u || many (≤-trans (steps-depth ys) da) v
  confluent aca aca = ε || ε
  confluent (d₁ _ eq) (d₁ _ _) = ε || ε
  confluent (d₂ _ eq) (d₂ _ _) = ε || ε
  confluent {n = suc n} (d₁ da eq) (d₂ db _) with from-StarSym (gconfluent {n}) eq
  ... | u || v = many da u || many db v
  confluent {n = suc n} (d₂ db eq) (d₁ da _) with from-StarSym (gconfluent {n}) eq
  ... | u || v = many db v || many da u
  confluent (d₁ da eq) (under-d u v) = many da u
                                     || d₁ (≤-trans (steps-depth u) da)
                                           (StarSym.into (bwd u) ◅◅ eq ◅◅ StarSym.into (fwd v))
  confluent (d₂ db eq) (under-d u v) = many db v
                                     || d₂ (≤-trans (steps-depth v) db)
                                           (StarSym.into (bwd u) ◅◅ eq ◅◅ StarSym.into (fwd v))
  confluent (under-d u v) (d₁ da eq) = d₁ (≤-trans (steps-depth u) da)
                                          (StarSym.into (bwd u) ◅◅ eq ◅◅ StarSym.into (fwd v)) || many da u
  confluent (under-d u v) (d₂ db eq) = d₂ (≤-trans (steps-depth v) db)
                                          (StarSym.into (bwd u) ◅◅ eq ◅◅ StarSym.into (fwd v)) || many db v
  confluent (under-c x) (under-c y) = CR.map under-c (confluent x y)
  confluent (under-d x y) (under-d u v) = CR.zip under-d (gconfluent x u) (gconfluent y v)

  gconfluent {n} = Confluent-Star (confluent {n})

  gconfluent-upto ≤′-refl = gconfluent
  gconfluent-upto (≤′-step m≤n) = gconfluent-upto m≤n


  ⟶-gconfluent : GlobalConfluent _⟶_
  ⟶-gconfluent x y with to-steps x | to-steps y
  ... | m , x' | n , y' with gconfluent (Star.map (lift-step (m≤m⊔n m n)) x') (Star.map (lift-step (n≤m⊔n m n)) y')
  ...   | u || v = Star.concatMap from-step u || Star.concatMap from-step v
  -- Q.E.D.

2013-11-13-relations.agda

-- Utilities about relations
-- In particular, define what confluence means.
module 2013-11-13-relations where

open import Level hiding (zero;suc)
open import Function -- using (_∘_;id;_⟨_⟩_)
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Empty

--------------------------------------------------------------------------------
-- Utility
--------------------------------------------------------------------------------

Rel₀ : Set → Set₁
Rel₀ A = Rel A Level.zero

Arrow : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
Arrow A B = A → B

--------------------------------------------------------------------------------
-- Transitive closure
--------------------------------------------------------------------------------

module Star where
  open import Data.Star public renaming (map to map'; fold to foldr)
  
  map : ∀ {i j t u} {I : Set i} {T : Rel I t} {J : Set j} {U : Rel J u} →
        {f : I → J} → T =[ f ]⇒ U → Star T =[ f ]⇒ Star U
  map g xs = gmap _ g xs

  concatMap : ∀ {i j t u}
                {I : Set i} {J : Set j} {T : Rel I t} {U : Rel J u}
                {f : I → J} → T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
  concatMap g xs = kleisliStar _ g xs

  foldMap : ∀ {i j t p} {I : Set i} {J : Set j} {T : Rel I t}
          {f : I → J} (P : Rel J p) →
          Transitive P → Reflexive P → T =[ f ]⇒ P → Star T =[ f ]⇒ P
  foldMap {f = f} P t r g = gfold f P (\a b → t (g a) b) r

  fold : ∀ {a r} {A : Set a} {R : Rel A r} → {f : A → Set} → (R =[ f ]⇒ Arrow) → (Star R =[ f ]⇒ Arrow)
  --fold {f = f} g = Data.Star.gfold f Arrow (\a b → b ∘ g a) id
  fold {f = f} g = foldMap {f = f} Arrow (\f g x → g (f x)) id g

open Star public using (Star;_◅_;_◅◅_;ε;_⋆)

--------------------------------------------------------------------------------
-- Reflexive closure
--------------------------------------------------------------------------------

-- reflexive closure
module Refl where
  data Refl {l r} {A : Set l} (R : Rel A r) (a : A) : A → Set (l ⊔ r) where
    ε : Refl R a a
    _◅ε : ∀ {b} → R a b → Refl R a b

  _?◅_ : ∀ {l r} {A : Set l} {R : Rel A r} {x y z : A} → Refl R x y → Star R y z → Star R x z
  ε ?◅ yz = yz
  xy ◅ε ?◅ yz = xy ◅ yz

  map : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
      → {f : A → B}
      → (∀ {a b} → R a b → S (f a) (f b))
      → ∀ {a b} → Refl R a b → Refl S (f a) (f b)
  map g ε = ε
  map g (x ◅ε) = g x ◅ε

open Refl public hiding (module Refl;map)

--------------------------------------------------------------------------------
-- Symmetric closure
--------------------------------------------------------------------------------

module Sym where
  data Sym {l r} {A : Set l} (R : Rel A r) (a : A) : A → Set (l ⊔ r) where
    fwd : ∀ {b} → R a b → Sym R a b
    bwd : ∀ {b} → R b a → Sym R a b
  
  sym : ∀ {l r} {A : Set l} {R : Rel A r} {a b : A} → Sym R a b → Sym R b a
  sym (fwd x) = bwd x
  sym (bwd x) = fwd x
  
  map : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
      → {f : A → B}
      → (∀ {a b} → R a b → S (f a) (f b))
      → ∀ {a b} → Sym R a b → Sym S (f a) (f b)
  map g (fwd x) = fwd (g x)
  map g (bwd x) = bwd (g x)

open Sym public hiding (module Sym;map;sym)

--------------------------------------------------------------------------------
-- Symmetric-transitive closure
--------------------------------------------------------------------------------

module StarSym where
  StarSym : ∀ {l r} {A : Set l} (R : Rel A r) → Rel A (l ⊔ r)
  StarSym R = Star (Sym R)

  map : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
      → {f : A → B}
      → (∀ {a b} → R a b → S (f a) (f b))
      → ∀ {a b} → StarSym R a b → StarSym S (f a) (f b)
  map g = Star.map (Sym.map g)

  into :  ∀ {l r A R} → Sym (Star R) ⇒ StarSym {l} {r} {A} R
  into (fwd xs) = Star.map     fwd xs
  into (bwd xs) = Star.reverse bwd xs

  symInto :  ∀ {l r A R} → Sym (StarSym R) ⇒ StarSym {l} {r} {A} R
  symInto (fwd xs) = xs
  symInto (bwd xs) = Star.reverse Sym.sym xs

  concat : ∀ {l r A R} → StarSym (StarSym {l} {r} {A} R) ⇒ StarSym R
  concat = Star.concat ∘ Star.map symInto

  concatMap : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
            → {f : A → B}
            → (∀ {a b} → R a b → StarSym S (f a) (f b))
            → ∀ {a b} → StarSym R a b → StarSym S (f a) (f b)
  concatMap g = Star.concat ∘ Star.map (symInto ∘ Sym.map g)

  concatMap' : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
             → {f : A → B}
             → (∀ {a b} → R a b → Star S (f a) (f b))
             → ∀ {a b} → StarSym R a b → StarSym S (f a) (f b)
  concatMap' g = Star.concat ∘ Star.map (into ∘ Sym.map g)

open StarSym public using (StarSym)

--------------------------------------------------------------------------------------------------
-- Relations
--------------------------------------------------------------------------------------------------

module Relations where
  infix 3 _||_
  -- Here are some lemmas about confluence
  record CommonReduct' {la lb lc r s} {A : Set la} {B : Set lb} {C : Set lc}
                       (R : A → C → Set r) (S : B → C → Set s)
                       (a : A) (b : B) : Set (la ⊔ lb ⊔ lc ⊔ r ⊔ s) where
    constructor _||_
    field {c} : C
    field reduce₁ : R a c
    field reduce₂ : S b c

  GenConfluent : ∀ {a r s t u} {A : Set a} (R : Rel A r) (S : Rel A s) (T : Rel A t) (U : Rel A u)
               → Set (a ⊔ r ⊔ s ⊔ t ⊔ u)
  GenConfluent R S T U = ∀ {a b c} → R a b → S a c → CommonReduct' T U b c
  
  Confluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  Confluent R = GenConfluent R R R R
  
  LocalConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  LocalConfluent R = GenConfluent R R (Star R) (Star R)
  
  ReflConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  ReflConfluent R = GenConfluent R R (Refl R) (Refl R)
  
  SemiConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  SemiConfluent R = GenConfluent R (Star R) (Star R) (Star R)
  
  GlobalConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  GlobalConfluent R = Confluent (Star R)
  
  --StrongConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  --StrongConfluent R = GenConfluent R R (Star R) (MaybeRel R)
  
  module CommonReduct where
    CommonReduct : ∀ {a r} {A : Set a} (R : Rel A r) → Rel A (a ⊔ r)
    CommonReduct R = CommonReduct' R R
    
    maps : ∀ {a b r s} {A : Set a} {B : Set b} {R : Rel A r} {S : Rel B s}
         → {f g h : A → B}
         → (∀ {u v} → R u v → S (f u) (h v))
         → (∀ {u v} → R u v → S (g u) (h v))
         → (∀ {u v} → CommonReduct R u v → CommonReduct S (f u) (g v))
    maps f g (u || v) = f u || g v
    
    map : ∀ {a b r s} {A : Set a} {B : Set b} {R : Rel A r} {S : Rel B s}
        → {f : A → B}
        → (R =[ f ]⇒ S) → (CommonReduct R =[ f ]⇒ CommonReduct S)
    map g (u || v) = g u || g v
  
    zip : ∀ {a b c r s t} {A : Set a} {B : Set b} {C : Set c} {R : Rel A r} {S : Rel B s} {T : Rel C t}
        → {f : A → B → C}
        → (f Preserves₂ R ⟶ S ⟶ T)
        → (f Preserves₂ CommonReduct R ⟶ CommonReduct S ⟶ CommonReduct T)
    zip f (ac || bc) (df || ef) = f ac df || f bc ef

    swap : ∀ {a r} {A : Set a} {R : Rel A r}
         → ∀ {x y} → CommonReduct R x y → CommonReduct R y x
    swap (u || v) = v || u

  open CommonReduct public using (CommonReduct)
  module CR = CommonReduct
  
  -- semi confluence implies confluence for R*
  SemiConfluent-to-GlobalConfluent : ∀ {a r A} {R : Rel {a} A r} → SemiConfluent R → GlobalConfluent R
  SemiConfluent-to-GlobalConfluent conf ε ab = ab || ε
  SemiConfluent-to-GlobalConfluent conf ab ε = ε || ab
  SemiConfluent-to-GlobalConfluent conf (ab ◅ bc) ad with conf ab ad
  ... | be || de with SemiConfluent-to-GlobalConfluent conf bc be
  ...   | cf || ef = cf || (de ◅◅ ef)

  -- note: could be weakened to require StrongConfluent
  Confluent-to-SemiConfluent : ∀ {a r A} {R : Rel {a} A r} → Confluent R → SemiConfluent R
  Confluent-to-SemiConfluent conf ab ε = ε || (ab ◅ ε)
  Confluent-to-SemiConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ce with Confluent-to-SemiConfluent conf ce cd
  ...   | ef || df = be ◅ ef || df
  
  ReflConfluent-to-SemiConfluent : ∀ {a r A} {R : Rel {a} A r} → ReflConfluent R → SemiConfluent R
  ReflConfluent-to-SemiConfluent conf ab ε = ε || (ab ◅ ε)
  ReflConfluent-to-SemiConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ε = be ?◅ cd || ε
  ... | be || ce ◅ε with ReflConfluent-to-SemiConfluent conf ce cd
  ...   | ef || df = be ?◅ ef || df

  Confluent-Star : ∀ {a r A} {R : Rel {a} A r} → Confluent R → GlobalConfluent R
  Confluent-Star = SemiConfluent-to-GlobalConfluent ∘ Confluent-to-SemiConfluent
  
  from-StarSym : ∀ {a r A} {R : Rel {a} A r} → GlobalConfluent R → Star (Sym R) ⇒ CommonReduct (Star R)
  from-StarSym conf ε = ε || ε
  from-StarSym conf (fwd ab ◅ bc) with from-StarSym conf bc
  ... | bd || cd = ab ◅ bd || cd
  from-StarSym conf (bwd ba ◅ bc) with from-StarSym conf bc
  ... | bd || cd with conf (ba ◅ ε) bd
  ...   | be || de = be || cd ◅◅ de

open Relations public

--------------------------------------------------------------------------------
-- Empty relation
--------------------------------------------------------------------------------

module Empty {a} {A : Set a} where
  Empty : Rel A Level.zero
  Empty _ _ = ⊥
  confluent : Confluent Empty
  confluent ()