some renaming and new definitions

agda/src/Monad/Instance/Setoids/Delay.lagda.md

@@ -84,6 +84,13 @@ module Bisimilarity (A : Setoid c (c ⊔ ℓ)) where
 
   open _∼′_ public
 
+  record _∼′′_ (x y : Delay′ ∣ A ∣) : Set (c ⊔ ℓ) where
+    coinductive
+
+    field
+      force∼′′ : force x ∼ force y
+  open _∼′′_ public
+
   -- strong bisimilarity of now and later leads to a clash
   now∼later : ∀ {ℓ'}{Z : Set ℓ'}{x : ∣ A ∣}{y : Delay′ ∣ A ∣} → now x ∼ later y → Z
   now∼later ()
@@ -190,14 +197,16 @@ module Bisimilarity (A : Setoid c (c ⊔ ℓ)) where
 
   open _≲′_ public
 
-open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_]; _≲_ to [_][_≲_]; _≲′_ to [_][_≲′_])
+open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _∼′′_ to [_][_∼′′_]; _↓_ to [_][_↓_]; _≲_ to [_][_≲_]; _≲′_ to [_][_≲′_])
 
 
 module DelayMonad where
   Delayₛ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
   Delayₛ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } }
-  Delayₛ' : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
+  Delayₛ∼ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
-  Delayₛ' A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }
+  Delayₛ∼ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }
+  Delayₛ∼′ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
+  Delayₛ∼′ A = record { Carrier = Delay′ ∣ A ∣ ; _≈_ = [_][_∼′′_] A ; isEquivalence = {!   !} }
   <_> = Π._⟨$⟩_
 
   ∼⇒≈ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ∼ y ] → [ A ][ x ≈ y ]
@@ -237,7 +246,7 @@ module DelayMonad where
   liftFₛ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delayₛ A ⟶ Delayₛ B
   liftFₛ {A} {B} f = record { _⟨$⟩_ = liftF < f > ; cong = lift-cong f }
 
-  liftFₛ∼ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delayₛ' A ⟶ Delayₛ' B
+  liftFₛ∼ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delayₛ∼ A ⟶ Delayₛ∼ B
   liftFₛ∼ {A} {B} f = record { _⟨$⟩_ = liftF < f > ; cong = ∼-cong }
     where
       ∼-cong : ∀ {x y} → [ A ][ x ∼ y ] → [ B ][ liftF < f > x ∼ liftF < f > y ]
@@ -336,11 +345,11 @@ module DelayMonad where
   μₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ (Delayₛ A) ⟶ Delayₛ A
   μₛ A = record { _⟨$⟩_ = μ {A} ; cong = μ-cong A }
 
-  μₛ∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ' (Delayₛ' A) ⟶ Delayₛ' A
+  μₛ∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ∼ (Delayₛ∼ A) ⟶ Delayₛ∼ A
   μₛ∼ A = record { _⟨$⟩_ = μ {A} ; cong = μ-cong∼ A }
     where
