diff options
Diffstat (limited to 'src/Cfe/Type')
| -rw-r--r-- | src/Cfe/Type/Properties.agda | 50 |
1 files changed, 33 insertions, 17 deletions
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda index 134bfce..37f491b 100644 --- a/src/Cfe/Type/Properties.agda +++ b/src/Cfe/Type/Properties.agda @@ -16,11 +16,12 @@ open import Cfe.Language.Construct.Union over open import Cfe.Language.Indexed.Construct.Iterate over open import Cfe.Type.Base over open import Data.Bool renaming (_≤_ to _≤ᵇ_; _∨_ to _∨ᵇ_) -open import Data.Bool.Properties hiding (≤-reflexive) +open import Data.Bool.Properties hiding (≤-reflexive; ≤-trans) open import Data.Empty open import Data.List hiding (null) open import Data.List.Relation.Binary.Equality.Setoid over -open import Data.Nat hiding (_≤_; _≤ᵇ_; _^_) +open import Data.Nat hiding (_≤ᵇ_; _^_) renaming (_≤_ to _≤ⁿ_) +open import Data.Nat.Properties using (≤-stepsˡ; ≤-stepsʳ) renaming (≤-refl to ≤ⁿ-refl) open import Data.Product as Product open import Data.Sum as Sum open import Function hiding (_⟶_) @@ -44,7 +45,7 @@ L⊨τ+¬N⇒ε∉L {L = L} {τ} L⊨τ ¬n ε∈L = case ∃[ b ] ((null L → ⊨-anticongˡ B≤A A⊨τ = record { n⇒n = A⊨τ.n⇒n ∘ B≤A.f ; f⇒f = A⊨τ.f⇒f ∘ Product.map₂ B≤A.f - ; l⇒l = A⊨τ.l⇒l ∘ Product.map₂ (Product.map₂ (Product.map₂ B≤A.f)) + ; l⇒l = A⊨τ.l⇒l ∘ Product.map₂ (Product.map₂ (Product.map B≤A.f (Product.map₂ B≤A.f))) } where module B≤A = _≤ˡ_ B≤A @@ -108,8 +109,8 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record ; f⇒f = λ {x} → λ {([] , (c∼x ∷ []≋[])) → c∼x} ; l⇒l = λ {x} → λ { ([] , []≢[] , _) → ⊥-elim ([]≢[] refl) - ; (y ∷ [] , _ , l′ , y∷x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y x l′ y∷x∷l′∈｛c｝) - ; (y ∷ z ∷ l , _ , l′ , y∷z∷l++x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y z (l ++ x ∷ l′) y∷z∷l++x∷l′∈｛c｝) + ; (y ∷ [] , _ , _ , l′ , y∷x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y x l′ y∷x∷l′∈｛c｝) + ; (y ∷ z ∷ l , _ , _ , l′ , y∷z∷l++x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y z (l ++ x ∷ l′) y∷z∷l++x∷l′∈｛c｝) } } where @@ -131,8 +132,8 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record module τ₁⊛τ₂ = _⊛_ τ₁⊛τ₂ ∪-⊨ : ∀ {a b fℓ₁ lℓ₁ fℓ₂ lℓ₂} {A : Language a} {B : Language b} {τ₁ : Type fℓ₁ lℓ₁} {τ₂ : Type fℓ₂ lℓ₂} → - A ⊨ τ₁ → B ⊨ τ₂ → A ∪ B ⊨ τ₁ ∨ τ₂ -∪-⊨ {A = A} {B} {τ₁} {τ₂} A⊨τ₁ B⊨τ₂ = record + A ⊨ τ₁ → B ⊨ τ₂ → τ₁ # τ₂ → A ∪ B ⊨ τ₁ ∨ τ₂ +∪-⊨ {A = A} {B} {τ₁} {τ₂} A⊨τ₁ B⊨τ₂ τ₁#τ₂ = record { n⇒n = λ { (inj₁ ε∈A) → case ∃[ b ] T b ∋ Null τ₁ , A⊨τ₁.n⇒n ε∈A return (λ {(x , _) → T (x ∨ᵇ Null τ₂)}) of λ { (true , _) → _ } @@ -144,21 +145,36 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record ; (l , inj₂ x∷l∈B) → inj₂ (B⊨τ₂.f⇒f (-, x∷l∈B)) } ; l⇒l = λ - { (l , l≢ε , l′ , inj₁ l++x∷l′∈A ) → inj₁ (A⊨τ₁.l⇒l (-, l≢ε , -, l++x∷l′∈A)) - ; (l , l≢ε , l′ , inj₂ l++x∷l′∈B ) → inj₂ (B⊨τ₂.l⇒l (-, l≢ε , -, l++x∷l′∈B)) + { ([] , l≢ε , l∈A∪B , l′ , l++x∷l′∈A∪B) → ⊥-elim (l≢ε refl) + ; (_ ∷ _ , _ , inj₁ l∈A , _ , inj₁ l++x∷l′∈A) → inj₁ (A⊨τ₁.l⇒l (-, (λ ()) , l∈A , -, l++x∷l′∈A)) + ; (c ∷ _ , _ , inj₁ c∷u∈A , l′ , inj₂ c∷v∈B) → ⊥-elim (τ₁#τ₂.∄[f₁∩f₂] c (A⊨τ₁.f⇒f (-, c∷u∈A) , B⊨τ₂.f⇒f (-, c∷v∈B))) + ; (c ∷ _ , _ , inj₂ c∷u∈B , l′ , inj₁ c∷v∈A) → ⊥-elim (τ₁#τ₂.∄[f₁∩f₂] c (A⊨τ₁.f⇒f (-, c∷v∈A) , B⊨τ₂.f⇒f (-, c∷u∈B))) + ; (_ ∷ _ , _ , inj₂ l∈B , _ , inj₂ l++x∷l′∈B) → inj₂ (B⊨τ₂.l⇒l (-, (λ ()) , l∈B , -, l++x∷l′∈B)) } } where + module τ₁#τ₂ = _#_ τ₁#τ₂ module A⊨τ₁ = _⊨_ A⊨τ₁ module B⊨τ₂ = _⊨_ B⊨τ₂ -⋃-⊨ : ∀ {a fℓ lℓ} {F : Op₁ (Language a)} {τ : Type fℓ lℓ} → (∀ {L} → L ⊨ τ → F L ⊨ τ) → ⋃ F ⊨ τ -⋃-⊨ {a} {F = F} {τ} mono = record - { n⇒n = λ { (n , l∈F^n) → _⊨_.n⇒n (F^n⊨τ n) l∈F^n} - ; f⇒f = λ { (_ , n , x∷l∈F^n) → _⊨_.f⇒f (F^n⊨τ n) (-, x∷l∈F^n) } - ; l⇒l = λ { (_ , l≢ε , _ , n , l++x∷l′∈F^n) → _⊨_.l⇒l (F^n⊨τ n) (-, l≢ε , -, l++x∷l′∈F^n) } +⋃-⊨ : ∀ {a fℓ lℓ} {F : Op₁ (Language a)} {τ : Type fℓ lℓ} → + (Congruent₁ _≤ˡ_ F) → + (∀ {L} → L ⊨ τ → F L ⊨ τ) → ⋃ F ⊨ τ +⋃-⊨ {a} {F = F} {τ} ≤-mono ⊨-mono = record + { n⇒n = λ { (n , l∈Fⁿ) → _⊨_.n⇒n (Fⁿ⊨τ n) l∈Fⁿ} + ; f⇒f = λ { (_ , n , x∷l∈Fⁿ) → _⊨_.f⇒f (Fⁿ⊨τ n) (-, x∷l∈Fⁿ) } + ; l⇒l = λ + { (_ , l≢ε , (m , l∈Fᵐ) , _ , (n , l++x∷l′∈Fⁿ)) → + _⊨_.l⇒l (Fⁿ⊨τ (m + n)) + (-, l≢ε , _≤ˡ_.f (^-mono (≤-stepsʳ {m} n ≤ⁿ-refl)) l∈Fᵐ , + -, _≤ˡ_.f (^-mono (≤-stepsˡ m ≤ⁿ-refl)) l++x∷l′∈Fⁿ) + } } where - F^n⊨τ : ∀ n → (F ^ n) (Lift a ∅) ⊨ τ - F^n⊨τ zero = ⊨-anticongˡ (≤-reflexive (lift-cong a ∅)) (⊨-congʳ (≤-min τ) ∅⊨τ⊥) - F^n⊨τ (suc n) = mono (F^n⊨τ n) + Fⁿ⊨τ : ∀ n → (F ^ n) (Lift a ∅) ⊨ τ + Fⁿ⊨τ zero = ⊨-anticongˡ (≤-reflexive (lift-cong a ∅)) (⊨-congʳ (≤-min τ) ∅⊨τ⊥) + Fⁿ⊨τ (suc n) = ⊨-mono (Fⁿ⊨τ n) + + ^-mono : ∀ {m n} → m ≤ⁿ n → (F ^ m) (Lift a ∅) ≤ˡ (F ^ n) (Lift a ∅) + ^-mono {n = n} z≤n = ≤-trans (≤-reflexive (lift-cong a ∅)) (≤ˡ-min ((F ^ n) (Lift a ∅))) + ^-mono (s≤s m≤n) = ≤-mono (^-mono m≤n) |