Make progress on lemma 3.5 (4).

2 files changed, 35 insertions, 10 deletions

diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index ef45432..428e8a4 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -26,10 +26,11 @@ module _
   (B : Language b)
   where
 
-  module A = Language A
-  module B = Language B
+  private
+    module A = Language A
+    module B = Language B
 
-  infix 4 _∙_
+  infix 7 _∙_
 
   Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
   Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≋ l
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index cfdf694..78212ba 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -9,19 +9,25 @@ module Cfe.Type.Properties
 open Setoid over using () renaming (Carrier to C; _≈_ to _∼_)
 
 open import Cfe.Language over
+open import Cfe.Language.Construct.Concatenate over renaming (_∙_ to _∙ˡ_)
 open import Cfe.Language.Construct.Single over
 open import Cfe.Type.Base over
+open import Data.Bool hiding (_≤_)
+open import Data.Bool.Properties
 open import Data.Empty
-open import Data.List
+open import Data.List hiding (null)
 open import Data.List.Relation.Binary.Equality.Setoid over
-open import Data.Product
+open import Data.Product as Product
+open import Data.Sum as Sum
+open import Data.Unit hiding (_≤_)
 open import Function
+open import Relation.Binary.PropositionalEquality
 
 ⊨-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
-  ; l⇒l = A⊨τ.l⇒l ∘ map₂ (map₂ (map₂ 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))
   }
   where
   module B≤A = _≤_ B≤A
@@ -51,8 +57,6 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
   { f = λ {l} → elim l
   }
   where
-  open import Data.Unit
-  open import Relation.Binary.PropositionalEquality
   module L⊨τε = _⊨_ L⊨τε
 
   elim : ∀ l → l ∈ L → l ∈ ｛ε｝
@@ -79,4 +83,24 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
     }
   }
   where
-  open import Relation.Binary.PropositionalEquality
+
+∙-⊨ : ∀ {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
+  { n⇒n = λ { ([] , l∈A , _) → ⊥-elim (¬n₁ l∈A) }
+  ; f⇒f = λ
+    { (_ , [] , l∈A , l′ , l′∈B , _) → ⊥-elim (¬n₁ l∈A)
+    ; (_ , x ∷ l , l∈A , l′ , l′∈B , x≈x ∷ _) → inj₁ (A⊨τ₁.f⇒f (l , A.∈-resp-≋ (x≈x ∷ ≋-refl) l∈A))
+    }
+  ; l⇒l = {!!}
+  }
+  where
+  module A = Language A
+  module A⊨τ₁ = _⊨_ A⊨τ₁
+  module B⊨τ₂ = _⊨_ B⊨τ₂
+  module τ₁⊛τ₂ = _⊛_ τ₁⊛τ₂
+
+  ¬n₁ : null A → ⊥
+  ¬n₁ ε∈A = case ∃[ b ] ((null A → T b) × T (not b)) ∋ Null τ₁ , A⊨τ₁.n⇒n , τ₁⊛τ₂.¬n₁ of λ
+    { (false , n⇒n , _) → n⇒n ε∈A
+    }