Prove sequential unique decomposition.

Fix faulty definition of flast set.

3 files changed, 119 insertions, 20 deletions

diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index bda9000..3e954b2 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -68,4 +68,4 @@ first : ∀ {a} → Language a → C → Set (c ⊔ a)
 first A x = ∃[ l ] x ∷ l ∈ A
 
 flast : ∀ {a} → Language a → C → Set (c ⊔ a)
-flast A x = ∃[ l ] (l ≢ [] × ∃[ l′ ] l ++ x ∷ l′ ∈ A)
+flast A x = ∃[ l ] (l ≢ [] × l ∈ A × ∃[ l′ ] l ++ x ∷ l′ ∈ A)
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index 428e8a4..8dff2ff 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -9,16 +9,19 @@ module Cfe.Language.Construct.Concatenate
 open import Algebra
 open import Cfe.Language over as 𝕃
 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.List.Properties
 open import Data.Product as Product
+open import Data.Unit using (⊤)
 open import Function
 open import Level
 open import Relation.Binary.PropositionalEquality as ≡
+open import Relation.Nullary
+open import Relation.Unary hiding (_∈_)
 import Relation.Binary.Indexed.Heterogeneous as I
 
-open Setoid over using () renaming (Carrier to C)
+open Setoid over using () renaming (Carrier to C; _≈_ to _∼_; refl to ∼-refl; sym to ∼-sym; trans to ∼-trans)
 
 module _
   {a b}
@@ -85,3 +88,83 @@ isMonoid {a} = record
   where
   module X≤Y = _≤_ X≤Y
   module U≤V = _≤_ U≤V
