From 117d423a923488657bf9be1179665567033a1e47 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jorge=20Bl=C3=A1zquez=20Saborido?=
 <jorge.jbs@protonmail.com>
Date: Sat, 25 Jul 2020 13:36:24 +0200
Subject: [PATCH] Redefine IsFinite and use it as typeclass

---
 Common.agda         | 13 +++++++++++++
 DFA.agda            | 45 ++++++++++++++++++++++-----------------------
 FA-Regex-Equiv.agda |  9 +++++----
 Fin.agda            | 30 +++++++++++++++++++++++++++++-
 Lang.agda           | 21 +--------------------
 NFA-e.agda          | 10 +++++-----
 NFA.agda            | 24 ++++++++++--------------
 PFA.agda            | 21 +++++++++++----------
 Regex.agda          | 25 +++++++++++--------------
 9 files changed, 107 insertions(+), 91 deletions(-)
 create mode 100644 Common.agda

diff --git a/Common.agda b/Common.agda
new file mode 100644
index 0000000..08b0343
--- /dev/null
+++ b/Common.agda
@@ -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
diff --git a/DFA.agda b/DFA.agda
index 133685d..5e4f50c 100644
--- a/DFA.agda
+++ b/DFA.agda
@@ -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 ∷ _) = ⊤
diff --git a/FA-Regex-Equiv.agda b/FA-Regex-Equiv.agda
index 3402c70..d5ebe3b 100644
--- a/FA-Regex-Equiv.agda
+++ b/FA-Regex-Equiv.agda
@@ -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-ε = {!!}
diff --git a/Fin.agda b/Fin.agda
index bf3f8eb..498ecb6 100644
--- a/Fin.agda
+++ b/Fin.agda
@@ -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 ∣
diff --git a/Lang.agda b/Lang.agda
index b34d8f6..8620689 100644
--- a/Lang.agda
+++ b/Lang.agda
@@ -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
 
diff --git a/NFA-e.agda b/NFA-e.agda
index 7ad1ed6..e80f31a 100644
--- a/NFA-e.agda
+++ b/NFA-e.agda
@@ -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 _ _
diff --git a/NFA.agda b/NFA.agda
index 15c816b..bfc26e0 100644
--- a/NFA.agda
+++ b/NFA.agda
@@ -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 ∷ _) = ⊤
diff --git a/PFA.agda b/PFA.agda
index 04533c0..0a5bccc 100644
--- a/PFA.agda
+++ b/PFA.agda
@@ -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
diff --git a/Regex.agda b/Regex.agda
index 95dce7e..66b1f44 100644
--- a/Regex.agda
+++ b/Regex.agda
@@ -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
   _ = {!!}
-- 
2.45.2