From ba7e3b5d9c868af4b5dd7c3af72c48a1dd27cc31 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 25 Mar 2021 18:01:19 +0000
Subject: Prove sequential unique decomposition.

Fix faulty definition of flast set.
---
 src/Cfe/Type/Properties.agda | 50 +++++++++++++++++++++++++++++---------------
 1 file changed, 33 insertions(+), 17 deletions(-)

(limited to 'src/Cfe/Type')

diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 134bfce..37f491b 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -16,11 +16,12 @@ 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 renaming (_≤_ to _≤ᵇ_; _∨_ to _∨ᵇ_)
-open import Data.Bool.Properties hiding (≤-reflexive)
+open import Data.Bool.Properties hiding (≤-reflexive; ≤-trans)
 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.Nat hiding (_≤ᵇ_; _^_) renaming (_≤_ to _≤ⁿ_)
+open import Data.Nat.Properties using (≤-stepsˡ; ≤-stepsʳ) renaming (≤-refl to ≤ⁿ-refl)
 open import Data.Product as Product
 open import Data.Sum as Sum
 open import Function hiding (_⟶_)
@@ -44,7 +45,7 @@ L⊨τ+¬N⇒ε∉L {L = L} {τ} L⊨τ ¬n ε∈L = case ∃[ b ] ((null L →
 ⊨-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))
+  ; l⇒l = A⊨τ.l⇒l ∘ Product.map₂ (Product.map₂ (Product.map B≤A.f (Product.map₂ B≤A.f)))
   }
   where
   module B≤A = _≤ˡ_ B≤A
@@ -108,8 +109,8 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
   ; f⇒f = λ {x} → λ {([] , (c∼x ∷ []≋[])) → c∼x}
   ; l⇒l = λ {x} → λ
     { ([] , []≢[] , _) → ⊥-elim ([]≢[] refl)
-    ; (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｝)
+    ; (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
@@ -131,8 +132,8 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
   module τ₁⊛τ₂ = _⊛_ τ₁⊛τ₂
 
 ∪-⊨ : ∀ {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
+      A ⊨ τ₁ → B ⊨ τ₂ → τ₁ # τ₂ → A ∪ B ⊨ τ₁ ∨ τ₂
+∪-⊨ {A = A} {B} {τ₁} {τ₂} A⊨τ₁ B⊨τ₂ τ₁#τ₂ = record
   { n⇒n = λ
     { (inj₁ ε∈A) → case ∃[ b ] T b ∋ Null τ₁ , A⊨τ₁.n⇒n ε∈A return (λ {(x , _) → T (x ∨ᵇ Null τ₂)}) of λ
       { (true , _) → _ }
@@ -144,21 +145,36 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
     ; (l , inj₂ x∷l∈B) → inj₂ (B⊨τ₂.f⇒f (-, x∷l∈B))
     }
   ; l⇒l = λ
-    { (l , l≢ε , l′ , inj₁ l++x∷l′∈A ) → inj₁ (A⊨τ₁.l⇒l (-, l≢ε , -, l++x∷l′∈A))
-    ; (l , l≢ε , l′ , inj₂ l++x∷l′∈B ) → inj₂ (B⊨τ₂.l⇒l (-, l≢ε , -, l++x∷l′∈B))
+    { ([] , l≢ε , l∈A∪B , l′ , l++x∷l′∈A∪B) → ⊥-elim (l≢ε refl)
+    ; (_ ∷ _ , _ , inj₁ l∈A , _ , inj₁ l++x∷l′∈A) → inj₁ (A⊨τ₁.l⇒l (-, (λ ()) , l∈A , -, l++x∷l′∈A))
+    ; (c ∷ _ , _ , inj₁ c∷u∈A , l′ , inj₂ c∷v∈B) → ⊥-elim (τ₁#τ₂.∄[f₁∩f₂] c (A⊨τ₁.f⇒f (-, c∷u∈A) , B⊨τ₂.f⇒f (-, c∷v∈B)))
+    ; (c ∷ _ , _ , inj₂ c∷u∈B , l′ , inj₁ c∷v∈A) → ⊥-elim (τ₁#τ₂.∄[f₁∩f₂] c (A⊨τ₁.f⇒f (-, c∷v∈A) , B⊨τ₂.f⇒f (-, c∷u∈B)))
+    ; (_ ∷ _ , _ , inj₂ l∈B , _ , inj₂ l++x∷l′∈B) → inj₂ (B⊨τ₂.l⇒l (-, (λ ()) , l∈B , -, l++x∷l′∈B))
     }
   }
   where
+  module τ₁#τ₂ = _#_ τ₁#τ₂
   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) }
+⋃-⊨ : ∀ {a fℓ lℓ} {F : Op₁ (Language a)} {τ : Type fℓ lℓ} →
+      (Congruent₁ _≤ˡ_ F) →
+      (∀ {L} → L ⊨ τ → F L ⊨ τ) → ⋃ F ⊨ τ
+⋃-⊨ {a} {F = F} {τ} ≤-mono ⊨-mono = record
+  { n⇒n = λ { (n , l∈Fⁿ) → _⊨_.n⇒n (Fⁿ⊨τ n) l∈Fⁿ}
+  ; f⇒f = λ { (_ , n , x∷l∈Fⁿ) → _⊨_.f⇒f (Fⁿ⊨τ n) (-, x∷l∈Fⁿ) }
+  ; l⇒l = λ
+    { (_ , l≢ε , (m , l∈Fᵐ) , _ , (n , l++x∷l′∈Fⁿ)) →
+         _⊨_.l⇒l (Fⁿ⊨τ (m + n))
+           (-, l≢ε , _≤ˡ_.f (^-mono (≤-stepsʳ {m} n ≤ⁿ-refl)) l∈Fᵐ ,
+            -, _≤ˡ_.f (^-mono (≤-stepsˡ m ≤ⁿ-refl)) l++x∷l′∈Fⁿ)
+    }
   }
   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)
+  Fⁿ⊨τ : ∀ n → (F ^ n) (Lift a ∅) ⊨ τ
+  Fⁿ⊨τ zero = ⊨-anticongˡ (≤-reflexive (lift-cong a ∅)) (⊨-congʳ (≤-min τ) ∅⊨τ⊥)
+  Fⁿ⊨τ (suc n) = ⊨-mono (Fⁿ⊨τ n)
+
+  ^-mono : ∀ {m n} → m ≤ⁿ n → (F ^ m) (Lift a ∅) ≤ˡ (F ^ n) (Lift a ∅)
+  ^-mono {n = n} z≤n = ≤-trans (≤-reflexive (lift-cong a ∅)) (≤ˡ-min ((F ^ n) (Lift a ∅)))
+  ^-mono (s≤s m≤n) = ≤-mono (^-mono m≤n)
-- 
cgit v1.2.3