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

01bffe64c76d2d059bff63b3b60d8257a140827a — Jorge Blázquez Saborido 4 years ago
```Add TODO keyword for incomplete proofs
```
```8 files changed, 30 insertions(+), 21 deletions(-)

M Common.agda
M DFA.agda
M FA-Regex-Equiv.agda
M Fin.agda
M Lang.agda
M NFA.agda
M PFA.agda
M Regex.agda
```
`M Common.agda => Common.agda +14 -0`
```@@ 11,3 11,17 @@ private

it : {{_ : A}} → A
it {{x}} = x
+
+infixr 0 _\$_
+
+_\$_
+  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
+  → ((x : A) → B x)
+  →  (x : A) → B x
+f \$ x = f x
+
+_∋_ : ∀ {ℓ} (A : Type ℓ) → A → A
+A ∋ t = t
+
+postulate
+  TODO : A

```
`M DFA.agda => DFA.agda +0 -11`
```@@ 21,17 21,6 @@ open import Common
open import Lang
open import Fin

-infixr 0 _\$_
-
-_\$_
-  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
-  → ((x : A) → B x)
-  →  (x : A) → B x
-f \$ x = f x
-
-_∋_ : ∀ {ℓ} (A : Type ℓ) → A → A
-A ∋ t = t
-
module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
record DFA : Type₁ where
field

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

+open import Common
open import Fin
open import Lang
open import DFA

@@ 14,10 15,10 @@ open import Regex

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

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

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

```
`M Fin.agda => Fin.agda +3 -1`
```@@ 24,6 24,8 @@ open import Data.Fin using (Fin; zero; suc) public
import Data.Fin.Properties
import Data.Empty as Empty

+open import Common
+
znots-std : ∀ {m} {n : Fin m} → zero ≡ suc n → [ ⊥ ]
znots-std {m} {n} p = subst F p tt
where

@@ 81,7 83,7 @@ FinSet = TypeWithStr _ isFinSet

-- Is this even true?
isFinSet→isSet : {{_ : isFinSet A}} → isSet A
-isFinSet→isSet = {!!}
+isFinSet→isSet = TODO

instance
isFinSetFin : ∀ {n} → isFinSet (Fin n)

```
`M Lang.agda => Lang.agda +4 -3`
```@@ 11,6 11,7 @@ open import Cubical.Data.Empty renaming (⊥ to Empty)

module Lang where

+open import Common
open import Fin

module _ {ℓ}{X : Type ℓ} where

@@ 55,10 56,10 @@ module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
⟦ε⟧ = _^_ 0

_ : _^* ≡ ⋃ ℕ (_^_)
-  _ = {!!}
+  _ = {!TODO!}

_ : _^+ ≡ ⋃ ℕ (_^_ ∘ suc)
-  _ = {!!}
+  _ = TODO

_ : _^* ≡ _^+ ∪ ⟦ε⟧
-  _ = {!!}
+  _ = TODO

```
`M NFA.agda => NFA.agda +1 -1`
```@@ 69,4 69,4 @@ module example-2-6 where
P (suc zero ∷ b ∷ w) = P (b ∷ w)

_ : L ≡ P
-  _ = {!!}
+  _ = {!TODO!}

```
`M PFA.agda => PFA.agda +2 -1`
```@@ 10,6 10,7 @@ open import Cubical.Data.List hiding ([_])
open import Cubical.Data.Maybe
open import Cubical.Data.Prod

+open import Common
open import Lang
open import Fin

@@ 92,7 93,7 @@ module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
EmptyStackPfaLangs N = ∃[ M ∶ PFA ] (empty-stack-lang M ≡ N) , powersets-are-sets _ _

_ : FinalStatePfaLangs ≡ EmptyStackPfaLangs
-  _ = {!!}
+  _ = {!TODO!}

{-
Languages definable by pushdown finite automata

```
`M Regex.agda => Regex.agda +2 -1`
```@@ 10,6 10,7 @@ open import Cubical.Data.Nat hiding (_+_; +-comm)
open import Cubical.Data.List hiding ([_])
open import Cubical.Data.List.Properties

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

@@ 79,4 80,4 @@ module example where
L = lang A x

_ : L ≡ P
-  _ = {!!}
+  _ = TODO

```