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

117d423a923488657bf9be1179665567033a1e47 — Jorge Blázquez Saborido 1 year, 9 months ago
```Redefine IsFinite and use it as typeclass
```
```9 files changed, 107 insertions(+), 91 deletions(-)

A Common.agda
M DFA.agda
M FA-Regex-Equiv.agda
M Fin.agda
M Lang.agda
M NFA-e.agda
M NFA.agda
M PFA.agda
M Regex.agda
```
`A Common.agda => Common.agda +13 -0`
```@@ 0,0 1,13 @@
+{-# OPTIONS --cubical #-}
+
+module Common where
+
+open import Cubical.Foundations.Prelude
+
+private
+  variable
+    ℓ : Level
+    A : Type ℓ
+
+it : {{_ : A}} → A
+it {{x}} = x

```
`M DFA.agda => DFA.agda +22 -23`
```@@ 17,6 17,7 @@ open import Data.Fin as S
import Data.Fin.Properties
import Data.Empty as Empty

+open import Common
open import Lang
open import Fin

@@ 31,26 32,27 @@ f \$ x = f x
_∋_ : ∀ {ℓ} (A : Type ℓ) → A → A
A ∋ t = t

-record DFA {A : Type₀} (A-alph : IsAlphabet A) : Type₁ where
-  field
-    Q : Type₀
-    Q-fin : IsFinite Q
-    δ : Q → A → Q
-    initial-state : Q
-    F : ℙ Q
+module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
+  record DFA : Type₁ where
+    field
+      Q : Type₀
+      instance isFinSetQ : isFinSet Q
+      δ : Q → A → Q
+      initial-state : Q
+      F : ℙ Q

-  δ̂ : Q → Word A-alph → Q
-  δ̂ q [] = q
-  δ̂ q (a ∷ w) = δ̂ (δ q a) w
+    δ̂ : Q → Word A → Q
+    δ̂ q [] = q
+    δ̂ q (a ∷ w) = δ̂ (δ q a) w

-  lang : Lang A-alph
-  lang w = F (δ̂ initial-state w)
+    lang : Lang A
+    lang w = F (δ̂ initial-state w)

-{-
-Languages definable by deterministic finite automata
--}
-DfaLangs : {A : Type₀} (IsA : IsAlphabet A) → ℙ (Lang IsA)
-DfaLangs IsA N = ∃[ M ∶ DFA IsA ] (DFA.lang M ≡ N) , powersets-are-sets _ _
+  {-
+  Languages definable by deterministic finite automata
+  -}
+  DfaLangs : ℙ (Lang A)
+  DfaLangs N = ∃[ M ∶ DFA ] (DFA.lang M ≡ N) , powersets-are-sets _ _

module example-2-1 where
δ : Fin 3 → Fin 2 → Fin 3

@@ 63,19 65,16 @@ module example-2-1 where
A : Type₀
A = Fin 2

-  A-alph : IsAlphabet A
-  A-alph = 2 , refl
-
-  M : DFA A-alph
+  M : DFA A
M = record
{ Q = Fin 3
-    ; Q-fin = 3 , refl
+    ; isFinSetQ = it
; δ = δ
; initial-state = zero
; F = λ q → (q ≡ suc zero) , isSetFin q (suc zero)
}

-  P : Word A-alph → hProp ℓ-zero
+  P : Word A → hProp ℓ-zero
P [] = ⊥
P (a ∷ []) = ⊥
P (zero ∷ suc zero ∷ _) = ⊤

```
`M FA-Regex-Equiv.agda => FA-Regex-Equiv.agda +5 -4`
```@@ 5,18 5,19 @@ module FA-Regex-Equiv where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic

+open import Fin
open import Lang
open import DFA
open import NFA
open import NFA-e
open import Regex

-module _ {A : Type₀} (IsA : IsAlphabet A) where
-  DFA~Regex : DfaLangs IsA ≡ RegexLangs IsA
+module _ {A : Type₀} {{isFinSetA : isFinSet A}} where
+  DFA~Regex : DfaLangs A ≡ RegexLangs A
DFA~Regex = {!!}

-  DFA~NFA : DfaLangs IsA ≡ NfaLangs IsA
+  DFA~NFA : DfaLangs A ≡ NfaLangs A
DFA~NFA = {!!}

-  DFA~NFA-ε : DfaLangs IsA ≡ NFAεLangs IsA
+  DFA~NFA-ε : DfaLangs A ≡ NFAεLangs A
DFA~NFA-ε = {!!}

```
`M Fin.agda => Fin.agda +29 -1`
```@@ 1,12 1,18 @@
-{-# OPTIONS --cubical --safe #-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}

module Fin where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic
open import Cubical.Foundations.Function
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Equiv
+open import Cubical.HITs.PropositionalTruncation
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sigma
open import Cubical.Relation.Nullary using (Discrete; yes; no; mapDec)
open import Cubical.Relation.Nullary.DecidableEq using (Discrete→isSet)
import Cubical.Data.Fin as C

@@ 58,3 64,25 @@ IsFinite A = Σ ℕ (λ n → A ≡ Fin n)

isFinite→isSet : {A : Type₀} → IsFinite A → isSet A
isFinite→isSet (n , r) = transport (cong isSet (sym r)) isSetFin
+
+private
+  variable
+    ℓ : Level
+    A : Type ℓ
+
+isFinSet : Type ℓ → Type ℓ
+isFinSet A = ∥ Σ ℕ (λ n → A ≃ Fin n) ∥
+
+isProp-isFinSet : isProp (isFinSet A)
+isProp-isFinSet = propTruncIsProp
+
+FinSet : Type (ℓ-suc ℓ)
+FinSet = TypeWithStr _ isFinSet
+
+-- Is this even true?
+isFinSet→isSet : {{_ : isFinSet A}} → isSet A
+isFinSet→isSet = {!!}
+
+instance
+  isFinSetFin : ∀ {n} → isFinSet (Fin n)
+  isFinSetFin = ∣ _ , pathToEquiv refl ∣

```
`M Lang.agda => Lang.agda +1 -20`
```@@ 13,22 13,6 @@ module Lang where

open import Fin

-Finite : {X : Type ℓ-zero} → ℙ X → Type (ℓ-suc ℓ-zero)
-Finite {X} A = Σ X (_∈ A) ≡ Σ ℕ Fin
-
-FiniteSubset : Type₀ → Type₁
-FiniteSubset X = Σ (ℙ X) Finite
-
-data FSSet (A : Type₀) : Type₁ where
-  [] : FSSet A
-  _∷_ : (x : A) → (xs : FSSet A) → FSSet A
-  comm : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
-  dedup : ∀ x xs → x ∷ x ∷ xs ≡ x ∷ xs
-  trunc : isSet (FSSet A)
-
-IsAlphabet : Type₀ → Type₁
-IsAlphabet A = Σ ℕ (λ n → A ≡ Fin n)
-
module _ {ℓ}{X : Type ℓ} where
∅ : ℙ X
∅ _ = Lift Empty , λ ()

@@ 48,10 32,7 @@ module _ {ℓ}{X : Type ℓ} where
_∩_ : ℙ X → ℙ X → ℙ X
(A ∩ B) x = A x ⊓ B x

-module _ {A : Type₀} (IsA : IsAlphabet A) where
-  IsAlphabet→IsSet : isSet A
-  IsAlphabet→IsSet = transport (cong isSet (sym (IsA .snd))) isSetFin
-
+module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
Word : Type₀
Word = List A

```
`M NFA-e.agda => NFA-e.agda +5 -5`
```@@ 12,11 12,11 @@ open import Cubical.Data.Maybe
open import Lang
open import Fin

-module _ {A : Type₀} (A-alph : IsAlphabet A) where
+module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
record NFA-ε : Type₁ where
field
Q : Type₀
-      Q-fin : IsFinite Q
+      instance isFinSetQ : isFinSet Q
δ : Q → Maybe A → ℙ Q
initial-state : Q
F : ℙ Q

@@ 29,13 29,13 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
closure : Q → ℙ Q
closure q p = ∃[ qs ∶ List Q ] is-path-of-εs (q ∷ qs ++ p ∷ [])

-    δ̂ : Q → Word A-alph → ℙ Q
+    δ̂ : Q → Word A → ℙ Q
δ̂ q [] = closure q
δ̂ q (a ∷ w) p = ∃[ r ∶ Q ] ∃[ s ∶ Q ] closure q r ⊓ δ r (just a) s ⊓ δ̂ s w p
-- p ∈ δ̂ q (a ∷ w) iff (for some states r and s):
--     there exists a path of the form q …—ε→… r —a→ s …—w→… p

-    lang : Lang A-alph
+    lang : Lang A
lang w = ∃[ p ∶ Q ] δ̂ initial-state w p ⊓ F p

open NFA-ε

@@ 43,5 43,5 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
{-
Languages definable by non-deterministic finite automata with empty transitions
-}
-  NFAεLangs : ℙ (Lang A-alph)
+  NFAεLangs : ℙ (Lang A)
NFAεLangs N = ∃[ M ∶ NFA-ε ] (lang M ≡ N) , powersets-are-sets _ _

```
`M NFA.agda => NFA.agda +10 -14`
```@@ 7,23 7,24 @@ open import Cubical.Foundations.Logic
open import Cubical.Foundations.Function
open import Cubical.Data.List hiding ([_])

+open import Common
open import Lang
open import Fin

-module _ {A : Type₀} (A-alph : IsAlphabet A) where
+module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
record NFA : Type₁ where
field
Q : Type₀
-      Q-fin : IsFinite Q
+      instance Q-fin : isFinSet Q
δ : Q → A → ℙ Q
initial-state : Q
F : ℙ Q

-    δ̂ : Q → Word A-alph → ℙ Q
-    δ̂ q [] p = (p ≡ q) , isFinite→isSet Q-fin _ _
+    δ̂ : Q → Word A → ℙ Q
+    δ̂ q [] p = (p ≡ q) , isFinSet→isSet _ _
δ̂ q (a ∷ w) p = ∃[ r ∶ Q ] δ q a r ⊓ δ̂ r w p

-    lang : Lang A-alph
+    lang : Lang A
--lang w = F ∩ δ̂ initial-state w ≢ ∅
lang w = ∃[ p ∶ Q ] δ̂ initial-state w p ⊓ F p

@@ 32,19 33,14 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
{-
Languages definable by non-deterministic finite automata
-}
-  NfaLangs : ℙ (Lang A-alph)
+  NfaLangs : ℙ (Lang A)
NfaLangs N = ∃[ M ∶ NFA ] (lang M ≡ N) , powersets-are-sets _ _

module example-2-6 where
A : Type₀
A = Fin 2

-  A-alph : IsAlphabet A
-  A-alph = 2 , refl
-
Q = Fin 3
-  Q-fin : IsFinite Q
-  Q-fin = 3 , refl

δ : Q → A → ℙ Q
δ zero zero q = ((q ≡ zero) , isSetFin _ _)  ⊓ ((q ≡ suc zero) , isSetFin _ _)

@@ 53,10 49,10 @@ module example-2-6 where
δ (suc zero) (suc zero) q = (q ≡ suc (suc zero)) , isSetFin _ _
δ (suc (suc zero)) _ q = ∅ q

-  M : NFA A-alph
+  M : NFA A
M = record
{ Q = Q
-    ; Q-fin = Q-fin
+    ; Q-fin = it
; δ = δ
; initial-state = zero
; F = λ p → (suc (suc zero) ≡ p) , isSetFin _ _

@@ 65,7 61,7 @@ module example-2-6 where
δ̂ = NFA.δ̂ M
L = NFA.lang M

-  P : Word A-alph → hProp ℓ-zero
+  P : Word A → hProp ℓ-zero
P [] = ⊥
P (a ∷ []) = ⊥
P (zero ∷ suc zero ∷ _) = ⊤

```
`M PFA.agda => PFA.agda +11 -10`
```@@ 21,16 21,17 @@ isEmpty X = X → [ ⊥ ]
Subset : {X : Type ℓ} (P : ℙ X) → Type ℓ
Subset {X = X} P = Σ X (_∈ P)

-module _ {A : Type₀} (A-alph : IsAlphabet A) where
+module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
record PFA : Type₁ where
field
Q : Type₀
-      Q-fin : IsFinite Q
+      instace isFinSetQ : isFinSet Q
S : Type₀
-      S-alph : IsAlphabet S
+      instance isFinSetS : isFinSet S
δ : Q → Maybe A → S → ℙ (Q × List S)
-      instance δ-fin : ∀ {q a s} → IsFinite (Subset (δ q a s))
+      instance δ-fin : ∀ {q a s} → isFinSet (Subset (δ q a s))
--δ : Q → Maybe A → S → Σ (ℙ (Q × List S)) (IsFinite ∘ Subset)
+      --δ : Q → Maybe A → S → LFSet (Q × List S)
initial-state : Q
initial-symbol : S
F : ℙ Q

@@ 39,7 40,7 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
constructor config
field
state : Q
-        word : Word A-alph
+        word : Word A
stack : List S

data _⊢_ : Config → Config → Type₀ where

@@ 65,13 66,13 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
→ J ⊢* K
→ I ⊢* K

-    final-state-lang : Lang A-alph
+    final-state-lang : Lang A
final-state-lang w =
∃[ q ∶ Q ] ∃[ α ∶ List S ]
F q ⊓
∥ config initial-state w (initial-symbol ∷ []) ⊢* config q [] α ∥ₚ

-    empty-stack-lang : Lang A-alph
+    empty-stack-lang : Lang A
empty-stack-lang w =
∃[ q ∶ Q ]
∥ config initial-state w (initial-symbol ∷ []) ⊢* config q [] [] ∥ₚ

@@ 84,10 85,10 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where

open PFA

-  FinalStatePfaLangs : ℙ (Lang A-alph)
+  FinalStatePfaLangs : ℙ (Lang A)
FinalStatePfaLangs N = ∃[ M ∶ PFA ] (final-state-lang M ≡ N) , powersets-are-sets _ _

-  EmptyStackPfaLangs : ℙ (Lang A-alph)
+  EmptyStackPfaLangs : ℙ (Lang A)
EmptyStackPfaLangs N = ∃[ M ∶ PFA ] (empty-stack-lang M ≡ N) , powersets-are-sets _ _

_ : FinalStatePfaLangs ≡ EmptyStackPfaLangs

@@ 96,5 97,5 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
{-
Languages definable by pushdown finite automata
-}
-  PfaLangs : ℙ (Lang A-alph)
+  PfaLangs : ℙ (Lang A)
PfaLangs = FinalStatePfaLangs

```
`M Regex.agda => Regex.agda +11 -14`
```@@ 17,7 17,7 @@ repeat : {A : Type₀} → ℕ → List A → List A
repeat zero xs = []
repeat (suc n) xs = xs ++ repeat n xs

-module _ {A : Type₀} (IsA : IsAlphabet A) where
+module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
infixr 10 _+_ _·_
infixr 11 _*
data Regex : Type₀ where

@@ 26,21 26,21 @@ module _ {A : Type₀} (IsA : IsAlphabet A) where
_+_ _·_ : Regex → Regex → Regex
_* : Regex → Regex

-  lang : Regex → Lang IsA
+  lang : Regex → Lang A
lang ∅ w = ⊥
-  lang ε w = ⟦ε⟧ IsA w
-  lang (char x) w = (w ≡ x ∷ []) , isOfHLevelList 0 (IsAlphabet→IsSet IsA) _ _
+  lang ε w = ⟦ε⟧ A w
+  lang (char x) w = (w ≡ x ∷ []) , isOfHLevelList 0 isFinSet→isSet _ _
lang (x + y) w = (lang x ∪ lang y) w
lang (x · y) w =
∃[ u ] ∃[ v ] lang x u ⊓ lang y v ⊓
( (u ++ v ≡ w)
-      , isOfHLevelList 0 (IsAlphabet→IsSet IsA) _ _
+      , isOfHLevelList 0 isFinSet→isSet _ _
)
lang (x *) w =
⋃ ℕ
(λ n u →
( (u ≡ repeat n w)
-        , isOfHLevelList 0 (IsAlphabet→IsSet IsA) _ _
+        , isOfHLevelList 0 isFinSet→isSet _ _
)
)
w

@@ 48,7 48,7 @@ module _ {A : Type₀} (IsA : IsAlphabet A) where
{-
Languages definable by regular expressions
-}
-  RegexLangs : ℙ (Lang IsA)
+  RegexLangs : ℙ (Lang A)
RegexLangs M = ∃[ x ∶ Regex ] (lang x ≡ M) , powersets-are-sets _ _

RegexQuot : Type₁

@@ 64,22 64,19 @@ module example where
A : Type₀
A = Fin 2

-  A-alph : IsAlphabet A
-  A-alph = 2 , refl
-
-- (0|1)*01(0|1)*
-  x : Regex A-alph
+  x : Regex A
x = (char zero + char (suc zero))* · char zero · char (suc zero) · (char zero + char (suc zero))*

-  P : Lang A-alph
+  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-alph
-  L = lang A-alph x
+  L : Lang A
+  L = lang A x

_ : L ≡ P
_ = {!!}

```