Prove satisfaction for concatenation.lemma3.5

2 files changed, 148 insertions, 83 deletions

diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index 3e954b2..a3b5136 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -20,6 +20,8 @@ open import Relation.Binary.PropositionalEquality
 
 infix 4 _∈_
 infix 4 _∉_
+infix 4 _≈_
+infix 4 _≤_
 
 record Language a : Set (c ⊔ ℓ ⊔ suc a) where
   field
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index 8dff2ff..c4a5670 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -16,83 +16,15 @@ open import Data.Product as Product
 open import Data.Unit using (⊤)
 open import Function
 open import Level
-open import Relation.Binary.PropositionalEquality as ≡
+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; _≈_ to _∼_; refl to ∼-refl; sym to ∼-sym; trans to ∼-trans)
 
-module _
-  {a b}
-  (A : Language a)
-  (B : Language b)
-  where
-
-  private
-    module A = Language A
-    module B = Language B
-
-  infix 7 _∙_
-
-  Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
-  Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≋ l
-
-  _∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b)
-  _∙_ = record
-    { 𝕃 = Concat
-    ; ∈-resp-≋ = λ { l≋l′ (_ , l₁∈A , _ , l₂∈B , eq) → -, l₁∈A , -, l₂∈B , ≋-trans eq l≋l′
-      }
-    }
-
-isMonoid : ∀ {a} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝)
-isMonoid {a} = record
-  { isSemigroup = record
-    { isMagma = record
-      { isEquivalence = ≈-isEquivalence
-      ; ∙-cong = λ X≈Y U≈V → record
-        { f = λ { (_ , l₁∈X , _ , l₂∈U , eq) → -, _≈_.f X≈Y l₁∈X , -, _≈_.f U≈V l₂∈U , eq }
-        ; f⁻¹ = λ { (_ , l₁∈Y , _ , l₂∈V , eq) → -, _≈_.f⁻¹ X≈Y l₁∈Y , -, _≈_.f⁻¹ U≈V l₂∈V , eq }
-        }
-      }
-    ; assoc = λ X Y Z → record
-      { f = λ {l} → λ { (l₁₂ , (l₁ , l₁∈X , l₂ , l₂∈Y , eq₁) , l₃ , l₃∈Z , eq₂) →
-        -, l₁∈X , -, (-, l₂∈Y , -, l₃∈Z , ≋-refl) , (begin
-          l₁ ++ l₂ ++ l₃ ≡˘⟨ ++-assoc l₁ l₂ l₃ ⟩
-          (l₁ ++ l₂) ++ l₃ ≈⟨ ++⁺ eq₁ ≋-refl ⟩
-          l₁₂ ++ l₃ ≈⟨ eq₂ ⟩
-          l ∎) }
-      ; f⁻¹ = λ {l} → λ { (l₁ , l₁∈X , l₂₃ , (l₂ , l₂∈Y , l₃ , l₃∈Z , eq₁) , eq₂) →
-        -, (-, l₁∈X , -, l₂∈Y , ≋-refl) , -, l₃∈Z , (begin
-          (l₁ ++ l₂) ++ l₃ ≡⟨ ++-assoc l₁ l₂ l₃ ⟩
-          l₁ ++ l₂ ++ l₃ ≈⟨ ++⁺ ≋-refl eq₁ ⟩
-          l₁ ++ l₂₃ ≈⟨ eq₂ ⟩
-          l ∎) }
-      }
-    }
-  ; identity = (λ X → record
-    { f = λ { ([] , _ , _ , l₂∈X , eq) → Language.∈-resp-≋ X eq l₂∈X }
-    ; f⁻¹ = λ l∈X → -, lift refl , -, l∈X , ≋-refl
-    }) , (λ X → record
-    { f = λ { (l₁ , l₁∈X , [] , _ , eq) → Language.∈-resp-≋ X (≋-trans (≋-reflexive (sym (++-identityʳ l₁))) eq) l₁∈X }
-    ; f⁻¹ = λ {l} l∈X → -, l∈X , -, lift refl , ≋-reflexive (++-identityʳ l)
-    })
-  }
-  where
-  open import Relation.Binary.Reasoning.Setoid ≋-setoid
-
-∙-mono : ∀ {a b} → _∙_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
-∙-mono X≤Y U≤V = record
-  { f = λ {(_ , l₁∈X , _ , l₂∈U , eq) → -, X≤Y.f l₁∈X , -, U≤V.f l₂∈U , eq}
-  }
-  where
-  module X≤Y = _≤_ X≤Y
-  module U≤V = _≤_ U≤V
-
-private
+module Compare where
   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