-      μ-cong∼ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ' A ][ x ∼ y ] → [ A ][ μ {A} x ∼ μ {A} y ]
+      μ-cong∼ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ∼ A ][ x ∼ y ] → [ A ][ μ {A} x ∼ μ {A} y ]
-      μ-cong∼′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ' A ][ x ∼′ y ] → [ A ][ μ {A} x ∼′ μ {A} y ]
+      μ-cong∼′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ∼ A ][ x ∼′ y ] → [ A ][ μ {A} x ∼′ μ {A} y ]
       force∼ (μ-cong∼′ A {x} {y} x∼y) = μ-cong∼ A (force∼ x∼y)
       μ-cong∼ A {.(now _)} {.(now _)} (now∼ x∼y) = x∼y
       μ-cong∼ A {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (μ-cong∼′ A x∼y)
@@ -470,7 +479,7 @@ module extra {A : Setoid c (c ⊔ ℓ)} where
   ι (x , zero)  = now x
   ι (x , suc n) = later (ι′ (x , n))
 
-  ιₛ' : A ×ₛ (ℕ-setoid {c}) ⟶ Delayₛ' A
+  ιₛ' : A ×ₛ (ℕ-setoid {c}) ⟶ Delayₛ∼ A
   ιₛ' = record { _⟨$⟩_ = ι ; cong = ι-cong }
     where
       ι-cong : ∀ {x y} → [ A ×ₛ (ℕ-setoid {c}) ][ x ≡ y ] → [ A ][ ι x ∼ ι y ]

agda/src/Monad/Instance/Setoids/K.lagda.md

@@ -168,28 +168,29 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
 
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
-  delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = ((B Elgot-Algebra.#) helper) ._⟨$⟩_ ; cong = helper#≈-cong } ; preserves = {!   !} }
+  delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = (helper #) ._⟨$⟩_ ; cong = helper#≈-cong } ; preserves = {!   !} }
     where
+    open Elgot-Algebra B using (_#)
     -- (f + id) ∘ out
     helper₁ : Delay ∣ A ∣ → ∣ ⟦ B ⟧ ∣ ⊎ Delay ∣ A ∣
     helper₁ (now x)   = inj₁ (< f > x)
     helper₁ (later x) = inj₂ (force x)
 
-    helper₁-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ helper₁ x ≡ helper₁ y ]
+    helper₁-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ helper₁ x ≡ helper₁ y ]
     helper₁-cong (now∼ x≡y)   = inj₁ (cong f x≡y)
     helper₁-cong (later∼ x≡y) = inj₂ (force∼ x≡y)
   
     -- -- setoid-morphism that preserves strong-bisimilarity
-    helper : Delayₛ' A ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ' A
+    helper : Delayₛ∼ A ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A
     helper = record { _⟨$⟩_ = helper₁ ; cong = helper₁-cong}
 
-    helper#∼-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper ⟨$⟩ x ≡ (B Elgot-Algebra.#) helper ⟨$⟩ y ]
+    helper#∼-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ][ helper # ⟨$⟩ x ≡ helper # ⟨$⟩ y ]
-    helper#∼-cong {x} {y} x∼y = cong ((B Elgot-Algebra.#) helper) x∼y
+    helper#∼-cong {x} {y} x∼y = cong (helper #) x∼y
 
-    helper#≈-cong : {x y : Delay ∣ A ∣} → (x≈y : [ A ][ x ≈ y ]) → [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper ⟨$⟩ x ≡ (B Elgot-Algebra.#) helper ⟨$⟩ y ]
+    helper#≈-cong : {x y : Delay ∣ A ∣} → (x≈y : [ A ][ x ≈ y ]) → [ ⟦ B ⟧ ][ helper # ⟨$⟩ x ≡ helper # ⟨$⟩ y ]
     
     -- key special case
-    helper#≈-cong' : {z : Delay (∣ A ∣ × ℕ)} → [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper ⟨$⟩ liftF proj₁ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ μ {A} (liftF (ι {A}) z) ]
+    helper#≈-cong' : {z : Delay (∣ A ∣ × ℕ)} → [ ⟦ B ⟧ ][ helper # ⟨$⟩ liftF proj₁ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z) ]
 
     helper#≈-cong x≈y =
       ≡-trans ⟦ B ⟧
@@ -209,7 +210,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
         outer : A ⟶ A ×ₛ ℕ-setoid {ℓ}
         outer = record { _⟨$⟩_ = λ z → z , zero ; cong = λ {x} {y} x≡y → x≡y , ≣-refl }
 
-        zero-helper : Delayₛ' A ⟶ Delayₛ' (A ×ₛ ℕ-setoid {ℓ})
+        zero-helper : Delayₛ∼ A ⟶ Delayₛ∼ (A ×ₛ ℕ-setoid {ℓ})
         zero-helper = liftFₛ∼ outer
 
         ι-cancel : ∀ {x} → [ A ][ (ι ∘′ (λ z → z , zero)) x ∼ now x ]
@@ -219,30 +220,60 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
         helper₁' (now (x , suc n)) = inj₂ (< zero-helper > (ι {A} (x , n)))
         helper₁' (later y)         = inj₂ (force y)
 
-        helper₁-cong' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ' (A ×ₛ ℕ-setoid) ][ helper₁' x ≡ helper₁' y ]
+        helper₁-cong' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper₁' x ≡ helper₁' y ]
         helper₁-cong' {now (x , zero)}  (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
         helper₁-cong' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (cong zero-helper (cong ιₛ' (x≡y , ≣-refl)))
         helper₁-cong' (later∼ x∼y) = inj₂ (force∼ x∼y)
 
