Initial commit: definition of regular expression, algebraic properties of + and ;
This commit is contained in:
commit
47c9a4a177
3
regex.agda-lib
Normal file
3
regex.agda-lib
Normal file
@ -0,0 +1,3 @@
|
||||
name: regex
|
||||
depend: standard-library-2.2
|
||||
include: src
|
||||
101
src/Regex.agda
Normal file
101
src/Regex.agda
Normal file
@ -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₂)
|
||||
|
||||
146
src/Regex/Properties.agda
Normal file
146
src/Regex/Properties.agda
Normal file
@ -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
|
||||
}
|
||||
|
||||
31
src/Regex/Properties/Core.agda
Normal file
31
src/Regex/Properties/Core.agda
Normal file
@ -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
|
||||
|
||||
|
||||
153
src/Regex/Properties/Sub.agda
Normal file
153
src/Regex/Properties/Sub.agda
Normal file
@ -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′
|
||||
133
src/Regex/Properties/Super.agda
Normal file
133
src/Regex/Properties/Super.agda
Normal file
@ -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)
|
||||
Loading…
x
Reference in New Issue
Block a user