diff options
Diffstat (limited to 'src/Cfe/Language')
| -rw-r--r-- | src/Cfe/Language/Base.agda | 95 | ||||
| -rw-r--r-- | src/Cfe/Language/Construct/Concatenate.agda | 116 | ||||
| -rw-r--r-- | src/Cfe/Language/Construct/Single.agda | 15 | ||||
| -rw-r--r-- | src/Cfe/Language/Construct/Union.agda | 44 | ||||
| -rw-r--r-- | src/Cfe/Language/Indexed/Construct/Iterate.agda | 52 | ||||
| -rw-r--r-- | src/Cfe/Language/Indexed/Homogeneous.agda | 7 | ||||
| -rw-r--r-- | src/Cfe/Language/Properties.agda | 42 |
7 files changed, 116 insertions, 255 deletions
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda index 74854df..bda9000 100644 --- a/src/Cfe/Language/Base.agda +++ b/src/Cfe/Language/Base.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} -open import Relation.Binary as B using (Setoid) +open import Relation.Binary module Cfe.Language.Base {c ℓ} (over : Setoid c ℓ) @@ -11,96 +11,61 @@ open Setoid over using () renaming (Carrier to C) open import Algebra open import Data.Empty open import Data.List hiding (null) +open import Data.List.Relation.Binary.Equality.Setoid over open import Data.Product open import Data.Unit using (⊤; tt) -open import Function hiding (Injection; Surjection; Inverse) -import Function.Equality as Equality using (setoid) +open import Function hiding (_⟶_) open import Level as L hiding (Lift) -open import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) -open import Relation.Binary.Indexed.Heterogeneous +open import Relation.Binary.PropositionalEquality infix 4 _∈_ infix 4 _∉_ -Language : ∀ a aℓ → Set (suc c ⊔ suc a ⊔ suc aℓ) -Language a aℓ = IndexedSetoid (List C) a aℓ +record Language a : Set (c ⊔ ℓ ⊔ suc a) where + field + 𝕃 : List C → Set a + ∈-resp-≋ : 𝕃 ⟶ 𝕃 Respects _≋_ -∅ : Language 0ℓ 0ℓ -∅ = Trivial.indexedSetoid (≡.setoid ⊥) +∅ : Language 0ℓ +∅ = record + { 𝕃 = const ⊥ + ; ∈-resp-≋ = λ _ () + } -｛ε｝ : Language c 0ℓ +｛ε｝ : Language c ｛ε｝ = record - { Carrier = [] ≡_ - ; _≈_ = λ _ _ → ⊤ - ; isEquivalence = record - { refl = tt - ; sym = λ _ → tt - ; trans = λ _ _ → tt - } + { 𝕃 = [] ≡_ + ; ∈-resp-≋ = λ { [] refl → refl} } -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) - } +Lift : ∀ {a} → (b : Level) → Language a → Language (a ⊔ b) +Lift b A = record + { 𝕃 = L.Lift b ∘ A.𝕃 + ; ∈-resp-≋ = λ { eq (lift l∈A) → lift (A.∈-resp-≋ eq l∈A)} } where - module A = IndexedSetoid A - -𝕃 : ∀ {a aℓ} → Language a aℓ → List C → Set a -𝕃 = IndexedSetoid.Carrier + module A = Language A -_∈_ : ∀ {a aℓ} → List C → Language a aℓ → Set a -_∈_ = flip 𝕃 +_∈_ : ∀ {a} → List C → Language a → Set a +_∈_ = flip Language.𝕃 -_∉_ : ∀ {a aℓ} → List C → Language a aℓ → Set a +_∉_ : ∀ {a} → List C → Language a → Set a l ∉ A = l ∈ A → ⊥ -∈-cong : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → l₁ ≡ l₂ → l₁ ∈ A → l₂ ∈ A -∈-cong A ≡.refl l∈A = l∈A - -≈ᴸ : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → 𝕃 A l₁ → 𝕃 A l₂ → Set aℓ -≈ᴸ = IndexedSetoid._≈_ - -≈ᴸ-refl : ∀ {a aℓ} → (A : Language a aℓ) → Reflexive (𝕃 A) (≈ᴸ A) -≈ᴸ-refl = IsIndexedEquivalence.refl ∘ IndexedSetoid.isEquivalence - -≈ᴸ-sym : ∀ {a aℓ} → (A : Language a aℓ) → Symmetric (𝕃 A) (≈ᴸ A) -≈ᴸ-sym = IsIndexedEquivalence.sym ∘ IndexedSetoid.isEquivalence - -≈ᴸ-trans : ∀ {a aℓ} → (A : Language a aℓ) → Transitive (𝕃 A) (≈ᴸ A) -≈ᴸ-trans = IsIndexedEquivalence.trans ∘ IndexedSetoid.isEquivalence - -≈ᴸ-cong : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂ l₃ l₄} → - (l₁≡l₂ : l₁ ≡ l₂) → (l₃≡l₄ : l₃ ≡ l₄) → - (l₁∈A : l₁ ∈ A) → (l₃∈A : l₃ ∈ A) → - ≈ᴸ A l₁∈A l₃∈A → - ≈ᴸ A (∈-cong A l₁≡l₂ l₁∈A) (∈-cong A l₃≡l₄ l₃∈A) -≈ᴸ-cong A ≡.refl ≡.refl l₁∈A l₃∈A eq = eq - -record _≤_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where +record _≤_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ a ⊔ 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 +record _≈_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔ 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) -null : ∀ {a} {aℓ} → Language a aℓ → Set a +null : ∀ {a} → Language a → Set a null A = [] ∈ A -first : ∀ {a} {aℓ} → Language a aℓ → C → Set (c ⊔ a) +first : ∀ {a} → Language a → C → Set (c ⊔ a) first A x = ∃[ l ] x ∷ l ∈ A -flast : ∀ {a} {aℓ} → Language a aℓ → C → Set (c ⊔ a) -flast A x = ∃[ l ] (l ≡.≢ [] × ∃[ l′ ] l ++ x ∷ l′ ∈ A) +flast : ∀ {a} → Language a → C → Set (c ⊔ a) +flast A x = ∃[ l ] (l ≢ [] × ∃[ l′ ] l ++ x ∷ l′ ∈ A) diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda index 62acf8f..ef45432 100644 --- a/src/Cfe/Language/Construct/Concatenate.agda +++ b/src/Cfe/Language/Construct/Concatenate.agda @@ -10,6 +10,7 @@ open import Algebra open import Cfe.Language over as 𝕃 open import Data.Empty open import Data.List +open import Data.List.Relation.Binary.Equality.Setoid over open import Data.List.Properties open import Data.Product as Product open import Function @@ -20,108 +21,65 @@ import Relation.Binary.Indexed.Heterogeneous as I open Setoid over using () renaming (Carrier to C) module _ - {a aℓ b bℓ} - (A : Language a aℓ) - (B : Language b bℓ) + {a b} + (A : Language a) + (B : Language b) where - infix 4 _≈ᶜ_ - infix 4 _∙_ + module A = Language A + module B = Language B - Concat : List C → Set (c ⊔ a ⊔ b) - Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≡ l + infix 4 _∙_ - _≈ᶜ_ : {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) + Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b) + Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≋ l - _∙_ : Language (c ⊔ a ⊔ b) (aℓ ⊔ bℓ) + _∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b) _∙_ = record - { Carrier = Concat - ; _≈_ = _≈ᶜ_ - ; isEquivalence = record - { refl = ≈ᴸ-refl A , ≈ᴸ-refl B - ; sym = Product.map (≈ᴸ-sym A) (≈ᴸ-sym B) - ; trans = Product.zip (≈ᴸ-trans A) (≈ᴸ-trans B) + { 𝕃 = Concat + ; ∈-resp-≋ = λ { l≋l′ (_ , l₁∈A , _ , l₂∈B , eq) → -, l₁∈A , -, l₂∈B , ≋-trans eq l≋l′ } } -isMonoid : ∀ {a aℓ} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) +isMonoid : ∀ {a} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝) isMonoid {a} = record { isSemigroup = record { isMagma = record { isEquivalence = ≈-isEquivalence ; ∙-cong = λ X≈Y U≈V → record - { f = λ { (l₁ , l₁∈X , l₂ , l₂∈U , l₁++l₂≡l) → l₁ , _≈_.f X≈Y l₁∈X , l₂ , _≈_.f U≈V l₂∈U , l₁++l₂≡l} - ; f⁻¹ = λ { (l₁ , l₁∈Y , l₂ , l₂∈V , l₁++l₂≡l) → l₁ , _≈_.f⁻¹ X≈Y l₁∈Y , l₂ , _≈_.f⁻¹ U≈V l₂∈V , l₁++l₂≡l} - ; cong₁ = λ { (x , y) → _≈_.cong₁ X≈Y x , _≈_.cong₁ U≈V y} - ; cong₂ = λ { (x , y) → _≈_.cong₂ X≈Y x , _≈_.cong₂ U≈V y} + { f = λ { (_ , l₁∈X , _ , l₂∈U , eq) → -, _≈_.f X≈Y l₁∈X , -, _≈_.f U≈V l₂∈U , eq } + ; f⁻¹ = λ { (_ , l₁∈Y , _ , l₂∈V , eq) → -, _≈_.f⁻¹ X≈Y l₁∈Y , -, _≈_.f⁻¹ U≈V l₂∈V , eq } } } ; assoc = λ X Y Z → record - { f = λ {l} → (λ { (l₁ , (l₁′ , l₁′∈X , l₂′ , l₂′∈Y , l₁′++l₂′≡l₁) , l₂ , l₂∈Z , l₁++l₂≡l) → - l₁′ , l₁′∈X , l₂′ ++ l₂ , (l₂′ , l₂′∈Y , l₂ , l₂∈Z , refl) , (begin - l₁′ ++ l₂′ ++ l₂ ≡˘⟨ ++-assoc l₁′ l₂′ l₂ ⟩ - (l₁′ ++ l₂′) ++ l₂ ≡⟨ cong (_++ l₂) l₁′++l₂′≡l₁ ⟩ - l₁ ++ l₂ ≡⟨ l₁++l₂≡l ⟩ - l ∎)}) - ; f⁻¹ = λ {l} → λ { (l₁ , l₁∈X , l₂ , (l₁′ , l₁′∈Y , l₂′ , l₂′∈Z , l₁′++l₂′≡l₂), l₁++l₂≡l) → - l₁ ++ l₁′ , ( l₁ , l₁∈X , l₁′ , l₁′∈Y , refl) , l₂′ , l₂′∈Z , (begin - (l₁ ++ l₁′) ++ l₂′ ≡⟨ ++-assoc l₁ l₁′ l₂′ ⟩ - l₁ ++ (l₁′ ++ l₂′) ≡⟨ cong (l₁ ++_) l₁′++l₂′≡l₂ ⟩ - l₁ ++ l₂ ≡⟨ l₁++l₂≡l ⟩ - l ∎)} - ; cong₁ = Product.assocʳ - ; cong₂ = Product.assocˡ + { f = λ {l} → λ { (l₁₂ , (l₁ , l₁∈X , l₂ , l₂∈Y , eq₁) , l₃ , l₃∈Z , eq₂) → + -, l₁∈X , -, (-, l₂∈Y , -, l₃∈Z , ≋-refl) , (begin + l₁ ++ l₂ ++ l₃ ≡˘⟨ ++-assoc l₁ l₂ l₃ ⟩ + (l₁ ++ l₂) ++ l₃ ≈⟨ ++⁺ eq₁ ≋-refl ⟩ + l₁₂ ++ l₃ ≈⟨ eq₂ ⟩ + l ∎) } + ; f⁻¹ = λ {l} → λ { (l₁ , l₁∈X , l₂₃ , (l₂ , l₂∈Y , l₃ , l₃∈Z , eq₁) , eq₂) → + -, (-, l₁∈X , -, l₂∈Y , ≋-refl) , -, l₃∈Z , (begin + (l₁ ++ l₂) ++ l₃ ≡⟨ ++-assoc l₁ l₂ l₃ ⟩ + l₁ ++ l₂ ++ l₃ ≈⟨ ++⁺ ≋-refl eq₁ ⟩ + l₁ ++ l₂₃ ≈⟨ eq₂ ⟩ + l ∎) } } } - ; identity = (λ A → record - { f = idˡ {a} A - ; f⁻¹ = λ {l} l∈A → [] , lift refl , l , l∈A , refl - ; cong₁ = λ {l₁} {l₂} {l₁∈A} {l₂∈A} → idˡ-cong {a} A {l₁} {l₂} {l₁∈A} {l₂∈A} - ; cong₂ = λ l₁≈l₂ → lift _ , l₁≈l₂ - }) , (λ A → record - { f = idʳ {a} A - ; f⁻¹ = λ {l} l∈A → l , l∈A , [] , lift refl , ++-identityʳ l - ; cong₁ = λ {l₁} {l₂} {l₁∈A} {l₂∈A} → idʳ-cong {a} A {l₁} {l₂} {l₁∈A} {l₂∈A} - ; cong₂ = λ l₁≈l₂ → l₁≈l₂ , lift _ + ; identity = (λ X → record + { f = λ { ([] , _ , _ , l₂∈X , eq) → Language.∈-resp-≋ X eq l₂∈X } + ; f⁻¹ = λ l∈X → -, lift refl , -, l∈X , ≋-refl + }) , (λ X → record + { f = λ { (l₁ , l₁∈X , [] , _ , eq) → Language.∈-resp-≋ X (≋-trans (≋-reflexive (sym (++-identityʳ l₁))) eq) l₁∈X } + ; f⁻¹ = λ {l} l∈X → -, l∈X , -, lift refl , ≋-reflexive (++-identityʳ l) }) } where - open ≡.≡-Reasoning - - idˡ : ∀ {a aℓ} → - (A : Language (c ⊔ ℓ ⊔ a) aℓ) → - ∀ {l} → - l ∈ ((𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) ∙ A) → - l ∈ A - idˡ _ ([] , _ , l , l∈A , refl) = l∈A - - idˡ-cong : ∀ {a aℓ} → - (A : Language (c ⊔ ℓ ⊔ a) aℓ) → - ∀ {l₁ l₂ l₁∈A l₂∈A} → - ≈ᴸ ((𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) ∙ A) {l₁} {l₂} l₁∈A l₂∈A → - ≈ᴸ A (idˡ {a} A l₁∈A) (idˡ {a} A l₂∈A) - idˡ-cong _ {l₁∈A = [] , _ , l₁ , l₁∈A , refl} {[] , _ , l₂ , l₂∈A , refl} (_ , l₁≈l₂) = l₁≈l₂ - - idʳ : ∀ {a aℓ} → - (A : Language (c ⊔ ℓ ⊔ a) aℓ) → - ∀ {l} → - l ∈ (A ∙ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)) → - l ∈ A - idʳ A (l , l∈A , [] , _ , refl) = ∈-cong A (sym (++-identityʳ l)) l∈A - - idʳ-cong : ∀ {a aℓ} → - (A : Language (c ⊔ ℓ ⊔ a) aℓ) → - ∀ {l₁ l₂ l₁∈A l₂∈A} → - ≈ᴸ (A ∙ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)) {l₁} {l₂} l₁∈A l₂∈A → - ≈ᴸ A (idʳ {a} A l₁∈A) (idʳ {a} A l₂∈A) - idʳ-cong A {l₁∈A = l₁ , l₁∈A , [] , _ , refl} {l₂ , l₂∈A , [] , _ , refl} (l₁≈l₂ , _) = - ≈ᴸ-cong A (sym (++-identityʳ l₁)) (sym (++-identityʳ l₂)) l₁∈A l₂∈A l₁≈l₂ + open import Relation.Binary.Reasoning.Setoid ≋-setoid -∙-monotone : ∀ {a aℓ b bℓ} → _∙_ Preserves₂ _≤_ {a} {aℓ} ⟶ _≤_ {b} {bℓ} ⟶ _≤_ -∙-monotone X≤Y U≤V = record - { f = λ {(_ , l₁∈X , _ , l₂∈U , l₁++l₂≡l) → -, X≤Y.f l₁∈X , -, U≤V.f l₂∈U , l₁++l₂≡l} - ; cong = Product.map X≤Y.cong U≤V.cong +∙-mono : ∀ {a b} → _∙_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_ +∙-mono X≤Y U≤V = record + { f = λ {(_ , l₁∈X , _ , l₂∈U , eq) → -, X≤Y.f l₁∈X , -, U≤V.f l₂∈U , eq} } where module X≤Y = _≤_ X≤Y diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda index b06be3d..ddea1a6 100644 --- a/src/Cfe/Language/Construct/Single.agda +++ b/src/Cfe/Language/Construct/Single.agda @@ -12,17 +12,16 @@ open Setoid over renaming (Carrier to C) open import Cfe.Language over hiding (_≈_) open import Data.List +open import Data.List.Relation.Binary.Equality.Setoid over open import Data.Product as Product open import Data.Unit open import Level -｛_｝ : C → Language (c ⊔ ℓ) 0ℓ +｛_｝ : C → Language (c ⊔ ℓ) ｛ c ｝ = record - { Carrier = λ l → ∃[ a ] (l ≡.≡ [ a ] × a ≈ c) - ; _≈_ = λ _ _ → ⊤ - ; isEquivalence = record - { refl = tt - ; sym = λ _ → tt - ; trans = λ _ _ → tt - } + { 𝕃 = [ c ] ≋_ + ; ∈-resp-≋ = λ l₁≋l₂ l₁∈｛c｝ → ≋-trans l₁∈｛c｝ l₁≋l₂ } + +xy∉｛c｝ : ∀ c x y l → x ∷ y ∷ l ∉ ｛ c ｝ +xy∉｛c｝ c x y l (_ ∷ ()) diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda index 5099d04..5e86124 100644 --- a/src/Cfe/Language/Construct/Union.agda +++ b/src/Cfe/Language/Construct/Union.agda @@ -19,33 +19,26 @@ open import Cfe.Language over as 𝕃 hiding (Lift) open Setoid over renaming (Carrier to C) module _ - {a aℓ b bℓ} - (A : Language a aℓ) - (B : Language b bℓ) + {a b} + (A : Language a) + (B : Language b) where - infix 4 _≈ᵁ_ + module A = Language A + module B = Language B + infix 6 _∪_ Union : List C → Set (a ⊔ b) Union l = l ∈ A ⊎ l ∈ B - data _≈ᵁ_ : {l₁ l₂ : List C} → REL (Union l₁) (Union l₂) (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where - A≈A : ∀ {l₁ l₂ x y} → ≈ᴸ A {l₁} {l₂} x y → (inj₁ x) ≈ᵁ (inj₁ y) - B≈B : ∀ {l₁ l₂ x y} → ≈ᴸ B {l₁} {l₂} x y → (inj₂ x) ≈ᵁ (inj₂ y) - - _∪_ : Language (a ⊔ b) (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) + _∪_ : Language (a ⊔ b) _∪_ = record - { Carrier = Union - ; _≈_ = _≈ᵁ_ - ; isEquivalence = record - { refl = λ {_} {x} → case x return (λ x → x ≈ᵁ x) of λ { (inj₁ x) → A≈A (≈ᴸ-refl A) ; (inj₂ y) → B≈B (≈ᴸ-refl B)} - ; sym = λ { (A≈A x) → A≈A (≈ᴸ-sym A x) ; (B≈B x) → B≈B (≈ᴸ-sym B x)} - ; trans = λ { (A≈A x) (A≈A y) → A≈A (≈ᴸ-trans A x y) ; (B≈B x) (B≈B y) → B≈B (≈ᴸ-trans B x y) } - } + { 𝕃 = Union + ; ∈-resp-≋ = λ l₁≋l₂ → Sum.map (A.∈-resp-≋ l₁≋l₂) (B.∈-resp-≋ l₁≋l₂) } -isCommutativeMonoid : ∀ {a aℓ} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a (c ⊔ a ⊔ aℓ) ∅) +isCommutativeMonoid : ∀ {a} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a ∅) isCommutativeMonoid = record { isMonoid = record { isSemigroup = record @@ -54,47 +47,36 @@ isCommutativeMonoid = record ; ∙-cong = λ X≈Y U≈V → record { f = Sum.map (_≈_.f X≈Y) (_≈_.f U≈V) ; f⁻¹ = Sum.map (_≈_.f⁻¹ X≈Y) (_≈_.f⁻¹ U≈V) - ; cong₁ = λ { (A≈A x) → A≈A (_≈_.cong₁ X≈Y x) ; (B≈B x) → B≈B (_≈_.cong₁ U≈V x) } - ; cong₂ = λ { (A≈A x) → A≈A (_≈_.cong₂ X≈Y x) ; (B≈B x) → B≈B (_≈_.cong₂ U≈V x) } } } ; assoc = λ A B C → record { f = Sum.assocʳ ; f⁻¹ = Sum.assocˡ - ; cong₁ = λ { (A≈A (A≈A x)) → A≈A x ; (A≈A (B≈B x)) → B≈B (A≈A x) ; (B≈B x) → B≈B (B≈B x) } - ; cong₂ = λ { (A≈A x) → A≈A (A≈A x) ; (B≈B (A≈A x)) → A≈A (B≈B x) ; (B≈B (B≈B x)) → B≈B x } } } ; identity = (λ A → record { f = λ { (inj₂ x) → x } ; f⁻¹ = inj₂ - ; cong₁ = λ { (B≈B x) → x } - ; cong₂ = B≈B }) , (λ A → record { f = λ { (inj₁ x) → x } ; f⁻¹ = inj₁ - ; cong₁ = λ { (A≈A x) → x } - ; cong₂ = A≈A }) } ; comm = λ A B → record { f = Sum.swap ; f⁻¹ = Sum.swap - ; cong₁ = λ { (A≈A x) → B≈B x ; (B≈B x) → A≈A x } - ; cong₂ = λ { (A≈A x) → B≈B x ; (B≈B x) → A≈A x } } } -∪-monotone : ∀ {a aℓ b bℓ} → _∪_ Preserves₂ _≤_ {a} {aℓ} ⟶ _≤_ {b} {bℓ} ⟶ _≤_ -∪-monotone X≤Y U≤V = record +∪-mono : ∀ {a b} → _∪_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_ +∪-mono X≤Y U≤V = record { f = Sum.map X≤Y.f U≤V.f - ; cong = λ { (A≈A l₁≈l₂) → A≈A (X≤Y.cong l₁≈l₂) ; (B≈B l₁≈l₂) → B≈B (U≤V.cong l₁≈l₂)} } where module X≤Y = _≤_ X≤Y module U≤V = _≤_ U≤V -∪-unique : ∀ {a aℓ b bℓ} {A : Language a aℓ} {B : Language b bℓ} → (∀ x → first A x → first B x → ⊥) → (𝕃.null A → 𝕃.null B → ⊥) → ∀ {l} → l ∈ A ∪ B → (l ∈ A × l ∉ B) ⊎ (l ∉ A × l ∈ B) +∪-unique : ∀ {a b} {A : Language a} {B : Language b} → (∀ x → first A x → first B x → ⊥) → (𝕃.null A → 𝕃.null B → ⊥) → ∀ {l} → l ∈ A ∪ B → (l ∈ A × l ∉ B) ⊎ (l ∉ A × l ∈ B) ∪-unique fA∩fB≡∅ ¬nA∨¬nB {[]} (inj₁ []∈A) = inj₁ ([]∈A , ¬nA∨¬nB []∈A) ∪-unique fA∩fB≡∅ ¬nA∨¬nB {x ∷ l} (inj₁ xl∈A) = inj₁ (xl∈A , (λ xl∈B → fA∩fB≡∅ x (-, xl∈A) (-, xl∈B))) ∪-unique fA∩fB≡∅ ¬nA∨¬nB {[]} (inj₂ []∈B) = inj₂ (flip ¬nA∨¬nB []∈B , []∈B) diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda index 3a78bd8..5ed031b 100644 --- a/src/Cfe/Language/Indexed/Construct/Iterate.agda +++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda @@ -49,60 +49,32 @@ module _ f≤g⇒fn≤gn f≤g (suc n) x = f≤g (f≤g⇒fn≤gn f≤g n x) module _ - {a aℓ} + {a} where - Iterate : (Language a aℓ → Language a aℓ) → IndexedLanguage 0ℓ 0ℓ a aℓ + Iterate : (Language a → Language a) → IndexedLanguage 0ℓ 0ℓ a Iterate f = record { Carrierᵢ = ℕ ; _≈ᵢ_ = ≡._≡_ ; isEquivalenceᵢ = ≡.isEquivalence - ; F = λ n → iter f n (Lift a aℓ ∅) + ; F = λ n → iter f n (Lift a ∅) ; cong = λ {≡.refl → ≈-refl} } - ≈ᵗ-refl : (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 : (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 : (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) - - ⋃ : (Language a aℓ → Language a aℓ) → Language a aℓ + ⋃ : (Language a → Language a) → Language a ⋃ f = record - { Carrier = Iter.Tagged - ; _≈_ = Iter._≈ᵗ_ - ; isEquivalence = record - { refl = ≈ᵗ-refl f - ; sym = ≈ᵗ-sym f - ; trans = ≈ᵗ-trans f - } + { 𝕃 = Iter.Tagged + ; ∈-resp-≋ = λ { l₁≋l₂ (i , l₁∈fi) → i , Language.∈-resp-≋ (Iter.F i) l₁≋l₂ l₁∈fi } } where module Iter = IndexedLanguage (Iterate f) - ⋃-cong : ∀ {f g : Language a aℓ → Language a aℓ} → (∀ {x y} → x ≈ y → f x ≈ g y) → ⋃ f ≈ ⋃ g + ⋃-cong : ∀ {f g} → (∀ {x y} → x ≈ y → f x ≈ g y) → ⋃ f ≈ ⋃ g ⋃-cong f≈g = record - { f = λ { (n , l∈fn) → n , _≈_.f (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g n (Lift a aℓ ∅)) l∈fn} - ; f⁻¹ = λ { (n , l∈gn) → n , _≈_.f⁻¹ (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g n (Lift a aℓ ∅)) l∈gn} - ; cong₁ = λ {_} {_} {(i , _)} → λ { (refl , l₁≈l₂) → refl , _≈_.cong₁ (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g i (Lift a aℓ ∅)) l₁≈l₂} - ; cong₂ = λ {_} {_} {(i , _)} → λ { (refl , l₁≈l₂) → refl , _≈_.cong₂ (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g i (Lift a aℓ ∅)) l₁≈l₂} + { f = λ { (n , l∈fn) → n , _≈_.f (f≈g⇒fn≈gn (L.setoid a) f≈g n (Lift a ∅)) l∈fn} + ; f⁻¹ = λ { (n , l∈gn) → n , _≈_.f⁻¹ (f≈g⇒fn≈gn (L.setoid a) f≈g n (Lift a ∅)) l∈gn} } - ⋃-monotone : ∀ {f g : Language a aℓ → Language a aℓ} → (∀ {x y} → x ≤ y → f x ≤ g y) → ⋃ f ≤ ⋃ g - ⋃-monotone f≤g = record - { f = λ { (n , l∈fn) → n , _≤_.f (f≤g⇒fn≤gn (poset a aℓ) f≤g n (Lift a aℓ ∅)) l∈fn } - ; cong = λ {_} {_} {(i , _)} → λ { (refl , l₁≈l₂) → refl , _≤_.cong (f≤g⇒fn≤gn (poset a aℓ) f≤g i (Lift a aℓ ∅)) l₁≈l₂ } + ⋃-mono : ∀ {f g} → (∀ {x y} → x ≤ y → f x ≤ g y) → ⋃ f ≤ ⋃ g + ⋃-mono f≤g = record + { f = λ { (n , l∈fn) → n , _≤_.f (f≤g⇒fn≤gn (poset a) f≤g n (Lift a ∅)) l∈fn } } diff --git a/src/Cfe/Language/Indexed/Homogeneous.agda b/src/Cfe/Language/Indexed/Homogeneous.agda index a1e284a..44e3b6c 100644 --- a/src/Cfe/Language/Indexed/Homogeneous.agda +++ b/src/Cfe/Language/Indexed/Homogeneous.agda @@ -16,18 +16,15 @@ open _≈_ open Setoid over using () renaming (Carrier to C) -record IndexedLanguage i iℓ a aℓ : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a ⊔ aℓ)) where +record IndexedLanguage i iℓ a : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a)) where field Carrierᵢ : Set i _≈ᵢ_ : B.Rel Carrierᵢ iℓ isEquivalenceᵢ : B.IsEquivalence _≈ᵢ_ - F : Carrierᵢ → Language a aℓ + F : Carrierᵢ → Language 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 diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda index 325b410..b2630ce 100644 --- a/src/Cfe/Language/Properties.agda +++ b/src/Cfe/Language/Properties.agda @@ -15,87 +15,75 @@ open import Data.List.Relation.Binary.Equality.Setoid over open import Function open import Level -≈-refl : ∀ {a aℓ} → Reflexive (_≈_ {a} {aℓ}) +≈-refl : ∀ {a} → Reflexive (_≈_ {a}) ≈-refl {x = A} = record { f = id ; f⁻¹ = id - ; cong₁ = id - ; cong₂ = id } -≈-sym : ∀ {a aℓ b bℓ} → Sym (_≈_ {a} {aℓ} {b} {bℓ}) _≈_ +≈-sym : ∀ {a b} → Sym (_≈_ {a} {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ℓ} → Trans (_≈_ {a} {aℓ}) (_≈_ {b} {bℓ} {c} {cℓ}) _≈_ +≈-trans : ∀ {a b c} → Trans (_≈_ {a}) (_≈_ {b} {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 -≈-isEquivalence : ∀ {a aℓ} → IsEquivalence (_≈_ {a} {aℓ} {a} {aℓ}) +≈-isEquivalence : ∀ {a} → IsEquivalence (_≈_ {a}) ≈-isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans } -setoid : ∀ a aℓ → Setoid (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ) -setoid a aℓ = record { isEquivalence = ≈-isEquivalence {a} {aℓ} } +setoid : ∀ a → Setoid (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) +setoid a = record { isEquivalence = ≈-isEquivalence {a} } -≤-refl : ∀ {a aℓ} → Reflexive (_≤_ {a} {aℓ}) +≤-refl : ∀ {a} → Reflexive (_≤_ {a}) ≤-refl = record { f = id - ; cong = id } -≤-reflexive : ∀ {a aℓ b bℓ} → _≈_ {a} {aℓ} {b} {bℓ} ⇒ _≤_ +≤-reflexive : ∀ {a b} → _≈_ {a} {b} ⇒ _≤_ ≤-reflexive A≈B = record { f = A≈B.f - ; cong = A≈B.cong₁ } where module A≈B = _≈_ A≈B -≤-trans : ∀ {a aℓ b bℓ c cℓ} → Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_ +≤-trans : ∀ {a b c} → Trans (_≤_ {a}) (_≤_ {b} {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ℓ} → Antisym (_≤_ {a} {aℓ} {b} {bℓ}) _≤_ _≈_ +≤-antisym : ∀ {a b} → Antisym (_≤_ {a} {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ℓ} → Min (_≤_ {b = b} {bℓ}) ∅ +≤-min : ∀ {b} → Min (_≤_ {b = b}) ∅ ≤-min A = record { f = λ () - ; cong = λ {_} {_} {} } -≤-isPartialOrder : ∀ a aℓ → IsPartialOrder (_≈_ {a} {aℓ}) _≤_ -≤-isPartialOrder a aℓ = record +≤-isPartialOrder : ∀ a → IsPartialOrder (_≈_ {a}) _≤_ +≤-isPartialOrder a = record { isPreorder = record { isEquivalence = ≈-isEquivalence ; reflexive = ≤-reflexive @@ -104,5 +92,5 @@ setoid a aℓ = record { isEquivalence = ≈-isEquivalence {a} {aℓ} } ; antisym = ≤-antisym } -poset : ∀ a aℓ → Poset (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ) (c ⊔ a ⊔ aℓ) -poset a aℓ = record { isPartialOrder = ≤-isPartialOrder a aℓ } +poset : ∀ a → Poset (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) (c ⊔ a) +poset a = record { isPartialOrder = ≤-isPartialOrder a } |