Complete proofs up to Proposition 3.2 (excluding unrolling)

1 files changed, 109 insertions, 21 deletions

diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index 29e635d..62acf8f 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -1,40 +1,128 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary
-import Cfe.Language
 
 module Cfe.Language.Construct.Concatenate
-  {c ℓ a aℓ b bℓ} (over : Setoid c ℓ)
-  (A : Cfe.Language.Language over a aℓ)
-  (B : Cfe.Language.Language over b bℓ)
+  {c ℓ} (over : Setoid c ℓ)
   where
 
+open import Algebra
+open import Cfe.Language over as 𝕃
 open import Data.Empty
 open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid over
+open import Data.List.Properties
 open import Data.Product as Product
 open import Function
 open import Level
-open import Cfe.Language over
+open import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.Indexed.Heterogeneous as I
 
-open Setoid over renaming (Carrier to C)
+open Setoid over using () renaming (Carrier to C)
 
-infix 4 _≈ᶜ_
-infix 4 _∙_
+module _
+  {a aℓ b bℓ}
+  (A : Language a aℓ)
+  (B : Language b bℓ)
+  where
+
+  infix 4 _≈ᶜ_
+  infix 4 _∙_
+
+  Concat : List C → Set (c ⊔ a ⊔ b)
+  Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B ×  l₁ ++ l₂ ≡ l
 
-Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
-Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B ×  l₁ ++ l₂ ≋ l
+  _≈ᶜ_ : {l₁ l₂ : List C} → REL (Concat l₁) (Concat l₂) (aℓ ⊔ bℓ)
+  (_ , l₁∈A , _ , l₂∈B , _) ≈ᶜ (_ , l₁′∈A , _ , l₂′∈B , _) = (≈ᴸ A l₁∈A l₁′∈A) × (≈ᴸ B l₂∈B l₂′∈B)
 
-_≈ᶜ_ : {l₁ l₂ : List C} → REL (Concat l₁) (Concat l₂) (aℓ ⊔ bℓ)
-(_ , l₁∈A , _ , l₂∈B , _) ≈ᶜ (_ , l₁′∈A , _ , l₂′∈B , _) = (≈ᴸ A l₁∈A l₁′∈A) × (≈ᴸ B l₂∈B l₂′∈B)
+  _∙_ : Language (c ⊔ a ⊔ b) (aℓ ⊔ bℓ)
+  _∙_ = record
+    { Carrier = Concat
+    ; _≈_ = _≈ᶜ_
+    ; isEquivalence = record
+      { refl = ≈ᴸ-refl A , ≈ᴸ-refl B
+      ; sym = Product.map (≈ᴸ-sym A) (≈ᴸ-sym B)
+      ; trans = Product.zip (≈ᴸ-trans A) (≈ᴸ-trans B)
+      }
+    }
 
