From 01ec93c5a03f6c4c660aa593b4c00afccc48907a Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Mon, 8 Feb 2021 17:40:04 +0000 Subject: Make languages records with more properties. --- src/Cfe/Language/Base.agda | 123 ++++++++++++++++++++++------ src/Cfe/Language/Construct/Concatenate.agda | 59 +++++++++++++ src/Cfe/Language/Construct/Single.agda | 88 ++++++++++++++++++++ src/Cfe/Language/Construct/Union.agda | 102 +++++++++++++++++++++++ src/Cfe/Language/Properties.agda | 28 ++++++- 5 files changed, 369 insertions(+), 31 deletions(-) create mode 100644 src/Cfe/Language/Construct/Concatenate.agda create mode 100644 src/Cfe/Language/Construct/Single.agda create mode 100644 src/Cfe/Language/Construct/Union.agda (limited to 'src/Cfe') diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda index 2e77b11..c1ff398 100644 --- a/src/Cfe/Language/Base.agda +++ b/src/Cfe/Language/Base.agda @@ -3,47 +3,116 @@ open import Relation.Binary module Cfe.Language.Base - {a ℓ} (setoid : Setoid a ℓ) + {c ℓ} (setoid : Setoid c ℓ) where open Setoid setoid renaming (Carrier to A) -open import Data.Empty.Polymorphic +open import Data.Empty open import Data.List open import Data.List.Relation.Binary.Equality.Setoid setoid -open import Data.Nat hiding (_≤_; _⊔_) -open import Data.Product -open import Data.Sum +open import Data.Product as Product open import Function -open import Level renaming (suc to lsuc) +open import Level +import Relation.Binary.PropositionalEquality as ≡ +import Relation.Binary.Indexed.Heterogeneous as I -Language : Set (lsuc a ⊔ lsuc ℓ) -Language = List A → Set (a ⊔ ℓ) +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₃∈𝕃 -∅ : Language -∅ = const ⊥ + ≈ᴸ-refl : ∀ {l} → Reflexive (_≈ᴸ_ {l}) + ≈ᴸ-refl = IsEquivalence.refl ≈ᴸ-isEquivalence -｛ε｝ : Language -｛ε｝ = [] ≋_ + ≈ᴸ-sym : ∀ {l} → Symmetric (_≈ᴸ_ {l}) + ≈ᴸ-sym = IsEquivalence.sym ≈ᴸ-isEquivalence -｛_｝ : A → Language -｛ a ｝ = [ a ] ≋_ + ≈ᴸ-trans : ∀ {l} → Transitive (_≈ᴸ_ {l}) + ≈ᴸ-trans = IsEquivalence.trans ≈ᴸ-isEquivalence -infix 4 _∪_ -infix 4 _∙_ + ≈ᴸ-reflexive : ∀ {l} → ≡._≡_ ⇒ (_≈ᴸ_ {l}) + ≈ᴸ-reflexive = IsEquivalence.reflexive ≈ᴸ-isEquivalence -_∪_ : Language → Language → Language -(A ∪ B) l = A l ⊎ B l + ⤖-injective : ∀ {l₁ l₂ l₁≋l₂} → Injective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ l₁≋l₂) + ⤖-injective = proj₁ ⤖-bijective -_∙_ : Language → Language → Language -(A ∙ B) l = ∃[ l₁ ] ∃[ l₂ ] (A l₁ × B l₂ × l₁ ++ l₂ ≋ l) + ⤖-surjective : ∀ {l₁ l₂ l₁≋l₂} → Surjective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ {l₁} l₁≋l₂) + ⤖-surjective = proj₂ ⤖-bijective -iterate : (Language → Language) → ℕ → Language → Language -iterate f ℕ.zero = id -iterate f (suc n) = f ∘ iterate f n + ⤖-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 + } -fix : (Language → Language) → Language -fix f l = ∃[ n ] iterate f n ∅ l + ⤖-reflexive : ∀ {l l∈𝕃 l∈𝕃′} → l∈𝕃 ≡.≡ l∈𝕃′ → ∃[ l≋l ]((⤖ {l} l≋l l∈𝕃) ≈ᴸ l∈𝕃′) + ⤖-reflexive = I.IsIndexedEquivalence.reflexive ⤖-isIndexedEquivalence -_≤_ : Language → Language → Set (a ⊔ ℓ) -A ≤ B = ∀ {l} → A l → B l +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 𝕃 _≈ᴸ_ ⤖ + + open IsLanguage isLanguage public + +open Language + +infix 4 _∈_ + +_∈_ : ∀ {a aℓ} → List A → Language a aℓ → Set a +l ∈ A = 𝕃 A l + +∅ : 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₁∈𝕃 + } + } + +⦃ε⦄ : 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 } + } + } + +_≤_ : {a aℓ b bℓ : Level} → REL (Language a aℓ) (Language b bℓ) (c ⊔ a ⊔ b) +A ≤ B = ∀ {l} → l ∈ A → l ∈ B 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) + } + } + } diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda index 8d024a8..52d4644 100644 --- a/src/Cfe/Language/Properties.agda +++ b/src/Cfe/Language/Properties.agda @@ -3,19 +3,39 @@ open import Relation.Binary module Cfe.Language.Properties - {a ℓ} (setoid : Setoid a ℓ) + {c ℓ} {setoid : Setoid c ℓ} where open Setoid setoid renaming (Carrier to A) - open import Cfe.Language setoid +open Language + +open import Data.List +open import Data.List.Relation.Binary.Equality.Setoid setoid open import Function +open import Level +open import Relation.Binary.Construct.InducedPoset + +_≤′_ : ∀ {a aℓ} → Rel (Language a aℓ) (c ⊔ a) +_≤′_ = _≤_ ------------------------------------------------------------------------ -- Properties of _≤_ -≤-refl : Reflexive _≤_ +≤-refl : ∀ {a aℓ} → Reflexive (_≤′_ {a} {aℓ}) ≤-refl = id -≤-trans : Transitive _≤_ +≤-trans : ∀ {a b c aℓ bℓ cℓ} → Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_ ≤-trans A≤B B≤C = B≤C ∘ A≤B + +≤-poset : ∀ {a aℓ} → Poset (c ⊔ ℓ ⊔ suc (a ⊔ aℓ)) (c ⊔ a) (c ⊔ a) +≤-poset {a} {aℓ} = InducedPoset (_≤′_ {a} {aℓ}) id (λ i≤j j≤k → j≤k ∘ i≤j) + +-- ------------------------------------------------------------------------ +-- -- Properties of _∪_ + +-- ∪-cong-≤ : Congruent₂ _≤_ _∪_ +-- ∪-cong-≤ A≤B C≤D = map A≤B C≤D + +-- ∪-cong : Congruent₂ _≈_ _∪_ +-- ∪-cong {A} {B} {C} {D} = ≤-cong₂→≈-cong₂ {_∪_} (λ A≤B C≤D → map A≤B C≤D) {A} {B} {C} {D} -- cgit v1.2.3