commit 47c9a4a17728ea86e3cd8a6857d111b7ef6ce4e8
Author: Nathan van Doorn <nvd1234@gmail.com>
Date:   Fri Sep 13 12:35:12 2024 +0200

    Initial commit: definition of regular expression, algebraic properties of + and ;

diff --git a/regex.agda-lib b/regex.agda-lib
new file mode 100644
index 0000000..bc2a4f0
--- /dev/null
+++ b/regex.agda-lib
@@ -0,0 +1,3 @@
+name: regex
+depend: standard-library-2.2
+include: src
diff --git a/src/Regex.agda b/src/Regex.agda
new file mode 100644
index 0000000..2362de1
--- /dev/null
+++ b/src/Regex.agda
@@ -0,0 +1,101 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Data.Nat.Base hiding (_+_)
+
+module Regex (α : ℕ) where
+
+import Algebra.Definitions
+open import Algebra.Structures
+open import Data.Bool.Base
+open import Data.Fin.Base using (Fin)
+open import Data.Fin.Properties using (_≟_)
+open import Data.List.Base
+open import Data.Product.Base
+open import Data.Sum.Base
+open import Function.Base
+open import Relation.Nullary
+open import Relation.Unary
+open import Relation.Binary hiding (Decidable)
+
+-- Note: we do not define negation or intersections.
+-- These can be derived, but only by a double-exponential blow-up in space.
+-- So in the future we should consider adding them.
+data Regex : Set where
+  -- Do not recognize any strings
+  Λ : Regex
+  -- Union
+  _+_ : Regex → Regex → Regex
+  -- Sequencing: first one, and then the other
+  _⨟_ : Regex → Regex → Regex
+  -- Kleene star
+  _⋆ : Regex → Regex
+  -- Recognize a single character
+  ⁅_⁆ : Fin α → Regex
+
+ε : Regex
+ε = Λ ⋆
+
+-- Do we accept the empty string?
+data A : Regex → Set where
+  +ₗ : ∀ {r₁ r₂} → A r₁ → A (r₁ + r₂)
+  +ᵣ : ∀ {r₁ r₂} → A r₂ → A (r₁ + r₂)
+  _⨟_ : ∀ {r₁ r₂} → A r₁ → A r₂ → A (r₁ ⨟ r₂)
+  star : ∀ {r} → A (r ⋆)
+
+-- ε accepts the empty string
+Aε : A ε
+Aε = star
+
+-- A is decidable!
+A? : Decidable A
+A? Λ = no λ ()
+A? (r₁ + r₂) = map′
+  [ +ₗ , +ᵣ ]′
+  (λ { (+ₗ Ar₁) → inj₁ Ar₁
+     ; (+ᵣ Ar₂) → inj₂ Ar₂
+     }
+  )
+  (A? r₁ ⊎-dec A? r₂)
+A? (r₁ ⨟ r₂) = map′
+  (uncurry _⨟_)
+  (λ { (Ar₁ ⨟ Ar₂) → Ar₁ , Ar₂})
+  (A? r₁ ×-dec A? r₂)
+A? (r ⋆) = yes star
+A? ⁅ x ⁆ = no λ ()
+
+-- Take the Brzozowski derivative of a regular expression by a
+-- character
+δ : Regex → Fin α → Regex
+δ Λ i = Λ
+δ (r₁ + r₂) i = δ r₁ i + δ r₂ i
+δ (r₁ ⨟ r₂) i = if does (A? r₁)
+  then δ r₂ i + (δ r₁ i ⨟ r₂)
+  else (δ r₁ i ⨟ r₂)
+δ (r ⋆) i = δ r i ⨟ (r ⋆)
+δ ⁅ x ⁆ i = if does (x ≟ i) then ε else Λ
+
+-- Take the Brzozowski derivative of a regular expression by a
+-- string of characters
+δ⋆ : Regex → List (Fin α) → Regex
+δ⋆ = foldl δ
+
+-- Whether a regular expression expresses a particular string
+Accepts : Regex → List (Fin α) → Set
+Accepts r as = A (δ⋆ r as)
+
+-- Accepts is decidable!
+Accepts? : ∀ r as → Dec (Accepts r as)
+Accepts? r as = A? (δ⋆ r as)
+
+------------------------------------------------------------------------
+-- Relations on regeces
+
+_⊑_ : Rel Regex _
+r₁ ⊑ r₂ = ∀ as → Accepts r₁ as → Accepts r₂ as
+
+_⊒_ : Rel Regex _
+r₁ ⊒ r₂ = r₂ ⊑ r₁
+
+_≈_ : Rel Regex _
+r₁ ≈ r₂ = (r₁ ⊑ r₂) × (r₁ ⊒ r₂)
+
diff --git a/src/Regex/Properties.agda b/src/Regex/Properties.agda
new file mode 100644
index 0000000..46e9426
--- /dev/null
+++ b/src/Regex/Properties.agda
@@ -0,0 +1,146 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Data.Nat.Base using (ℕ)
+
+module Regex.Properties (α : ℕ) where
+
+open import Regex α
+import Regex.Properties.Sub α as ⊑
+import Regex.Properties.Super α as ⊒
+
+open import Algebra.Definitions _≈_
+open import Algebra.Structures _≈_
+open import Data.Product.Base using (_,_)
+open import Relation.Binary
+
+------------------------------------------------------------------------
+-- General properties
+
+≈-refl : Reflexive _≈_
+≈-refl = ⊑.refl , ⊒.refl
+
+≈-sym : Symmetric _≈_
+≈-sym (p , q) = q , p
+
+≈-trans : Transitive _≈_
+≈-trans (p , q) (r , s) = ⊑.trans p r , ⊒.trans q s
+
+≈-isEquivalence : IsEquivalence _≈_
+≈-isEquivalence = record
+  { refl = ≈-refl
+  ; sym = ≈-sym
+  ; trans = ≈-trans
+  }
+
+setoid : Setoid _ _
+setoid = record { isEquivalence = ≈-isEquivalence }
+
+------------------------------------------------------------------------
+-- Algebraic properties
+
+-- Properties of _+_
+
++-cong : Congruent₂ _+_
++-cong (x⊑y , x⊒y) (u⊑v , u⊒v) = ⊑.+-cong x⊑y u⊑v , ⊒.+-cong x⊒y u⊒v
+
++-assoc : Associative _+_
++-assoc r₁ r₂ r₃ = ⊑.+-assoc r₁ r₂ r₃ , ⊒.+-assoc r₁ r₂ r₃
+
++-comm : Commutative _+_
++-comm r₁ r₂ = ⊑.+-comm r₁ r₂ , ⊒.+-comm r₁ r₂
+
++-idem : Idempotent _+_
++-idem r = ⊑.+-idem r , ⊒.+-idem r
+
++-identityˡ : LeftIdentity Λ _+_
++-identityˡ r = ⊑.+-identityˡ r , ⊒.+-identityˡ r
+
++-identityʳ : RightIdentity Λ _+_
++-identityʳ r = ⊑.+-identityʳ r , ⊒.+-identityʳ r
+
++-identity : Identity Λ _+_
++-identity = +-identityˡ , +-identityʳ
+
+-- Properties of _⨟_
+
+⨟-cong : Congruent₂ _⨟_
+⨟-cong (x⊑y , x⊒y) (u⊑v , u⊒v) = ⊑.⨟-cong x⊑y u⊑v , ⊒.⨟-cong x⊒y u⊒v
+
+⨟-distribˡ-+ : _⨟_ DistributesOverˡ _+_
+⨟-distribˡ-+ r₁ r₂ r₃ = ⊑.⨟-distribˡ-+ r₁ r₂ r₃ , ⊒.⨟-distribˡ-+ r₁ r₂ r₃
+
+⨟-distribʳ-+ : _⨟_ DistributesOverʳ _+_
+⨟-distribʳ-+ r₁ r₂ r₃ = ⊑.⨟-distribʳ-+ r₁ r₂ r₃ , ⊒.⨟-distribʳ-+ r₁ r₂ r₃
+
+⨟-distrib-+ : _⨟_ DistributesOver _+_
+⨟-distrib-+ = ⨟-distribˡ-+ , ⨟-distribʳ-+
+
+⨟-assoc : Associative _⨟_
+⨟-assoc r₁ r₂ r₃ = ⊑.⨟-assoc r₁ r₂ r₃ , ⊒.⨟-assoc r₁ r₂ r₃
+
+⨟-zeroˡ : LeftZero Λ _⨟_
+⨟-zeroˡ r = ⊑.⨟-zeroˡ r , ⊒.⨟-zeroˡ r
+
+⨟-zeroʳ : RightZero Λ _⨟_
+⨟-zeroʳ r = ⊑.⨟-zeroʳ r , ⊒.⨟-zeroʳ r
+
+⨟-zero : Zero Λ _⨟_
+⨟-zero = ⨟-zeroˡ , ⨟-zeroʳ
+
+⨟-identityˡ : LeftIdentity ε _⨟_
+⨟-identityˡ r = ⊑.⨟-identityˡ r , ⊒.⨟-identityˡ r
+
+⨟-identityʳ : RightIdentity ε _⨟_
+⨟-identityʳ r = ⊑.⨟-identityʳ r , ⊒.⨟-identityʳ r
+
+⨟-identity : Identity ε _⨟_
+⨟-identity = ⨟-identityˡ , ⨟-identityʳ
+
+------------------------------------------------------------------------
+-- Algebraic structures
+
++-isMagma : IsMagma _+_
++-isMagma = record
+  { isEquivalence = ≈-isEquivalence
+  ; ∙-cong = +-cong
+  }
+
++-isSemigroup : IsSemigroup _+_
++-isSemigroup = record
+  { isMagma = +-isMagma
+  ; assoc = +-assoc
+  }
+
++-isMonoid : IsMonoid _+_ Λ
++-isMonoid = record
+  { isSemigroup = +-isSemigroup
+  ; identity = +-identity
+  }
+
++-isCommutativeMonoid : IsCommutativeMonoid _+_ Λ
++-isCommutativeMonoid = record
+  { isMonoid = +-isMonoid
+  ; comm = +-comm
+  }
+
++-⨟-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _+_ _⨟_ Λ ε
++-⨟-isSemiringWithoutAnnihilatingZero = record
+  { +-isCommutativeMonoid = +-isCommutativeMonoid
+  ; *-cong = ⨟-cong
+  ; *-assoc = ⨟-assoc
+  ; *-identity = ⨟-identity
+  ; distrib = ⨟-distrib-+
+  }
+
++-⨟-isSemiring : IsSemiring _+_ _⨟_ Λ ε
++-⨟-isSemiring = record
+  { isSemiringWithoutAnnihilatingZero = +-⨟-isSemiringWithoutAnnihilatingZero
+  ; zero = ⨟-zero
+  }
+
++-⨟-isIdempotentSemiring : IsIdempotentSemiring _+_ _⨟_ Λ ε
++-⨟-isIdempotentSemiring = record
+  { isSemiring = +-⨟-isSemiring
+  ; +-idem = +-idem
+  }
+
diff --git a/src/Regex/Properties/Core.agda b/src/Regex/Properties/Core.agda
new file mode 100644
index 0000000..d4dd3ef
--- /dev/null
+++ b/src/Regex/Properties/Core.agda
@@ -0,0 +1,31 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Data.Nat.Base using (ℕ)
+
+module Regex.Properties.Core (α : ℕ) where
+
+open import Regex α
+
+open import Data.List.Base using ([]; _∷_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary.Negation.Core using (¬_)
+
+-- Λ does not accept any string
+end : ∀ as → ¬ Accepts Λ as
+end [] ()
+end (a ∷ as) p = end as p
+
+split : ∀ {r₁ r₂} as → Accepts (r₁ + r₂) as → Accepts r₁ as ⊎ Accepts r₂ as
+split [] (+ₗ p) = inj₁ p
+split [] (+ᵣ p) = inj₂ p
+split (a ∷ as) p = split as p
+
+join₁ : ∀ {r₁ r₂} as → Accepts r₁ as → Accepts (r₁ + r₂) as
+join₁ [] p = +ₗ p
+join₁ (a ∷ as) p = join₁ as p
+
+join₂ : ∀ {r₁ r₂} as → Accepts r₂ as → Accepts (r₁ + r₂) as
+join₂ [] p = +ᵣ p
+join₂ (a ∷ as) p = join₂ as p
+
+
diff --git a/src/Regex/Properties/Sub.agda b/src/Regex/Properties/Sub.agda
new file mode 100644
index 0000000..6ea6589
--- /dev/null
+++ b/src/Regex/Properties/Sub.agda
@@ -0,0 +1,153 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Data.Nat.Base using (ℕ)
+
+module Regex.Properties.Sub (α : ℕ) where
+
+open import Regex α
+open import Regex.Properties.Core α
+
+open import Algebra.Definitions _⊑_
+open import Data.List.Base using ([]; _∷_)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Relation.Binary.Definitions
+open import Relation.Nullary.Decidable.Core using (no; yes)
+open import Relation.Nullary.Negation.Core using (contradiction)
+
+------------------------------------------------------------------------
+-- General properties
+
+refl : Reflexive _⊑_
+refl as p = p
+
+trans : Transitive _⊑_
+trans x y as p = y as (x as p)
+
+------------------------------------------------------------------------
+-- Algebraic properties
+
+-- Properties of _+_
+
++-cong : Congruent₂ _+_
++-cong x⊑y u⊑v as p with split as p
+... | inj₁ p′ = join₁ as (x⊑y as p′)
+... | inj₂ p′ = join₂ as (u⊑v as p′)
+
++-congˡ : LeftCongruent _+_
++-congˡ x⊑y = +-cong refl x⊑y
+
++-congʳ : RightCongruent _+_
++-congʳ x⊑y = +-cong x⊑y refl
+
++-assoc : Associative _+_
++-assoc r₁ r₂ r₃ [] (+ₗ (+ₗ p)) = +ₗ p
++-assoc r₁ r₂ r₃ [] (+ₗ (+ᵣ p)) = +ᵣ (+ₗ p)
++-assoc r₁ r₂ r₃ [] (+ᵣ p) = +ᵣ (+ᵣ p)
++-assoc r₁ r₂ r₃ (a ∷ as) p = +-assoc _ _ _ as p
+
++-comm : Commutative _+_
++-comm r₁ r₂ [] (+ₗ p) = +ᵣ p
++-comm r₁ r₂ [] (+ᵣ p) = +ₗ p
++-comm r₁ r₂ (a ∷ as) p = +-comm _ _ as p
+
++-idem : Idempotent _+_
++-idem r [] (+ₗ p) = p
++-idem r [] (+ᵣ p) = p
++-idem r (a ∷ as) p = +-idem _ as p
+
++-identityˡ : LeftIdentity Λ _+_
++-identityˡ r [] (+ᵣ p) = p
++-identityˡ r (a ∷ as) p = +-identityˡ _ as p
+
++-identityʳ : RightIdentity Λ _+_
++-identityʳ r [] (+ₗ p) = p
++-identityʳ r (a ∷ as) p = +-identityʳ _ as p
+
+-- Properties of _⨟_
+
+⨟-cong : Congruent₂ _⨟_
+⨟-cong x⊑y u⊑v [] (p₁ ⨟ p₂) = x⊑y [] p₁ ⨟ u⊑v [] p₂
+⨟-cong {x = x} {y = y} x⊑y u⊑v (a ∷ as) p with A? x | A? y
+... | no ¬Ax | no ¬Ay = ⨟-cong (λ as′ → x⊑y (a ∷ as′)) u⊑v as p
+... | no ¬Ax | yes Ay = join₂ as (⨟-cong (λ as′ → x⊑y (a ∷ as′)) u⊑v as p)
+... | yes Ax | no ¬Ay = contradiction (x⊑y [] Ax) ¬Ay
+... | yes Ax | yes Ay with split as p
+... | inj₁ p′ = join₁ as (u⊑v (a ∷ as) p′)
+... | inj₂ p′ = join₂ as (⨟-cong (λ as′ → x⊑y (a ∷ as′)) u⊑v as p′)
+
+⨟-congʳ : RightCongruent _⨟_
+⨟-congʳ x⊑y = ⨟-cong x⊑y refl
+
+⨟-distribˡ-+ : _⨟_ DistributesOverˡ _+_
+⨟-distribˡ-+ r₁ r₂ r₃ [] (p₁ ⨟ +ₗ p₂) = +ₗ (p₁ ⨟ p₂)
+⨟-distribˡ-+ r₁ r₂ r₃ [] (p₁ ⨟ +ᵣ p₂) = +ᵣ (p₁ ⨟ p₂)
+⨟-distribˡ-+ r₁ r₂ r₃ (a ∷ as) p with A? r₁
+... | no ¬Ar₁ = ⨟-distribˡ-+ _ _ _ as p
+... | yes Ar₁ with split as p
+... | inj₁ p′ with split as p′
+... | inj₁ p″ = join₁ as (join₁ as p″)
+... | inj₂ p″ = join₂ as (join₁ as p″)
+⨟-distribˡ-+ r₁ r₂ r₃ (a ∷ as) p | yes Ar₁ | inj₂ p′ with split as (⨟-distribˡ-+ _ _ _ as p′)
+... | inj₁ p″ = join₁ as (join₂ as p″)
+... | inj₂ p″ = join₂ as (join₂ as p″)
+
+⨟-distribʳ-+ : _⨟_ DistributesOverʳ _+_
+⨟-distribʳ-+ r₁ r₂ r₃ [] (+ₗ p₁ ⨟ p₂) = +ₗ (p₁ ⨟ p₂)
+⨟-distribʳ-+ r₁ r₂ r₃ [] (+ᵣ p₁ ⨟ p₂) = +ᵣ (p₁ ⨟ p₂)
+⨟-distribʳ-+ r₁ r₂ r₃ (a ∷ as) p with A? r₂ | A? r₃
+... | no ¬Ar₂ | no ¬Ar₃ = ⨟-distribʳ-+ r₁ (δ r₂ a) (δ r₃ a) as p
+... | no ¬Ar₂ | yes Ar₃ with split as p
+... | inj₁ p′ = join₂ as (join₁ as p′)
+... | inj₂ p′ with split as (⨟-distribʳ-+ r₁ _ _ as p′)
+... | inj₁ p″ = join₁ as p″
+... | inj₂ p″ = join₂ as (join₂ as p″)
+⨟-distribʳ-+ r₁ r₂ r₃ (a ∷ as) p | yes Ar₂ | no ¬Ar₃ with split as p
+... | inj₁ p′ = join₁ as (join₁ as p′)
+... | inj₂ p′ with split as (⨟-distribʳ-+ r₁ (δ r₂ a) (δ r₃ a) as p′)
+... | inj₁ p″ = join₁ as (join₂ as p″)
+... | inj₂ p″ = join₂ as p″
+⨟-distribʳ-+ r₁ r₂ r₃ (a ∷ as) p | yes Ar₂ | yes Ar₃ with split as p
+... | inj₁ p′ = join₁ as (join₁ as p′)
+... | inj₂ p′ with split as (⨟-distribʳ-+ _ _ _ as p′)
+... | inj₁ p″ = join₁ as (join₂ as p″)
+... | inj₂ p″ = join₂ as (join₂ as p″)
+
+⨟-assoc : Associative _⨟_
+⨟-assoc r₁ r₂ r₃ [] ((p₁ ⨟ p₂) ⨟ p₃) = p₁ ⨟ (p₂ ⨟ p₃)
+⨟-assoc r₁ r₂ r₃ (a ∷ as) p with A? r₁
+... | no ¬Ar₁ = ⨟-assoc (δ r₁ a) r₂ r₃ as p
+... | yes Ar₁ with A? r₂
+... | no ¬Ar₂ with split as (⨟-distribʳ-+ _ _ _ as p)
+... | inj₁ p′ = join₁ as p′
+... | inj₂ p′ = join₂ as (⨟-assoc _ _ _ as p′)
+⨟-assoc r₁ r₂ r₃ (a ∷ as) p | yes Ar₁ | yes Ar₂ with split as p
+... | inj₁ p′ = join₁ as (join₁ as p′)
+... | inj₂ p′ with split as (⨟-distribʳ-+ _ _ _ as p′)
+... | inj₁ p″ = join₁ as (join₂ as p″)
+... | inj₂ p″ = join₂ as (⨟-assoc _ _ _ as p″)
+
+⨟-zeroˡ : LeftZero Λ _⨟_
+⨟-zeroˡ r [] (() ⨟ _)
+⨟-zeroˡ r (a ∷ as) p = ⨟-zeroˡ r as p
+
+⨟-zeroʳ : RightZero Λ _⨟_
+⨟-zeroʳ r [] (p₁ ⨟ p₂) = p₂
+⨟-zeroʳ r (a ∷ as) p with A? r
+... | no ¬Ar = ⨟-zeroʳ _ as p
+... | yes Ar with split as p
+... | inj₁ p′ = p′
+... | inj₂ p′ = ⨟-zeroʳ _ as p′
+
+⨟-identityˡ : LeftIdentity ε _⨟_
+⨟-identityˡ r [] (star ⨟ p) = p
+⨟-identityˡ r (a ∷ as) p with split as p
+... | inj₁ p′ = p′
+... | inj₂ p′ = contradiction (⨟-zeroˡ _ as (⨟-assoc _ _ _ as p′)) (end as)
+
+⨟-identityʳ : RightIdentity ε _⨟_
+⨟-identityʳ r [] (p ⨟ star) = p
+⨟-identityʳ r (a ∷ as) p with A? r
+... | no ¬Ar = ⨟-identityʳ _ as p
+... | yes Ar with split as p
+... | inj₁ p′ = contradiction (⨟-zeroˡ _ as p′) (end as)
+... | inj₂ p′ = ⨟-identityʳ _ as p′
diff --git a/src/Regex/Properties/Super.agda b/src/Regex/Properties/Super.agda
new file mode 100644
index 0000000..c172a64
--- /dev/null
+++ b/src/Regex/Properties/Super.agda
@@ -0,0 +1,133 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Data.Nat.Base using (ℕ)
+
+module Regex.Properties.Super (α : ℕ) where
+
+open import Regex α
+open import Regex.Properties.Core α
+
+open import Algebra.Definitions _⊒_
+open import Data.List.Base using ([]; _∷_)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Relation.Binary.Definitions
+open import Relation.Nullary.Decidable.Core using (no; yes)
+open import Relation.Nullary.Negation.Core using (contradiction)
+
+------------------------------------------------------------------------
+-- General properties
+
+refl : Reflexive _⊒_
+refl as p = p
+
+trans : Transitive _⊒_
+trans x y as p = x as (y as p)
+
+------------------------------------------------------------------------
+-- Algebraic properties
+
++-cong : Congruent₂ _+_
++-cong x⊒y u⊒v as p with split as p
+... | inj₁ p′ = join₁ as (x⊒y as p′)
+... | inj₂ p′ = join₂ as (u⊒v as p′)
+
++-assoc : Associative _+_
++-assoc r₁ r₂ r₃ [] (+ₗ p) = +ₗ (+ₗ p)
++-assoc r₁ r₂ r₃ [] (+ᵣ (+ₗ p)) = +ₗ (+ᵣ p)
++-assoc r₁ r₂ r₃ [] (+ᵣ (+ᵣ p)) = +ᵣ p
++-assoc r₁ r₂ r₃ (a ∷ as) p = +-assoc _ _ _ as p
+
++-comm : Commutative _+_
++-comm r₁ r₂ [] (+ₗ p) = +ᵣ p
++-comm r₁ r₂ [] (+ᵣ p) = +ₗ p
++-comm r₁ r₂ (a ∷ as) p = +-comm _ _ as p
+
++-idem : Idempotent _+_
++-idem r [] p = +ₗ p -- annoyingly not unique
++-idem r (a ∷ as) p = +-idem _ as p
+
++-identityˡ : LeftIdentity Λ _+_
++-identityˡ r [] p = +ᵣ p
++-identityˡ r (a ∷ as) p = +-identityˡ _ as p
+
++-identityʳ : RightIdentity Λ _+_
++-identityʳ r [] p = +ₗ p
++-identityʳ r (a ∷ as) p = +-identityʳ _ as p
+
+⨟-cong : Congruent₂ _⨟_
+⨟-cong x⊒y u⊒v [] (p₁ ⨟ p₂) = x⊒y [] p₁ ⨟ u⊒v [] p₂
+⨟-cong {x = x} {y = y} x⊒y u⊒v (a ∷ as) p with A? x | A? y
+... | no ¬Ax | no ¬Ay = ⨟-cong (λ as′ → x⊒y (a ∷ as′)) u⊒v as p
+... | no ¬Ax | yes Ay = contradiction (x⊒y [] Ay) ¬Ax
+... | yes Ax | no ¬Ay = join₂ as (⨟-cong (λ as′ → x⊒y (a ∷ as′)) u⊒v as p)
+... | yes Ax | yes Ay with split as p
+... | inj₁ p′ = join₁ as (u⊒v (a ∷ as) p′)
+... | inj₂ p′ = join₂ as (⨟-cong (λ as′ → x⊒y (a ∷ as′)) u⊒v as p′)
+
+⨟-distribˡ-+ : _⨟_ DistributesOverˡ _+_
+⨟-distribˡ-+ r₁ r₂ r₃ [] (+ₗ (p₁ ⨟ p₂)) = p₁ ⨟ +ₗ p₂
+⨟-distribˡ-+ r₁ r₂ r₃ [] (+ᵣ (p₁ ⨟ p₂)) = p₁ ⨟ +ᵣ p₂
+⨟-distribˡ-+ r₁ r₂ r₃ (a ∷ as) p with A? r₁
+... | no ¬Ar₁ with split as p
+... | inj₁ p′ = ⨟-distribˡ-+ _ _ _ as (join₁ as p′)
+... | inj₂ p′ = ⨟-distribˡ-+ _ _ _ as (join₂ as p′)
+⨟-distribˡ-+ r₁ r₂ r₃ (a ∷ as) p | yes Ar₁ with split as p
+... | inj₁ p′ with split as p′
+... | inj₁ p″ = join₁ as (join₁ as p″)
+... | inj₂ p″ = join₂ as (⨟-distribˡ-+ _ _ _ as (join₁ as p″))
+⨟-distribˡ-+ r₁ r₂ r₃ (a ∷ as) p | yes Ar₁ | inj₂ p′ with split as p′
+... | inj₁ p″ = join₁ as (join₂ as p″)
+... | inj₂ p″ = join₂ as (⨟-distribˡ-+ _ _ _ as (join₂ as p″))
+
+⨟-distribʳ-+ : _⨟_ DistributesOverʳ _+_
+⨟-distribʳ-+ r₁ r₂ r₃ [] (+ₗ (p₁ ⨟ p₂)) = +ₗ p₁ ⨟ p₂
+⨟-distribʳ-+ r₁ r₂ r₃ [] (+ᵣ (p₁ ⨟ p₂)) = +ᵣ p₁ ⨟ p₂
+⨟-distribʳ-+ r₁ r₂ r₃ (a ∷ as) p with A? r₂ | A? r₃
+... | no ¬Ar₂ | no ¬Ar₃ = ⨟-distribʳ-+ _ _ _ as p
+... | no ¬Ar₂ | yes Ar₃ with split as p
+... | inj₁ p′ = join₂ as (⨟-distribʳ-+ _ _ _ as (join₁ as p′))
+... | inj₂ p′ with split as p′
+... | inj₁ p″ = join₁ as p″
+... | inj₂ p″ = join₂ as (⨟-distribʳ-+ _ _ _ as (join₂ as p″))
+⨟-distribʳ-+ r₁ r₂ r₃ (a ∷ as) p | yes Ar₂ | no ¬Ar₃ with split as p
+... | inj₂ p′ = join₂ as (⨟-distribʳ-+ _ _ _ as (join₂ as p′))
+... | inj₁ p′ with split as p′
+... | inj₁ p″ = join₁ as p″
+... | inj₂ p″ = join₂ as (⨟-distribʳ-+ _ _ _ as (join₁ as p″))
+⨟-distribʳ-+ r₁ r₂ r₃ (a ∷ as) p | yes Ar₂ | yes Ar₃ with split as p
+... | inj₁ p′ with split as p′
+... | inj₁ p″ = join₁ as p″
+... | inj₂ p″ = join₂ as (⨟-distribʳ-+ _ _ _ as (join₁ as p″))
+⨟-distribʳ-+ r₁ r₂ r₃ (a ∷ as) p | yes Ar₂ | yes Ar₃ | inj₂ p′ with split as p′
+... | inj₁ p″ = join₁ as p″
+... | inj₂ p″ = join₂ as (⨟-distribʳ-+ _ _ _ as (join₂ as p″))
+
+⨟-assoc : Associative _⨟_
+⨟-assoc r₁ r₂ r₃ [] (p₁ ⨟ (p₂ ⨟ p₃)) = (p₁ ⨟ p₂) ⨟ p₃
+⨟-assoc r₁ r₂ r₃ (a ∷ as) p with A? r₁ | A? r₂
+... | no ¬Ar₁ | no ¬Ar₂ = ⨟-assoc _ _ _ as p
+... | no ¬Ar₁ | yes Ar₂ = ⨟-assoc _ _ _ as p
+... | yes Ar₁ | no ¬Ar₂ with split as p
+... | inj₁ p′ = ⨟-distribʳ-+ _ _ _ as (join₁ as p′)
+... | inj₂ p′ = ⨟-distribʳ-+ _ _ _ as (join₂ as (⨟-assoc _ _ _ as p′))
+⨟-assoc r₁ r₂ r₃ (a ∷ as) p | yes Ar₁ | yes Ar₂ with split as p
+... | inj₂ p′ = join₂ as (⨟-distribʳ-+ _ _ _ as (join₂ as (⨟-assoc _ _ _ as p′)))
+... | inj₁ p′ with split as p′
+... | inj₁ p″ = join₁ as p″
+... | inj₂ p″ = join₂ as (⨟-distribʳ-+ _ _ _ as (join₁ as p″))
+
+⨟-zeroˡ : LeftZero Λ _⨟_
+⨟-zeroˡ r as p = contradiction p (end as)
+
+⨟-zeroʳ : RightZero Λ _⨟_
+⨟-zeroʳ r as p = contradiction p (end as)
+
+⨟-identityˡ : LeftIdentity ε _⨟_
+⨟-identityˡ r [] p = star ⨟ p
+⨟-identityˡ r (a ∷ as) p = join₁ as p
+
+⨟-identityʳ : RightIdentity ε _⨟_
+⨟-identityʳ r [] p = p ⨟ star
+⨟-identityʳ r (a ∷ as) p with A? r
+... | no ¬Ar = ⨟-identityʳ _ as p
+... | yes Ar = join₂ as (⨟-identityʳ _ as p)