diff options
Diffstat (limited to 'src/Cfe/Language')
| -rw-r--r-- | src/Cfe/Language/Base.agda | 17 | ||||
| -rw-r--r-- | src/Cfe/Language/Properties.agda | 172 |
2 files changed, 162 insertions, 27 deletions
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda index d9be456..d73fe19 100644 --- a/src/Cfe/Language/Base.agda +++ b/src/Cfe/Language/Base.agda @@ -8,14 +8,14 @@ module Cfe.Language.Base open Setoid over using () renaming (Carrier to C) -open import Cfe.Function.Power open import Data.Empty.Polymorphic using (⊥) open import Data.List open import Data.List.Relation.Binary.Equality.Setoid over +open import Data.Nat using (ℕ; zero; suc) open import Data.Product open import Data.Sum open import Function -open import Level +open import Level renaming (suc to ℓsuc) open import Relation.Binary.PropositionalEquality using (_≡_) open import Relation.Nullary using (Dec; ¬_) @@ -26,7 +26,7 @@ private ------------------------------------------------------------------------ -- Definition -record Language a : Set (c ⊔ ℓ ⊔ suc a) where +record Language a : Set (c ⊔ ℓ ⊔ ℓsuc a) where field 𝕃 : List C → Set a ∈-resp-≋ : 𝕃 ⟶ 𝕃 Respects _≋_ @@ -82,11 +82,16 @@ A ∪ B = record ; ∈-resp-≋ = uncurry Data.Sum.map ∘ < Language.∈-resp-≋ A , Language.∈-resp-≋ B > } +Iter : (Language a → Language a) → Language a → ℕ → Language _ +Iter F A zero = A +Iter F A (suc n) = F (Iter F A n) + Sup : (Language a → Language a) → Language a → Language _ Sup F A = record - { 𝕃 = λ w → ∃[ n ] w ∈ (F ^ n) A - ; ∈-resp-≋ = λ w≋w′ (n , w∈FⁿA) → n , Language.∈-resp-≋ ((F ^ n) A) w≋w′ w∈FⁿA + { 𝕃 = λ w → ∃[ n ] w ∈ Iter F A n + ; ∈-resp-≋ = λ w≋w′ (n , w∈FⁿA) → n , Iter.∈-resp-≋ F A n w≋w′ w∈FⁿA } + where module Iter F A n = Language (Iter F A n) ⋃_ : (Language a → Language a) → Language _ ⋃ F = Sup F ∅ @@ -96,7 +101,7 @@ Sup F A = record infix 4 _⊆_ _≈_ -data _⊆_ {a b} : REL (Language a) (Language b) (c ⊔ ℓ ⊔ suc (a ⊔ b)) where +data _⊆_ {a b} : REL (Language a) (Language b) (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where sub : ∀ {A : Language a} {B : Language b} → (∀ {w} → w ∈ A → w ∈ B) → A ⊆ B _⊇_ : REL (Language a) (Language b) _ diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda index fe153b1..ca288a8 100644 --- a/src/Cfe/Language/Properties.agda +++ b/src/Cfe/Language/Properties.agda @@ -16,7 +16,6 @@ open Setoid over using () ) open import Algebra -open import Cfe.Function.Power open import Cfe.Language.Base over open import Cfe.List.Compare over open import Data.Empty using (⊥-elim) @@ -25,11 +24,11 @@ open import Data.List as L open import Data.List.Properties open import Data.List.Relation.Binary.Equality.Setoid over import Data.List.Relation.Unary.Any as Any -import Data.Nat as ℕ +open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s) open import Data.Product as P open import Data.Sum as S open import Function hiding (_⟶_) -open import Level +open import Level renaming (suc to ℓsuc) import Relation.Binary.Construct.On as On open import Relation.Binary.PropositionalEquality hiding (setoid; [_]) open import Relation.Nullary hiding (Irrelevant) @@ -82,6 +81,12 @@ First-resp-∼ A c∼c′ (w , cw∈A) = w , ∈-resp-≋ (c∼c′ ∷ ≋-refl ⊆-min : Min (_⊆_ {a} {b}) ∅ ⊆-min _ = sub λ () +⊆-respʳ-≈ : Y ≈ Z → X ⊆ Y → X ⊆ Z +⊆-respʳ-≈ Y≈Z X⊆Y = ⊆-trans X⊆Y (⊆-reflexive Y≈Z) + +⊆-respˡ-≈ : Y ≈ Z → Y ⊆ X → Z ⊆ X +⊆-respˡ-≈ Y≈Z Y⊆X = ⊆-trans (⊇-reflexive Y≈Z) Y⊆X + ------------------------------------------------------------------------ -- Membership properties of _⊆_ @@ -108,6 +113,9 @@ Flast-resp-⊆ (sub A⊆B) = P.map₂ (P.map₂ (P.map A⊆B (P.map₂ A⊆B))) ≈-refl : Reflexive (_≈_ {a}) ≈-refl = ⊆-refl , ⊆-refl +≈-reflexive : _≡_ ⇒ (_≈_ {a}) +≈-reflexive refl = ≈-refl + ≈-sym : Sym (_≈_ {a} {b}) _≈_ ≈-sym = P.swap @@ -158,6 +166,93 @@ setoid {a} = record { isEquivalence = ≈-isEquivalence {a} } ⊆-poset : ∀ {a} → Poset _ _ _ ⊆-poset {a} = record { isPartialOrder = ⊆-isPartialOrder {a} } +-- Shamelessly adapted from Relation.Binary.Reasoning.Base.Double +module ⊆-Reasoning where + infix 4 _IsRelatedTo_ + + data _IsRelatedTo_ (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where + nonstrict : (A⊆B : A ⊆ B) → A IsRelatedTo B + equals : (A≈B : A ≈ B) → A IsRelatedTo B + + ------------------------------------------------------------------------ + -- A record that is used to ensure that the final relation proved by the + -- chain of reasoning can be converted into the required relation. + + data IsEquality {A : Language a} {B : Language b} : A IsRelatedTo B → Set (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where + isEquality : ∀ A≈B → IsEquality (equals A≈B) + + IsEquality? : ∀ (A⊆B : A IsRelatedTo B) → Dec (IsEquality A⊆B) + IsEquality? (nonstrict _) = no λ() + IsEquality? (equals A≈B) = yes (isEquality A≈B) + + extractEquality : ∀ {A⊆B : A IsRelatedTo B} → IsEquality A⊆B → A ≈ B + extractEquality (isEquality A≈B) = A≈B + + ------------------------------------------------------------------------ + -- Reasoning combinators + + -- See `Relation.Binary.Reasoning.Base.Partial` for the design decisions + -- behind these combinators. + + infix 1 begin_ begin-equality_ + infixr 2 step-⊆ step-≈ step-≈˘ step-≡ step-≡˘ _≡⟨⟩_ + infix 3 _∎ + + -- Beginnings of various types of proofs + + begin_ : (r : A IsRelatedTo B) → A ⊆ B + begin (nonstrict A⊆B) = A⊆B + begin (equals A≈B) = ⊆-reflexive A≈B + + begin-equality_ : ∀ (r : A IsRelatedTo B) → {s : True (IsEquality? r)} → A ≈ B + begin-equality_ r {s} = extractEquality (toWitness s) + + -- Step with the main relation + + step-⊆ : ∀ (X : Language a) → Y IsRelatedTo Z → X ⊆ Y → X IsRelatedTo Z + step-⊆ X (nonstrict Y⊆Z) X⊆Y = nonstrict (⊆-trans X⊆Y Y⊆Z) + step-⊆ X (equals Y≈Z) X⊆Y = nonstrict (⊆-respʳ-≈ Y≈Z X⊆Y) + + -- Step with the setoid equality + + step-≈ : ∀ (X : Language a) → Y IsRelatedTo Z → X ≈ Y → X IsRelatedTo Z + step-≈ X (nonstrict Y⊆Z) X≈Y = nonstrict (⊆-respˡ-≈ (≈-sym X≈Y) Y⊆Z) + step-≈ X (equals Y≈Z) X≈Y = equals (≈-trans X≈Y Y≈Z) + + -- Flipped step with the setoid equality + + step-≈˘ : ∀ (X : Language a) → Y IsRelatedTo Z → Y ≈ X → X IsRelatedTo Z + step-≈˘ X Y⊆Z Y≈X = step-≈ X Y⊆Z (≈-sym Y≈X) + + -- Step with non-trivial propositional equality + + step-≡ : ∀ (X : Language a) → Y IsRelatedTo Z → X ≡ Y → X IsRelatedTo Z + step-≡ X (nonstrict Y⊆Z) X≡Y = nonstrict (case X≡Y of λ { refl → Y⊆Z }) + step-≡ X (equals Y≈Z) X≡Y = equals (case X≡Y of λ { refl → Y≈Z }) + + -- Flipped step with non-trivial propositional equality + + step-≡˘ : ∀ (X : Language a) → Y IsRelatedTo Z → Y ≡ X → X IsRelatedTo Z + step-≡˘ X Y⊆Z Y≡X = step-≡ X Y⊆Z (sym Y≡X) + + -- Step with trivial propositional equality + + _≡⟨⟩_ : ∀ (X : Language a) → X IsRelatedTo Y → X IsRelatedTo Y + X ≡⟨⟩ X⊆Y = X⊆Y + + -- Termination step + + _∎ : ∀ (X : Language a) → X IsRelatedTo X + X ∎ = equals ≈-refl + + -- Syntax declarations + + syntax step-⊆ X Y⊆Z X⊆Y = X ⊆⟨ X⊆Y ⟩ Y⊆Z + syntax step-≈ X Y⊆Z X≈Y = X ≈⟨ X≈Y ⟩ Y⊆Z + syntax step-≈˘ X Y⊆Z Y≈X = X ≈˘⟨ Y≈X ⟩ Y⊆Z + syntax step-≡ X Y⊆Z X≡Y = X ≡⟨ X≡Y ⟩ Y⊆Z + syntax step-≡˘ X Y⊆Z Y≡X = X ≡˘⟨ Y≡X ⟩ Y⊆Z + ------------------------------------------------------------------------ -- Membership properties of _≈_ @@ -797,26 +892,57 @@ _∪?_ : Decidable A → Decidable B → Decidable (A ∪ B) (A? ∪? B?) w = A? w ⊎-dec B? w ------------------------------------------------------------------------ +-- Properties of Iter +------------------------------------------------------------------------ +-- Membership properties of Iter + +FⁿFA≡Fⁿ⁺¹A : ∀ n → Iter {a} F (F A) n ≡ Iter F A (suc n) +FⁿFA≡Fⁿ⁺¹A zero = refl +FⁿFA≡Fⁿ⁺¹A {F = F} (suc n) = cong F (FⁿFA≡Fⁿ⁺¹A n) + +Iter-monoˡ : (∀ {A B} → A ⊆ B → F A ⊆ G B) → ∀ n → A ⊆ B → Iter F A n ⊆ Iter G B n +Iter-monoˡ mono zero A⊆B = A⊆B +Iter-monoˡ mono (suc n) A⊆B = mono (Iter-monoˡ mono n A⊆B) + +Iter-congˡ : (∀ {A B} → A ≈ B → F A ≈ G B) → ∀ n → A ≈ B → Iter F A n ≈ Iter G B n +Iter-congˡ cong zero A≈B = A≈B +Iter-congˡ cong (suc n) A≈B = cong (Iter-congˡ cong n A≈B) + +Iter-step : (∀ {A B} → A ⊆ B → F A ⊆ F B) → A ⊆ F A → ∀ n → Iter F A n ⊆ Iter F A (suc n) +Iter-step mono A⊆FA zero = A⊆FA +Iter-step mono A⊆FA (suc n) = mono (Iter-step mono A⊆FA n) + +Iter-monoʳ : (∀ {A B} → A ⊆ B → F A ⊆ F B) → A ⊆ F A → ∀ {m n} → m ≤ n → Iter F A m ⊆ Iter F A n +Iter-monoʳ mono A⊆FA {n = zero} z≤n = ⊆-refl +Iter-monoʳ {F = F} {A = A} mono A⊆FA {n = suc n} z≤n = begin + A ⊆⟨ A⊆FA ⟩ + F A ⊆⟨ mono (Iter-monoʳ mono A⊆FA {n = n} z≤n) ⟩ + F (Iter F A n) ∎ + where open ⊆-Reasoning +Iter-monoʳ mono A⊆FA (s≤s m≤n) = mono (Iter-monoʳ mono A⊆FA m≤n) + +------------------------------------------------------------------------ -- Properties of Sup ------------------------------------------------------------------------ -- Membership properties of Sup -FⁿA⊆SupFA : ∀ n → (F ^ n) A ⊆ Sup F A +FⁿA⊆SupFA : ∀ n → Iter F A n ⊆ Sup F A FⁿA⊆SupFA n = sub (n ,_) -FⁿFA⊆SupFA : ∀ n → (F ^ n) (F A) ⊆ Sup F A -FⁿFA⊆SupFA {F = F} {A = A} n = ⊆-trans (sub (go n)) (FⁿA⊆SupFA (ℕ.suc n)) - where - go : ∀ {w} n → w ∈ (F ^ n) (F A) → w ∈ (F ^ (ℕ.suc n)) A - go {w = w} n w∈Fⁿ̂FA = subst (λ x → w ∈ x A) (fⁿf≡fⁿ⁺¹ F n) w∈Fⁿ̂FA +FⁿFA⊆SupFA : ∀ n → Iter F (F A) n ⊆ Sup F A +FⁿFA⊆SupFA {F = F} {A = A} n = begin + Iter F (F A) n ≡⟨ FⁿFA≡Fⁿ⁺¹A n ⟩ + Iter F A (suc n) ⊆⟨ FⁿA⊆SupFA (suc n) ⟩ + Sup F A ∎ + where open ⊆-Reasoning -∀[FⁿA⊆B]⇒SupFA⊆B : (∀ n → (F ^ n) A ⊆ B) → Sup F A ⊆ B +∀[FⁿA⊆B]⇒SupFA⊆B : (∀ n → Iter F A n ⊆ B) → Sup F A ⊆ B ∀[FⁿA⊆B]⇒SupFA⊆B FⁿA⊆B = sub λ (n , w∈FⁿA) → ∈-resp-⊆ (FⁿA⊆B n) w∈FⁿA -∃[B⊆FⁿA]⇒B⊆SupFA : ∀ n → B ⊆ (F ^ n) A → B ⊆ Sup F A +∃[B⊆FⁿA]⇒B⊆SupFA : ∀ n → B ⊆ Iter F A n → B ⊆ Sup F A ∃[B⊆FⁿA]⇒B⊆SupFA n B⊆FⁿA = sub λ w∈B → n , ∈-resp-⊆ B⊆FⁿA w∈B -∀[FⁿA≈GⁿB]⇒SupFA≈SupGB : (∀ n → (F ^ n) A ≈ (G ^ n) B) → Sup F A ≈ Sup G B +∀[FⁿA≈GⁿB]⇒SupFA≈SupGB : (∀ n → Iter F A n ≈ Iter G B n) → Sup F A ≈ Sup G B ∀[FⁿA≈GⁿB]⇒SupFA≈SupGB FⁿA≈GⁿB = ⊆-antisym (sub λ (n , w∈FⁿA) → n , ∈-resp-≈ (FⁿA≈GⁿB n) w∈FⁿA) @@ -826,34 +952,38 @@ FⁿFA⊆SupFA {F = F} {A = A} n = ⊆-trans (sub (go n)) (FⁿA⊆SupFA (ℕ.su ------------------------------------------------------------------------ -- Membership properties of ⋃_ -Fⁿ⊆⋃F : ∀ n → (F ^ n) ∅ ⊆ ⋃ F +Fⁿ⊆⋃F : ∀ n → Iter F ∅ n ⊆ ⋃ F Fⁿ⊆⋃F = FⁿA⊆SupFA -∀[Fⁿ⊆B]⇒⋃F⊆B : (∀ n → (F ^ n) ∅ ⊆ B) → ⋃ F ⊆ B +∀[Fⁿ⊆B]⇒⋃F⊆B : (∀ n → Iter F ∅ n ⊆ B) → ⋃ F ⊆ B ∀[Fⁿ⊆B]⇒⋃F⊆B = ∀[FⁿA⊆B]⇒SupFA⊆B -∃[B⊆Fⁿ]⇒B⊆⋃F : ∀ n → B ⊆ (F ^ n) ∅ → B ⊆ ⋃ F +∃[B⊆Fⁿ]⇒B⊆⋃F : ∀ n → B ⊆ Iter F ∅ n → B ⊆ ⋃ F ∃[B⊆Fⁿ]⇒B⊆⋃F = ∃[B⊆FⁿA]⇒B⊆SupFA -∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G : (∀ n → (F ^ n) ∅ ≈ (G ^ n) ∅) → ⋃ F ≈ ⋃ G +∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G : (∀ n → Iter F ∅ n ≈ Iter G ∅ n) → ⋃ F ≈ ⋃ G ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G = ∀[FⁿA≈GⁿB]⇒SupFA≈SupGB ------------------------------------------------------------------------ -- Functional properties of ⋃_ ⋃-mono : (∀ {A B} → A ⊆ B → F A ⊆ G B) → ⋃ F ⊆ ⋃ G -⋃-mono mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ n → ⊆-trans (f∼g⇒fⁿ∼gⁿ _⊆_ (⊆-min ∅) mono-ext n) (Fⁿ⊆⋃F n) +⋃-mono {F = F} {G = G} mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ n → (begin + Iter F ∅ n ⊆⟨ Iter-monoˡ mono-ext n (⊆-min ∅) ⟩ + Iter G ∅ n ⊆⟨ Fⁿ⊆⋃F n ⟩ + ⋃ G ∎) + where open ⊆-Reasoning ⋃-cong : (∀ {A B} → A ≈ B → F A ≈ G B) → ⋃ F ≈ ⋃ G -⋃-cong ext = ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G (f∼g⇒fⁿ∼gⁿ _≈_ (⊆-antisym (⊆-min ∅) (⊆-min ∅)) ext) +⋃-cong ext = ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G λ n → Iter-congˡ ext n (⊆-antisym (⊆-min ∅) (⊆-min ∅)) ⋃-inverseʳ : ∀ (A : Language a) → ⋃ (const A) ≈ A -⋃-inverseʳ _ = ⊆-antisym (sub λ {(ℕ.suc _ , w∈A) → w∈A}) (Fⁿ⊆⋃F 1) +⋃-inverseʳ _ = ⊆-antisym (sub λ {(suc _ , w∈A) → w∈A}) (Fⁿ⊆⋃F 1) ⋃-unroll : (∀ {A B} → A ⊆ B → F A ⊆ F B) → ⋃ F ⊆ F (⋃ F) ⋃-unroll {F = F} mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ - { ℕ.zero → ⊆-min (F (⋃ F)) - ; (ℕ.suc n) → mono-ext (Fⁿ⊆⋃F n) + { zero → ⊆-min (F (⋃ F)) + ; (suc n) → mono-ext (Fⁿ⊆⋃F n) } ------------------------------------------------------------------------ |