diff options
Diffstat (limited to 'src/Cfe/Language/Construct/Concatenate.agda')
| -rw-r--r-- | src/Cfe/Language/Construct/Concatenate.agda | 116 |
1 files changed, 37 insertions, 79 deletions
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 |