New proof of confluence thing (see https://gist.github.com/twanvl/7453495), which will hopefully also extend to lambda calculus.

2013-12-20-confluence-problem-v2.agda

module 2013-12-20-confluence-problem-v2 where

open import 2013-12-20-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

--------------------------------------------------------------------------------------------------
-- Inverse d step based solution
--------------------------------------------------------------------------------------------------

module InverseBased where
  -- Step with inverse d reduction
  -- this doesn't matter when it is used in a symmetric transitive closure
  data IStep : Rel₀ V where
    aca     : IStep (`A) (`C `A)
    d       : ∀ {a} → IStep a (`D a a)
    under-c : ∀ {a a'} → (x : IStep a a') → IStep (`C a) (`C a')
    under-d : ∀ {a b a' b'} → (x : IStep a a') → (y : IStep b b') → IStep (`D a b) (`D a' b')
    ε       : ∀ {a} → IStep a a
  
  iunder-ds : ∀ {a b a' b'} → (x : StarSym IStep a a') → (y : StarSym IStep b b') → StarSym IStep (`D a b) (`D a' b')
  iunder-ds {a} {b} {a'} {b'} xs ys =
    StarSym.map (\x → under-d x ε) xs ◅◅
    StarSym.map (\y → under-d ε y) ys

  iconfluent : Confluent IStep
  iconfluent ε u = u || ε
  iconfluent x ε = ε || x
  iconfluent x d = d || under-d x x
  iconfluent d u = under-d u u || d
  iconfluent aca aca = ε || ε
  iconfluent (under-c x) (under-c u) = CR.map under-c (iconfluent x u)
  iconfluent (under-d x y) (under-d u v) = CR.zip under-d (iconfluent x u) (iconfluent y v)

  a-to-is : _⟶_ ⇒ StarSym IStep
  as-to-is : StarSym _⟶_ ⇒ StarSym IStep
  a-to-is aca = fwd aca ◅ ε
  a-to-is (d₁ eq) = iunder-ds ε (StarSym.sym $ as-to-is eq) ◅◅ bwd d ◅ ε
  a-to-is (d₂ eq) = iunder-ds (as-to-is eq) ε ◅◅ bwd d ◅ ε
  a-to-is (under-c x) = StarSym.map under-c (a-to-is x)
  a-to-is (under-d₁ x) = iunder-ds (a-to-is x) ε
  a-to-is (under-d₂ x) = iunder-ds ε (a-to-is x)
  --as-to-is = StarSym.concatMap a-to-is -- doesn't pass termination checker
  as-to-is ε = ε
  as-to-is (fwd x ◅ xs) = a-to-is x ◅◅ as-to-is xs
  as-to-is (bwd x ◅ xs) = StarSym.sym (a-to-is x) ◅◅ as-to-is xs

  i-to-as : IStep ⇒ StarSym _⟶_
  i-to-as aca = fwd aca ◅ ε
  i-to-as d = bwd (d₁ ε) ◅ ε
  i-to-as (under-c x) = StarSym.map under-c (i-to-as x)
  i-to-as (under-d x y) = StarSym.map under-d₁ (i-to-as x) ◅◅ StarSym.map under-d₂ (i-to-as y)
  i-to-as ε = ε

  -- We can use IStep as a condition for steps
  -- note that we only need d₁
  data BStep : Rel₀ V where
    aca     : BStep (`A) (`C `A)
    d₁      : ∀ {a b} → StarSym IStep a b → BStep (`D a b) a
    under-c : ∀ {a a'} → (x : BStep a a') → BStep (`C a) (`C a')
    under-d : ∀ {a b a' b'} → (x : BStep a a') → (y : BStep b b') → BStep (`D a b) (`D a' b')
    ε       : ∀ {a} → BStep a a

  bunder-ds : ∀ {a b a' b'} → (x : Star BStep a a') → (y : Star BStep b b') → Star BStep (`D a b) (`D a' b')
  bunder-ds {a} {b} {a'} {b'} xs ys =
    Star.map (\x → under-d {b = b}  x ε) xs ◅◅
    Star.map (\y → under-d {a = a'} ε y) ys
  
  b-to-is : BStep ⇒ StarSym IStep
  b-to-is aca = fwd aca ◅ ε
  b-to-is (d₁ x) = StarSym.map (under-d ε) (StarSym.sym x) ◅◅ bwd d ◅ ε
  b-to-is (under-c x) = StarSym.map under-c (b-to-is x)
  b-to-is (under-d {b' = b'} x y) = iunder-ds (b-to-is x) (b-to-is y)
  b-to-is ε = ε

  bconfluent : Confluent BStep
  bconfluent ε u = u || ε
  bconfluent x ε = ε || x
  bconfluent aca aca = ε || ε
  bconfluent (under-c x) (under-c u) = CR.map under-c (bconfluent x u)
  bconfluent (d₁ x) (d₁ u) = ε || ε
  bconfluent (d₁ x) (under-d u v) = u || d₁ (StarSym.sym (b-to-is u) ◅◅ x ◅◅ b-to-is v)
  bconfluent (under-d x y) (d₁ u) = d₁ (StarSym.sym (b-to-is x) ◅◅ u ◅◅ b-to-is y) || x
  bconfluent (under-d x y) (under-d u v) = CR.zip under-d (bconfluent x u) (bconfluent y v)

  i-to-bs : IStep ⇒ CommonReduct (Star BStep)
  i-to-bs aca = aca ◅ ε || ε
  i-to-bs d = ε || d₁ ε ◅ ε
  i-to-bs (under-c x) with i-to-bs x
  ... | u || v = Star.map under-c u || Star.map under-c v
  i-to-bs (under-d x y) with i-to-bs x | i-to-bs y
  ... | u || v | p || q = bunder-ds u p || bunder-ds v q
  i-to-bs ε = ε || ε

  is-to-bs : StarSym IStep ⇒ CommonReduct (Star BStep)
  is-to-bs ε = ε || ε
  is-to-bs (fwd ab ◅ bc) with i-to-bs ab | is-to-bs bc
  ... | ad || bd | be || ce with Confluent-Star bconfluent bd be
  ... | df || ef = ad ◅◅ df || ce ◅◅ ef
  is-to-bs (bwd ba ◅ bc) with i-to-bs ba | is-to-bs bc
  ... | bd || ad | be || ce with Confluent-Star bconfluent bd be
  ... | df || ef = ad ◅◅ df || ce ◅◅ ef

  b-to-as : BStep ⇒ Star _⟶_
  b-to-as aca = aca ◅ ε
  b-to-as (d₁ x) = d₁ (StarSym.concatMap i-to-as x) ◅ ε
  b-to-as (under-c x) = Star.map under-c (b-to-as x)
  b-to-as (under-d x y) = Star.map under-d₁ (b-to-as x) ◅◅ Star.map under-d₂ (b-to-as y)
  b-to-as ε = ε

  aconfluent : GlobalConfluent _⟶_
  aconfluent ab ac with is-to-bs (Star.concatMap a-to-is ab) | is-to-bs (Star.concatMap a-to-is ac)
  ... | ad || bd | ae || ce with Confluent-Star bconfluent ad ae
  ... | df || ef = Star.concatMap b-to-as (bd ◅◅ df) || Star.concatMap b-to-as (ce ◅◅ ef)

2013-12-20-relations.agda

module 2013-12-20-relations where

open import Level hiding (zero;suc)
open import Function
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Empty
open import Data.Product using (∃)
open import Induction.WellFounded

--------------------------------------------------------------------------------
-- 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

Any : ∀ {a b r} {A : Set a} {B : Set b} → (A → Rel B r) → Rel B _
Any r u v = ∃ \x → r x u v

--------------------------------------------------------------------------------
-- 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;_◅_;_◅◅_;ε;_⋆)

--------------------------------------------------------------------------------
-- Non-Reflexive Transitive closure
--------------------------------------------------------------------------------

module Plus where
  data Plus {l r} {A : Set l} (R : Rel A r) (a : A) (c : A) : Set (l ⊔ r) where
    _◅_ : ∀ {b} → R a b → Star R b c → Plus R a c

  plus-acc : ∀ {l} {A : Set l} {R : Rel A l} {x} → Acc (flip R) x → Acc (flip (Plus R)) x
  plus-acc' : ∀ {l} {A : Set l} {R : Rel A l} {x y} → Acc (flip R) x → Plus R x y → Acc (flip (Plus R)) y
  star-acc' : ∀ {l} {A : Set l} {R : Rel A l} {x y} → Acc (flip R) x → Star R x y → Acc (flip (Plus R)) y
  plus-acc a = acc (\_ → plus-acc' a)
  plus-acc' (acc a) (ab ◅ bc) = star-acc' (a _ ab) bc
  star-acc' a ε = plus-acc a
  star-acc' (acc a) (ab ◅ bc) = star-acc' (a _ ab) bc
  
  well-founded : ∀ {l} {A : Set l} {R : Rel A l} → Well-founded (flip R) → Well-founded (flip (Plus R))
  well-founded wf = plus-acc ∘ wf

open Plus public using (Plus;_◅_)

--------------------------------------------------------------------------------
-- 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 ◅ε

  fromRefl : ∀ {a A r} {R : Rel {a} A r} → Reflexive R → Refl R ⇒ R
  fromRefl refl ε = refl
  fromRefl refl (x ◅ε) = x

open Refl public hiding (module Refl;map)

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

module Sym where
  data CoSym {l r s} {A : Set l} (R : Rel A r) (S : Rel A s) (a : A) : A → Set (l ⊔ r ⊔ s) where
    fwd : ∀ {b} → R a b → CoSym R S a b
    bwd : ∀ {b} → S b a → CoSym R S a b
  
  Sym : ∀ {l r} {A : Set l} (R : Rel A r) (a : A) → A → Set (l ⊔ r)
  Sym R = CoSym R R

  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 (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)

  sym :  ∀ {l r A R} → StarSym {l} {r} {A} R ⇒ flip (StarSym R)
  sym = Star.reverse Sym.sym

  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) = 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
  -- Here are some lemmas about confluence
  -- First the generic stuff
  infix 3 _||_
  record CommonReduct' {la lb lc r s} {A : Set la} {B : Set lb} {C : Set lc}
                       (R : REL A C r) (S : REL B C 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

  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 c d e f r s t u} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e} {F : Set f}
              {R : REL A C r} {S : REL B C s} {T : REL D F t} {U : REL E F u}
              {f : A → D} {g : B → E} {h : C → F}
         → (∀ {u v} → R u v → T (f u) (h v))
         → (∀ {u v} → S u v → U (g u) (h v))
         → (∀ {u v} → CommonReduct' R S u v → CommonReduct' T U (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 S : Rel A r}
         → ∀ {x y} → CommonReduct' R S x y → CommonReduct' S R y x
    swap (u || v) = v || u

  open CommonReduct public using (CommonReduct)
  module CR = CommonReduct
  
  
  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
  
  -- With two relations
  CoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  CoConfluent R S = GenConfluent R S S R
  
  SemiCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  SemiCoConfluent R S = GenConfluent R (Star S) (Star S) (Star R)
  
  HalfCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  HalfCoConfluent R S = GenConfluent R S (Star S) R
  
  StrongCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  StrongCoConfluent R S = GenConfluent R (Star S) (Star S) (Refl R)
  
  StrongerCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  StrongerCoConfluent R S = GenConfluent R (Star S) (Star S) R
  
  ReflCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  ReflCoConfluent R S = GenConfluent R S (Refl S) (Refl R)
  
  GlobalCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  GlobalCoConfluent R S = CoConfluent (Star R) (Star S)
  
  -- Now with a single relation
  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)
  
  -- semi confluence implies confluence for R*
  SemiConfluent-to-GlobalConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → SemiCoConfluent R S → GlobalCoConfluent R S
  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)

  Confluent-to-StrongConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → StrongCoConfluent R S
  Confluent-to-StrongConfluent conf ab ε = ε || (ab ◅ε)
  Confluent-to-StrongConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ce with Confluent-to-StrongConfluent conf ce cd
  ...   | ef || df = be ◅ ef || df

  Confluent-to-StrongerConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → StrongerCoConfluent R S
  Confluent-to-StrongerConfluent conf ab ε = ε || ab
  Confluent-to-StrongerConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ce with Confluent-to-StrongerConfluent conf ce cd
  ...   | ef || df = be ◅ ef || df

  HalfConfluent-to-StrongerConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → HalfCoConfluent R S → StrongerCoConfluent R S
  HalfConfluent-to-StrongerConfluent conf ab ε = ε || ab
  HalfConfluent-to-StrongerConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ce with HalfConfluent-to-StrongerConfluent conf ce cd
  ...   | ef || df = be ◅◅ ef || df

  -- note: could be weakened to require StrongConfluent
  Confluent-to-SemiConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → SemiCoConfluent R S
  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 s A} {R : Rel {a} A r} {S : Rel {a} A s} → ReflCoConfluent R S → SemiCoConfluent R S
  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 s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → GlobalCoConfluent R S
  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

  to-StarSym : ∀ {a r A} {R : Rel {a} A r} → CommonReduct (Star R) ⇒ Star (Sym R)
  to-StarSym (xs || ys) = Star.map fwd xs ◅◅ Star.reverse bwd ys

  -- strong normalization + local confluence implies global confluence
  -- we can write SN R as Well-founded (flip R)
  well-founded-confluent : ∀ {a A} {R : Rel {a} A a} → Well-founded (flip R) → LocalConfluent R → GlobalConfluent R
  well-founded-confluent wf conf = acc-confluent conf (Plus.well-founded wf _)
    where
    acc-confluent : ∀ {a A} {R : Rel {a} A a} → LocalConfluent R → ∀ {a b c} → Acc (flip (Plus R)) a → Star R a b → Star R a c → CommonReduct (Star R) b c
    acc-confluent conf _ ε ac = ac || ε
    acc-confluent conf _ ab ε = ε || ab
    acc-confluent conf (acc a) (ab ◅ bc) (ad ◅ de) with conf ab ad
    ... | bf || df with acc-confluent conf (a _ (ab ◅ ε)) bc bf
    ... | cg || fg with acc-confluent conf (a _ (ad ◅ ε)) de df
    ... | eh || fh with acc-confluent conf (a _ (ab ◅ bf)) fg fh
    ... | gi || hi = cg ◅◅ gi || eh ◅◅ hi

  confluent-by : ∀ {a A r s} {R : Rel {a} A r} {S : Rel A s}
               → (S ⇒ R) → (R ⇒ S)
               → Confluent R → Confluent S
  confluent-by toR fromR confR ab ac = CR.map fromR (confR (toR ab) (toR ac))
  


open Relations public