@@ -142,29 +74,160 @@ private
   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
+  eq-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → isEqual cmp → ws ≋ ys × xs ≋ zs
+  eq-split (back xs≋zs) e = [] , xs≋zs
+  eq-split (front cmp w∼y) e = map₁ (w∼y ∷_) (eq-split cmp e)
+
+module _
+  {a b}
+  (A : Language a)
+  (B : Language b)
+  where
+
+  private
+    module A = Language A
+    module B = Language B
+
+  infix 7 _∙_
+
+  record Concat (l : List C) : Set (c ⊔ ℓ ⊔ a ⊔ b) where
+    field
+      l₁ : List C
+      l₂ : List C
+      l₁∈A : l₁ ∈ A
+      l₂∈B : l₂ ∈ B
+      eq : l₁ ++ l₂ ≋ l
+
+  _∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b)
+  _∙_ = record
+    { 𝕃 = Concat
+    ; ∈-resp-≋ = λ
+      { l≋l′ record { l₁ = _ ; l₂ = _ ; l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = eq } → record
+        { l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = ≋-trans eq l≋l′ }
+      }
+    }
+
+∙-cong : ∀ {a} → Congruent₂ _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
+∙-cong X≈Y U≈V = record
+  { f = λ
+    { record { l₁∈A = l₁∈X ; l₂∈B = l₂∈Y ; eq = eq } → record
+      { l₁∈A = X≈Y.f l₁∈X
+      ; l₂∈B = U≈V.f l₂∈Y
+      ; eq = eq
+      }
+    }
+  ; f⁻¹ = λ
+    { record { l₁∈A = l₁∈Y ; l₂∈B = l₂∈V ; eq = eq } → record
+      { l₁∈A = X≈Y.f⁻¹ l₁∈Y
+      ; l₂∈B = U≈V.f⁻¹ l₂∈V
+      ; eq = eq
+      }
+    }
+  }
+  where
+  module X≈Y = _≈_ X≈Y
+  module U≈V = _≈_ U≈V
+
+∙-assoc : ∀ {a b c} (A : Language a) (B : Language b) (C : Language c) →
+          (A ∙ B) ∙ C ≈ A ∙ (B ∙ C)
+∙-assoc A B C = record
+  { f = λ
+    { record
+      { l₂ = l₃
+      ; l₁∈A = record { l₁ = l₁ ; l₂ = l₂ ; l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = eq₁ }
+      ; l₂∈B = l₃∈C
+      ; eq = eq₂
+      } → record
+      { l₁∈A = l₁∈A
+      ; l₂∈B = record
+        { l₁∈A = l₂∈B
+        ; l₂∈B = l₃∈C
+        ; eq = ≋-refl
+        }
+      ; eq = ≋-trans (≋-sym (≋-reflexive (++-assoc l₁ l₂ l₃))) (≋-trans (++⁺ eq₁ ≋-refl) eq₂)
+      }
+    }
+  ; f⁻¹ = λ
+    { record
+      { l₁ = l₁
+      ; l₁∈A = l₁∈A
+      ; l₂∈B = record { l₁ = l₂ ; l₂ = l₃ ; l₁∈A = l₂∈B ; l₂∈B = l₃∈C ; eq = eq₁ }
+      ; eq = eq₂
+      } → record
+      { l₁∈A = record
+        { l₁∈A = l₁∈A
+        ; l₂∈B = l₂∈B
+        ; eq = ≋-refl
+        }
+      ; l₂∈B = l₃∈C
+      ; eq = ≋-trans (≋-reflexive (++-assoc l₁ l₂ l₃)) (≋-trans (++⁺ ≋-refl eq₁) eq₂)
+      }
+    }
+  }
+
+∙-identityˡ : ∀ {a} → LeftIdentity _≈_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝) _∙_
+∙-identityˡ X = record
+  { f = λ
+    { record { l₁ = [] ; l₂∈B = l∈X ; eq = eq } → X.∈-resp-≋ eq l∈X
+    }
+  ; f⁻¹ = λ l∈X → record
+    { l₁∈A = lift ≡.refl
+    ; l₂∈B = l∈X
+    ; eq = ≋-refl
+    }
+  }
+  where
+  module X = Language X
 
