## ~jorge-jbs/theory-of-computation

628d592ee7fecedbff5fe081782e009ed369677b — Jorge Blázquez Saborido 1 year, 9 months ago
```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

```