~jorge-jbs/theory-of-computation

01bffe64c76d2d059bff63b3b60d8257a140827a — Jorge Blázquez Saborido 1 year, 9 months ago 117d423
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