Instantly share code, notes, and snippets.

# twanvl/2013-11-13-confluence-problem.agda

Created November 13, 2013 18:01
Show Gist options
• Save twanvl/7453495 to your computer and use it in GitHub Desktop.
Proof of the open problem in section 7 of "Pure Subtype Systems" by DeLesley S. Hutchins.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 -- 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 ()
to join this conversation on GitHub. Already have an account? Sign in to comment