Move Delay-related files to Semantics

formalizations/guarded-cubical/Results/Delay.agda → formalizations/guarded-cubical/Semantics/Delay.agda

@@ -9,14 +9,14 @@
 open import Common.Later
 open import Common.Common
 
-module Results.Delay where
+module Semantics.Delay where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Data.Sum
 open import Cubical.Data.Unit renaming (Unit to ⊤)
 open import Cubical.Data.Sigma
-open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_ ; _^_)
+open import Cubical.Data.Nat -- renaming (ℕ to Nat) hiding (_·_ ; _^_)
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Structure
 open import Cubical.Data.Empty as ⊥
@@ -26,7 +26,7 @@ open import Cubical.Relation.Binary.Poset
 
 import Cubical.Data.Equality as Eq
 
-open import Semantics.Predomains
+open import Semantics.Predomains hiding (ℕ)
 open import Semantics.StrongBisimulation
 open import Semantics.Lift
 
@@ -44,93 +44,121 @@ private
 record Delay (Res : Type ℓ) : Type ℓ
 
 data State (Res : Type ℓ) : Type ℓ where
-  done : Res -> State Res  -- should rename result to done
+  done : Res -> State Res
   running : Delay Res -> State Res
-  -- squash : isSet (State Res)
 
 record Delay Res where
   coinductive
   field view : State Res
 
-
 open Delay public
 
 
-delayUnit : State X → Delay X
-view (delayUnit s) = s
+fromState : State X → Delay X
+view (fromState s) = s
 
 -- The delay that returns the given value of type X in one step.
 doneD : X -> Delay X
-doneD x = delayUnit (done x)
+doneD x = fromState (done x)
 
 
 -- Given a delay d, returns the delay d' that takes runs for one step
 -- and then behaves as d.
 stepD : Delay X -> Delay X