+
+private
+  data Compare : List C → List C → List C → List C → Set (c ⊔ ℓ) where
+    -- left : ∀ {ws₁ w ws₂ xs ys z zs₁ zs₂} → (ws₁≋ys : ws₁ ≋ ys) → (w∼z : w ∼ z) → (ws₂≋zs₁ : ws₂ ≋ zs₁) → (xs≋zs₂ : xs ≋ zs₂) → Compare (ws₁ ++ w ∷ ws₂) xs ys (z ∷ zs₁ ++ zs₂)
+    -- right : ∀ {ws x xs₁ xs₂ ys₁ y ys₂ zs} → (ws≋ys₁ : ws ≋ ys₁) → (x∼y : x ∼ y) → (xs₁≋ys₂ : xs₁ ≋ ys₂) → (xs₂≋zs : xs₂ ≋ zs) → Compare ws (x ∷ xs₁ ++ xs₂) (ys₁ ++ y ∷ ys₂) zs
+    back : ∀ {xs zs} → (xs≋zs : xs ≋ zs) → Compare [] xs [] zs
+    left : ∀ {w ws xs z zs} → Compare ws xs [] zs → (w∼z : w ∼ z) → Compare (w ∷ ws) xs [] (z ∷ zs)
+    right : ∀ {x xs y ys zs} → Compare [] xs ys zs → (x∼y : x ∼ y) → Compare [] (x ∷ xs) (y ∷ ys) zs
+    front : ∀ {w ws xs y ys zs} → Compare ws xs ys zs → (w∼y : w ∼ y) → Compare (w ∷ ws) xs (y ∷ ys) zs
+
+  isLeft : ∀ {ws xs ys zs} → Compare ws xs ys zs → Set
+  isLeft (back xs≋zs) = ⊥
+  isLeft (left cmp w∼z) = ⊤
+  isLeft (right cmp x∼y) = ⊥
+  isLeft (front cmp w∼y) = isLeft cmp
+
+  isRight : ∀ {ws xs ys zs} → Compare ws xs ys zs → Set
+  isRight (back xs≋zs) = ⊥
+  isRight (left cmp w∼z) = ⊥
+  isRight (right cmp x∼y) = ⊤
+  isRight (front cmp w∼y) = isRight cmp
+
+  isEqual : ∀ {ws xs ys zs} → Compare ws xs ys zs → Set
+  isEqual (back xs≋zs) = ⊤
+  isEqual (left cmp w∼z) = ⊥
+  isEqual (right cmp x∼y) = ⊥
+  isEqual (front cmp w∼y) = isEqual cmp
+
+  <?> : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → Tri (isLeft cmp) (isEqual cmp) (isRight cmp)
+  <?> (back xs≋zs) = tri≈ id _ id
+  <?> (left cmp w∼z) = tri< _ id id
+  <?> (right cmp x∼y) = tri> id id _
+  <?> (front cmp w∼y) = <?> cmp
+
+  compare : ∀ ws xs ys zs → ws ++ xs ≋ ys ++ zs → Compare ws xs ys zs
+  compare [] xs [] zs eq = back eq
+  compare [] (x ∷ xs) (y ∷ ys) zs (x∼y ∷ eq) = right (compare [] xs ys zs eq) x∼y
+  compare (w ∷ ws) xs [] (z ∷ zs) (w∼z ∷ eq) = left (compare ws xs [] zs eq) w∼z
+  compare (w ∷ ws) xs (y ∷ ys) zs (w∼y ∷ eq) = front (compare ws xs ys zs eq) w∼y
+
+  left-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → isLeft cmp → ∃[ w ] ∃[ ws′ ] ws ≋ ys ++ w ∷ ws′ × w ∷ ws′ ++ xs ≋ zs
+  left-split (left (back xs≋zs) w∼z) _ = -, -, ≋-refl , w∼z ∷ xs≋zs
+  left-split (left (left cmp w′∼z′) w∼z) _ with left-split (left cmp w′∼z′) _
+  ... | (_ , _ , eq₁ , eq₂) = -, -, ∼-refl ∷ eq₁ , w∼z ∷ eq₂
+  left-split (front cmp w∼y) l with left-split cmp l
+  ... | (_ , _ , eq₁ , eq₂) = -, -, w∼y ∷ eq₁ , eq₂
+
+  right-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → isRight cmp → ∃[ y ] ∃[ ys′ ] ws ++ y ∷ ys′ ≋ ys × xs ≋ y ∷ ys′ ++ zs
+  right-split (right (back xs≋zs) x∼y) _ = -, -, ≋-refl , x∼y ∷ xs≋zs
+  right-split (right (right cmp x′∼y′) x∼y) _ with right-split (right cmp x′∼y′) _
+  ... | (_ , _ , eq₁ , eq₂) = -, -, ∼-refl ∷ eq₁ , x∼y ∷ eq₂
+  right-split (front cmp w∼y) r with right-split cmp r
+  ... | (_ , _ , eq₁ , eq₂) = -, -, w∼y ∷ eq₁ , eq₂
+
+  eq-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → isEqual cmp → ws ≋ ys
+  eq-split (back xs≋zs) e = []
+  eq-split (front cmp w∼y) e = w∼y ∷ eq-split cmp e
+
+∙-unique-prefix : ∀ {a b} (A : Language a) (B : Language b) → Empty (flast A ∩ first B) → ¬ (null A) → ∀ {l} → (l∈A∙B l∈A∙B′ : l ∈ A ∙ B) → proj₁ l∈A∙B ≋ proj₁ l∈A∙B′
+∙-unique-prefix _ _ _ ¬n₁ ([] , l₁∈A , _) _ = ⊥-elim (¬n₁ l₁∈A)
+∙-unique-prefix _ _ _ ¬n₁ (_ ∷ _ , _) ([] , l₁′∈A , _) = ⊥-elim (¬n₁ l₁′∈A)
+∙-unique-prefix A B ∄[l₁∩f₂] _ (c ∷ l₁ , l₁∈A , l₂ , l₂∈B , eq₁) (c′ ∷ l₁′ , l₁′∈A , l₂′ , l₂′∈B , eq₂) with compare (c ∷ l₁) l₂ (c′ ∷ l₁′) l₂′ (≋-trans eq₁ (≋-sym eq₂))
+... | cmp with <?> cmp
+... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] w ((-, (λ ()) , l₁′∈A , -, A.∈-resp-≋ eq₃ l₁∈A) , (-, B.∈-resp-≋ (≋-sym eq₄) l₂′∈B)))
+  where
+  module A = Language A
+  module B = Language B
+  lsplit = left-split cmp l
+  w = proj₁ lsplit
+  eq₃ = (proj₁ ∘ proj₂ ∘ proj₂) lsplit
+  eq₄ = (proj₂ ∘ proj₂ ∘ proj₂) lsplit
+... | tri≈ _ e _ = eq-split cmp e
+... | tri> _ _ r = ⊥-elim (∄[l₁∩f₂] w ((-, (λ ()) , l₁∈A , -, A.∈-resp-≋ (≋-sym eq₃) l₁′∈A) , (-, (B.∈-resp-≋ eq₄ l₂∈B))))
+  where
+  module A = Language A
+  module B = Language B
+  rsplit = right-split cmp r
+  w = proj₁ rsplit
+  eq₃ = (proj₁ ∘ proj₂ ∘ proj₂) rsplit
+  eq₄ = (proj₂ ∘ proj₂ ∘ proj₂) rsplit
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)