summaryrefslogtreecommitdiff
path: root/src/Cfe/Language/Construct
diff options
context:
space:
mode:
Diffstat (limited to 'src/Cfe/Language/Construct')
-rw-r--r--src/Cfe/Language/Construct/Concatenate.agda59
-rw-r--r--src/Cfe/Language/Construct/Single.agda88
-rw-r--r--src/Cfe/Language/Construct/Union.agda102
3 files changed, 249 insertions, 0 deletions
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
new file mode 100644
index 0000000..b75f822
--- /dev/null
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -0,0 +1,59 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+import Cfe.Language
+
+module Cfe.Language.Construct.Concatenate
+ {c ℓ a aℓ b bℓ} (setoid : Setoid c ℓ)
+ (A : Cfe.Language.Language setoid a aℓ)
+ (B : Cfe.Language.Language setoid b bℓ)
+ where
+
+open import Data.Empty
+open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid setoid
+open import Data.Product as Product
+open import Function
+open import Level
+open import Cfe.Language setoid
+open Language
+
+open Setoid setoid renaming (Carrier to C)
+
+infix 4 _≈ᶜ_
+infix 4 _∙_
+
+Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
+Concat l = ∃[ l₁ ](l₁ ∈ A × ∃[ l₂ ](l₂ ∈ B × (l₁ ++ l₂ ≋ l)))
+
+_≈ᶜ_ : {l : List C} → Rel (Concat l) (c ⊔ ℓ ⊔ aℓ ⊔ bℓ)
+(l₁ , l₁∈A , l₂ , l₂∈B , l₁++l₂) ≈ᶜ (l₁′ , l₁′∈A , l₂′ , l₂′∈B , l₁′++l₂′) =
+ ∃[ l₁≋l₁′ ](_≈ᴸ_ A (⤖ A l₁≋l₁′ l₁∈A) l₁′∈A)
+ × ∃[ l₂≋l₂′ ](_≈ᴸ_ B (⤖ B l₂≋l₂′ l₂∈B) l₂′∈B)
+
+⤖ᶜ : {l₁ l₂ : List C} → l₁ ≋ l₂ → Concat l₁ → Concat l₂
+⤖ᶜ l₁≋l₂ = map₂ (map₂ (map₂ (map₂ (flip ≋-trans l₁≋l₂))))
+
+_∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b) (c ⊔ ℓ ⊔ aℓ ⊔ bℓ)
+_∙_ = record
+ { 𝕃 = Concat
+ ; _≈ᴸ_ = _≈ᶜ_
+ ; ⤖ = ⤖ᶜ
+ ; isLanguage = record
+ { ≈ᴸ-isEquivalence = record
+ { refl = (≋-refl , ⤖-refl A) , (≋-refl , ⤖-refl B)
+ ; sym = Product.map (Product.map ≋-sym (⤖-sym A))
+ (Product.map ≋-sym (⤖-sym B))
+ ; trans = Product.zip (Product.zip ≋-trans (⤖-trans A))
+ (Product.zip ≋-trans (⤖-trans B))
+ }
+ ; ⤖-cong = id
+ ; ⤖-bijective = λ {_} {_} {l₁≋l₂} → id , λ l₂∈𝕃 →
+ ⤖ᶜ (≋-sym l₁≋l₂) l₂∈𝕃 , (≋-refl , ⤖-refl A) , (≋-refl , ⤖-refl B)
+ ; ⤖-refl = (≋-refl , ⤖-refl A) , (≋-refl , ⤖-refl B)
+ ; ⤖-sym = Product.map (Product.map ≋-sym (⤖-sym A))
+ (Product.map ≋-sym (⤖-sym B))
+ ; ⤖-trans = Product.zip (Product.zip ≋-trans (⤖-trans A))
+ (Product.zip ≋-trans (⤖-trans B))
+ }
+ }
diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda
new file mode 100644
index 0000000..f54e015
--- /dev/null
+++ b/src/Cfe/Language/Construct/Single.agda
@@ -0,0 +1,88 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Function
+open import Relation.Binary
+import Relation.Binary.PropositionalEquality as ≡
+
+module Cfe.Language.Construct.Single
+ {a ℓ} (setoid : Setoid a ℓ)
+ (≈-trans-bijₗ : ∀ {a b c : Setoid.Carrier setoid}
+ → {b≈c : Setoid._≈_ setoid b c}
+ → Bijective ≡._≡_ ≡._≡_ (flip (Setoid.trans setoid {a}) b≈c))
+ (≈-trans-reflₗ : ∀ {a b : Setoid.Carrier setoid} {a≈b : Setoid._≈_ setoid a b}
+ → Setoid.trans setoid a≈b (Setoid.refl setoid) ≡.≡ a≈b)
+ (≈-trans-symₗ : ∀ {a b c : Setoid.Carrier setoid}
+ → {a≈b : Setoid._≈_ setoid a b}
+ → {a≈c : Setoid._≈_ setoid a c}
+ → {b≈c : Setoid._≈_ setoid b c}
+ → Setoid.trans setoid a≈b b≈c ≡.≡ a≈c
+ → Setoid.trans setoid a≈c (Setoid.sym setoid b≈c) ≡.≡ a≈b)
+ (≈-trans-transₗ : ∀ {a b c d : Setoid.Carrier setoid}
+ → {a≈b : Setoid._≈_ setoid a b}
+ → {a≈c : Setoid._≈_ setoid a c}
+ → {a≈d : Setoid._≈_ setoid a d}
+ → {b≈c : Setoid._≈_ setoid b c}
+ → {c≈d : Setoid._≈_ setoid c d}
+ → Setoid.trans setoid a≈b b≈c ≡.≡ a≈c
+ → Setoid.trans setoid a≈c c≈d ≡.≡ a≈d
+ → Setoid.trans setoid a≈b (Setoid.trans setoid b≈c c≈d) ≡.≡ a≈d)
+ where
+
+open Setoid setoid renaming (Carrier to A)
+
+open import Cfe.Language setoid
+open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid setoid
+open import Data.Product as Product
+open import Level
+
+private
+ ∷-inj : {a b : A} {l₁ l₂ : List A} {a≈b a≈b′ : a ≈ b} {l₁≋l₂ l₁≋l₂′ : l₁ ≋ l₂} → ≡._≡_ {A = a ∷ l₁ ≋ b ∷ l₂} (a≈b ∷ l₁≋l₂) (a≈b′ ∷ l₁≋l₂′) → (a≈b ≡.≡ a≈b′) × (l₁≋l₂ ≡.≡ l₁≋l₂′)
+ ∷-inj ≡.refl = ≡.refl , ≡.refl
+
+ ≋-trans-injₗ : {x l₁ l₂ : List A} → {l₁≋l₂ : l₁ ≋ l₂} → Injective ≡._≡_ ≡._≡_ (flip (≋-trans {x}) l₁≋l₂)
+ ≋-trans-injₗ {_} {_} {_} {_} {[]} {[]} _ = ≡.refl
+ ≋-trans-injₗ {_} {_} {_} {_ ∷ _} {_ ∷ _} {_ ∷ _} = uncurry (≡.cong₂ _∷_)
+ ∘ Product.map (proj₁ ≈-trans-bijₗ) ≋-trans-injₗ
+ ∘ ∷-inj
+
+ ≋-trans-surₗ : {x l₁ l₂ : List A} → {l₁≋l₂ : l₁ ≋ l₂} → Surjective {A = x ≋ l₁} ≡._≡_ ≡._≡_ (flip (≋-trans {x}) l₁≋l₂)
+ ≋-trans-surₗ {_} {_} {_} {[]} [] = [] , ≡.refl
+ ≋-trans-surₗ {_} {_} {_} {_ ∷ _} (a≈c ∷ x≋l₂) = Product.zip _∷_ (≡.cong₂ _∷_) (proj₂ ≈-trans-bijₗ a≈c) (≋-trans-surₗ x≋l₂)
+
+ ≋-trans-reflₗ : {l₁ l₂ : List A} {l₁≋l₂ : l₁ ≋ l₂} → ≋-trans l₁≋l₂ ≋-refl ≡.≡ l₁≋l₂
+ ≋-trans-reflₗ {_} {_} {[]} = ≡.refl
+ ≋-trans-reflₗ {_} {_} {a≈b ∷ l₁≋l₂} = ≡.cong₂ _∷_ ≈-trans-reflₗ ≋-trans-reflₗ
+
+ ≋-trans-symₗ : {l₁ l₂ l₃ : List A} {l₁≋l₂ : l₁ ≋ l₂} {l₁≋l₃ : l₁ ≋ l₃} {l₂≋l₃ : l₂ ≋ l₃}
+ → ≋-trans l₁≋l₂ l₂≋l₃ ≡.≡ l₁≋l₃
+ → ≋-trans l₁≋l₃ (≋-sym l₂≋l₃) ≡.≡ l₁≋l₂
+ ≋-trans-symₗ {_} {_} {_} {[]} {[]} {[]} _ = ≡.refl
+ ≋-trans-symₗ {_} {_} {_} {_ ∷ _} {_ ∷ _} {_ ∷ _} = uncurry (≡.cong₂ _∷_)
+ ∘ Product.map ≈-trans-symₗ ≋-trans-symₗ
+ ∘ ∷-inj
+
+ ≋-trans-transₗ : {l₁ l₂ l₃ l₄ : List A}
+ → {l₁≋l₂ : l₁ ≋ l₂} {l₁≋l₃ : l₁ ≋ l₃} {l₁≋l₄ : l₁ ≋ l₄} {l₂≋l₃ : l₂ ≋ l₃} {l₃≋l₄ : l₃ ≋ l₄}
+ → ≋-trans l₁≋l₂ l₂≋l₃ ≡.≡ l₁≋l₃
+ → ≋-trans l₁≋l₃ l₃≋l₄ ≡.≡ l₁≋l₄
+ → ≋-trans l₁≋l₂ (≋-trans l₂≋l₃ l₃≋l₄) ≡.≡ l₁≋l₄
+ ≋-trans-transₗ {l₁≋l₂ = []} {[]} {[]} {[]} {[]} _ _ = ≡.refl
+ ≋-trans-transₗ {l₁≋l₂ = _ ∷ _} {_ ∷ _} {_ ∷ _} {_ ∷ _} {_ ∷ _} = uncurry (≡.cong₂ _∷_)
+ ∘₂ uncurry (Product.zip ≈-trans-transₗ ≋-trans-transₗ)
+ ∘₂ curry (Product.map ∷-inj ∷-inj)
+
+｛_｝ : List A → Language (a ⊔ ℓ) (a ⊔ ℓ)
+｛ l ｝ = record
+ { 𝕃 = l ≋_
+ ; _≈ᴸ_ = ≡._≡_
+ ; ⤖ = flip ≋-trans
+ ; isLanguage = record
+ { ≈ᴸ-isEquivalence = ≡.isEquivalence
+ ; ⤖-cong = λ {_} {_} {l₁≋l₂} → ≡.cong (flip ≋-trans l₁≋l₂)
+ ; ⤖-bijective = ≋-trans-injₗ , ≋-trans-surₗ
+ ; ⤖-refl = ≋-trans-reflₗ
+ ; ⤖-sym = ≋-trans-symₗ
+ ; ⤖-trans = ≋-trans-transₗ
+ }
+ }
diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda
new file mode 100644
index 0000000..44d4c3f
--- /dev/null
+++ b/src/Cfe/Language/Construct/Union.agda
@@ -0,0 +1,102 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+import Cfe.Language
+
+module Cfe.Language.Construct.Union
+ {c ℓ a aℓ b bℓ} (setoid : Setoid c ℓ)
+ (A : Cfe.Language.Language setoid a aℓ)
+ (B : Cfe.Language.Language setoid b bℓ)
+ where
+
+open import Data.Empty
+open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid setoid
+open import Data.Product as Product
+open import Data.Sum as Sum
+open import Function
+open import Level
+open import Cfe.Language setoid
+open Language
+
+open Setoid setoid renaming (Carrier to C)
+
+infix 4 _≈ᵁ_
+infix 4 _∪_
+
+Union : List C → Set (a ⊔ b)
+Union l = 𝕃 A l ⊎ 𝕃 B l
+
+_≈ᵁ_ : {l : List C} → Rel (Union l) (aℓ ⊔ bℓ)
+(inj₁ x) ≈ᵁ (inj₁ y) = Lift bℓ (_≈ᴸ_ A x y)
+(inj₁ _) ≈ᵁ (inj₂ _) = Lift (aℓ ⊔ bℓ) ⊥
+(inj₂ _) ≈ᵁ (inj₁ _) = Lift (aℓ ⊔ bℓ) ⊥
+(inj₂ x) ≈ᵁ (inj₂ y) = Lift aℓ (_≈ᴸ_ B x y)
+
+⤖ᵁ : {l₁ l₂ : List C} → l₁ ≋ l₂ → Union l₁ → Union l₂
+⤖ᵁ l₁≋l₂ = Sum.map (⤖ A l₁≋l₂) (⤖ B l₁≋l₂)
+
+_∪_ : Language (a ⊔ b) (aℓ ⊔ bℓ)
+_∪_ = record
+ { 𝕃 = Union
+ ; _≈ᴸ_ = _≈ᵁ_
+ ; ⤖ = ⤖ᵁ
+ ; isLanguage = record
+ { ≈ᴸ-isEquivalence = record
+ { refl = λ {x} → case x return (λ x → _≈ᵁ_ x x) of λ
+ { (inj₁ x) → lift (≈ᴸ-refl A)
+ ; (inj₂ y) → lift (≈ᴸ-refl B)
+ }
+ ; sym = λ {x} {y} x≈ᵁy →
+ case (∃[ x ](∃[ y ](x ≈ᵁ y)) ∋ x , y , x≈ᵁy)
+ return (λ (x , y , _) → y ≈ᵁ x) of λ
+ { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (≈ᴸ-sym A x≈ᵁy)
+ ; (inj₂ y₁ , inj₂ y , lift x≈ᵁy) → lift (≈ᴸ-sym B x≈ᵁy)
+ }
+ ; trans = λ {i} {j} {k} i≈ᵁj j≈ᵁk →
+ case ∃[ i ](∃[ j ](∃[ k ](i ≈ᵁ j × j ≈ᵁ k))) ∋ i , j , k , i≈ᵁj , j≈ᵁk
+ return (λ (i , _ , k , _) → i ≈ᵁ k) of λ
+ { (inj₁ _ , inj₁ _ , inj₁ _ , lift x≈ᵁy , lift y≈ᵁz) →
+ lift (≈ᴸ-trans A x≈ᵁy y≈ᵁz)
+ ; (inj₂ _ , inj₂ _ , inj₂ _ , lift x≈ᵁy , lift y≈ᵁz) →
+ lift (≈ᴸ-trans B x≈ᵁy y≈ᵁz)
+ }
+ }
+ ; ⤖-cong = λ {_} {_} {l₁≋l₂} {x} {y} x≈ᵁy →
+ case ∃[ x ](∃[ y ](x ≈ᵁ y)) ∋ x , y , x≈ᵁy
+ return (λ (x , y , _) → (_≈ᵁ_ on ⤖ᵁ l₁≋l₂) x y) of λ
+ { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (⤖-cong A x≈ᵁy)
+ ; (inj₂ x , inj₂ y , lift x≈ᵁy) → lift (⤖-cong B x≈ᵁy)
+ }
+ ; ⤖-bijective = λ {_} {_} {l₁≋l₂} →
+ ( λ {x} {y} x≈ᵁy →
+ case ∃[ x ](∃[ y ]((_≈ᵁ_ on ⤖ᵁ l₁≋l₂) x y)) ∋ x , y , x≈ᵁy
+ return (λ (x , y , _) → x ≈ᵁ y) of λ
+ { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (⤖-injective A x≈ᵁy)
+ ; (inj₂ x , inj₂ y , lift x≈ᵁy) → lift (⤖-injective B x≈ᵁy)
+ })
+ , ( λ
+ { (inj₁ x) → Product.map inj₁ lift (⤖-surjective A x)
+ ; (inj₂ x) → Product.map inj₂ lift (⤖-surjective B x)
+ })
+ ; ⤖-refl = λ {_} {x} → case x return (λ x → ⤖ᵁ ≋-refl x ≈ᵁ x) of λ
+ { (inj₁ x) → lift (⤖-refl A)
+ ; (inj₂ y) → lift (⤖-refl B)
+ }
+ ; ⤖-sym = λ {_} {_} {x} {y} {l₁≋l₂} x≈ᵁy →
+ case ∃[ x ](∃[ y ](⤖ᵁ l₁≋l₂ x ≈ᵁ y)) ∋ x , y , x≈ᵁy
+ return (λ (x , y , _) → ⤖ᵁ (≋-sym l₁≋l₂) y ≈ᵁ x) of λ
+ { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (⤖-sym A x≈ᵁy)
+ ; (inj₂ x , inj₂ y , lift x≈ᵁy) → lift (⤖-sym B x≈ᵁy)
+ }
+ ; ⤖-trans = λ {_} {_} {_} {x} {y} {z} {l₁≋l₂} {l₂≋l₃} x≈ᵁy y≈ᵁz →
+ case (∃[ x ](∃[ y ](∃[ z ]((⤖ᵁ l₁≋l₂ x ≈ᵁ y) × (⤖ᵁ l₂≋l₃ y ≈ᵁ z))))) ∋
+ x , y , z , x≈ᵁy , y≈ᵁz
+ return (λ (x , _ , z , _ , _) → ⤖ᵁ (≋-trans l₁≋l₂ l₂≋l₃) x ≈ᵁ z) of λ
+ { (inj₁ x , inj₁ y , inj₁ z , lift x≈ᵁy , lift y≈ᵁz) →
+ lift (⤖-trans A x≈ᵁy y≈ᵁz)
+ ; (inj₂ x , inj₂ y , inj₂ z , lift x≈ᵁy , lift y≈ᵁz) →
+ lift (⤖-trans B x≈ᵁy y≈ᵁz)
+ }
+ }
+ }
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 11:40:57 +0000