RegExp structures

test.agda

module test where

import Level
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Function
open import Function.Injection hiding (_∘_ ; id)
open import Data.Sum
open import Data.Product

-- Regular Expressions
-- α, β ⩴ ∅      empty set
--       | ε      empty string
--       | σ      literal where σ ∈ Σ
--       | α∣β     union
--       | α·β    concatenation
--       | α⋆     Kleene-closure
data RegExp : Set where
  ∅       : RegExp                     -- Empty language
  ε       : RegExp                     -- Empty string
  literal : (σ : ℕ) → RegExp          -- Literal, single symbol
  _∣_     : RegExp  → RegExp → RegExp -- Concatenation
  _∙_     : RegExp  → RegExp → RegExp -- Union
  _⋆      : RegExp  → RegExp           -- Kleene closure

-- Structural equality, does not take into account the algebraic properties
data _≡r_ : Rel RegExp Level.zero where
  ∅≡∅ :                                                  ∅ ≡r ∅
  ε≡ε :                                                  ε ≡r ε
  ℓ≡ℓ : {σ σ₁ : ℕ}                → (σ ≡ σ₁) → literal σ ≡r literal σ₁
  ∣≡∣ :            {α β : RegExp} →               (α ∣ β) ≡r (α ∣ β)
  ∙≡∙ :            {α β : RegExp} →               (α ∙ β) ≡r (α ∙ β)
  ⋆≡⋆ :            {α   : RegExp} →                 (α ⋆) ≡r (α ⋆)

-- {x : RegExp} → x ≡r x
reflexive : Reflexive {A = RegExp} _≡r_
reflexive {∅}         = ∅≡∅
reflexive {ε}         = ε≡ε
reflexive {literal _} = ℓ≡ℓ refl
reflexive {_ ∣ _}     = ∣≡∣
reflexive {_ ∙ _}     = ∙≡∙
reflexive {_ ⋆}       = ⋆≡⋆

-- {i j : RegExp} → i ≡r j → (j ≡r i)
symmetric : Symmetric {A = RegExp} _≡r_
symmetric {∅}         ∅≡∅        = ∅≡∅
symmetric {ε}         ε≡ε        = ε≡ε
symmetric {literal _} (ℓ≡ℓ refl) = ℓ≡ℓ refl
symmetric {_ ∣ _}     ∣≡∣        = ∣≡∣
symmetric {_ ∙ _}     ∙≡∙        = ∙≡∙
symmetric {_ ⋆}       ⋆≡⋆        = ⋆≡⋆


-- {i j k : RegExp} → i ≡r j → j ≡r k → (i ≡r k)
transitive : Transitive {A = RegExp} _≡r_
transitive ∅≡∅        ∅≡∅        = ∅≡∅
transitive ε≡ε        ε≡ε        = ε≡ε
transitive (ℓ≡ℓ refl) (ℓ≡ℓ refl) = ℓ≡ℓ refl
transitive ∣≡∣        ∣≡∣        = ∣≡∣
transitive ∙≡∙        ∙≡∙        = ∙≡∙
transitive ⋆≡⋆        ⋆≡⋆        = ⋆≡⋆

-- (P : RegExp → Set) {x y : RegExp} → x ≡r y → P x → P y
substitutive : Substitutive _≡r_ Level.zero
substitutive _ ∅≡∅        = id
substitutive _ ε≡ε        = id
substitutive _ (ℓ≡ℓ refl) = id
substitutive _ ∣≡∣        = id
substitutive _ ∙≡∙        = id
substitutive _ ⋆≡⋆        = id

structural-equivalence : IsEquivalence {A = RegExp} _≡r_
structural-equivalence = record
  { refl  = reflexive
  ; sym   = symmetric
  ; trans = transitive
  }

structure-setoid : Setoid Level.zero Level.zero
structure-setoid = record
  { Carrier       = RegExp
  ; _≈_           = _≡r_
  ; isEquivalence = structural-equivalence
  }

-- (x : literal σ ≡r literal σ₁) → σ ≡ σ₁
ℓ-injectivity : Injective {A = setoid ℕ} {B = structure-setoid} (record { _⟨$⟩_ = literal; cong = ℓ≡ℓ })
ℓ-injectivity (ℓ≡ℓ refl) = refl

-- Strict inequality for RegExp structures
-- The order chosen here is arbritrary (but hopefully intuitive)
data _<r_ : Rel RegExp Level.zero where
  ∅<ε  :                                                                            ∅ <r ε
  ∅<ℓ  : {σ    : ℕ}                    →                                           ∅ <r literal σ
  ∅<∣  :            {α β     : RegExp} →                                           ∅ <r (α ∣ β)
  ∅<∙  :            {α β     : RegExp} →                                           ∅ <r (α ∙ β)
  ∅<⋆  :            {α       : RegExp} →                                           ∅ <r (α ⋆)
  ε<ℓ  : {σ    : ℕ}                    →                                           ε <r literal σ
  ε<∣  :            {α β     : RegExp} →                                           ε <r (α ∣ β)
  ε<∙  :            {α β     : RegExp} →                                           ε <r (α ∙ β)
  ε<⋆  :            {α       : RegExp} →                                           ε <r (α ⋆)
  ℓ<ℓ₁ : {σ σ₁ : ℕ}                    → (σ < σ₁) →                       literal σ <r literal σ₁
  ℓ<∣  : {σ    : ℕ} {α β     : RegExp} →                                   literal σ <r (α ∣ β)
  ℓ<∙  : {σ    : ℕ} {α β     : RegExp} →                                   literal σ <r (α ∙ β)
  ℓ<⋆  : {σ    : ℕ} {α       : RegExp} →                                   literal σ <r (α ⋆)
  ∣<∣  :            {α β γ δ : RegExp} → (α <r γ) ⊎ ((α ≡r γ) × (β <r δ)) → (α ∣ β) <r (γ ∣ δ)
  ∣<∙  :            {α β γ δ : RegExp} →                                     (α ∣ β) <r (γ ∙ δ)
  ∣<⋆  :            {α β γ   : RegExp} →                                     (α ∣ β) <r (γ ⋆)
  ∙<∙  :            {α β γ δ : RegExp} → (α <r γ) ⊎ ((α ≡r γ) × (β <r δ)) → (α ∙ β) <r (γ ∙ δ)
  ∙<⋆  :            {α β γ   : RegExp} →                                     (α ∙ β) <r (γ ⋆)
  ⋆<⋆  :            {α β     : RegExp} → (α <r β) →                           (α ⋆) <r (β ⋆)

-- I can do this for now:
ℓ<ℓ₁⇒σ<σ₁ : ∀ {σ σ₁ : ℕ} → (literal σ) <r (literal σ₁) → σ < σ₁
ℓ<ℓ₁⇒σ<σ₁ (ℓ<ℓ₁ p) = p

-- But I would like to write this using Injective similar to ℓ-injectivity above.