blob: 08651239e7f7b40c6dc6af8b90549ea24c9433c4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary
module Cfe.Language.Construct.Union
{c ℓ} (over : Setoid c ℓ)
where
open import Algebra
open import Data.Empty
open import Data.List
open import Data.List.Relation.Binary.Equality.Setoid over
open import Data.Product as Product
open import Data.Sum as Sum
open import Function
open import Level
open import Cfe.Language over as 𝕃 hiding (Lift)
open Setoid over renaming (Carrier to C)
module _
{a b}
(A : Language a)
(B : Language b)
where
private
module A = Language A
module B = Language B
infix 6 _∪_
Union : List C → Set (a ⊔ b)
Union l = l ∈ A ⊎ l ∈ B
_∪_ : Language (a ⊔ b)
_∪_ = record
{ 𝕃 = Union
; ∈-resp-≋ = λ l₁≋l₂ → Sum.map (A.∈-resp-≋ l₁≋l₂) (B.∈-resp-≋ l₁≋l₂)
}
isCommutativeMonoid : ∀ {a} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a ∅)
isCommutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = ≈-isEquivalence
; ∙-cong = λ X≈Y U≈V → record
{ f = Sum.map (_≈_.f X≈Y) (_≈_.f U≈V)
; f⁻¹ = Sum.map (_≈_.f⁻¹ X≈Y) (_≈_.f⁻¹ U≈V)
}
}
; assoc = λ A B C → record
{ f = Sum.assocʳ
; f⁻¹ = Sum.assocˡ
}
}
; identity = (λ A → record
{ f = λ { (inj₂ x) → x }
; f⁻¹ = inj₂
}) , (λ A → record
{ f = λ { (inj₁ x) → x }
; f⁻¹ = inj₁
})
}
; comm = λ A B → record
{ f = Sum.swap
; f⁻¹ = Sum.swap
}
}
∪-mono : ∀ {a b} → _∪_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
∪-mono X≤Y U≤V = record
{ f = Sum.map X≤Y.f U≤V.f
}
where
module X≤Y = _≤_ X≤Y
module U≤V = _≤_ U≤V
∪-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)
∪-unique fA∩fB≡∅ ¬nA∨¬nB {x ∷ l} (inj₂ xl∈B) = inj₂ ((λ xl∈A → fA∩fB≡∅ x (-, xl∈A) (-, xl∈B)) , xl∈B)
|
