A Axioms.agda => Axioms.agda +22 -0
@@ 0,0 1,22 @@
+{-# OPTIONS --cubical #-}
+
+module Axioms where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Sum
+
+record LEM {ℓ : Level} : Type (ℓ-suc ℓ) where
+ field
+ decide : ∀ (P : Type ℓ) → isProp P → P ⊎ (¬ P)
+
+classical-decide : ∀ {ℓ} {{lem : LEM {ℓ}}} (P : Type ℓ) → isProp P → P ⊎ (¬ P)
+classical-decide {{lem}} = lem .LEM.decide
+
+private
+ open import Cubical.Data.Nat
+ open import Common
+ example : {{lem : LEM}} → ℕ → ℕ
+ example x with classical-decide (x ≡ 0) (isSetℕ x 0)
+ ... | inl _ = x + 1
+ ... | inr _ = x ∸ 1
M Lang.agda => Lang.agda +108 -26
@@ 1,16 1,21 @@
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
+{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Logic
+open import Cubical.Relation.Nullary.DecidableEq
+open import Cubical.HITs.PropositionalTruncation as PT hiding (∣_∣)
+open import Cubical.Relation.Nullary using (Discrete)
open import Cubical.Data.Nat
--open import Cubical.Data.Fin
-open import Cubical.Data.List
+open import Cubical.Data.List hiding ([_])
open import Cubical.Data.Unit.Properties
-open import Cubical.Data.Empty renaming (⊥ to Empty)
+open import Cubical.Data.Sum as ⊎
+open import Cubical.Data.Empty as ⊥ renaming (⊥ to Empty)
module Lang where
+open import Axioms
open import Common
open import Fin
@@ 33,33 38,110 @@ module _ {ℓ}{X : Type ℓ} where
_∩_ : ℙ X → ℙ X → ℙ X
(A ∩ B) x = A x ⊓ B x
+ _ᶜ : ℙ X → ℙ X
+ (A ᶜ) x = ¬ A x
+
+ de-morgan-∪-ᶜ : {A B : ℙ X} → (A ∪ B)ᶜ ≡ (A ᶜ) ∩ (B ᶜ)
+ de-morgan-∪-ᶜ {A = A} {B = B} = ⊆-extensionality _ _ (⇒ , ⇐)
+ where
+ ⇒ : ∀ x → x ∈ ((A ∪ B)ᶜ) → x ∈ ((A ᶜ) ∩ (B ᶜ))
+ ⇒ x ¬A∨B
+ = (λ [A] → ¬A∨B PT.∣ ⊎.inl [A] ∣)
+ , (λ [B] → ¬A∨B PT.∣ ⊎.inr [B] ∣)
+ ⇐ : ∀ x → x ∈ ((A ᶜ) ∩ (B ᶜ)) → x ∈ ((A ∪ B)ᶜ)
+ ⇐ x (¬A , ¬B) = PT.rec isProp⊥
+ λ { (⊎.inl [A]) → ¬A [A]
+ ; (⊎.inr [B]) → ¬B [B]
+ }
+ {-
+ de-morgan-∩-ᶜ : {A B : ℙ X} → (A ∩ B)ᶜ ≡ (A ᶜ) ∪ (B ᶜ)
+ de-morgan-∩-ᶜ {A = A} {B = B} = ⊆-extensionality _ _ (⇒ , ⇐)
+ where
+ ⇒ : ∀ x → x ∈ ((A ∩ B)ᶜ) → x ∈ ((A ᶜ) ∪ (B ᶜ))
+ ⇒ x ¬A∧B = {!!}
+ ⇐ : ∀ x → x ∈ ((A ᶜ) ∪ (B ᶜ)) → x ∈ ((A ∩ B)ᶜ)
+ ⇐ = {!!}
+ -}
+
+ de-morgan-∩
+ : {A B : ℙ X}
+ → {{_ : LEM}}
+ → A ∩ B ≡ ((A ᶜ) ∪ (B ᶜ))ᶜ
+ de-morgan-∩ {A = A} {B = B} = ⊆-extensionality _ _ (⇒ , ⇐)
+ where
+ ⇒ : ∀ x → x ∈ (A ∩ B) → x ∈ (((A ᶜ) ∪ (B ᶜ))ᶜ)
+ ⇒ x ([A] , [B]) = PT.rec isProp⊥
+ λ { (⊎.inl ¬A) → ¬A [A]
+ ; (⊎.inr ¬B) → ¬B [B]
+ }
+ ⇐ : ∀ x → x ∈ (((A ᶜ) ∪ (B ᶜ))ᶜ) → x ∈ (A ∩ B)
+ ⇐ x ¬[¬A∨¬B]
+ with classical-decide (x ∈ A) (∈-isProp A x)
+ | classical-decide (x ∈ B) (∈-isProp B x)
+ ... | ⊎.inl [A] | ⊎.inl [B] = [A] , [B]
+ ... | ⊎.inl [A] | ⊎.inr ¬B = ⊥.elim (¬[¬A∨¬B] PT.∣ ⊎.inr ¬B ∣)
+ ... | ⊎.inr ¬A | _ = ⊥.elim (¬[¬A∨¬B] PT.∣ ⊎.inl ¬A ∣)
+
module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
Word : Type₀
Word = List A
- ∣_∣ : Word → ℕ
- ∣ w ∣ = length w
-
Lang : Type₁
Lang = ℙ Word
- _^_ : ℕ → Lang
- _^_ n w = (∣ w ∣ ≡ n) , isSetℕ (∣ w ∣) n
-
- _^* : Lang
- _^* w = ⊤
-
- _^+ : Lang
- _^+ w = ¬ ((∣ w ∣ ≡ 0) , isSetℕ (∣ w ∣) 0)
-
- ⟦ε⟧ : Lang
- ⟦ε⟧ = _^_ 0
-
- _ : _^* ≡ ⋃ ℕ (_^_)
- _ = TODO
-
- _ : _^+ ≡ ⋃ ℕ (_^_ ∘ suc)
- _ = TODO
-
- _ : _^* ≡ _^+ ∪ ⟦ε⟧
- _ = TODO
+∣_∣ : {A : Type₀} {{_ : isFinSet A}} → Word A → ℕ
+∣ w ∣ = length w
+
+_^_ : (A : Type₀) {{_ : isFinSet A}} → ℕ → Lang A
+(A ^ n) w = (∣ w ∣ ≡ n) , isSetℕ (∣ w ∣) n
+
+_* : (A : Type₀) {{_ : isFinSet A}} → Lang A
+(A *) w = ⊤
+
+_⁺ : (A : Type₀) {{_ : isFinSet A}} → Lang A
+(A ⁺) w = ¬ ((∣ w ∣ ≡ 0) , isSetℕ (∣ w ∣) 0)
+
+⟦ε⟧ : {A : Type₀} {{_ : isFinSet A}} → Lang A
+⟦ε⟧ {A = A} = A ^ 0
+
+module _ {A : Type₀} {{isFinSetA : isFinSet A}} where
+ private
+ isSet-List : isSet (List A)
+ isSet-List = Discrete→isSet (discreteList isFinSet→Discrete)
+
+ *≡⋃ : A * ≡ ⋃ ℕ (λ n → A ^ n)
+ *≡⋃ = ⊆-extensionality _ _ (⇒ , ⇐)
+ where
+ ⇒ : ∀ w → w ∈ (A *) → w ∈ (⋃ ℕ (λ n → A ^ n))
+ ⇒ w _ = PT.∣ ∣ w ∣ , refl ∣
+
+ ⇐ : ∀ w → w ∈ (⋃ ℕ (λ n → A ^ n)) → w ∈ (A *)
+ ⇐ _ _ = tt
+
+ ⁺≡⋃ : A ⁺ ≡ ⋃ ℕ λ n → A ^ suc n
+ ⁺≡⋃ = ⊆-extensionality _ _ (⇒ , ⇐)
+ where
+ ⇒ : ∀ w → w ∈ (A ⁺) → w ∈ (⋃ ℕ (λ n → A ^ suc n))
+ ⇒ w p with ∣ w ∣
+ ... | zero = ⊥.elim (p refl)
+ ... | suc n = PT.∣ n , refl ∣
+
+ ⇐ : ∀ w → w ∈ (⋃ ℕ (λ n → A ^ suc n)) → w ∈ (A ⁺)
+ ⇐ w PT.∣ n , p ∣ w-empty = znots (0 ≡⟨ sym w-empty ⟩ ∣ w ∣ ≡⟨ p ⟩ suc n ∎)
+ ⇐ w (squash p q i) w-empty = isProp⊥ (⇐ w p w-empty) (⇐ w q w-empty) i
+
+ *≡⁺∪ε : A * ≡ (A ⁺) ∪ ⟦ε⟧
+ *≡⁺∪ε = ⊆-extensionality _ _ (⇒ , ⇐)
+ where
+ ⇒ : ∀ w → w ∈ (A *) → w ∈ ((A ⁺) ∪ ⟦ε⟧)
+ ⇒ w tt with ∣ w ∣
+ ... | zero = PT.∣ ⊎.inr refl ∣
+ ... | suc n = PT.∣ ⊎.inl (znots ∘ sym) ∣
+
+ ⇐ : ∀ w → w ∈ ((A ⁺) ∪ ⟦ε⟧) → w ∈ (A *)
+ ⇐ w x = tt
+
+ _·_ : Lang A → Lang A → Lang A
+ (L · M) w =
+ ∃[ a ∶ Word A ] ∃[ b ∶ Word A ]
+ L a ⊓ M b ⊓ ((a ++ b ≡ w) , isSet-List _ _)
M Regex.agda => Regex.agda +38 -33
@@ 11,7 11,7 @@ open import Cubical.Data.List hiding ([_])
open import Cubical.Data.List.Properties
open import Common
-open import Lang hiding (∅)
+open import Lang
open import Fin
repeat : {A : Type₀} → ℕ → List A → List A
@@ 19,25 19,26 @@ repeat zero xs = []
repeat (suc n) xs = xs ++ repeat n xs
module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
- infixr 10 _+_ _·_
- infixr 11 _*
+ infixr 10 _+′_ _·′_
+ infixr 11 _*′
data Regex : Type₀ where
- ∅ ε : Regex
+ ∅′ ε′ : Regex
char : A → Regex
- _+_ _·_ : Regex → Regex → Regex
- _* : Regex → Regex
+ _+′_ _·′_ : Regex → Regex → Regex
+ _*′ : Regex → Regex
- lang : Regex → Lang A
- lang ∅ w = ⊥
- lang ε w = ⟦ε⟧ A w
+module _ {A : Type₀} {{isFinSetA : isFinSet A}} where
+ lang : Regex A → Lang A
+ lang ∅′ w = ⊥
+ lang ε′ w = ⟦ε⟧ w
lang (char x) w = (w ≡ x ∷ []) , isOfHLevelList 0 isFinSet→isSet _ _
- lang (x + y) w = (lang x ∪ lang y) w
- lang (x · y) w =
+ lang (x +′ y) = lang x ∪ lang y
+ lang (x ·′ y) w =
∃[ u ] ∃[ v ] lang x u ⊓ lang y v ⊓
( (u ++ v ≡ w)
, isOfHLevelList 0 isFinSet→isSet _ _
)
- lang (x *) w =
+ lang (x *′) w =
⋃ ℕ
(λ n u →
( (u ≡ repeat n w)
@@ 46,38 47,42 @@ module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
)
w
- {-
+ {-|
Languages definable by regular expressions
-}
RegexLangs : ℙ (Lang A)
- RegexLangs M = ∃[ x ∶ Regex ] (lang x ≡ M) , powersets-are-sets _ _
+ RegexLangs M = ∃[ x ∶ Regex A ] (lang x ≡ M) , powersets-are-sets _ _
RegexQuot : Type₁
- RegexQuot = Regex / λ x y → lang x ≡ lang y
+ RegexQuot = Regex A / λ x y → lang x ≡ lang y
- [_] : Regex → RegexQuot
+ [_] : Regex A → RegexQuot
[_] = _/_.[_]
- +-comm : ∀ {x y} → [ x + y ] ≡ [ y + x ]
+ +-comm : ∀ {x y} → [ x +′ y ] ≡ [ y +′ x ]
+-comm {x} {y} = eq/ _ _ (∪-comm (lang x) (lang y))
-module example where
- A : Type₀
- A = Fin 2
+private
+ module example where
+ A : Type₀
+ A = Fin 2
- -- (0|1)*01(0|1)*
- x : Regex A
- x = (char zero + char (suc zero))* · char zero · char (suc zero) · (char zero + char (suc zero))*
+ -- (0|1)*01(0|1)*
+ x : Regex A
+ x
+ = (char zero +′ char (suc zero))*′
+ ·′ char zero ·′ char (suc zero)
+ ·′ (char zero +′ char (suc zero))*′
- 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)
+ 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
- L = lang A x
+ L : Lang A
+ L = lang x
- _ : L ≡ P
- _ = TODO
+ _ : L ≡ P
+ _ = TODO
A Regular.agda => Regular.agda +77 -0
@@ 0,0 1,77 @@
+{-# OPTIONS --cubical #-}
+
+module Regular where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Logic
+open import Cubical.HITs.PropositionalTruncation as PT
+
+open import Axioms
+open import Common
+open import Fin
+open import Lang
+open import Regex
+
+private
+ variable
+ ℓ : Level
+
+isRegular : {A : Type₀} {{isFinSet-A : isFinSet A}} → Lang A → Type₁
+isRegular w = w ∈ RegexLangs
+
+rec2′ : ∀ {A B P : Type ℓ} → isProp P → (A → B → P) → ∥ A ∥ → ∥ B ∥ → P
+rec2′ Pprop f =
+ rec (isPropΠ (λ _ → Pprop))
+ (λ a → rec Pprop (f a))
+
+module _
+ {A : Type₀}
+ {{isFinSet-A : isFinSet A}}
+ {L M : Lang A}
+ {{isRegular-L : isRegular L}}
+ {{isRegular-M : isRegular M}}
+ where
+ instance
+ reg-closed-under-∪ : isRegular (L ∪ M)
+ reg-closed-under-∪ = prf it it
+ where
+ prf : isRegular L → isRegular M → isRegular (L ∪ M)
+ prf = rec2′ squash λ (x , lang-x≡L) (y , lang-y≡M) →
+ ∥_∥.∣
+ ( x +′ y
+ , ( lang (x +′ y) ≡⟨ refl ⟩
+ lang x ∪ lang y ≡⟨ cong₂ _∪_ lang-x≡L lang-y≡M ⟩
+ L ∪ M ∎
+ )
+ )
+ ∣
+
+module _
+ {A : Type₀}
+ {{isFinSet-A : isFinSet A}}
+ {L : Lang A}
+ {{isRegular-L : isRegular L}}
+ where
+ instance
+ reg-closed-under-¬ : isRegular (L ᶜ)
+ reg-closed-under-¬ = TODO
+
+module _
+ {A : Type₀}
+ {{isFinSet-A : isFinSet A}}
+ {L M : Lang A}
+ {{isRegular-L : isRegular L}}
+ {{isRegular-M : isRegular M}}
+ where
+ instance
+ reg-closed-under-∩ : {{_ : LEM}} → isRegular (L ∩ M)
+ reg-closed-under-∩ = proof
+ where
+ lemma : isRegular (((L ᶜ) ∪ (M ᶜ))ᶜ)
+ lemma = it
+
+ proof : isRegular (L ∩ M)
+ proof = subst
+ isRegular
+ (sym (de-morgan-∩ {A = L} {B = M}))
+ lemma