Complete proofs up to Proposition 3.2 (excluding unrolling)

1 files changed, 78 insertions, 40 deletions

diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
index 62a946e..3a78bd8 100644
--- a/src/Cfe/Language/Indexed/Construct/Iterate.agda
+++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda
@@ -8,10 +8,10 @@ module Cfe.Language.Indexed.Construct.Iterate
 
 open Setoid over using () renaming (Carrier to C)
 
-open import Cfe.Language over
+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.Nat as ℕ hiding (_⊔_; _≤_)
 open import Data.Product as Product
 open import Function
 open import Level hiding (Lift) renaming (suc to lsuc)
@@ -24,47 +24,85 @@ iter : ∀ {a} {A : Set a} → (A → A) → ℕ → A → A
 iter f ℕ.zero = id
 iter f (ℕ.suc n) = f ∘ iter f n
 
-Iterate : ∀ {a aℓ} → (Language a aℓ → Language a aℓ) → IndexedLanguage 0ℓ 0ℓ a aℓ
-Iterate {a} {aℓ} f = record
-  { Carrierᵢ = ℕ
-  ; _≈ᵢ_ = ≡._≡_
-  ; isEquivalenceᵢ = ≡.isEquivalence
-  ; F = λ n → iter f n (Lift a aℓ ∅)
-  ; cong = λ {≡.refl → ≈-refl}
-  }
-
-≈ᵗ-refl : ∀ {a aℓ} →
-          (g : Language a aℓ → Language a aℓ) →
-          Reflexive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
-≈ᵗ-refl g {_} {n , _} = refl , (≈ᴸ-refl (Iter.F n))
+f-fn-x≡fn-f-x : ∀ {a} {A : Set a} (f : A → A) n x → f (iter f n x) ≡ iter 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
-  module Iter = IndexedLanguage (Iterate g)
 
-≈ᵗ-sym : ∀ {a aℓ} →
-         (g : Language a aℓ → Language a aℓ) →
-         Symmetric (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
-≈ᵗ-sym g {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) =
-  refl , (≈ᴸ-sym (Iter.F n) x∈Fn≈y∈Fn)
+  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 → iter f n x A.≈ iter 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
-  module Iter = IndexedLanguage (Iterate g)
 
-≈ᵗ-trans : ∀ {a aℓ} →
-          (g : Language a aℓ → Language a aℓ) →
-          Transitive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
-≈ᵗ-trans g {_} {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) (refl , y∈Fn≈z∈Fn) =
-  refl , (≈ᴸ-trans (Iter.F n) x∈Fn≈y∈Fn y∈Fn≈z∈Fn)
+  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 → iter f n x A′.≤ iter 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ℓ}
   where
-  module Iter = IndexedLanguage (Iterate g)
-
-⋃ : ∀ {a aℓ} → (Language a aℓ → Language a aℓ) → Language a aℓ
-⋃ f = record
-  { Carrier = Iter.Tagged
-  ; _≈_ = Iter._≈ᵗ_
-  ; isEquivalence = record
-    { refl = ≈ᵗ-refl f
-    ; sym = ≈ᵗ-sym f
-    ; trans = ≈ᵗ-trans f
+  Iterate : (Language a aℓ → Language a aℓ) → IndexedLanguage 0ℓ 0ℓ a aℓ
+  Iterate f = record
+    { Carrierᵢ = ℕ
+    ; _≈ᵢ_ = ≡._≡_
+    ; isEquivalenceᵢ = ≡.isEquivalence
+    ; F = λ n → iter f n (Lift a aℓ ∅)
+    ; cong = λ {≡.refl → ≈-refl}
+    }
+
+  ≈ᵗ-refl : (g : Language a aℓ → Language a aℓ) →
+            Reflexive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
+  ≈ᵗ-refl g {_} {n , _} = refl , (≈ᴸ-refl (Iter.F n))
+    where
+    module Iter = IndexedLanguage (Iterate g)
+
+  ≈ᵗ-sym : (g : Language a aℓ → Language a aℓ) →
+           Symmetric (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
+  ≈ᵗ-sym g {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) =
+    refl , (≈ᴸ-sym (Iter.F n) x∈Fn≈y∈Fn)
+    where
+    module Iter = IndexedLanguage (Iterate g)
+
+  ≈ᵗ-trans : (g : Language a aℓ → Language a aℓ) →
+             Transitive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
+  ≈ᵗ-trans g {_} {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) (refl , y∈Fn≈z∈Fn) =
+    refl , (≈ᴸ-trans (Iter.F n) x∈Fn≈y∈Fn y∈Fn≈z∈Fn)
+    where
+    module Iter = IndexedLanguage (Iterate g)
+
+  ⋃ : (Language a aℓ → Language a aℓ) → Language a aℓ
+  ⋃ f = record
+    { Carrier = Iter.Tagged
+    ; _≈_ = Iter._≈ᵗ_
+    ; isEquivalence = record
+      { refl = ≈ᵗ-refl f
+      ; sym = ≈ᵗ-sym f
+      ; trans = ≈ᵗ-trans f
+      }
+    }
+    where
+    module Iter = IndexedLanguage (Iterate f)
+
+  ⋃-cong : ∀ {f g : Language a aℓ → Language a aℓ} → (∀ {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 aℓ) f≈g n (Lift a aℓ ∅)) l∈fn}
+    ; f⁻¹ = λ { (n , l∈gn) → n , _≈_.f⁻¹ (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g n (Lift a aℓ ∅)) l∈gn}
+    ; cong₁ = λ {_} {_} {(i , _)} → λ { (refl , l₁≈l₂) → refl , _≈_.cong₁ (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g i (Lift a aℓ ∅)) l₁≈l₂}
+    ; cong₂ = λ {_} {_} {(i , _)} → λ { (refl , l₁≈l₂) → refl , _≈_.cong₂ (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g i (Lift a aℓ ∅)) l₁≈l₂}
+    }
+
+  ⋃-monotone : ∀ {f g : Language a aℓ → Language a aℓ} → (∀ {x y} → x ≤ y → f x ≤ g y) → ⋃ f ≤ ⋃ g
+  ⋃-monotone f≤g = record
+    { f = λ { (n , l∈fn) → n , _≤_.f (f≤g⇒fn≤gn (poset a aℓ) f≤g n (Lift a aℓ ∅)) l∈fn }
+    ; cong = λ {_} {_} {(i , _)} → λ { (refl , l₁≈l₂) → refl , _≤_.cong (f≤g⇒fn≤gn (poset a aℓ) f≤g i (Lift a aℓ ∅)) l₁≈l₂ }
     }
-  }
-  where
-  module Iter = IndexedLanguage (Iterate f)