Change Language definition to respects instead of custom congruence.

3 files changed, 57 insertions, 118 deletions

diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index 62acf8f..ef45432 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -10,6 +10,7 @@ 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
@@ -20,108 +21,65 @@ import Relation.Binary.Indexed.Heterogeneous as I
 open Setoid over using () renaming (Carrier to C)
 
 module _
-  {a aℓ b bℓ}
-  (A : Language a aℓ)
-  (B : Language b bℓ)
+  {a b}
+  (A : Language a)
+  (B : Language b)
   where
 
-  infix 4 _≈ᶜ_
-  infix 4 _∙_
+  module A = Language A
+  module B = Language B
 
-  Concat : List C → Set (c ⊔ a ⊔ b)
-  Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B ×  l₁ ++ l₂ ≡ l
+  infix 4 _∙_
 
-  _≈ᶜ_ : {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)
+  Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
+  Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≋ l
 
-  _∙_ : Language (c ⊔ a ⊔ b) (aℓ ⊔ bℓ)
+  _∙_ : Language (c ⊔ ℓ ⊔ 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)
+    { 𝕃 = Concat
+    ; ∈-resp-≋ = λ { l≋l′ (_ , l₁∈A , _ , l₂∈B , eq) → -, l₁∈A , -, l₂∈B , ≋-trans eq l≋l′
       }
     }
 
