From abe9461e0dc194c160d97fee23a1646097a0c264 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 24 Mar 2021 17:01:29 +0000
Subject: Prove lemma 3.5 (7).

---
 src/Cfe/Type/Base.agda       | 25 ++++++++++++++++--
 src/Cfe/Type/Properties.agda | 61 +++++++++++++++++++++++++++++++++++---------
 2 files changed, 72 insertions(+), 14 deletions(-)

(limited to 'src/Cfe/Type')

diff --git a/src/Cfe/Type/Base.agda b/src/Cfe/Type/Base.agda
index a5ed780..438dd65 100644
--- a/src/Cfe/Type/Base.agda
+++ b/src/Cfe/Type/Base.agda
@@ -8,10 +8,11 @@ module Cfe.Type.Base
 
 open Setoid over using () renaming (Carrier to C; _≈_ to _∼_)
 
-open import Cfe.Language over
-open import Data.Bool as 𝔹 hiding (_∨_)
+open import Cfe.Language over hiding (_≤_; _≈_)
+open import Data.Bool as 𝔹 hiding (_∨_) renaming (_≤_ to _≤ᵇ_)
 open import Level as L renaming (suc to lsuc)
 open import Relation.Unary as U
+open import Relation.Binary.PropositionalEquality using (_≡_)
 
 infix 7 _∙_
 infix 6 _∨_
@@ -69,3 +70,23 @@ record _#_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} (τ₁ : Type fℓ₁ lℓ₁
   field
     ∄[f₁∩f₂] : Empty (τ₁.First ∩ τ₂.First)
     ¬n₁∨¬n₂ : T (not (τ₁.Null 𝔹.∨ τ₂.Null))
+
+record _≤_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
+
+  field
+    n≤n : τ₁.Null ≤ᵇ τ₂.Null
+    f⊆f : τ₁.First ⊆ τ₂.First
+    l⊆l : τ₁.Flast ⊆ τ₂.Flast
+
+record _≈_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
+
+  field
+    n≡n : τ₁.Null ≡ τ₂.Null
+    f₁⊆f₂ : τ₁.First ⊆ τ₂.First
+    f₁⊇f₂ : τ₁.First ⊇ τ₂.First
+    l₁⊆l₂ : τ₁.Flast ⊆ τ₂.Flast
+    l₁⊇l₂ : τ₁.Flast ⊇ τ₂.Flast
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 0d024b5..134bfce 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary
 
 module Cfe.Type.Properties
   {c ℓ} (over : Setoid c ℓ)
@@ -8,36 +8,62 @@ module Cfe.Type.Properties
 
 open Setoid over using () renaming (Carrier to C; _≈_ to _∼_)
 
-open import Cfe.Language over
+open import Algebra
+open import Cfe.Language over renaming (_≤_ to _≤ˡ_; _≈_ to _≈ˡ_; ≤-min to ≤ˡ-min)
 open import Cfe.Language.Construct.Concatenate over renaming (_∙_ to _∙ˡ_)
 open import Cfe.Language.Construct.Single over
 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 hiding (_≤_) renaming (_∨_ to _∨ᵇ_)
-open import Data.Bool.Properties
+open import Data.Bool renaming (_≤_ to _≤ᵇ_; _∨_ to _∨ᵇ_)
+open import Data.Bool.Properties hiding (≤-reflexive)
 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.Product as Product
 open import Data.Sum as Sum
-open import Function
+open import Function hiding (_⟶_)
+open import Relation.Unary.Properties
 open import Relation.Binary.PropositionalEquality
 
-⊨-anticongˡ : ∀ {a b fℓ lℓ} {A : Language a} {B : Language b} {τ : Type fℓ lℓ} → B ≤ A → A ⊨ τ → B ⊨ τ
+≤-min : ∀ {fℓ lℓ} → Min (_≤_ {_} {_} {fℓ} {lℓ}) τ⊥
+≤-min τ = record
+  { n≤n = ≤-minimum τ.Null
+  ; f⊆f = λ ()
+  ; l⊆l = λ ()
+  }
+  where
+  module τ = Type τ
+
+L⊨τ+¬N⇒ε∉L : ∀ {a fℓ lℓ} {L : Language a} {τ : Type fℓ lℓ} → L ⊨ τ → T (not (Type.Null τ)) → [] ∉ L
+L⊨τ+¬N⇒ε∉L {L = L} {τ} L⊨τ ¬n ε∈L = case ∃[ b ] ((null L → T b) × T (not b)) ∋ Null τ , _⊨_.n⇒n L⊨τ , ¬n of λ
+  { (false , n⇒n , _) → n⇒n ε∈L }
+
+⊨-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 ∘ 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
+  module B≤A = _≤ˡ_ B≤A
   module A⊨τ = _⊨_ A⊨τ
 
-L⊨τ+¬N⇒ε∉L : ∀ {a fℓ lℓ} {L : Language a} {τ : Type fℓ lℓ} → L ⊨ τ → T (not (Type.Null τ)) → [] ∉ L
-L⊨τ+¬N⇒ε∉L {L = L} {τ} L⊨τ ¬n ε∈L = case ∃[ b ] ((null L → T b) × T (not b)) ∋ Null τ , _⊨_.n⇒n L⊨τ , ¬n of λ
-  { (false , n⇒n , _) → n⇒n ε∈L }
+⊨-congʳ : ∀ {a fℓ₁ lℓ₁ fℓ₂ lℓ₂} {A : Language a} → (A ⊨_) ⟶ (A ⊨_) Respects (_≤_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂})
+⊨-congʳ {A = A} τ₁≤τ₂ A⊨τ₁ = record
+  { n⇒n = λ ε∈A → case ∃[ b ] (null A → T b) × ∃[ b′ ] b ≤ᵇ b′ ∋ τ₁.Null , A⊨τ₁.n⇒n , τ₂.Null , n≤n return (λ (_ , _ , x , _) → T x) of λ
+    { (_ , _ , true , _) → _
+    ; (false , n⇒n , false , _) → n⇒n ε∈A
+    }
+  ; f⇒f = f⊆f ∘ A⊨τ₁.f⇒f
+  ; l⇒l = l⊆l ∘ A⊨τ₁.l⇒l
+  }
+  where
+  open _≤_ τ₁≤τ₂
+  module A⊨τ₁ = _⊨_ A⊨τ₁
 
-L⊨τ⊥⇒L≈∅ : ∀ {a} {L : Language a} → L ⊨ τ⊥ → L ≈ ∅
+L⊨τ⊥⇒L≈∅ : ∀ {a} {L : Language a} → L ⊨ τ⊥ → L ≈ˡ ∅
 L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   { f = λ {l} → elim l
   ; f⁻¹ = λ ()
@@ -56,7 +82,7 @@ L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   ; l⇒l = λ ()
   }
 
-L⊨τε⇒L≤｛ε｝ : ∀ {a} {L : Language a} → L ⊨ τε → L ≤ ｛ε｝
+L⊨τε⇒L≤｛ε｝ : ∀ {a} {L : Language a} → L ⊨ τε → L ≤ˡ ｛ε｝
 L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
   { f = λ {l} → elim l
   }
@@ -125,3 +151,14 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
   where
   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) }
+  }
+  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)
-- 
cgit v1.2.3