diff options
Diffstat (limited to 'src/Cfe/Type')
| -rw-r--r-- | src/Cfe/Type/Base.agda | 2 | ||||
| -rw-r--r-- | src/Cfe/Type/Properties.agda | 22 |
2 files changed, 9 insertions, 15 deletions
diff --git a/src/Cfe/Type/Base.agda b/src/Cfe/Type/Base.agda index 371bc2f..a5ed780 100644 --- a/src/Cfe/Type/Base.agda +++ b/src/Cfe/Type/Base.agda @@ -48,7 +48,7 @@ _∙_ {lℓ₁ = lℓ₁} {fℓ₂} {lℓ₂} τ₁ τ₂ = record ; Flast = Flast τ₂ ∪ (if Null τ₂ then First τ₂ ∪ Flast τ₁ else λ x → L.Lift (lℓ₁ ⊔ fℓ₂) (x U.∈ U.∅)) } -record _⊨_ {a} {aℓ} {fℓ} {lℓ} (A : Language a aℓ) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where +record _⊨_ {a} {fℓ} {lℓ} (A : Language a) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where field n⇒n : null A → T (Null τ) f⇒f : first A ⊆ First τ diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda index 2222fbe..cfdf694 100644 --- a/src/Cfe/Type/Properties.agda +++ b/src/Cfe/Type/Properties.agda @@ -13,10 +13,11 @@ open import Cfe.Language.Construct.Single over open import Cfe.Type.Base over open import Data.Empty open import Data.List +open import Data.List.Relation.Binary.Equality.Setoid over open import Data.Product open import Function -⊨-anticongˡ : ∀ {a aℓ b bℓ fℓ lℓ} {A : Language a aℓ} {B : Language b bℓ} {τ : Type fℓ lℓ} → B ≤ A → A ⊨ τ → B ⊨ τ +⊨-anticongˡ : ∀ {a b fℓ lℓ} {A : Language a} {B : Language b} {τ : Type fℓ lℓ} → B ≤ A → A ⊨ τ → B ⊨ τ ⊨-anticongˡ B≤A A⊨τ = record { n⇒n = A⊨τ.n⇒n ∘ B≤A.f ; f⇒f = A⊨τ.f⇒f ∘ map₂ B≤A.f @@ -26,12 +27,10 @@ open import Function module B≤A = _≤_ B≤A module A⊨τ = _⊨_ A⊨τ -L⊨τ⊥⇒L≈∅ : ∀ {a aℓ} {L : Language a aℓ} → L ⊨ τ⊥ → L ≈ ∅ +L⊨τ⊥⇒L≈∅ : ∀ {a} {L : Language a} → L ⊨ τ⊥ → L ≈ ∅ L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record { f = λ {l} → elim l ; f⁻¹ = λ () - ; cong₁ = λ {l} {_} {l∈L} → ⊥-elim (elim l l∈L) - ; cong₂ = λ {_} {_} {} } where module L⊨τ⊥ = _⊨_ L⊨τ⊥ @@ -47,10 +46,9 @@ L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record ; l⇒l = λ () } -L⊨τε⇒L≤｛ε｝ : ∀ {a aℓ} {L : Language a aℓ} → L ⊨ τε → L ≤ ｛ε｝ +L⊨τε⇒L≤｛ε｝ : ∀ {a} {L : Language a} → L ⊨ τε → L ≤ ｛ε｝ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record { f = λ {l} → elim l - ; cong = const tt } where open import Data.Unit @@ -73,16 +71,12 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record ｛c｝⊨τ[c] : ∀ c → ｛ c ｝ ⊨ τ[ c ] ｛c｝⊨τ[c] c = record { n⇒n = λ () - ; f⇒f = λ {x} → λ {([] , (a , eq , a∼c)) → begin - c ≈˘⟨ a∼c ⟩ - a ≡˘⟨ proj₁ (∷-injective eq) ⟩ - x ∎} - ; l⇒l = λ + ; f⇒f = λ {x} → λ {([] , (c∼x ∷ []≋[])) → c∼x} + ; l⇒l = λ {x} → λ { ([] , []≢[] , _) → ⊥-elim ([]≢[] refl) - ; (x ∷ [] , x∷[]≢[] , ()) + ; (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 - open import Data.List.Properties - open import Relation.Binary.Reasoning.Setoid over open import Relation.Binary.PropositionalEquality |