From ff3600687249a19ae63353f7791b137094f5a5a1 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 18 Feb 2021 19:04:09 +0000 Subject: Another redefinition of Language. --- src/Cfe/Language/Base.agda | 233 ++++++++++++++---------- src/Cfe/Language/Construct/Concatenate.agda | 51 ++---- src/Cfe/Language/Construct/Single.agda | 71 +++----- src/Cfe/Language/Construct/Union.agda | 99 +++------- src/Cfe/Language/Indexed/Construct/Iterate.agda | 70 +++++++ src/Cfe/Language/Indexed/Homogeneous.agda | 47 +++++ 6 files changed, 329 insertions(+), 242 deletions(-) create mode 100644 src/Cfe/Language/Indexed/Construct/Iterate.agda create mode 100644 src/Cfe/Language/Indexed/Homogeneous.agda diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda index c1ff398..f0d1bb7 100644 --- a/src/Cfe/Language/Base.agda +++ b/src/Cfe/Language/Base.agda @@ -1,118 +1,163 @@ {-# OPTIONS --without-K --safe #-} -open import Relation.Binary +open import Relation.Binary as B using (Setoid) module Cfe.Language.Base - {c ℓ} (setoid : Setoid c ℓ) + {c ℓ} (over : Setoid c ℓ) where -open Setoid setoid renaming (Carrier to A) +open Setoid over using () renaming (Carrier to C) +open import Cfe.Relation.Indexed 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 Data.List.Relation.Binary.Equality.Setoid over +open import Data.Product +open import Function hiding (Injection; Surjection; Inverse) +import Function.Equality as Equality using (setoid) +open import Level as L hiding (Lift) +open import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial import Relation.Binary.PropositionalEquality as ≡ -import Relation.Binary.Indexed.Heterogeneous as I +open import Relation.Binary.Indexed.Heterogeneous -record IsLanguage {a aℓ} (𝕃 : List A → Set a) (_≈ᴸ_ : ∀ {l} → Rel (𝕃 l) aℓ) (⤖ : ∀ {l₁ l₂} → l₁ ≋ l₂ → 𝕃 l₁ → 𝕃 l₂) : Set (c ⊔ ℓ ⊔ a ⊔ aℓ) where - field - ≈ᴸ-isEquivalence : ∀ {l} → IsEquivalence (_≈ᴸ_ {l}) - ⤖-cong : ∀ {l₁ l₂ l₁≋l₂} → (⤖ l₁≋l₂) Preserves _≈ᴸ_ {l₁} ⟶ _≈ᴸ_ {l₂} - ⤖-bijective : ∀ {l₁ l₂ l₁≋l₂} → Bijective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ l₁≋l₂) - ⤖-refl : ∀ {l l∈𝕃} → (⤖ {l} ≋-refl l∈𝕃) ≈ᴸ l∈𝕃 - ⤖-sym : ∀ {l₁ l₂ l₁∈𝕃 l₂∈𝕃 l₁≋l₂} - → (⤖ {l₁} l₁≋l₂ l₁∈𝕃) ≈ᴸ l₂∈𝕃 - → (⤖ {l₂} (≋-sym l₁≋l₂) l₂∈𝕃) ≈ᴸ l₁∈𝕃 - ⤖-trans : ∀ {l₁ 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₃∈𝕃 - - ≈ᴸ-refl : ∀ {l} → Reflexive (_≈ᴸ_ {l}) - ≈ᴸ-refl = IsEquivalence.refl ≈ᴸ-isEquivalence - - ≈ᴸ-sym : ∀ {l} → Symmetric (_≈ᴸ_ {l}) - ≈ᴸ-sym = IsEquivalence.sym ≈ᴸ-isEquivalence - - ≈ᴸ-trans : ∀ {l} → Transitive (_≈ᴸ_ {l}) - ≈ᴸ-trans = IsEquivalence.trans ≈ᴸ-isEquivalence - - ≈ᴸ-reflexive : ∀ {l} → ≡._≡_ ⇒ (_≈ᴸ_ {l}) - ≈ᴸ-reflexive = IsEquivalence.reflexive ≈ᴸ-isEquivalence - - ⤖-injective : ∀ {l₁ l₂ l₁≋l₂} → Injective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ l₁≋l₂) - ⤖-injective = proj₁ ⤖-bijective - - ⤖-surjective : ∀ {l₁ l₂ l₁≋l₂} → Surjective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ {l₁} l₁≋l₂) - ⤖-surjective = proj₂ ⤖-bijective - - ⤖-isIndexedEquivalence : I.IsIndexedEquivalence 𝕃 (λ l₁∈𝕃 l₂∈𝕃 → ∃[ l₁≋l₂ ] ((⤖ l₁≋l₂ l₁∈𝕃) ≈ᴸ l₂∈𝕃)) - ⤖-isIndexedEquivalence = record - { refl = ≋-refl , ⤖-refl - ; sym = Product.map ≋-sym ⤖-sym - ; trans = Product.zip ≋-trans ⤖-trans +Language : ∀ a aℓ → Set (suc c ⊔ suc a ⊔ suc aℓ) +Language a aℓ = IndexedSetoid (List C) a aℓ + +∅ : Language 0ℓ 0ℓ +∅ = Trivial.indexedSetoid (≡.setoid ⊥) + +｛ε｝ : Language (c ⊔ ℓ) (c ⊔ ℓ) +｛ε｝ = record + { Carrier = [] ≋_ + ; _≈_ = λ {l₁} {l₂} []≋l₁ []≋l₂ → ∃[ l₁≋l₂ ] (≋-trans []≋l₁ l₁≋l₂ ≡.≡ []≋l₂) + ; isEquivalence = record + { refl = λ {_} {x} → + ≋-refl , + ( case x return (λ x → ≋-trans x ≋-refl ≡.≡ x) of λ {[] → ≡.refl} ) + ; sym = λ {_} {_} {x} {y} (z , _) → + ≋-sym z , + ( case (x , y , z) + return (λ (x , y , z) → ≋-trans y (≋-sym z) ≡.≡ x) + of λ {([] , [] , []) → ≡.refl} ) + ; trans = λ {_} {_} {_} {v} {w} {x} (y , _) (z , _) → + ≋-trans y z , + ( case (v , w , x , y , z) + return (λ (v , _ , x , y , z) → ≋-trans v (≋-trans y z) ≡.≡ x) + of λ {([] , [] , [] , [] , []) → ≡.refl} ) } + } - ⤖-reflexive : ∀ {l l∈𝕃 l∈𝕃′} → l∈𝕃 ≡.≡ l∈𝕃′ → ∃[ l≋l ]((⤖ {l} l≋l l∈𝕃) ≈ᴸ l∈𝕃′) - ⤖-reflexive = I.IsIndexedEquivalence.reflexive ⤖-isIndexedEquivalence +Lift : ∀ {a aℓ} → (b bℓ : Level) → Language a aℓ → Language (a ⊔ b) (aℓ ⊔ bℓ) +Lift b bℓ A = record + { Carrier = L.Lift b ∘ A.Carrier + ; _≈_ = λ (lift x) (lift y) → L.Lift bℓ (x A.≈ y) + ; isEquivalence = record + { refl = lift A.refl + ; sym = λ (lift x) → lift (A.sym x) + ; trans = λ (lift x) (lift y) → lift (A.trans x y) + } + } + where + module A = IndexedSetoid A -record Language a aℓ : Set (c ⊔ ℓ ⊔ suc (a ⊔ aℓ)) where - infix 4 _≈ᴸ_ - field - 𝕃 : List A → Set a - _≈ᴸ_ : ∀ {l} → Rel (𝕃 l) aℓ - ⤖ : ∀ {l₁ l₂} → l₁ ≋ l₂ → 𝕃 l₁ → 𝕃 l₂ - isLanguage : IsLanguage 𝕃 _≈ᴸ_ ⤖ +𝕃 : ∀ {a aℓ} → Language a aℓ → List C → Set a +𝕃 = IndexedSetoid.Carrier - open IsLanguage isLanguage public +_∈_ : ∀ {a aℓ} → List C → Language a aℓ → Set a +_∈_ = flip 𝕃 -open Language +≈ᴸ : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → 𝕃 A l₁ → 𝕃 A l₂ → Set aℓ +≈ᴸ = IndexedSetoid._≈_ -infix 4 _∈_ +≈ᴸ-refl : ∀ {a aℓ} → (A : Language a aℓ) → Reflexive (𝕃 A) (≈ᴸ A) +≈ᴸ-refl = IsIndexedEquivalence.refl ∘ IndexedSetoid.isEquivalence -_∈_ : ∀ {a aℓ} → List A → Language a aℓ → Set a -l ∈ A = 𝕃 A l +≈ᴸ-sym : ∀ {a aℓ} → (A : Language a aℓ) → Symmetric (𝕃 A) (≈ᴸ A) +≈ᴸ-sym = IsIndexedEquivalence.sym ∘ IndexedSetoid.isEquivalence -∅ : Language 0ℓ 0ℓ -∅ = record - { 𝕃 = const ⊥ - ; _≈ᴸ_ = ≡._≡_ - ; ⤖ = const id - ; isLanguage = record - { ≈ᴸ-isEquivalence = ≡.isEquivalence - ; ⤖-cong = ≡.cong id - ; ⤖-bijective = (λ {x} → ⊥-elim x) , (λ ()) - ; ⤖-refl = λ {_} {l∈𝕃} → ⊥-elim l∈𝕃 - ; ⤖-sym = λ {_} {_} {l₁∈𝕃} → ⊥-elim l₁∈𝕃 - ; ⤖-trans = λ {_} {_} {_} {l₁∈𝕃} → ⊥-elim l₁∈𝕃 - } +≈ᴸ-trans : ∀ {a aℓ} → (A : Language a aℓ) → Transitive (𝕃 A) (≈ᴸ A) +≈ᴸ-trans = IsIndexedEquivalence.trans ∘ IndexedSetoid.isEquivalence + +record _≤_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where + field + f : ∀ {l} → l ∈ A → l ∈ B + cong : ∀ {l₁ l₂ l₁∈A l₂∈A} → ≈ᴸ A {l₁} {l₂} l₁∈A l₂∈A → ≈ᴸ B (f l₁∈A) (f l₂∈A) + +record _≈_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (c ⊔ ℓ ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where + field + f : ∀ {l} → l ∈ A → l ∈ B + f⁻¹ : ∀ {l} → l ∈ B → l ∈ A + cong₁ : ∀ {l₁ l₂ l₁∈A l₂∈A} → ≈ᴸ A {l₁} {l₂} l₁∈A l₂∈A → ≈ᴸ B (f l₁∈A) (f l₂∈A) + cong₂ : ∀ {l₁ l₂ l₁∈B l₂∈B} → ≈ᴸ B {l₁} {l₂} l₁∈B l₂∈B → ≈ᴸ A (f⁻¹ l₁∈B) (f⁻¹ l₂∈B) + +≈-refl : ∀ {a aℓ} → B.Reflexive (_≈_ {a} {aℓ}) +≈-refl {x = A} = record + { f = id + ; f⁻¹ = id + ; cong₁ = id + ; cong₂ = id } -⦃ε⦄ : Language (c ⊔ ℓ) (c ⊔ ℓ) -⦃ε⦄ = record - { 𝕃 = [] ≋_ - ; _≈ᴸ_ = ≡._≡_ - ; ⤖ = flip ≋-trans - ; isLanguage = record - { ≈ᴸ-isEquivalence = ≡.isEquivalence - ; ⤖-cong = λ {_} {_} {l₁≋l₂} → ≡.cong (flip ≋-trans l₁≋l₂) - ; ⤖-bijective = λ {_} {_} {l₁≋l₂} → - ( (λ {x} {y} x≡y → case x , y return (λ (x , y) → x ≡.≡ y) of λ { ([] , []) → ≡.refl }) - , (λ { [] → (case l₁≋l₂ return (λ x → ∃[ y ](≋-trans y x ≡.≡ [])) of λ { [] → [] , ≡.refl})})) - ; ⤖-refl = λ {_} {[]≋l} → case []≋l return (λ []≋l → ≋-trans []≋l ≋-refl ≡.≡ []≋l) of λ {[] → ≡.refl} - ; ⤖-sym = λ {_} {_} {[]≋l₁} {[]≋l₂} {l₁≋l₂} _ → - case []≋l₁ , []≋l₂ , l₁≋l₂ - return (λ ([]≋l₁ , []≋l₂ , l₁≋l₂) → ≋-trans []≋l₂ (≋-sym l₁≋l₂) ≡.≡ []≋l₁) - of λ { ([] , [] , []) → ≡.refl } - ; ⤖-trans = λ {_} {_} {_} {[]≋l₁} {[]≋l₂} {[]≋l₃} {l₁≋l₂} {l₂≋l₃} _ _ → - case []≋l₁ , []≋l₂ , []≋l₃ , l₁≋l₂ , l₂≋l₃ - return (λ ([]≋l₁ , []≋l₂ , []≋l₃ , l₁≋l₂ , l₂≋l₃) → ≋-trans []≋l₁ (≋-trans l₁≋l₂ l₂≋l₃) ≡.≡ []≋l₃) - of λ { ([] , [] , [] , [] , []) → ≡.refl } +≈-sym : ∀ {a aℓ b bℓ} → B.Sym (_≈_ {a} {aℓ} {b} {bℓ}) _≈_ +≈-sym A≈B = record + { f = A≈B.f⁻¹ + ; f⁻¹ = A≈B.f + ; cong₁ = A≈B.cong₂ + ; cong₂ = A≈B.cong₁ + } + where + module A≈B = _≈_ A≈B + +≈-trans : ∀ {a aℓ b bℓ c cℓ} → B.Trans (_≈_ {a} {aℓ}) (_≈_ {b} {bℓ} {c} {cℓ}) _≈_ +≈-trans {i = A} {B} {C} A≈B B≈C = record + { f = B≈C.f ∘ A≈B.f + ; f⁻¹ = A≈B.f⁻¹ ∘ B≈C.f⁻¹ + ; cong₁ = B≈C.cong₁ ∘ A≈B.cong₁ + ; cong₂ = A≈B.cong₂ ∘ B≈C.cong₂ + } + where + module A≈B = _≈_ A≈B + module B≈C = _≈_ B≈C + +setoid : ∀ a aℓ → B.Setoid (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ) +setoid a aℓ = record + { Carrier = Language a aℓ + ; _≈_ = _≈_ + ; isEquivalence = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans } } -_≤_ : {a aℓ b bℓ : Level} → REL (Language a aℓ) (Language b bℓ) (c ⊔ a ⊔ b) -A ≤ B = ∀ {l} → l ∈ A → l ∈ B +≤-refl : ∀ {a aℓ} → B.Reflexive (_≤_ {a} {aℓ}) +≤-refl = record + { f = id + ; cong = id + } + +≤-trans : ∀ {a aℓ b bℓ c cℓ} → B.Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_ +≤-trans A≤B B≤C = record + { f = B≤C.f ∘ A≤B.f + ; cong = B≤C.cong ∘ A≤B.cong + } + where + module A≤B = _≤_ A≤B + module B≤C = _≤_ B≤C + +≤-antisym : ∀ {a aℓ b bℓ} → B.Antisym (_≤_ {a} {aℓ} {b} {bℓ}) _≤_ _≈_ +≤-antisym A≤B B≤A = record + { f = A≤B.f + ; f⁻¹ = B≤A.f + ; cong₁ = A≤B.cong + ; cong₂ = B≤A.cong + } + where + module A≤B = _≤_ A≤B + module B≤A = _≤_ B≤A + +≤-min : ∀ {b bℓ} → B.Min (_≤_ {b = b} {bℓ}) ∅ +≤-min A = record + { f = λ () + ; cong = λ {_} {_} {} + } diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda index b75f822..29e635d 100644 --- a/src/Cfe/Language/Construct/Concatenate.agda +++ b/src/Cfe/Language/Construct/Concatenate.agda @@ -4,56 +4,37 @@ 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ℓ) + {c ℓ a aℓ b bℓ} (over : Setoid c ℓ) + (A : Cfe.Language.Language over a aℓ) + (B : Cfe.Language.Language over b bℓ) where open import Data.Empty open import Data.List -open import Data.List.Relation.Binary.Equality.Setoid setoid +open import Data.List.Relation.Binary.Equality.Setoid over open import Data.Product as Product open import Function open import Level -open import Cfe.Language setoid -open Language +open import Cfe.Language over -open Setoid setoid renaming (Carrier to C) +open Setoid over 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))) +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} → REL (Concat l₁) (Concat l₂) (aℓ ⊔ bℓ) +(_ , l₁∈A , _ , l₂∈B , _) ≈ᶜ (_ , l₁′∈A , _ , l₂′∈B , _) = (≈ᴸ A l₁∈A l₁′∈A) × (≈ᴸ B 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ℓ) +_∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b) (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)) + { Carrier = Concat + ; _≈_ = _≈ᶜ_ + ; isEquivalence = record + { refl = ≈ᴸ-refl A , ≈ᴸ-refl B + ; sym = Product.map (≈ᴸ-sym A) (≈ᴸ-sym B) + ; trans = Product.zip (≈ᴸ-trans A) (≈ᴸ-trans B) } } diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda index f54e015..daa1628 100644 --- a/src/Cfe/Language/Construct/Single.agda +++ b/src/Cfe/Language/Construct/Single.agda @@ -5,56 +5,47 @@ 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) + {c ℓ} (over : Setoid c ℓ) + (≈-trans-bijₗ : ∀ {a b c b≈c} + → Bijective ≡._≡_ ≡._≡_ (flip (Setoid.trans over {a} {b} {c}) b≈c)) + (≈-trans-reflₗ : ∀ {a b a≈b} + → Setoid.trans over {a} a≈b (Setoid.refl over {b}) ≡.≡ a≈b) + (≈-trans-symₗ : ∀ {a b c a≈b a≈c b≈c} + → Setoid.trans over {a} {b} {c} a≈b b≈c ≡.≡ a≈c + → Setoid.trans over a≈c (Setoid.sym over b≈c) ≡.≡ a≈b) + (≈-trans-transₗ : ∀ {a b c d a≈b a≈c a≈d b≈c c≈d} + → Setoid.trans over {a} {b} a≈b b≈c ≡.≡ a≈c + → Setoid.trans over {a} {c} {d} a≈c c≈d ≡.≡ a≈d + → Setoid.trans over a≈b (Setoid.trans over b≈c c≈d) ≡.≡ a≈d) where -open Setoid setoid renaming (Carrier to A) +open Setoid over renaming (Carrier to C) -open import Cfe.Language setoid +open import Cfe.Language over hiding (_≈_) open import Data.List -open import Data.List.Relation.Binary.Equality.Setoid setoid +open import Data.List.Relation.Binary.Equality.Setoid over 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 : {a b : C} {l₁ l₂ : List C} {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ₗ : {x l₁ l₂ : List C} → {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ₗ : {x l₁ l₂ : List C} → {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ₗ : {l₁ l₂ : List C} {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-symₗ : {l₁ l₂ l₃ : List C} {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 @@ -62,7 +53,7 @@ private ∘ Product.map ≈-trans-symₗ ≋-trans-symₗ ∘ ∷-inj - ≋-trans-transₗ : {l₁ l₂ l₃ l₄ : List A} + ≋-trans-transₗ : {l₁ l₂ l₃ l₄ : List C} → {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₄ @@ -72,17 +63,13 @@ private ∘₂ 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ₗ +｛_｝ : C → Language (c ⊔ ℓ) (c ⊔ ℓ) +｛ c ｝ = record + { Carrier = [ c ] ≋_ + ; _≈_ = λ l≋m l≋n → ∃[ m≋n ] ≋-trans l≋m m≋n ≡.≡ l≋n + ; isEquivalence = record + { refl = ≋-refl , ≋-trans-reflₗ + ; sym = Product.map ≋-sym ≋-trans-symₗ + ; trans = Product.zip ≋-trans ≋-trans-transₗ } } diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda index 44d4c3f..ee8b0f7 100644 --- a/src/Cfe/Language/Construct/Union.agda +++ b/src/Cfe/Language/Construct/Union.agda @@ -4,99 +4,56 @@ 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ℓ) + {c ℓ a aℓ b bℓ} (over : Setoid c ℓ) + (A : Cfe.Language.Language over a aℓ) + (B : Cfe.Language.Language over b bℓ) where open import Data.Empty open import Data.List -open import Data.List.Relation.Binary.Equality.Setoid setoid +open import Data.List.Relation.Binary.Equality.Setoid over 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 import Cfe.Language over hiding (Lift) -open Setoid setoid renaming (Carrier to C) +open Setoid over renaming (Carrier to C) infix 4 _≈ᵁ_ infix 4 _∪_ Union : List C → Set (a ⊔ b) -Union l = 𝕃 A l ⊎ 𝕃 B l +Union l = l ∈ A ⊎ l ∈ B -_≈ᵁ_ : {l : List C} → Rel (Union l) (aℓ ⊔ bℓ) -(inj₁ x) ≈ᵁ (inj₁ y) = Lift bℓ (_≈ᴸ_ A x y) +_≈ᵁ_ : {l₁ l₂ : List C} → REL (Union l₁) (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₂) +(inj₂ x) ≈ᵁ (inj₂ y) = Lift aℓ (≈ᴸ B x y) _∪_ : 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) + { Carrier = Union + ; _≈_ = _≈ᵁ_ + ; isEquivalence = record + { refl = λ {_} {x} → case x return (λ x → 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) + ; 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 = λ {_} {_} {_} {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) + ; trans = λ {_} {_} {_} {x} {y} {z} x≈ᵁy y≈ᵁz → + case ∃[ x ] ∃[ y ] ∃[ z ] x ≈ᵁ y × y ≈ᵁ z ∋ x , y , z , x≈ᵁy , y≈ᵁz + return (λ (x , _ , z , _) → x ≈ᵁ z) 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) } } } diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda new file mode 100644 index 0000000..62a946e --- /dev/null +++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda @@ -0,0 +1,70 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary as B using (Setoid) + +module Cfe.Language.Indexed.Construct.Iterate + {c ℓ} (over : Setoid c ℓ) + where + +open Setoid over using () renaming (Carrier to C) + +open import Cfe.Language over +open import Cfe.Language.Indexed.Homogeneous over +open import Data.List +open import Data.Nat as ℕ hiding (_⊔_) +open import Data.Product as Product +open import Function +open import Level hiding (Lift) renaming (suc to lsuc) +open import Relation.Binary.Indexed.Heterogeneous +open import Relation.Binary.PropositionalEquality as ≡ + +open IndexedLanguage + +iter : ∀ {a} {A : Set a} → (A → A) → ℕ → A → A +iter f ℕ.zero = id +iter f (ℕ.suc n) = f ∘ iter f n + +Iterate : ∀ {a aℓ} → (Language a aℓ → Language a aℓ) → IndexedLanguage 0ℓ 0ℓ a aℓ +Iterate {a} {aℓ} f = record + { Carrierᵢ = ℕ + ; _≈ᵢ_ = ≡._≡_ + ; isEquivalenceᵢ = ≡.isEquivalence + ; F = λ n → iter f n (Lift a aℓ ∅) + ; cong = λ {≡.refl → ≈-refl} + } + +≈ᵗ-refl : ∀ {a aℓ} → + (g : Language a aℓ → Language a aℓ) → + Reflexive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g)) +≈ᵗ-refl g {_} {n , _} = refl , (≈ᴸ-refl (Iter.F n)) + where + module Iter = IndexedLanguage (Iterate g) + +≈ᵗ-sym : ∀ {a aℓ} → + (g : Language a aℓ → Language a aℓ) → + Symmetric (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g)) +≈ᵗ-sym g {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) = + refl , (≈ᴸ-sym (Iter.F n) x∈Fn≈y∈Fn) + where + module Iter = IndexedLanguage (Iterate g) + +≈ᵗ-trans : ∀ {a aℓ} → + (g : Language a aℓ → Language a aℓ) → + Transitive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g)) +≈ᵗ-trans g {_} {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) (refl , y∈Fn≈z∈Fn) = + refl , (≈ᴸ-trans (Iter.F n) x∈Fn≈y∈Fn y∈Fn≈z∈Fn) + where + module Iter = IndexedLanguage (Iterate g) + +⋃ : ∀ {a aℓ} → (Language a aℓ → Language a aℓ) → Language a aℓ +⋃ f = record + { Carrier = Iter.Tagged + ; _≈_ = Iter._≈ᵗ_ + ; isEquivalence = record + { refl = ≈ᵗ-refl f + ; sym = ≈ᵗ-sym f + ; trans = ≈ᵗ-trans f + } + } + where + module Iter = IndexedLanguage (Iterate f) diff --git a/src/Cfe/Language/Indexed/Homogeneous.agda b/src/Cfe/Language/Indexed/Homogeneous.agda new file mode 100644 index 0000000..c032978 --- /dev/null +++ b/src/Cfe/Language/Indexed/Homogeneous.agda @@ -0,0 +1,47 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary as B using (Setoid) + +module Cfe.Language.Indexed.Homogeneous + {c ℓ} (over : Setoid c ℓ) + where + +open import Cfe.Language over +open import Level +open import Data.List +open import Data.Product +open import Relation.Binary.Indexed.Heterogeneous + +open _≈_ + +open Setoid over using () renaming (Carrier to C) + +record IndexedLanguage i iℓ a aℓ : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a ⊔ aℓ)) where + field + Carrierᵢ : Set i + _≈ᵢ_ : B.Rel Carrierᵢ iℓ + isEquivalenceᵢ : B.IsEquivalence _≈ᵢ_ + F : Carrierᵢ → Language a aℓ + cong : F B.Preserves _≈ᵢ_ ⟶ _≈_ + + open B.IsEquivalence isEquivalenceᵢ using () renaming (refl to reflᵢ; sym to symᵢ; trans to transᵢ) public + + Tagged : List C → Set (i ⊔ a) + Tagged l = ∃[ i ] l ∈ F i + + _≈ᵗ_ : IRel Tagged (iℓ ⊔ aℓ) + _≈ᵗ_ (i , l∈Fi) (j , m∈Fj) = Σ (i ≈ᵢ j) λ i≈j → ≈ᴸ (F j) (f (cong i≈j) l∈Fi) m∈Fj + + -- ≈ᵗ-refl : Reflexive Tagged _≈ᵗ_ + -- ≈ᵗ-refl {l} {i , l∈Fi} = reflᵢ , {!≈ᴸ-refl!} + + -- ⋃ : Language (i ⊔ a) (iℓ ⊔ aℓ) + -- ⋃ = record + -- { Carrier = Tagged + -- ; _≈_ = _≈ᵗ_ + -- ; isEquivalence = record + -- { refl = λ i≈j → {!!} + -- ; sym = {!!} + -- ; trans = {!!} + -- } + -- } -- cgit v1.2.3