~jorge-jbs/theory-of-computation: 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
   _ = {!!}