~jorge-jbs/theory-of-computation

628d592ee7fecedbff5fe081782e009ed369677b — Jorge Blázquez Saborido 1 year, 9 months ago 763a0ed
Add closure properties of regular languages
4 files changed, 245 insertions(+), 59 deletions(-)

A Axioms.agda
M Lang.agda
M Regex.agda
A Regular.agda
A Axioms.agda => Axioms.agda +22 -0
@@ 0,0 1,22 @@
{-# OPTIONS --cubical #-}

module Axioms where

open import Cubical.Foundations.Prelude
open import Cubical.Relation.Nullary
open import Cubical.Data.Sum

record LEM {ℓ : Level} : Type (ℓ-suc ℓ) where
  field
    decide : ∀ (P : Type ℓ) → isProp P → P ⊎ (¬ P)

classical-decide : ∀ {ℓ} {{lem : LEM {ℓ}}}  (P : Type ℓ) → isProp P → P ⊎ (¬ P)
classical-decide {{lem}} = lem .LEM.decide

private
  open import Cubical.Data.Nat
  open import Common
  example : {{lem : LEM}} → ℕ → ℕ
  example x with classical-decide (x ≡ 0) (isSetℕ x 0)
  ... | inl _ = x + 1
  ... | inr _ = x ∸ 1

M Lang.agda => Lang.agda +108 -26
@@ 1,16 1,21 @@
{-# OPTIONS --cubical --allow-unsolved-metas #-}
{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Logic
open import Cubical.Relation.Nullary.DecidableEq
open import Cubical.HITs.PropositionalTruncation as PT hiding (∣_∣)
open import Cubical.Relation.Nullary using (Discrete)
open import Cubical.Data.Nat
--open import Cubical.Data.Fin
open import Cubical.Data.List
open import Cubical.Data.List hiding ([_])
open import Cubical.Data.Unit.Properties
open import Cubical.Data.Empty renaming (⊥ to Empty)
open import Cubical.Data.Sum as ⊎
open import Cubical.Data.Empty as ⊥ renaming (⊥ to Empty)

module Lang where

open import Axioms
open import Common
open import Fin



@@ 33,33 38,110 @@ module _ {ℓ}{X : Type ℓ} where
  _∩_ : ℙ X → ℙ X → ℙ X
  (A ∩ B) x = A x ⊓ B x

  _ᶜ : ℙ X → ℙ X
  (A ᶜ) x = ¬ A x

  de-morgan-∪-ᶜ : {A B : ℙ X} → (A ∪ B)ᶜ ≡ (A ᶜ) ∩ (B ᶜ)
  de-morgan-∪-ᶜ {A = A} {B = B} = ⊆-extensionality _ _ (⇒ , ⇐)
    where
      ⇒ : ∀ x → x ∈ ((A ∪ B)ᶜ) → x ∈ ((A ᶜ) ∩ (B ᶜ))
      ⇒ x ¬A∨B
        = (λ [A] → ¬A∨B PT.∣ ⊎.inl [A] ∣)
        , (λ [B] → ¬A∨B PT.∣ ⊎.inr [B] ∣)
      ⇐ : ∀ x → x ∈ ((A ᶜ) ∩ (B ᶜ)) → x ∈ ((A ∪ B)ᶜ)
      ⇐ x (¬A , ¬B) = PT.rec isProp⊥
        λ { (⊎.inl [A]) → ¬A [A]
          ; (⊎.inr [B]) → ¬B [B]
          }
  {-
  de-morgan-∩-ᶜ : {A B : ℙ X} → (A ∩ B)ᶜ ≡ (A ᶜ) ∪ (B ᶜ)
  de-morgan-∩-ᶜ {A = A} {B = B} = ⊆-extensionality _ _ (⇒ , ⇐)
    where
      ⇒ : ∀ x → x ∈ ((A ∩ B)ᶜ) → x ∈ ((A ᶜ) ∪ (B ᶜ))
      ⇒ x ¬A∧B = {!!}
      ⇐ : ∀ x → x ∈ ((A ᶜ) ∪ (B ᶜ)) → x ∈ ((A ∩ B)ᶜ)
      ⇐ = {!!}
  -}

  de-morgan-∩
    : {A B : ℙ X}
    → {{_ : LEM}}
    → A ∩ B ≡ ((A ᶜ) ∪ (B ᶜ))ᶜ
  de-morgan-∩ {A = A} {B = B} = ⊆-extensionality _ _ (⇒ , ⇐)
    where
      ⇒ : ∀ x → x ∈ (A ∩ B) → x ∈ (((A ᶜ) ∪ (B ᶜ))ᶜ)
      ⇒ x ([A] , [B]) = PT.rec isProp⊥
        λ { (⊎.inl ¬A) → ¬A [A]
          ; (⊎.inr ¬B) → ¬B [B]
          }
      ⇐ : ∀ x → x ∈ (((A ᶜ) ∪ (B ᶜ))ᶜ) → x ∈ (A ∩ B)
      ⇐ x ¬[¬A∨¬B]
        with classical-decide (x ∈ A) (∈-isProp A x)
           | classical-decide (x ∈ B) (∈-isProp B x)
      ... | ⊎.inl [A] | ⊎.inl [B] = [A] , [B]
      ... | ⊎.inl [A] | ⊎.inr ¬B  = ⊥.elim (¬[¬A∨¬B] PT.∣ ⊎.inr ¬B ∣)
      ... | ⊎.inr ¬A  | _         = ⊥.elim (¬[¬A∨¬B] PT.∣ ⊎.inl ¬A ∣)

module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
  Word : Type₀
  Word = List A

  ∣_∣ : Word → ℕ
  ∣ w ∣ = length w

  Lang : Type₁
  Lang = ℙ Word

  _^_ : ℕ → Lang
  _^_ n w = (∣ w ∣ ≡ n) , isSetℕ (∣ w ∣) n

  _^* : Lang
  _^* w = ⊤

  _^+ : Lang
  _^+ w = ¬ ((∣ w ∣ ≡ 0) , isSetℕ (∣ w ∣) 0)

  ⟦ε⟧ : Lang
  ⟦ε⟧ = _^_ 0

  _ : _^* ≡ ⋃ ℕ (_^_)
  _ = TODO

  _ : _^+ ≡ ⋃ ℕ (_^_ ∘ suc)
  _ = TODO

  _ : _^* ≡ _^+ ∪ ⟦ε⟧
  _ = TODO
∣_∣ : {A : Type₀} {{_ : isFinSet A}} → Word A → ℕ
∣ w ∣ = length w

_^_ : (A : Type₀) {{_ : isFinSet A}} → ℕ → Lang A
(A ^ n) w = (∣ w ∣ ≡ n) , isSetℕ (∣ w ∣) n

_* : (A : Type₀) {{_ : isFinSet A}} → Lang A
(A *) w = ⊤

_⁺ : (A : Type₀) {{_ : isFinSet A}} → Lang A
(A ⁺) w = ¬ ((∣ w ∣ ≡ 0) , isSetℕ (∣ w ∣) 0)

⟦ε⟧ : {A : Type₀} {{_ : isFinSet A}} → Lang A
⟦ε⟧ {A = A} = A ^ 0

module _ {A : Type₀} {{isFinSetA : isFinSet A}} where
  private
    isSet-List : isSet (List A)
    isSet-List = Discrete→isSet (discreteList isFinSet→Discrete)

  *≡⋃ : A * ≡ ⋃ ℕ (λ n → A ^ n)
  *≡⋃ = ⊆-extensionality _ _ (⇒ , ⇐)
    where
      ⇒ : ∀ w → w ∈ (A *) → w ∈ (⋃ ℕ (λ n → A ^ n))
      ⇒ w _ = PT.∣ ∣ w ∣ , refl ∣

      ⇐ : ∀ w → w ∈ (⋃ ℕ (λ n → A ^ n)) → w ∈ (A *)
      ⇐ _ _ = tt

  ⁺≡⋃ : A ⁺ ≡ ⋃ ℕ λ n → A ^ suc n
  ⁺≡⋃ = ⊆-extensionality _ _ (⇒ , ⇐)
    where
      ⇒ : ∀ w → w ∈ (A ⁺) → w ∈ (⋃ ℕ (λ n → A ^ suc n))
      ⇒ w p with ∣ w ∣
      ... | zero = ⊥.elim (p refl)
      ... | suc n = PT.∣ n , refl ∣

      ⇐ : ∀ w → w ∈ (⋃ ℕ (λ n → A ^ suc n)) → w ∈ (A ⁺)
      ⇐ w PT.∣ n , p ∣ w-empty = znots (0 ≡⟨ sym w-empty ⟩ ∣ w ∣ ≡⟨ p ⟩ suc n ∎)
      ⇐ w (squash p q i) w-empty = isProp⊥ (⇐ w p w-empty) (⇐ w q w-empty) i

  *≡⁺∪ε : A * ≡ (A ⁺) ∪ ⟦ε⟧
  *≡⁺∪ε = ⊆-extensionality _ _ (⇒ , ⇐)
    where
      ⇒ : ∀ w → w ∈ (A *) → w ∈ ((A ⁺) ∪ ⟦ε⟧)
      ⇒ w tt with ∣ w ∣
      ... | zero = PT.∣ ⊎.inr refl ∣
      ... | suc n = PT.∣ ⊎.inl (znots ∘ sym) ∣

      ⇐ : ∀ w → w ∈ ((A ⁺) ∪ ⟦ε⟧) → w ∈ (A *)
      ⇐ w x = tt

  _·_ : Lang A → Lang A → Lang A
  (L · M) w =
    ∃[ a ∶ Word A ] ∃[ b ∶ Word A ]
      L a ⊓ M b ⊓ ((a ++ b ≡ w) , isSet-List _ _)

M Regex.agda => Regex.agda +38 -33
@@ 11,7 11,7 @@ open import Cubical.Data.List hiding ([_])
open import Cubical.Data.List.Properties

open import Common
open import Lang hiding (∅)
open import Lang
open import Fin

repeat : {A : Type₀} → ℕ → List A → List A


@@ 19,25 19,26 @@ repeat zero xs = []
repeat (suc n) xs = xs ++ repeat n xs

module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
  infixr 10 _+_ _·_
  infixr 11 _*
  infixr 10 _+′_ _·′_
  infixr 11 _*′
  data Regex : Type₀ where
    ∅ ε : Regex
    ∅′ ε′ : Regex
    char : A → Regex
    _+_ _·_ : Regex → Regex → Regex
    _* : Regex → Regex
    _+′_ _·′_ : Regex → Regex → Regex
    _*′ : Regex → Regex

  lang : Regex → Lang A
  lang ∅ w = ⊥
  lang ε w = ⟦ε⟧ A w
module _ {A : Type₀} {{isFinSetA : isFinSet A}} where
  lang : Regex A → Lang A
  lang ∅′ w = ⊥
  lang ε′ w = ⟦ε⟧ w
  lang (char x) w = (w ≡ x ∷ []) , isOfHLevelList 0 isFinSet→isSet _ _
  lang (x + y) w = (lang x ∪ lang y) w
  lang (x · y) w =
  lang (x +′ y) = lang x ∪ lang y
  lang (x ·′ y) w =
    ∃[ u ] ∃[ v ] lang x u ⊓ lang y v ⊓
      ( (u ++ v ≡ w)
      , isOfHLevelList 0 isFinSet→isSet _ _
      )
  lang (x *) w =
  lang (x *′) w =
    ⋃ ℕ
      (λ n u →
        ( (u ≡ repeat n w)


@@ 46,38 47,42 @@ module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
      )
      w

  {-
  {-|
  Languages definable by regular expressions
  -}
  RegexLangs : ℙ (Lang A)
  RegexLangs M = ∃[ x ∶ Regex ] (lang x ≡ M) , powersets-are-sets _ _
  RegexLangs M = ∃[ x ∶ Regex A ] (lang x ≡ M) , powersets-are-sets _ _

  RegexQuot : Type₁
  RegexQuot = Regex / λ x y → lang x ≡ lang y
  RegexQuot = Regex A / λ x y → lang x ≡ lang y

  [_] : Regex → RegexQuot
  [_] : Regex A → RegexQuot
  [_] = _/_.[_]

  +-comm : ∀ {x y} → [ x + y ] ≡ [ y + x ]
  +-comm : ∀ {x y} → [ x +′ y ] ≡ [ y +′ x ]
  +-comm {x} {y} = eq/ _ _ (∪-comm (lang x) (lang y))

module example where
  A : Type₀
  A = Fin 2
private
  module example where
    A : Type₀
    A = Fin 2

  -- (0|1)*01(0|1)*
  x : Regex A
  x = (char zero + char (suc zero))* · char zero · char (suc zero) · (char zero + char (suc zero))*
    -- (0|1)*01(0|1)*
    x : Regex A
    x
      =  (char zero +′ char (suc zero))*′
      ·′ char zero ·′ char (suc zero)
      ·′ (char zero +′ char (suc zero))*′

  P : Lang A
  P [] = ⊥
  P (a ∷ []) = ⊥
  P (zero ∷ suc zero ∷ _) = ⊤
  P (zero ∷ zero ∷ w) = P (zero ∷ w)
  P (suc zero ∷ b ∷ w) = P (b ∷ w)
    P : Lang A
    P [] = ⊥
    P (a ∷ []) = ⊥
    P (zero ∷ suc zero ∷ _) = ⊤
    P (zero ∷ zero ∷ w) = P (zero ∷ w)
    P (suc zero ∷ b ∷ w) = P (b ∷ w)

  L : Lang A
  L = lang A x
    L : Lang A
    L = lang x

  _ : L ≡ P
  _ = TODO
    _ : L ≡ P
    _ = TODO

A Regular.agda => Regular.agda +77 -0
@@ 0,0 1,77 @@
{-# OPTIONS --cubical #-}

module Regular where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic
open import Cubical.HITs.PropositionalTruncation as PT

open import Axioms
open import Common
open import Fin
open import Lang
open import Regex

private
  variable
    ℓ : Level

isRegular : {A : Type₀} {{isFinSet-A : isFinSet A}} → Lang A → Type₁
isRegular w = w ∈ RegexLangs

rec2′ : ∀ {A B P : Type ℓ} → isProp P → (A → B → P) → ∥ A ∥ → ∥ B ∥ → P
rec2′ Pprop f =
  rec (isPropΠ (λ _ → Pprop))
    (λ a → rec Pprop (f a))

module _
    {A : Type₀}
    {{isFinSet-A : isFinSet A}}
    {L M : Lang A}
    {{isRegular-L : isRegular L}}
    {{isRegular-M : isRegular M}}
    where
  instance
    reg-closed-under-∪ : isRegular (L ∪ M)
    reg-closed-under-∪ = prf it it
      where
        prf : isRegular L → isRegular M → isRegular (L ∪ M)
        prf = rec2′ squash λ (x , lang-x≡L) (y , lang-y≡M) →
            ∥_∥.∣
              ( x +′ y
              , ( lang (x +′ y) ≡⟨ refl ⟩
                  lang x ∪ lang y ≡⟨ cong₂ _∪_ lang-x≡L lang-y≡M ⟩
                  L ∪ M ∎
                )
              )

module _
    {A : Type₀}
    {{isFinSet-A : isFinSet A}}
    {L : Lang A}
    {{isRegular-L : isRegular L}}
    where
  instance
    reg-closed-under-¬ : isRegular (L ᶜ)
    reg-closed-under-¬ = TODO

module _
    {A : Type₀}
    {{isFinSet-A : isFinSet A}}
    {L M : Lang A}
    {{isRegular-L : isRegular L}}
    {{isRegular-M : isRegular M}}
    where
  instance
    reg-closed-under-∩ : {{_ : LEM}} → isRegular (L ∩ M)
    reg-closed-under-∩ = proof
      where
        lemma : isRegular (((L ᶜ) ∪ (M ᶜ))ᶜ)
        lemma = it

        proof : isRegular (L ∩ M)
        proof = subst
          isRegular
          (sym (de-morgan-∩ {A = L} {B = M}))
          lemma