~jorge-jbs/theory-of-computation: Use type classes for operators

3 files changed, 86 insertions(+), 40 deletions(-)

M DFA.agda
M Lang.agda
A Operators.agda

M DFA.agda => DFA.agda +42 -38

@@ 7,7 7,7 @@ open import Cubical.Foundations.Logic
 open import Cubical.Foundations.Function
 open import Cubical.Data.Nat
 open import Cubical.Data.Nat.Order
-open import Cubical.Data.Sigma
+open import Cubical.Data.Sigma hiding (_×_)
 open import Cubical.Data.Sum as ⊎
 open import Cubical.HITs.PropositionalTruncation as PT
 open import Cubical.Relation.Nullary using (Discrete; yes; no; mapDec)


@@ 24,6 24,7 @@ open import Axioms
 open import Common
 open import Lang
 open import Fin
+open import Operators
 
 module _ (Symbol : Type₀) {{isFinSetA : isFinSet Symbol}} where
   record DFA : Type₁ where


@@ 53,52 54,54 @@ module _ (Symbol : Type₀) {{isFinSetA : isFinSet Symbol}} where
   DfaLangs : ℙ (Lang Symbol)
   DfaLangs N = ∃[ M ∶ DFA ] (lang M ≡ N) , powersets-are-sets _ _
 
-  _×ₐ_ : DFA → DFA → DFA
-  M ×ₐ N = record
-    { State = (M .State) × (N .State)
-    ; next = λ (p , q) a → next M p a , next N q a
-    ; start-state = start-state M , start-state N
-    ; FinalState = λ (p , q) → FinalState M p ⊓ FinalState N q
-    }
+  instance
+    Has-×-DFA : Has-× DFA DFA DFA
+    Has-×-DFA ._×_ M N = record
+      { State = (M .State) × (N .State)
+      ; next = λ (p , q) a → next M p a , next N q a
+      ; start-state = start-state M , start-state N
+      ; FinalState = λ (p , q) → FinalState M p ⊓ FinalState N q
+      }
 
-  lang-× : (M N : DFA) → lang (M ×ₐ N) ≡ lang M ∩ lang N
+  lang-× : (M N : DFA) → lang (M × N) ≡ lang M ∩ lang N
   lang-× M N = ⊆-extensionality _ _ (⇒ , ⇐)
     where
       run-ext
         : ∀ w p q
-        → run (M ×ₐ N) (p , q) w
+        → run (M × N) (p , q) w
         ≡ (run M p w , run N q w)
       run-ext [] _ _ = refl
       run-ext (x ∷ w) p q = run-ext w (next M p x) (next N q x)
 
-      ⇒ : ∀ w → w ∈ lang (M ×ₐ N) → w ∈ (lang M ∩ lang N)
+      ⇒ : ∀ w → w ∈ lang (M × N) → w ∈ (lang M ∩ lang N)
       ⇒ w = subst
-        (_∈ FinalState (M ×ₐ N))
+        (_∈ FinalState (M × N))
         (run-ext w (start-state M) (start-state N))
-      ⇐ : ∀ w → w ∈ (lang M ∩ lang N) → w ∈ lang (M ×ₐ N)
+      ⇐ : ∀ w → w ∈ (lang M ∩ lang N) → w ∈ lang (M × N)
       ⇐ w = subst
-        (_∈ FinalState (M ×ₐ N))
+        (_∈ FinalState (M × N))
         (sym (run-ext w (start-state M) (start-state N)))
 
-  _⊕ₐ_ : DFA → DFA → DFA
-  M ⊕ₐ N = record
-    { State = (M .State) × (N .State)
-    ; next = λ (p , q) a → next M p a , next N q a
-    ; start-state = start-state M , start-state N
-    ; FinalState = λ (p , q) → FinalState M p ⊔ FinalState N q
-    }
+  instance
+    Has-⊕-DFA : Has-⊕ DFA DFA DFA
+    Has-⊕-DFA ._⊕_ M N = record
+      { State = (M .State) × (N .State)
+      ; next = λ (p , q) a → next M p a , next N q a
+      ; start-state = start-state M , start-state N
+      ; FinalState = λ (p , q) → FinalState M p ⊔ FinalState N q
+      }
 
