Prove lemma 3.5 (7).

4 files changed, 95 insertions, 26 deletions

diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
index 5ed031b..1a37326 100644
--- a/src/Cfe/Language/Indexed/Construct/Iterate.agda
+++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda
@@ -8,10 +8,11 @@ module Cfe.Language.Indexed.Construct.Iterate
 
 open Setoid over using () renaming (Carrier to C)
 
+open import Algebra
 open import Cfe.Language over as L
 open import Cfe.Language.Indexed.Homogeneous over
 open import Data.List
-open import Data.Nat as ℕ hiding (_⊔_; _≤_)
+open import Data.Nat as ℕ hiding (_⊔_; _≤_; _^_)
 open import Data.Product as Product
 open import Function
 open import Level hiding (Lift) renaming (suc to lsuc)
@@ -20,11 +21,13 @@ open import Relation.Binary.PropositionalEquality as ≡
 
 open IndexedLanguage
 
-iter : ∀ {a} {A : Set a} → (A → A) → ℕ → A → A
-iter f ℕ.zero = id
-iter f (ℕ.suc n) = f ∘ iter f n
+infix 9 _^_
 
-f-fn-x≡fn-f-x : ∀ {a} {A : Set a} (f : A → A) n x → f (iter f n x) ≡ iter f n (f x)
+_^_ : ∀ {a} {A : Set a} → Op₁ A → ℕ → Op₁ A
+f ^ zero = id
+f ^ (suc n) = f ∘ (f ^ n)
+
+f-fn-x≡fn-f-x : ∀ {a} {A : Set a} (f : A → A) n x → f ((f ^ n) x) ≡ (f ^ n) (f x)
 f-fn-x≡fn-f-x f ℕ.zero x = refl
 f-fn-x≡fn-f-x f (suc n) x = ≡.cong f (f-fn-x≡fn-f-x f n x)
 
@@ -32,9 +35,10 @@ module _
   {a aℓ} (A : B.Setoid a aℓ)
   where
 
-  module A = B.Setoid A
+  private
+    module A = B.Setoid A
 
-  f≈g⇒fn≈gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≈ y → f x A.≈ g y) → ∀ n x → iter f n x A.≈ iter g n x
+  f≈g⇒fn≈gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≈ y → f x A.≈ g y) → ∀ n x → (f ^ n) x A.≈ (g ^ n) x
   f≈g⇒fn≈gn f≈g ℕ.zero x = A.refl
   f≈g⇒fn≈gn f≈g (suc n) x = f≈g (f≈g⇒fn≈gn f≈g n x)
 
@@ -42,10 +46,11 @@ module _
   {a aℓ₁ aℓ₂} (A : B.Poset a aℓ₁ aℓ₂)
   where
 
-  module A′ = B.Poset A
+  private
+    module A = B.Poset A
 
-  f≤g⇒fn≤gn : {f g : A′.Carrier → A′.Carrier} → (∀ {x y} → x A′.≤ y → f x A′.≤ g y) → ∀ n x → iter f n x A′.≤ iter g n x
-  f≤g⇒fn≤gn f≤g ℕ.zero x = A′.refl
+  f≤g⇒fn≤gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≤ y → f x A.≤ g y) → ∀ n x → (f ^ n) x A.≤ (g ^ n) x
+  f≤g⇒fn≤gn f≤g ℕ.zero x = A.refl
   f≤g⇒fn≤gn f≤g (suc n) x = f≤g (f≤g⇒fn≤gn f≤g n x)
 
 module _
@@ -56,7 +61,7 @@ module _
     { Carrierᵢ = ℕ
     ; _≈ᵢ_ = ≡._≡_
     ; isEquivalenceᵢ = ≡.isEquivalence
-    ; F = λ n → iter f n (Lift a ∅)
+    ; F = λ n → (f ^ n) (Lift a ∅)
     ; cong = λ {≡.refl → ≈-refl}
     }
 
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index b2630ce..756877c 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -13,7 +13,7 @@ open import Cfe.Language.Base over
 open import Data.List
 open import Data.List.Relation.Binary.Equality.Setoid over
 open import Function
-open import Level
+open import Level hiding (Lift)
 
 ≈-refl : ∀ {a} → Reflexive (_≈_ {a})
 ≈-refl {x = A} = record
@@ -94,3 +94,9 @@ setoid a = record { isEquivalence = ≈-isEquivalence {a} }
 
 poset : ∀ a → Poset (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) (c ⊔ a)
 poset a = record { isPartialOrder = ≤-isPartialOrder a }
+
+lift-cong : ∀ {a} b (L : Language a) → Lift b L ≈ L
+lift-cong b L = record
+  { f = lower
+  ; f⁻¹ = lift
+  }
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)