-        helper' : Delayₛ' (A ×ₛ ℕ-setoid) ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ' (A ×ₛ ℕ-setoid)
+        helper' : Delayₛ∼ (A ×ₛ ℕ-setoid) ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)
         helper' = record { _⟨$⟩_ = helper₁' ; cong = helper₁-cong'}
 
-        -- Should follow by compositionality + fixpoint
+        -- an unfolding lemma for delay (on setoids)
-        eq₁ :  ∀ {z} → [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper' ⟨$⟩ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ liftF proj₁ z ]
-        eq₁ {now (x , n)} = {!    !}
-        eq₁ {later p} = {!   !}
 
-        eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
+        out : ∀ {X} → Delay X → X ⊎ Delay′ X
+        out {X} (now x) = inj₁ x
+        out {X} (later x) = inj₂ x
+
+        out⁻¹ : ∀ {X} → X ⊎ Delay′ X → Delay X
+        out⁻¹ {X} = [ now , later ]
+
+        out∼ : ∀ {X} → (Delayₛ∼ X) ⟶ (X ⊎ₛ (Delayₛ∼′ X))
+        out∼ {X} = record { _⟨$⟩_ = out {∣ X ∣} ; cong = out-cong }
+          where
+            out-cong : ∀ {x y} → [ X ][ x ∼ y ] → [ X ⊎ₛ (Delayₛ∼′ X) ][ out x ≡ out y ]
+            out-cong {.(now _)} {.(now _)} (now∼ x≡y) = inj₁ x≡y
+            out-cong {.(later _)} {.(later _)} (later∼ x∼y) = inj₂ (record { force∼′′ = force∼ x∼y })
+
+        out⁻¹∼ : ∀ {X} → X ⊎ₛ Delayₛ∼′ X ⟶ Delayₛ∼ X
+        out⁻¹∼ {X} = record { _⟨$⟩_ = out⁻¹ ; cong = out⁻¹-cong }
+          where
+            out⁻¹-cong : ∀ {x y} → [ X ⊎ₛ (Delayₛ∼′ X) ][ x ≡ y ] → [ X ][ out⁻¹ x ∼ out⁻¹ y ]
+            out⁻¹-cong {.(inj₁ _)} {.(inj₁ _)} (inj₁ x≡y) = now∼ x≡y
+            out⁻¹-cong {.(inj₂ _)} {.(inj₂ _)} (inj₂ x∼y) = later∼ (record { force∼ = force∼′′ x∼y })
+
+        -- TODO out∘out⁻¹≡id and out⁻¹∘out≡id
+
+        -- Should follow by compositionality + fixpoint
+        eq₁ : ∀ {z} → [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ liftF proj₁ z ]
+        eq₁ {x} = {!   !}
+          where
+            step₁ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ (< ([ inj₁ₛ , inj₂ₛ ∘ out∼ ]ₛ ∘ helper' ∘ out⁻¹∼) # > ∘′ out) z ]
+            step₁ = {!   !} -- should follow by uniformity
+
+            step₂ : [ ⟦ B ⟧ ][ (< ([ inj₁ₛ , inj₂ₛ ∘ out∼ ]ₛ ∘ helper' ∘ out⁻¹∼) # > ∘′ out) z ≡ helper # ⟨$⟩ liftF proj₁ z ]
+            step₂ = {!   !} -- ?
+
+        eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
         eq {now (x , n)} {now (y , .n)} (now∼ (x∼y , ≣-refl)) = eq'
           where
-            eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ]
+            eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ]
             eq' {zero}  = inj₁ (cong f x∼y)
-            eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ' A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
+            eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
         eq (later∼ x∼y) = inj₂ (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x∼y)))
 
         -- Should follow by uniformity
-        eq₂ : [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper' ⟨$⟩ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ μ {A} (liftF (ι {A}) z)]
+        eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)]
-        eq₂ = Elgot-Algebra.#-Uniformity B {Delayₛ' (A ×ₛ ℕ-setoid {ℓ})} {Delayₛ' A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} eq
+        eq₂ = Elgot-Algebra.#-Uniformity B {Delayₛ∼ (A ×ₛ ℕ-setoid {ℓ})} {Delayₛ∼ A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} eq
             (∼-refl (A ×ₛ ℕ-setoid))
 
   <<_>> = Elgot-Algebra-Morphism.h