blob: 0ae9100ee9a524dc67906a48510c5cd3c6d8f29b (
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
85
86
87
88
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary as B using (Setoid)
module Cfe.Language.Indexed.Construct.Iterate
{c ℓ} (over : Setoid c ℓ)
where
open Setoid over using () renaming (Carrier to C)
open import Algebra
open import Cfe.Language over as L
open import Cfe.Language.Indexed.Homogeneous over
open import Data.List
open import Data.Nat as ℕ hiding (_⊔_; _≤_; _^_)
open import Data.Product as Product
open import Function
open import Level hiding (Lift) renaming (suc to lsuc)
open import Relation.Binary.Indexed.Heterogeneous
open import Relation.Binary.PropositionalEquality as ≡
open IndexedLanguage
infix 9 _^_
_^_ : ∀ {a} {A : Set a} → Op₁ A → ℕ → Op₁ A
f ^ zero = id
f ^ (suc n) = f ∘ (f ^ n)
f-fn-x≡fn-f-x : ∀ {a} {A : Set a} (f : A → A) n x → f ((f ^ n) x) ≡ (f ^ n) (f x)
f-fn-x≡fn-f-x f ℕ.zero x = refl
f-fn-x≡fn-f-x f (suc n) x = ≡.cong f (f-fn-x≡fn-f-x f n x)
module _
{a aℓ} (A : B.Setoid a aℓ)
where
private
module A = B.Setoid A
f≈g⇒fn≈gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≈ y → f x A.≈ g y) → ∀ n x → (f ^ n) x A.≈ (g ^ n) x
f≈g⇒fn≈gn f≈g ℕ.zero x = A.refl
f≈g⇒fn≈gn f≈g (suc n) x = f≈g (f≈g⇒fn≈gn f≈g n x)
module _
{a aℓ₁ aℓ₂} (A : B.Poset a aℓ₁ aℓ₂)
where
private
module A = B.Poset A
f≤g⇒fn≤gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≤ y → f x A.≤ g y) → ∀ n x → (f ^ n) x A.≤ (g ^ n) x
f≤g⇒fn≤gn f≤g ℕ.zero x = A.refl
f≤g⇒fn≤gn f≤g (suc n) x = f≤g (f≤g⇒fn≤gn f≤g n x)
module _
{a}
where
Iterate : (Language a → Language a) → IndexedLanguage 0ℓ 0ℓ a
Iterate f = record
{ Carrierᵢ = ℕ
; _≈ᵢ_ = ≡._≡_
; isEquivalenceᵢ = ≡.isEquivalence
; F = λ n → (f ^ n) (Lift a ∅)
; cong = λ {≡.refl → ≈-refl}
}
⋃ : (Language a → Language a) → Language a
⋃ f = record
{ 𝕃 = Iter.Tagged
; ∈-resp-≋ = λ { l₁≋l₂ (i , l₁∈fi) → i , Language.∈-resp-≋ (Iter.F i) l₁≋l₂ l₁∈fi }
}
where
module Iter = IndexedLanguage (Iterate f)
fⁿ≤⋃f : ∀ f n → (f ^ n) (Lift a ∅) ≤ ⋃ f
fⁿ≤⋃f f n = record { f = n ,_ }
⋃-cong : ∀ {f g} → (∀ {x y} → x ≈ y → f x ≈ g y) → ⋃ f ≈ ⋃ g
⋃-cong f≈g = record
{ f = λ { (n , l∈fn) → n , _≈_.f (f≈g⇒fn≈gn (L.setoid a) f≈g n (Lift a ∅)) l∈fn}
; f⁻¹ = λ { (n , l∈gn) → n , _≈_.f⁻¹ (f≈g⇒fn≈gn (L.setoid a) f≈g n (Lift a ∅)) l∈gn}
}
⋃-mono : ∀ {f g} → (∀ {x y} → x ≤ y → f x ≤ g y) → ⋃ f ≤ ⋃ g
⋃-mono f≤g = record
{ f = λ { (n , l∈fn) → n , _≤_.f (f≤g⇒fn≤gn (poset a) f≤g n (Lift a ∅)) l∈fn }
}
|