-stepD d = delayUnit (running d)
-
-_↓_#_ : Delay X -> X -> Nat -> Type
-d ↓ x # n = {!!}
-
-
--- Given a delay d, return a function on nats n that,
--- when d ≡ running ^ n (done x), maps n to x and every other number to undefined
-toFun : Delay X -> (Nat -> (X ⊎ Unit))
-toFun d zero with view d
-... | done x = inl x
-... | running x = inr _
-toFun d (suc n) with view d
-... | done x = inr _
-... | running d' = toFun d' n
-
--- Given a function f on nats, return a delay that runs for n0 steps and returns x,
--- where n0 is the smallest nat such that f n0 = inl x
-fromFun : {X : Type ℓ} -> (Nat -> (X ⊎ Unit)) -> Delay X
-fromFun {X = X} f .view with f 0
-... | inl x = done x
-... | inr _ = running (fromFun (f ∘ suc))
-
-retrFun : (d : Delay X) -> fromFun (toFun d) ≡ d
-retrFun d i .view with d .view in eq
-... | done x = done x
-... | running d' = running (goal _ eq i)
-  where
-    goal : ∀ s -> s Eq.≡ running d' -> fromFun (toFun (delayUnit s) ∘ suc) ≡ d'
-    goal .(running d') Eq.refl = retrFun d'
-
-   
-isSetDelay : isSet X -> isSet (Delay X)
-isSetDelay H = isSetRetract toFun fromFun retrFun (isSetΠ λ _ -> isSet⊎ H isSetUnit)
-
-
-isSetDelay' : ∀ {ℓ : Level} -> {X : Type ℓ} → isSet X → isSet (Delay X)
-isSetDelay' {X = X} p = isSetRetract f g h (isSetΠ λ n → isSet⊎ p isSetUnit)
-    where
-      -- f : Delay X → (Nat → X ⊎ Unit)
-      -- f d zero with d .view
-      -- ... | done x = inl x
-      -- ... | running x = {!inr tt!}
-      -- f d (suc n) with d .view
-      -- ... | done x = inr tt
-      -- ... | running d' = f d' n
-      
-      f : Delay X → (Nat → X ⊎ Unit)
-      f d n with d .view
+stepD d = fromState (running d)
+
+
+-- An alternative definition of the Delay type using functions from natural numbers
+-- to X ⊎ Unit
+module Alternative (X : Type ℓ) where
+
+  -- Given a delay d, return a function on nats that, when d ≡ running ^ n (done x),
+  -- maps n to x and every other number to undefined.
+  fromDelay : Delay X → (ℕ → X ⊎ Unit)
+  fromDelay d n with d .view
 --      f d n       | done x  = inl x
-      f d zero    | done x = inl x
-      f d (suc n) | done x = inr tt
-      f d zero    | running _ = inr tt
-      f d (suc n) | running d' = f d' n
+  fromDelay d zero    | done x = inl x
+  fromDelay d (suc n) | done x = inr tt
+  fromDelay d zero    | running _ = inr tt
+  fromDelay d (suc n) | running d' = fromDelay d' n
+
+  -- Given a function f on nats, return a delay that runs for n0 steps and returns x,
+  -- where n0 is the smallest nat such that f n0 = inl x.
+  toDelay : (ℕ → X ⊎ Unit) → Delay X
+  toDelay f .view with f zero
+  ... | inl x  = done x
+  ... | inr tt = running (toDelay λ n → f (suc n))
+
+  retr : (d : Delay X) → toDelay (fromDelay d) ≡ d
+  retr d i .view with d .view
+  ... | done x  = done x
+  ... | running d' = running (retr d' i)
+
+
+  PreDelay' : Type ℓ
+  PreDelay' = ℕ -> (X ⊎ Unit)
+
+  Delay' : Type ℓ
+  Delay' = Σ[ f ∈ PreDelay' ] fromDelay (toDelay f) ≡ f
+
+  terminatesWith : PreDelay' -> X -> Type ℓ
+  terminatesWith d x = Σ[ n ∈ ℕ ] d n ≡ inl x
+
+  terminates : PreDelay' -> Type ℓ
+  terminates d = Σ[ n ∈ ℕ ] Σ[ x ∈ X ] d n ≡ inl x
+
+  -- We can characterize the functions f for which fromDelay (toDelay f) ≡ f
+  -- These are the functions that are defined at most once, i.e.,
+  -- if f n ≡ inl x and f m ≡ inl x', then n ≡ m
+
+
+  -- Iso with global lift
+
+  f' : (∀ k -> L k X) -> PreDelay'
+  f' y n with y k0
+  f' y zero    | η x = inl x
+  f' y (suc n) | η x = inr tt
+  f' y zero    | θ l~ = inr tt
+  f' y (suc n) | θ l~ = f' y n
+
+  f : (∀ k -> L k X) -> Delay'
+  f y = (f' y) , {!!}
+
+  g'' : (k : Clock) -> (▹ k , (Delay' -> L k X)) -> Delay' -> L k X
+  g'' k rec h with fst h zero
+  ... | inl x = η x
+  ... | inr tt = θ (λ t → rec t ((λ n -> fst h (suc n)) , {!!}))
+
+  g' : ∀ k -> Delay' -> L k X
+  g' k = fix (g'' k)
+
+  g : Delay' -> (∀ k -> L k X)
+  g h k = g' k h
+
+  sec' : (h : Delay') -> (k : Clock) ->
+    (▹ k , (f (λ k' -> g'' k' (next (g' k')) h) ≡ h)) ->
+           (f (λ k' -> g'' k' (next (g' k')) h) ≡ h)
+  sec' h k IH with fst h zero in eq
+  ... | inl x = Σ≡Prop {!!} aux
+    where
+      aux : f' (λ k' -> η x) ≡ h .fst
+      aux = funExt λ { zero → sym (Eq.eqToPath eq) ; (suc n) → {!!}}
+  ... | inr x = Σ≡Prop {!!} {!!}
+  
+
+  unfold-g' : {k : Clock} -> g' k ≡ g'' k (next (g' k))
+  unfold-g' {k} = fix-eq (g'' k)
+
+  sec : section f g
+  sec = {!!}
+
+
+isSetDelay : ∀ {ℓ : Level} -> {X : Type ℓ} → isSet X → isSet (Delay X)
+isSetDelay {X = X} p = isSetRetract fromDelay toDelay retr (isSetΠ λ n → isSet⊎ p isSetUnit)
+  where open Alternative X
+
 
-      g : (Nat → X ⊎ Unit) → Delay X
-      g f .view with f zero
-      ... | inl x  = done x
-      ... | inr tt = running (g λ n → f (suc n))
 
-      h : (d : Delay X) → g (f d) ≡ d
-      h d i .view with d .view
-      ... | done x  = done x
-      ... | running d' = running (h d' i)
 
 
 
@@ -184,121 +212,6 @@ result-inj {x = x} eq = cong′ (pred' x) eq
 
 
 
-{-
-module Isomorphism {X : Type} where
-
-  -- to : L℧F X -> Delay (Result (□ X))
-  -- to l = to' (Iso.fun L℧F-iso l)
-
-  to' : (((□ X) ⊎ ⊤) ⊎ (L℧F X)) -> Delay (Result (□ X))
-  view (to' (inl (inl x))) = done (value x)
-  view (to' (inl (inr tt))) = done error
-  view (to' (inr l')) = running (to' (inr l'))
-
-  to : L℧F X -> Delay (Result (□ X))
-  to l = to' (Iso.fun L℧F-iso l)
-
-  fro' : (k : Clock) -> ▹ k ,
-    (Delay (Result (□ X)) -> L℧ k X) ->
-    (Delay (Result (□ X)) -> L℧ k X)
-  fro' k rec m with (view m)
-  ... | done (value x) = η (x k)
-  ... | done error = ℧
-  ... | running m' = θ (λ t -> rec t m')
-
-  fro : Delay (Result (□ X)) -> L℧F X
-  fro d k = fix (fro' k) d
-
-  unfold-fro : (d : Delay (Result (□ X))) (k : Clock) ->
-    fro d k ≡ fro' k (next (λ d -> fro d k)) d
-  unfold-fro d k = let eq = fix-eq (fro' k) in
-    λ i -> eq i d
-
-
-  sec : section to fro
-  sec d = {!!}
-
-
-  retr' : (k : Clock) -> (l : L℧F X) -> ▹ k ,
-    (fro' k (next (λ d -> fro d k)) (to' (Iso.fun L℧F-iso l)) ≡ l k) ->
-    (fro' k (next (λ d -> fro d k)) (to' (Iso.fun L℧F-iso l)) ≡ l k)
-  retr' k l IH with (Iso.fun L℧F-iso l) in eq
-  ... | inl (inl x) = let eq' = L℧F-iso-η-inv l x {!!} in {!!}
-  ... | inl (inr tt) = let eq' = {!L℧F-iso-inv-℧!} in {!!}
-  ... | inr l' = {!!}
-
-  retr : retract to fro
-  retr l with (Iso.fun L℧F-iso l) in eq
-  ... | inl (inl x) = {!!}
-  ... | inl (inr tt) =
-    {!!} ≡⟨ funExt (λ k -> unfold-fro (to' (inl (inr tt))) k) ⟩
-    {!!} ≡⟨ {!!} ⟩ {!!}
-    l ∎ 
-  ... | inr l' = {!!} 
-
-
-
-module Isomorphism2 {X : Type} where
-
-  to' : (k : Clock) -> L℧ k X -> Delay (Result (□ X))
-  view (to' k (η x)) = done (value (λ k -> x))
-  view (to' k ℧) = done error
-  view (to' k (θ x)) = running (to' k (x ◇))
-
-  to : L℧F X -> Delay (Result (□ X))
-  to l = to' k0 (l k0)
-
-  
-
--- TODO should X have type Clock -> Type?
--- Then the correct iso would be
--- L℧F X ≅ Delay (∀ k -> X k)
-module Isom {X : Type} (H-irrel : clock-irrel X) where
-
-   X? = Result X
-
-   ∀-to-delay : (L℧F X) -> Delay (Result X)
-   view (∀-to-delay l) with (Iso.fun (L℧F-iso-irrel H-irrel) l)
-   ... | inl (inl x) = done (value x)
-   ... | inl (inr tt) = done error
-   ... | inr l' = running (∀-to-delay l')
-
-
-   delay-to-∀'' : (k : Clock) -> ▹ k , (Delay X? -> L℧ k X) -> (Delay X? -> L℧ k X)
-   delay-to-∀'' k rec m with (view m)
-   ... | done (value x) = η x
-   ... | done error = ℧
-   ... | running m' = θ (λ t → rec t m')
-
-   delay-to-∀' : (k : Clock) -> (Delay X?) -> L℧ k X
-   delay-to-∀' k = fix (delay-to-∀'' k)
-
-   unfold-d2∀ : (k : Clock) -> delay-to-∀' k ≡ delay-to-∀'' k (next (delay-to-∀' k))
-   unfold-d2∀ k = fix-eq (delay-to-∀'' k)
-
-   delay-to-∀ : Delay X? -> L℧F X
-   delay-to-∀ m k = fix (delay-to-∀'' k) m
-
-   sec : section ∀-to-delay delay-to-∀
-   sec b = {!!}
-
-   retr : retract ∀-to-delay delay-to-∀
-   retr l with (Iso.fun (L℧F-iso-irrel H-irrel) l)
-   ... | inl (inl x) = clock-ext (λ k → {!!})
-   ... | inl (inr _) = {!!}
-   ... | inr x = {!!}
-
-
-  -- Showing these are inverses requires a notion of equality for Delays,
-  -- which is the bisimilarity relation defined below.
-
--}
-
-
-
-
-
-
 module IsSet (X : Type) (isSetX : isSet X)  where
 
   X? : Type
@@ -376,138 +289,3 @@ module StrongBisim (X : Type) where -- (H-irrel : clock-irrel ⟨ X ⟩) where
   dec' {running x} {done x₁} (con ())
   dec' {running x} {running x₁} (con x₂) = cong running (dec x₂)
 
-
-  {-
-  iso1 : ∀ {m m'} -> (p : m ≈ m') -> enc (dec p) ≡ p
-  iso1' : ∀ {s s'} -> (p : s ≈'' s') -> enc' (dec' p) ≡ p
-  -}
-
-  {-
-  iso2 : ∀ {m m'} -> (p : m ≡ m') -> dec (enc p) ≡ p
-  iso2' : ∀ {s s'} -> (p : s ≡ s') -> dec' (enc' p) ≡ p
-
-  view (iso2 p i j) = iso2' (cong view p) i j
-  
-  iso2' {done x} {done y} p = λ i j → {!!}
-  iso2' {done x} {running d'} p = {!!}
-  iso2' {running d} {done y} p = {!!}
-  iso2' {running m} {running m'} p i j = {!!}
-  -}
-
-{-
-
-  bisim : ∀ {m m'} -> m ≈ m' -> m ≡ m'
-  bisim' : ∀ {m m'} -> m ≈' m' -> m ≡ m'
-
-  -- bisim' {result x} {result y} (con (xRy , yRx)) = cong result (antisym X x y xRy yRx)
-  bisim' {done x} {done y} (con p) = cong done p
-  bisim' {running m} {running m'} (con m≈m') = cong running (bisim m≈m')
-
-  view (bisim m≈m' i) = bisim' (prove m≈m') i
-
-  misib : ∀ {m m'} → m ≡ m' → m ≈ m'
-  misib' : ∀ {m m'} → m ≡ m' → m ≈' m'
-
-  misib' {done x} {done y} eq = con (result-inj eq)
-  misib' {running m} {running m'} p = con (misib (cong pred'' p))
-  misib' {done x} {running m} = result≠running {X}
-  misib' {running m} {done x} eq = result≠running {X} (sym eq)
-
-  prove (misib m≡m') = misib' (cong view m≡m')
-
-  iso1 : ∀ {m m'} -> (p : m ≈ m') -> misib (bisim p) ≡ p
-  iso1' : ∀ {s s'} -> (p : s ≈' s') -> misib' (bisim' p) ≡ p
-
-  iso1' {done x} {done y} (con p) = refl
-  iso1' {running m} {running m'} (con p) = cong con (iso1 p)
-
-  prove (iso1 p i) = iso1' (prove p) i
-
-
-  iso2 : ∀ {m m'} -> (p : m ≡ m') -> bisim (misib p) ≡ p
-  iso2' : ∀ {s s'} -> (p : s ≡ s') -> bisim' (misib' p) ≡ p
-
-  iso2' {running m} {running m'} p = {!!}
-  iso2' _ = {!!}
-
-  iso2 = {!!}
-
-
-module Evaluate {ℓ : Level} (X : Type ℓ) where
-
-  _↓_ : Delay X -> X -> Type ℓ
-  d ↓ x = X
-
-
-module WeakBisim {ℓ ℓ' : Level}
-  (X : Type ℓ) (Y : Type ℓ') (R : X -> Y -> Type (ℓ-max ℓ ℓ')) where
-  module EvX = Evaluate X
-  module EvY = Evaluate Y
-  _↓X_ = EvX._↓_
-  _↓Y_ = EvY._↓_
-
-   -- Coinductive lock-step bisimilarity on delays
-  record _≈_ (d : Delay X) (d' : Delay Y) : Type (ℓ-suc (ℓ-max ℓ ℓ'))
-
-  -- Bisimilarity on states
-  {- _≈''_ : State X -> State Y -> Type -}
-
-  -- Inductive type of proofs of bisimilarity
-  data _≈'_ : (s : State X) (s' : State Y) -> Type (ℓ-suc (ℓ-max ℓ ℓ'))
-   where
-    -- con : s ≈'' s' -> s ≈' s'
-    done-done : ∀ x y -> R x y -> done x ≈' done y
-    done-run : ∀ x y d' -> d' ↓Y y -> R x y -> done x ≈' running d'
-    run-done : ∀ x y d -> d ↓X x -> R x y -> running d ≈' done y
-    run-run : ∀ d d' -> d ≈ d' -> running d ≈' running d'
-
-  record _≈_ m m' where
-    coinductive
-    field prove : view m ≈' view m'
-
-
--- Ret and Ext for Delays
-ret-delay : {X : Type} -> X -> Delay X
-ret-delay = doneD
-
-ext-delay : {X Y : Type} -> (X -> Delay Y) -> Delay X -> Delay Y
-ext-state : {X Y : Type} -> (X -> State Y) -> State X -> State Y
-
-view (ext-delay f mx) = ext-state (view ∘ f) (view mx)
-
-ext-state f (done x) = f x
-ext-state f (running m) = running (ext-delay (delay ∘ f) m)
-
--}
-
-
-{-
-∀-to-delay : (L℧F X) -> (Delay (X ⊎ ⊤))
-view (∀-to-delay l) with (l k0)
-... | η x   = inl (inl x)  -- done (inl x) }
-... | ℧     = inl (inr tt) -- done (inr tt) }
-... | θ lx~ = inr (tt , (∀-to-delay l)) -- running }
-
-{-# TERMINATING #-}
-delay-to-∀ : Delay (X ⊎ ⊤) -> L℧F X
-delay-to-∀ m with (view m)
-... | inl (inl x) = λ k -> η x
-... | inl (inr tt) = λ k -> ℧
-... | inr (tt , m') = λ k -> θ λ t → delay-to-∀ m' k
-
-isom : {X : Type} -> Iso (L℧F X) (Delay (X ⊎ ⊤))
-isom {X} = iso ∀-to-delay delay-to-∀ sec retr
-  where
-    sec : section ∀-to-delay delay-to-∀
-    sec m with (view m)
-    ... | inl (inl x) = {!!}
-    ... | inl (inr tt) = {!!}
-    ... | inr (_ , m') = {!!}
-
-    retr : retract ∀-to-delay delay-to-∀
-    retr l with (l k0) in eq
-    ... | η x = clock-ext {!!}
-    ... | ℧ = clock-ext {!!}
-    ... | θ l~ = {!!}
-   
--}

formalizations/guarded-cubical/Results/DelayCoalgebra.agda → formalizations/guarded-cubical/Semantics/DelayCoalgebra.agda

@@ -2,7 +2,10 @@
 {-# OPTIONS --guardedness #-}
 {-# OPTIONS -W noUnsupportedIndexedMatch #-}
 
-module Results.DelayCoalgebra where
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Semantics.DelayCoalgebra where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
@@ -16,7 +19,7 @@ open import Cubical.Foundations.Isomorphism
 
 import Cubical.Data.Equality as Eq
 
-open import Results.Delay
+open import Semantics.Delay
 
 private
   variable
@@ -114,7 +117,7 @@ module _ (X : Type ℓ) (isSetX : isSet X)  where
   DelayCoalgFinal : {ℓc : Level} -> (c : Coalg ℓ) ->
     isContr (Σ[ h ∈ (c .V -> Delay X) ] unfold-delay ∘ h ≡ liftSum h ∘ c. un) -- isContr (CoalgMorphism c DelayCoalg)
   DelayCoalgFinal c =
-    (fun , (funExt commute)) , {!!}
+    (fun , (funExt commute)) , unique' (fun , (funExt commute))
     where
       
       fun : c .V -> Delay X
@@ -131,8 +134,8 @@ module _ (X : Type ℓ) (isSetX : isSet X)  where
       unique' : (s s' : Σ[ h ∈ (c .V → Delay X) ]
                     (unfold-delay ∘ (h) ≡ liftSum h ∘ (c .un))) ->
         s ≡ s'
-      unique' (h , com) (h' , com') = {!!}
-        -- Σ≡Prop (λ g -> isPropΠ (λ v -> {!!})) (funExt eq-fun)
+      unique' (h , com) (h' , com') =
+        Σ≡Prop (λ g -> isSetΠ (λ v -> isSet⊎ isSetX (isSetDelay isSetX)) _ _) (funExt eq-fun)
         where
           eq-fun : (v : c .V) -> h v ≡ h' v
           view (eq-fun v i) with c .un v in eq
@@ -168,47 +171,3 @@ module _ (X : Type ℓ) (isSetX : isSet X)  where
                 s1 ≡ s2
               goal .(running (h v')) .(running (h' v')) Eq.refl Eq.refl =
                 cong running (eq-fun v')
-
-             
-
-              
-
-
-{-
-      unique : (s : Σ[ h' ∈ (c .V → Delay X) ] (unfold-delay ∘ h' ≡ liftSum h' ∘ c .un)) →
-        (fun , funExt commute) ≡ s
-      unique (h' , com') = Σ≡Prop (λ g -> isSetΠ (λ v -> isSet⊎ isSetX (isSetDelay isSetX)) _ _) (funExt aux)
-        where
-          -- aux : (v : c .V) → fun v ≡ h' v
-          -- aux v with c .un v
-          -- ... | inl x = λ i -> {!!}
-          -- ... | inr x = {!!}
-
-          aux : (v : c .V) → fun v ≡ h' v
-          view (aux v i) with c. un v in eq
-          ... | inl x =
-            let com-v = funExtS⁻ com' v in
-            let eq' = lem1 (view (h' v)) x
-                        (com-v ∙ λ j -> liftSum h' (Eq.eqToPath eq j)) in
-            sym eq' i
-          ... | inr v' =
-            let com-v = funExtS⁻ com' v in
-            {-let eq' = lem2 (view (h' v)) (fun v')
-                        (com-v ∙ (λ j -> liftSum h' (Eq.eqToPath eq j)) ∙ cong inr (sym (aux v'))) in
-            sym eq' i -}
-            view (goal _ eq {!!})
-              where
-                goal : ∀ w -> w Eq.≡ inr v' -> (fun v') ≡ (h' v')
-                goal w Eq.refl = λ j -> (aux v' j) -- view (aux v')
--}
-
-  --  NTS: liftSum h' (c .un v) ≡ inr (fun v')
-  --  Have : c .un v Eq.≡ inr v'
-  --
-  --  Substituting, NTS:
-  --    liftSum h' (inr v') ≡ inr (fun v')
-  --  i.e.
-  --    inr (h' v') ≡ inr (fun v')
-  --  i.e.
-  --    h' v' ≡ fun v'
-