-isMonoid : ∀ {a aℓ} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)
+isMonoid : ∀ {a} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ 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}
+        { 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 , 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ˡ
+      { 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 = (λ 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 _
+  ; 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 ≡.≡-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₂
+  open import Relation.Binary.Reasoning.Setoid ≋-setoid
 
-∙-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
+∙-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
diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda
index b06be3d..ddea1a6 100644
--- a/src/Cfe/Language/Construct/Single.agda
+++ b/src/Cfe/Language/Construct/Single.agda
@@ -12,17 +12,16 @@ open Setoid over renaming (Carrier to C)
 
 open import Cfe.Language over hiding (_≈_)
 open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Product as Product
 open import Data.Unit
 open import Level
 
-｛_｝ : C → Language (c ⊔ ℓ) 0ℓ
+｛_｝ : C → Language (c ⊔ ℓ)
 ｛ c ｝ = record
-  { Carrier = λ l → ∃[ a ] (l ≡.≡ [ a ] × a ≈ c)
-  ; _≈_ = λ _ _ → ⊤
-  ; isEquivalence = record
-    { refl = tt
-    ; sym = λ _ → tt
-    ; trans = λ _ _ → tt
-    }
+  { 𝕃 = [ c ] ≋_
+  ; ∈-resp-≋ = λ l₁≋l₂ l₁∈｛c｝ → ≋-trans l₁∈｛c｝ l₁≋l₂
   }
+
+xy∉｛c｝ : ∀ c x y l → x ∷ y ∷ l ∉ ｛ c ｝
+xy∉｛c｝ c x y l (_ ∷ ())
diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda
index 5099d04..5e86124 100644
--- a/src/Cfe/Language/Construct/Union.agda
+++ b/src/Cfe/Language/Construct/Union.agda
@@ -19,33 +19,26 @@ open import Cfe.Language over as 𝕃 hiding (Lift)
 open Setoid over renaming (Carrier to C)
 
 module _
-  {a aℓ b bℓ}
-  (A : Language a aℓ)
-  (B : Language b bℓ)
+  {a b}
+  (A : Language a)
+  (B : Language b)
   where
 
-  infix 4 _≈ᵁ_
+  module A = Language A
+  module B = Language B
+
   infix 6 _∪_
 
   Union : List C → Set (a ⊔ b)
   Union l = l ∈ A ⊎ l ∈ B
 
-  data _≈ᵁ_ : {l₁ l₂ : List C} → REL (Union l₁) (Union l₂) (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where
-    A≈A : ∀ {l₁ l₂ x y} → ≈ᴸ A {l₁} {l₂} x y → (inj₁ x) ≈ᵁ (inj₁ y)
-    B≈B : ∀ {l₁ l₂ x y} → ≈ᴸ B {l₁} {l₂} x y → (inj₂ x) ≈ᵁ (inj₂ y)
-
-  _∪_ : Language (a ⊔ b) (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ)
+  _∪_ : Language (a ⊔ b)
   _∪_ = record
-    { Carrier = Union
-    ; _≈_ = _≈ᵁ_
-    ; isEquivalence = record
-      { refl = λ {_} {x} → case x return (λ x → x ≈ᵁ x) of λ { (inj₁ x) → A≈A (≈ᴸ-refl A) ; (inj₂ y) → B≈B (≈ᴸ-refl B)}
-      ; sym = λ { (A≈A x) → A≈A (≈ᴸ-sym A x) ; (B≈B x) → B≈B (≈ᴸ-sym B x)}
-      ; trans = λ { (A≈A x) (A≈A y) → A≈A (≈ᴸ-trans A x y) ; (B≈B x) (B≈B y) → B≈B (≈ᴸ-trans B x y) }
-      }
+    { 𝕃 = Union
+    ; ∈-resp-≋ = λ l₁≋l₂ → Sum.map (A.∈-resp-≋ l₁≋l₂) (B.∈-resp-≋ l₁≋l₂)
     }
 
-isCommutativeMonoid : ∀ {a aℓ} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a (c ⊔ a ⊔ aℓ) ∅)
+isCommutativeMonoid : ∀ {a} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a ∅)
 isCommutativeMonoid = record
   { isMonoid = record
     { isSemigroup = record
@@ -54,47 +47,36 @@ isCommutativeMonoid = record
         ; ∙-cong = λ X≈Y U≈V → record
           { f = Sum.map (_≈_.f X≈Y) (_≈_.f U≈V)
           ; f⁻¹ = Sum.map (_≈_.f⁻¹ X≈Y) (_≈_.f⁻¹ U≈V)
-          ; cong₁ = λ { (A≈A x) → A≈A (_≈_.cong₁ X≈Y x) ; (B≈B x) → B≈B (_≈_.cong₁ U≈V x) }
-          ; cong₂ = λ { (A≈A x) → A≈A (_≈_.cong₂ X≈Y x) ; (B≈B x) → B≈B (_≈_.cong₂ U≈V x) }
           }
         }
       ; assoc = λ A B C → record
         { f = Sum.assocʳ
         ; f⁻¹ = Sum.assocˡ
-        ; cong₁ = λ { (A≈A (A≈A x)) → A≈A x ; (A≈A (B≈B x)) → B≈B (A≈A x) ; (B≈B x) → B≈B (B≈B x) }
-        ; cong₂ = λ { (A≈A x) → A≈A (A≈A x) ; (B≈B (A≈A x)) → A≈A (B≈B x) ; (B≈B (B≈B x)) → B≈B x }
         }
       }
     ; identity = (λ A → record
       { f = λ { (inj₂ x) → x }
       ; f⁻¹ = inj₂
-      ; cong₁ = λ { (B≈B x) → x }
-      ; cong₂ = B≈B
       }) , (λ A → record
       { f = λ { (inj₁ x) → x }
       ; f⁻¹ = inj₁
-      ; cong₁ = λ { (A≈A x) → x }
-      ; cong₂ = A≈A
       })
     }
   ; comm = λ A B → record
     { f = Sum.swap
     ; f⁻¹ = Sum.swap
-    ; cong₁ = λ { (A≈A x) → B≈B x ; (B≈B x) → A≈A x }
-    ; cong₂ = λ { (A≈A x) → B≈B x ; (B≈B x) → A≈A x }
     }
   }
 
-∪-monotone : ∀ {a aℓ b bℓ} → _∪_ Preserves₂ _≤_ {a} {aℓ} ⟶ _≤_ {b} {bℓ} ⟶ _≤_
-∪-monotone X≤Y U≤V = record
+∪-mono : ∀ {a b} → _∪_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
+∪-mono X≤Y U≤V = record
   { f = Sum.map X≤Y.f U≤V.f
-  ; cong = λ { (A≈A l₁≈l₂) → A≈A (X≤Y.cong l₁≈l₂) ; (B≈B l₁≈l₂) → B≈B (U≤V.cong l₁≈l₂)}
   }
   where
   module X≤Y = _≤_ X≤Y
   module U≤V = _≤_ U≤V
 
-∪-unique : ∀ {a aℓ b bℓ} {A : Language a aℓ} {B : Language b bℓ} → (∀ x → first A x → first B x → ⊥) → (𝕃.null A → 𝕃.null B → ⊥) → ∀ {l} → l ∈ A ∪ B → (l ∈ A × l ∉ B) ⊎ (l ∉ A × l ∈ B)
+∪-unique : ∀ {a b} {A : Language a} {B : Language b} → (∀ x → first A x → first B x → ⊥) → (𝕃.null A → 𝕃.null B → ⊥) → ∀ {l} → l ∈ A ∪ B → (l ∈ A × l ∉ B) ⊎ (l ∉ A × l ∈ B)
 ∪-unique fA∩fB≡∅ ¬nA∨¬nB {[]}    (inj₁ []∈A) = inj₁ ([]∈A , ¬nA∨¬nB []∈A)
 ∪-unique fA∩fB≡∅ ¬nA∨¬nB {x ∷ l} (inj₁ xl∈A) = inj₁ (xl∈A , (λ xl∈B → fA∩fB≡∅ x (-, xl∈A) (-, xl∈B)))
 ∪-unique fA∩fB≡∅ ¬nA∨¬nB {[]}    (inj₂ []∈B) = inj₂ (flip ¬nA∨¬nB []∈B , []∈B)