-  lang-⊕ : ∀ M N → lang (M ⊕ₐ N) ≡ lang M ∪ lang N
+  lang-⊕ : ∀ M N → lang (M ⊕ N) ≡ lang M ∪ lang N
   lang-⊕ M N = ⊆-extensionality _ _  (⇒ , ⇐)
     where
       run-ext
         : ∀ w p q
-        → run (M ⊕ₐ N) (p , q) w
+        → run (M ⊕ N) (p , q) w
         ≡ (run M p w , run N q w)
       run-ext [] _ _ = refl
       run-ext (x ∷ w) p q = run-ext w (next M p x) (next N q x)
 
-      ⇒ : ∀ w → w ∈ lang (M ⊕ₐ N) → w ∈ (lang M ∪ lang N)
+      ⇒ : ∀ w → w ∈ lang (M ⊕ N) → w ∈ (lang M ∪ lang N)
       ⇒ w = PT.rec (∈-isProp (lang M ∪ lang N) w)
         λ { (⊎.inl x) → PT.∣ ⊎.inl (subst
               (_∈ FinalState M ∘ fst)


@@ 111,8 114,8 @@ module _ (Symbol : Type₀) {{isFinSetA : isFinSet Symbol}} where
               x
             ) ∣
           }
-      ⇐ : ∀ w → w ∈ (lang M ∪ lang N) → w ∈ lang (M ⊕ₐ N)
-      ⇐ w = rec (∈-isProp (lang (M ⊕ₐ N)) w)
+      ⇐ : ∀ w → w ∈ (lang M ∪ lang N) → w ∈ lang (M ⊕ N)
+      ⇐ w = rec (∈-isProp (lang (M ⊕ N)) w)
         λ { (⊎.inl x) → PT.∣ ⊎.inl (subst
               (_∈ FinalState M ∘ fst)
               (sym (run-ext w (start-state M) (start-state N)))


@@ 125,30 128,31 @@ module _ (Symbol : Type₀) {{isFinSetA : isFinSet Symbol}} where
             ) ∣
           }
 
-  _ᶜᵃ : DFA → DFA
-  M ᶜᵃ = record
-    { State = M .State
-    ; next = M .next
-    ; start-state = M .start-state
-    ; FinalState = λ q → ¬ FinalState M q
-    }
+  instance
+    Has-ᶜ-DFA : Has-ᶜ DFA DFA
+    Has-ᶜ-DFA ._ᶜ M = record
+      { State = M .State
+      ; next = M .next
+      ; start-state = M .start-state
+      ; FinalState = λ q → ¬ FinalState M q
+      }
 
-  lang-ᶜ : ∀ M → lang (M ᶜᵃ) ≡ (lang M) ᶜ
+  lang-ᶜ : ∀ M → lang (M ᶜ) ≡ (lang M) ᶜ
   lang-ᶜ M = ⊆-extensionality _ _  (⇒ , ⇐)
     where
       run-ext
         : ∀ w p
-        → run (M ᶜᵃ) p w
+        → run (M ᶜ) p w
         ≡ run M p w
       run-ext [] _ = refl
       run-ext (x ∷ w) p = run-ext w (next M p x)
 
-      ⇒ : ∀ w → w ∈ lang (M ᶜᵃ) → w ∈ ((lang M)ᶜ)
+      ⇒ : ∀ w → w ∈ lang (M ᶜ) → w ∈ ((lang M)ᶜ)
       ⇒ w = subst
         (λ h → fst (FinalState M h) → ⊥.⊥)
         (run-ext w (start-state M))
 