-_∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b) (aℓ ⊔ bℓ)
-_∙_ = record
-  { Carrier = Concat
-  ; _≈_ = _≈ᶜ_
-  ; isEquivalence = record
-    { refl = ≈ᴸ-refl A , ≈ᴸ-refl B
-    ; sym = Product.map (≈ᴸ-sym A) (≈ᴸ-sym B)
-    ; trans = Product.zip (≈ᴸ-trans A) (≈ᴸ-trans B)
+isMonoid : ∀ {a aℓ} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)
+isMonoid {a} = record
+  { isSemigroup = record
+    { isMagma = record
+      { isEquivalence = ≈-isEquivalence
+      ; ∙-cong = λ X≈Y U≈V → record
+        { f = λ { (l₁ , l₁∈X , l₂ , l₂∈U , l₁++l₂≡l) → l₁ , _≈_.f X≈Y l₁∈X , l₂ , _≈_.f U≈V l₂∈U , l₁++l₂≡l}
+        ; f⁻¹ = λ { (l₁ , l₁∈Y , l₂ , l₂∈V , l₁++l₂≡l) → l₁ , _≈_.f⁻¹ X≈Y l₁∈Y , l₂ , _≈_.f⁻¹ U≈V l₂∈V , l₁++l₂≡l}
+        ; cong₁ = λ { (x , y) → _≈_.cong₁ X≈Y x ,  _≈_.cong₁ U≈V y}
+        ; cong₂ = λ { (x , y) → _≈_.cong₂ X≈Y x ,  _≈_.cong₂ U≈V y}
+        }
+      }
+    ; assoc = λ X Y Z → record
+      { f = λ {l} → (λ { (l₁ , (l₁′ , l₁′∈X , l₂′ , l₂′∈Y , l₁′++l₂′≡l₁) , l₂ , l₂∈Z , l₁++l₂≡l) →
+        l₁′ , l₁′∈X , l₂′ ++ l₂ , (l₂′ , l₂′∈Y , l₂ , l₂∈Z , refl) , (begin
+          l₁′ ++ l₂′ ++ l₂   ≡˘⟨ ++-assoc l₁′ l₂′ l₂ ⟩
+          (l₁′ ++ l₂′) ++ l₂ ≡⟨ cong (_++ l₂) l₁′++l₂′≡l₁ ⟩
+          l₁ ++ l₂          ≡⟨ l₁++l₂≡l ⟩
+          l                 ∎)})
+      ; f⁻¹ = λ {l} → λ { (l₁ , l₁∈X , l₂ , (l₁′ , l₁′∈Y , l₂′ , l₂′∈Z , l₁′++l₂′≡l₂), l₁++l₂≡l) →
+        l₁ ++ l₁′ , ( l₁ , l₁∈X , l₁′ , l₁′∈Y , refl) , l₂′ , l₂′∈Z , (begin
+          (l₁ ++ l₁′) ++ l₂′ ≡⟨ ++-assoc l₁ l₁′ l₂′ ⟩
+          l₁ ++ (l₁′ ++ l₂′) ≡⟨ cong (l₁ ++_) l₁′++l₂′≡l₂ ⟩
+          l₁ ++ l₂          ≡⟨ l₁++l₂≡l ⟩
+          l                 ∎)}
+      ; cong₁ = Product.assocʳ
+      ; cong₂ = Product.assocˡ
+      }
     }
+  ; identity = (λ A → record
+    { f = idˡ {a} A
+    ; f⁻¹ = λ {l} l∈A → [] , lift refl , l , l∈A , refl
+    ; cong₁ = λ {l₁} {l₂} {l₁∈A} {l₂∈A} → idˡ-cong {a} A {l₁} {l₂} {l₁∈A} {l₂∈A}
+    ; cong₂ = λ l₁≈l₂ → lift _ , l₁≈l₂
+    }) , (λ A → record
+    { f = idʳ {a} A
+    ; f⁻¹ = λ {l} l∈A → l , l∈A , [] , lift refl , ++-identityʳ l
+    ; cong₁ = λ {l₁} {l₂} {l₁∈A} {l₂∈A} → idʳ-cong {a} A {l₁} {l₂} {l₁∈A} {l₂∈A}
+    ; cong₂ = λ l₁≈l₂ → l₁≈l₂ , lift _
+    })
+  }
+  where
+  open ≡.≡-Reasoning
+
+  idˡ : ∀ {a aℓ} →
+        (A : Language (c ⊔ ℓ ⊔ a) aℓ) →
+        ∀ {l} →
+        l ∈ ((𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) ∙ A) →
+        l ∈ A
+  idˡ _ ([] , _ , l , l∈A , refl) = l∈A
+
+  idˡ-cong : ∀ {a aℓ} →
+             (A : Language (c ⊔ ℓ ⊔ a) aℓ) →
+             ∀ {l₁ l₂ l₁∈A l₂∈A} →
+             ≈ᴸ ((𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) ∙ A) {l₁} {l₂} l₁∈A l₂∈A →
+             ≈ᴸ A (idˡ {a} A l₁∈A) (idˡ {a} A l₂∈A)
+  idˡ-cong _ {l₁∈A = [] , _ , l₁ , l₁∈A , refl} {[] , _ , l₂ , l₂∈A , refl} (_ , l₁≈l₂) = l₁≈l₂
+
+  idʳ : ∀ {a aℓ} →
+        (A : Language (c ⊔ ℓ ⊔ a) aℓ) →
+        ∀ {l} →
+        l ∈ (A ∙ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)) →
+        l ∈ A
+  idʳ A (l , l∈A , [] , _ , refl) = ∈-cong A (sym (++-identityʳ l)) l∈A
+
+  idʳ-cong : ∀ {a aℓ} →
+             (A : Language (c ⊔ ℓ ⊔ a) aℓ) →
+             ∀ {l₁ l₂ l₁∈A l₂∈A} →
+             ≈ᴸ (A ∙ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)) {l₁} {l₂} l₁∈A l₂∈A →
+             ≈ᴸ A (idʳ {a} A l₁∈A) (idʳ {a} A l₂∈A)
+  idʳ-cong A {l₁∈A = l₁ , l₁∈A , [] , _ , refl} {l₂ , l₂∈A , [] , _ , refl} (l₁≈l₂ , _) =
+    ≈ᴸ-cong A (sym (++-identityʳ l₁)) (sym (++-identityʳ l₂)) l₁∈A l₂∈A l₁≈l₂
+
+∙-monotone : ∀ {a aℓ b bℓ} → _∙_ Preserves₂ _≤_ {a} {aℓ} ⟶ _≤_ {b} {bℓ} ⟶ _≤_
+∙-monotone X≤Y U≤V = record
+  { f = λ {(_ , l₁∈X , _ , l₂∈U , l₁++l₂≡l) → -, X≤Y.f l₁∈X , -, U≤V.f l₂∈U , l₁++l₂≡l}
+  ; cong = Product.map X≤Y.cong U≤V.cong
   }
+  where
+  module X≤Y = _≤_ X≤Y
+  module U≤V = _≤_ U≤V