diff options
Diffstat (limited to 'src/Cfe/Type')
| -rw-r--r-- | src/Cfe/Type/Properties.agda | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda index 4b38c1e..985219f 100644 --- a/src/Cfe/Type/Properties.agda +++ b/src/Cfe/Type/Properties.agda @@ -55,6 +55,7 @@ open import Data.Empty using (⊥-elim) open import Data.Empty.Polymorphic using (⊥) open import Data.List using ([]; _∷_; _++_) open import Data.List.Properties using (++-assoc; ++-identityʳ) +open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_) open import Data.List.Relation.Binary.Pointwise as Pw hiding (refl; setoid; map) open import Data.Nat using (suc; zero; _+_; z≤n; s≤s) renaming (_≤_ to _≤ⁿ_) open import Data.Nat.Properties using (m≤m+n; m≤n+m) @@ -759,6 +760,24 @@ L⊨τε⇒L≤｛ε｝ {A = A} A⊨τε = ∄[First[A]]⇒A⊆｛ε｝ λ _ xw y ∷ w₁ ++ u ∷ w′′ ≈˘⟨ ++⁺ (∼-refl ∷ Pw.refl ∼-refl) (y′∼u ∷ Pw.refl ∼-refl) ⟩ y ∷ w₁ ++ y′ ∷ w′′ ∎ +⊛⇒uniqueₗ : + τ₁ ⊛ τ₂ → A ⊨ τ₁ → B ⊨ τ₂ → + ∀ {w} → (p q : w ∈ A ∙ˡ B) → (_≋_ on proj₁) p q +⊛⇒uniqueₗ {A = A} {B = B} τ₁⊛τ₂ A⊨τ₁ B⊨τ₂ = + ∙-uniqueₗ A B + (λ (c∈l[A] , c∈f[B]) → ∄[l₁∩f₂] (A⊨τ₁ .l⇒l c∈l[A] , B⊨τ₂ .f⇒f c∈f[B])) + (λ ε∈A → ¬n₁ (A⊨τ₁ .n⇒n ε∈A)) + where open _⊛_ τ₁⊛τ₂; open _⊨_ + +⊛⇒uniqueᵣ : + τ₁ ⊛ τ₂ → A ⊨ τ₁ → B ⊨ τ₂ → + ∀ {w} → (p q : w ∈ A ∙ˡ B) → (_≋_ on proj₁ ∘ proj₂) p q +⊛⇒uniqueᵣ {A = A} {B = B} τ₁⊛τ₂ A⊨τ₁ B⊨τ₂ = + ∙-uniqueᵣ A B + (λ (c∈l[A] , c∈f[B]) → ∄[l₁∩f₂] (A⊨τ₁ .l⇒l c∈l[A] , B⊨τ₂ .f⇒f c∈f[B])) + (λ ε∈A → ¬n₁ (A⊨τ₁ .n⇒n ε∈A)) + where open _⊛_ τ₁⊛τ₂; open _⊨_ + ------------------------------------------------------------------------ -- Properties of _∨_ ------------------------------------------------------------------------ @@ -986,3 +1005,11 @@ L⊨τε⇒L≤｛ε｝ {A = A} A⊨τε = ∄[First[A]]⇒A⊆｛ε｝ λ _ xw open _#_ τ₁#τ₂ module A⊨τ₁ = _⊨_ A⊨τ₁ module B⊨τ₂ = _⊨_ B⊨τ₂ + +#⇒selective : τ₁ # τ₂ → A ⊨ τ₁ → B ⊨ τ₂ → ∀ {w} → ¬ (w ∈ A × w ∈ B) +#⇒selective τ₁#τ₂ A⊨τ₁ B⊨τ₂ {[]} (ε∈A , ε∈B) = + ¬n₁∨¬n₂ (A⊨τ₁ .n⇒n ε∈A , B⊨τ₂ .n⇒n ε∈B) + where open _#_ τ₁#τ₂; open _⊨_ +#⇒selective τ₁#τ₂ A⊨τ₁ B⊨τ₂ {c ∷ w} (cw∈A , cw∈B) = + ∄[f₁∩f₂] (A⊨τ₁ .f⇒f (w , cw∈A) , B⊨τ₂ .f⇒f (w , cw∈B)) + where open _#_ τ₁#τ₂; open _⊨_ |