-      ⇐ : ∀ w → w ∈ ((lang M)ᶜ) → w ∈ lang (M ᶜᵃ)
+      ⇐ : ∀ w → w ∈ ((lang M)ᶜ) → w ∈ lang (M ᶜ)
       ⇐ w = subst
         (λ h → fst (FinalState M h) → ⊥.⊥)
         (sym (run-ext w (start-state M)))


@@ 176,7 180,7 @@ module _ (Symbol : Type₀) {{isFinSetA : isFinSet Symbol}} where
       ... | ⊎.inr ¬P  | ⊎.inl [Q] = PT.∣ ⊎.inr [Q] ∣
       ... | ⊎.inr ¬P  | ⊎.inr ¬Q  = ⊥.elim (¬[¬P∧¬Q] (¬P , ¬Q))
 
-  de-morgan-⊕ : {{_ : LEM}} → ∀ M N → M ⊕ₐ N ≡ ((M ᶜᵃ) ×ₐ (N ᶜᵃ)) ᶜᵃ
+  de-morgan-⊕ : {{_ : LEM}} → ∀ M N → M ⊕ N ≡ (M ᶜ × N ᶜ)ᶜ
   de-morgan-⊕ M N i = record
     { State = refl i
     ; isFinSetState = it

M Lang.agda => Lang.agda +4 -2

@@ 18,6 18,7 @@ module Lang where
 open import Axioms
 open import Common
 open import Fin
+open import Operators
 
 module _ {ℓ}{X : Type ℓ} where
   ∅ : ℙ X


@@ 38,8 39,9 @@ module _ {ℓ}{X : Type ℓ} where
   _∩_ : ℙ X → ℙ X → ℙ X
   (A ∩ B) x = A x ⊓ B x
 
-  _ᶜ : ℙ X → ℙ X
-  (A ᶜ) x = ¬ A x
+  instance
+    Has-ᶜ-ℙ : Has-ᶜ (ℙ X) (ℙ X)
+    Has-ᶜ-ℙ ._ᶜ A x = ¬ A x
 
   de-morgan-∪-ᶜ : {A B : ℙ X} → (A ∪ B)ᶜ ≡ (A ᶜ) ∩ (B ᶜ)
   de-morgan-∪-ᶜ {A = A} {B = B} = ⊆-extensionality _ _ (⇒ , ⇐)

A Operators.agda => Operators.agda +40 -0

@@ 0,0 1,40 @@
+{-# OPTIONS --cubical #-}
+
+module Operators where
+
+open import Cubical.Foundations.Prelude
+
+open import Common
+
+private
+  variable
+    ℓ ℓ′ ℓ₁ ℓ₂ ℓ₃ : Level
+
+record Has-× (A : Type ℓ₁) (B : Type ℓ₂) (C : Type ℓ₃)
+    : Type (ℓ-max ℓ₁ (ℓ-max ℓ₂ ℓ₃)) where
+  infixr 5 _×_
+  field
+    _×_ : A → B → C
+
+open Has-× {{...}} public
+
+instance
+  Has-×-Type : Has-× (Type ℓ) (Type ℓ) (Type ℓ)
+  Has-×-Type = record { _×_ = Sigma._×_ }
+    where
+      import Cubical.Data.Sigma as Sigma
+
+record Has-⊕ (A : Type ℓ₁) (B : Type ℓ₂) (C : Type ℓ₃)
+    : Type (ℓ-max ℓ₁ (ℓ-max ℓ₂ ℓ₃)) where
+  field
+    _⊕_ : A → B → C
+
+open Has-⊕ {{...}} public
+
+record Has-ᶜ (A : Type ℓ₁) (B : Type ℓ₂)
+    : Type (ℓ-max ℓ₁ ℓ₂) where
+  infix 6 _ᶜ
+  field
+    _ᶜ : A → B
+
+open Has-ᶜ {{...}} public