-∙-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)))
+∙-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) → Concat.l₁ l∈A∙B ≋ Concat.l₁ l∈A∙B′ × Concat.l₂ l∈A∙B ≋ Concat.l₂ l∈A∙B′
+∙-unique-prefix A B ∄[l₁∩f₂] ¬n₁ l∈A∙B l∈A∙B′ with Compare.compare (Concat.l₁ l∈A∙B) (Concat.l₂ l∈A∙B) (Concat.l₁ l∈A∙B′) (Concat.l₂ l∈A∙B′) (≋-trans (Concat.eq l∈A∙B) (≋-sym (Concat.eq l∈A∙B′)))
+... | cmp with Compare.<?> cmp
+... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] w ((-, (λ { ≡.refl → ¬n₁ (Concat.l₁∈A l∈A∙B′)}) , (Concat.l₁∈A l∈A∙B′) , -, A.∈-resp-≋ eq₃ (Concat.l₁∈A l∈A∙B)) , (-, B.∈-resp-≋ (≋-sym eq₄) (Concat.l₂∈B l∈A∙B′))))
   where
   module A = Language A
   module B = Language B
-  lsplit = left-split cmp l
+  lsplit = Compare.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))))
+... | tri≈ _ e _ = Compare.eq-split cmp e
+... | tri> _ _ r = ⊥-elim (∄[l₁∩f₂] w ((-, (λ { ≡.refl → ¬n₁ (Concat.l₁∈A l∈A∙B)}) , (Concat.l₁∈A l∈A∙B) , -, A.∈-resp-≋ (≋-sym eq₃) (Concat.l₁∈A l∈A∙B′)) , (-, (B.∈-resp-≋ eq₄ (Concat.l₂∈B l∈A∙B)))))
   where
   module A = Language A
   module B = Language B
-  rsplit = right-split cmp r
+  rsplit = Compare.right-split cmp r
   w = proj₁ rsplit
   eq₃ = (proj₁ ∘ proj₂ ∘ proj₂) rsplit
   eq₄ = (proj₂ ∘ proj₂ ∘ proj₂) rsplit
+
+∙-identityʳ : ∀ {a} → RightIdentity _≈_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝) _∙_
+∙-identityʳ X = record
+  { f = λ
+    { record { l₁ = l₁ ; l₂ = [] ; l₁∈A = l∈X ; eq = eq } → X.∈-resp-≋ (≋-trans (≋-sym (≋-reflexive (++-identityʳ l₁))) eq) l∈X
+    }
+  ; f⁻¹ = λ {l} l∈X → record
+    { l₁∈A = l∈X
+    ; l₂∈B = lift ≡.refl
+    ; eq = ≋-reflexive (++-identityʳ l)
+    }
+  }
+  where
+  module X = Language X
+
+isMagma : ∀ {a} → IsMagma _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
+isMagma {a} = record
+  { isEquivalence = ≈-isEquivalence
+  ; ∙-cong = ∙-cong {a}
+  }
+
+isSemigroup : ∀ {a} → IsSemigroup _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
+isSemigroup {a} = record
+  { isMagma = isMagma {a}
+  ; assoc = ∙-assoc
+  }
+
+isMonoid : ∀ {a} → IsMonoid _≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝)
+isMonoid {a} = record
+  { isSemigroup = isSemigroup {a}
+  ; identity = ∙-identityˡ {a} , ∙-identityʳ {a}
+  }