Skip to content
Snippets Groups Projects
Commit 1d467b88 authored by Eric Giovannini's avatar Eric Giovannini
Browse files

move files related to coinductive Delay type

parent 15abb492
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
formalizations/guarded-cubical/Semantics/Delay.agda → formalizations/guarded-cubical/Semantics/Adequacy/Coinductive/Delay.agda
+ 176
− 0
View file @ 1d467b88
......@@ -9,7 +9,7 @@
open import Common.Later
open import Common.Common
module Semantics.Delay where
module Semantics.Adequacy.Coinductive.Delay where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
......@@ -22,16 +22,9 @@ open import Cubical.Foundations.Structure
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary
open import Cubical.Foundations.Path
open import Cubical.Relation.Binary.Poset
import Cubical.Data.Equality as Eq
open import Semantics.Predomains hiding (ℕ)
open import Semantics.StrongBisimulation
open import Semantics.Lift
open import Results.IntensionalAdequacy
open import Cubical.Foundations.HLevels
......@@ -54,6 +47,7 @@ record Delay Res where
open Delay public
-- Turn a State into a Delay.
fromState : State X → Delay X
view (fromState s) = s
......@@ -62,18 +56,18 @@ doneD : X -> Delay X
doneD x = fromState (done x)
-- Given a delay d, returns the delay d' that takes runs for one step
-- 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 = fromState (running d)
-- An alternative definition of the Delay type using functions from natural numbers
-- to X ⊎ Unit
-- to X ⊎ Unit that are defined at most once.
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.
-- Given a Delay d, return a function on nats that, when d ≡ running ^ n (done x),
-- maps n to inl x and every other number to inr tt.
fromDelay : Delay X → (ℕ → X ⊎ Unit)
fromDelay d n with d .view
-- f d n | done x = inl x
......@@ -101,6 +95,7 @@ module Alternative (X : Type ℓ) where
Delay' : Type ℓ
Delay' = Σ[ f ∈ PreDelay' ] fromDelay (toDelay f) ≡ f
terminatesWith : PreDelay' -> X -> Type ℓ
terminatesWith d x = Σ[ n ∈ ℕ ] d n ≡ inl x
......@@ -110,182 +105,72 @@ module Alternative (X : Type ℓ) where
-- 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
data Result (X : Type) : Type where
value : X -> Result X
error : Result X
ResToSum : Result X -> X ⊎ Unit
ResToSum (value x) = inl x
ResToSum error = inr tt
SumToRes : X ⊎ Unit -> Result X
SumToRes (inl x) = value x
SumToRes (inr tt) = error
result-retr : (x : Result X) → SumToRes (ResToSum x) ≡ x
result-retr (value x) = refl
result-retr error = refl
isSetResult : isSet X -> isSet (Result X)
isSetResult H = isSetRetract ResToSum SumToRes result-retr (isSet⊎ H isSetUnit)
_^? : Type -> Type
X ^? = Result X
diag : (Res Run : Type) -> State X -> Type₀
diag Res Run (done x) = Res
diag Res Run (running m) = Run
result≠running : {X : Type} -> ∀ {x : X} {m : Delay X} {ℓ} {Whatever : Type ℓ} →
done x ≡ running m → Whatever
result≠running eq = ⊥.rec (transport (cong (diag ⊤ ⊥) eq) tt)
-- used for showing that the result constructor is injective
pred' : X -> State X → X
pred' _ (done x) = x
pred' x (running m) = x
-- used for showing that the running constructor is injective
pred'' : State X -> Delay X
view (pred'' (done x)) = done x
pred'' (running m) = m
result-inj : {ℓ : Level} {X : Type ℓ} {x y : X} -> done x ≡ done y -> x ≡ y
result-inj {x = x} eq = cong′ (pred' x) eq
module IsSet (X : Type) (isSetX : isSet X) where
X? : Type
X? = Result X
≡-stable : {m m' : Delay X?} → Stable (m ≡ m')
≡'-stable : {s s' : State X?} → Stable (s ≡ s')
view (≡-stable ¬¬p i) = ≡'-stable (λ ¬p → ¬¬p (λ p → ¬p (cong view p))) i
-- This is needed for showing that terminatesWith is a Prop.
≡'-stable {done x} {done y} ¬¬p' =
cong′ done {!!}
≡'-stable {running m} {running m'} ¬¬p' =
cong′ running (≡-stable (λ ¬p -> ¬¬p' (λ p -> ¬p (cong pred'' p))))
≡'-stable {done x} {running m} ¬¬p' = ⊥.rec (¬¬p' (result≠running {X?}))
≡'-stable {running m} {done x} ¬¬p' = ⊥.rec (¬¬p' (λ p → result≠running {X?} (sym p)))
retrState : State X? -> X? ⊎ Delay X?
retrState (done x) = inl x
retrState (running d) = inr d
secState : X? ⊎ Delay X? -> State X?
secState (inl x) = done x
secState (inr d) = running d
fromDelay-def-atmost-once : (d : Delay X) (n m : ℕ) -> (x x' : X) ->
fromDelay d n ≡ inl x -> fromDelay d m ≡ inl x' -> n ≡ m
fromDelay-def-atmost-once d n m x x' eq1 eq2 with n | m | d .view
... | zero | zero | done x = refl
... | suc n' | suc m' | running d' =
cong suc (fromDelay-def-atmost-once d' n' m' x x' eq1 eq2)
-- Impossible cases
... | n | suc m' | done x = ⊥.rec (inl≠inr _ _ (sym eq2))
... | suc n' | m | done x = ⊥.rec (inl≠inr _ _ (sym eq1))
... | zero | m | running d' = ⊥.rec (inl≠inr _ _ (sym eq1))
... | n | zero | running d' = ⊥.rec (inl≠inr _ _ (sym eq2))
delay'-necessary : (f : Delay') -> (n m : ℕ) (x x' : X) ->
(fst f n ≡ inl x) -> (fst f m ≡ inl x') -> (n ≡ m)
delay'-necessary f n m x x' eq1 eq2 = fromDelay-def-atmost-once
(toDelay (fst f)) n m x x'
((λ i -> snd f i n) ∙ eq1) ((λ i -> snd f i m) ∙ eq2)
-- Can also formulate the converse implication (TODO)
delay'-sufficient : (f : PreDelay') ->
((n m : ℕ) (x x' : X) ->
(f n ≡ inl x) -> (f m ≡ inl x') -> (n ≡ m)) ->
fromDelay (toDelay f) ≡ f
delay'-sufficient f H = {!!}
-- Given a delay d, convert it to a function f using fromDelay,
-- satisfying the condition that fromDelay (toDelay f) ≡ f.
-- This condition is trivially satisfied since we have
-- fromDelay (toDelay (fromDelay d)) ≡ fromDelay d
-- (using the retraction property).
Delay→Fun : (d : Delay X) -> Delay'
fst (Delay→Fun d) = fromDelay d
snd (Delay→Fun d) = cong fromDelay (retr d)
isProp-terminatesWith : (d : Delay') (x : X) -> isProp (terminatesWith (fst d) x)
isProp-terminatesWith d x = {!!}
-- "Constructors" for Delay' corresponding to done and running
delayFunDone : (x : X) -> Delay'
delayFunDone x = {!!}
where
delayFunDone' : (x : X) -> PreDelay'
delayFunDone' x zero = inl x
delayFunDone' x (suc n) = inr tt
doneD-corresp : (x : X) -> fromDelay (doneD x) ≡ delayFunDone x .fst
doneD-corresp x = funExt (λ { zero → refl ; (suc n) → refl})
delayFunRunning : (d : PreDelay') -> PreDelay'
delayFunRunning d = {!!}
-- isSetState = isSetRetract retrState secState {!!} (isSet⊎ (isSetResult isSetX) isSetDelay)
-- Lock-step bisimilarity relation on Delays, but with no error ordering.
module StrongBisim (X : Type) where -- (H-irrel : clock-irrel ⟨ X ⟩) where
-- Mutually define coinductive bisimilarity of delays
-- along with the relation on states of a delay.
-- Coinductive lock-step bisimilarity on delays
record _≈_ (m m' : Delay X) : Type
-- Bisimilarity on states
_≈'_ : State X -> State X -> Type
done x ≈' done x' = x ≡ x' -- rel X x x' × rel X x' x
running m ≈' running m' = m ≈ m' -- using the coinductive bisimilarity on delays
_ ≈' _ = ⊥
data _≈''_ : State X -> State X -> Type where
con : {s s' : State X} -> (s ≈' s') -> (s ≈'' s')
record _≈_ m m' where
coinductive
field prove : view m ≈'' view m'
-- runningD-corresp : (d : Delay) -> fromDelay (runningD d)
open _≈_ public
enc : {d d' : Delay X} -> d ≡ d' -> d ≈ d'
enc' : {s s' : State X} -> s ≡ s' -> s ≈'' s'
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
enc {d} {d'} eq .prove = enc' (cong view eq)
enc' {done x} {done y} eq = con (result-inj eq)
enc' {done x} {running d'} eq = result≠running eq
enc' {running d} {done y} eq = result≠running (sym eq)
enc' {running d} {running d'} eq = con (enc (cong pred'' eq))
dec : {d d' : Delay X} -> d ≈ d' -> d ≡ d'
dec' : {s s' : State X} -> s ≈'' s' -> s ≡ s'
view (dec {d} {d'} eq i) = dec' (eq .prove) i
dec' {done x} {done x₁} (con p) = cong done p
dec' {done x} {running x₁} (con ())
dec' {running x} {done x₁} (con ())
dec' {running x} {running x₁} (con x₂) = cong running (dec x₂)
formalizations/guarded-cubical/Semantics/DelayCoalgebra.agda → formalizations/guarded-cubical/Semantics/Adequacy/Coinductive/DelayCoalgebra.agda
+ 11
− 26
View file @ 1d467b88
......@@ -5,7 +5,7 @@
-- to allow opening this module in other files while there are still holes
{-# OPTIONS --allow-unsolved-metas #-}
module Semantics.DelayCoalgebra where
module Semantics.Adequacy.Coinductive.DelayCoalgebra where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
......@@ -19,7 +19,8 @@ open import Cubical.Foundations.Isomorphism
import Cubical.Data.Equality as Eq
open import Semantics.Delay
open import Common.Common
open import Semantics.Adequacy.Coinductive.Delay
private
variable
......@@ -38,14 +39,7 @@ module _ (X : Type ℓ) (isSetX : isSet X) where
liftSum f (inr a) = inr (f a)
open Coalg
{-
record CoalgMorphism {ℓ1 ℓ2 : Level} (c : Coalg ℓ1) (d : Coalg ℓ2) :
Type (ℓ-max ℓ (ℓ-max ℓ1 ℓ2)) where
field
f : c .V -> d .V
com : d .un ∘ f ≡ liftSum f ∘ c .un
-}
CoalgMorphism : {ℓ1 ℓ2 : Level} (c : Coalg ℓ1) (d : Coalg ℓ2) ->
Type (ℓ-max (ℓ-max ℓ ℓ1) ℓ2)
......@@ -56,18 +50,6 @@ module _ (X : Type ℓ) (isSetX : isSet X) where
final-coalgebra : ∀ {ℓd : Level} -> Coalg ℓd ->
Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓd))
final-coalgebra {ℓd} d = ∀ (c : Coalg ℓd) -> isContr (CoalgMorphism c d)
-- Doesn't work: {ℓc : Level} -> (c : Coalg ℓc) -> isContr (CoalgMorphism c d)
inl≠inr : ∀ {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} ->
(a : A) (b : B) -> inl a ≡ inr b -> ⊥
inl≠inr {_} {_} {A} {B} a b eq = transport (cong (diagonal ⊤ ⊥) eq) tt
where
diagonal : (Left Right : Type) -> (A ⊎ B) -> Type
diagonal Left Right (inl a) = Left
diagonal Left Right (inr b) = Right
unfold-delay : Delay X -> X ⊎ Delay X
......@@ -105,7 +87,8 @@ module _ (X : Type ℓ) (isSetX : isSet X) where
unfold-inv2 : (d : Delay X) -> (d' : Delay X) ->
unfold-delay d ≡ inr d' -> d .view ≡ running d'
unfold-inv2 d d' H = cong view (isoFunInjective delay-iso-sum d (stepD d') H)
unfold-inv2 d d' H =
cong view (isoFunInjective delay-iso-sum d (stepD d') H)
......@@ -114,10 +97,11 @@ module _ (X : Type ℓ) (isSetX : isSet X) where
V = Delay X ;
un = unfold-delay }
DelayCoalgFinal : {ℓc : Level} -> (c : Coalg ℓ) ->
isContr (Σ[ h ∈ (c .V -> Delay X) ] unfold-delay ∘ h ≡ liftSum h ∘ c. un) -- isContr (CoalgMorphism c DelayCoalg)
DelayCoalgFinal : {ℓc : Level} ->
(c : Coalg ℓ) ->
isContr (CoalgMorphism c DelayCoalg) -- i.e. isContr (Σ[ h ∈ (c .V -> Delay X) ] unfold-delay ∘ h ≡ liftSum h ∘ c. un)
DelayCoalgFinal c =
(fun , (funExt commute)) , unique' (fun , (funExt commute))
(fun , (funExt commute)) , unique' (fun , funExt commute)
where
fun : c .V -> Delay X
......@@ -139,6 +123,7 @@ module _ (X : Type ℓ) (isSetX : isSet X) where
where
eq-fun : (v : c .V) -> h v ≡ h' v
view (eq-fun v i) with c .un v in eq
... | inl x = view (unfold-delay-inj (h v) (h' v) (com-v ∙ sym com'-v) i)
where
com-v : (unfold-delay (h v)) ≡ inl x
......
formalizations/guarded-cubical/Semantics/DelayErrorOrdering.agda → formalizations/guarded-cubical/Semantics/Adequacy/Coinductive/DelayErrorOrdering.agda
+ 157
− 0
View file @ 1d467b88
{-# OPTIONS --rewriting --guarded #-}
{-# OPTIONS --guardedness #-}
module Semantics.DelayErrorOrdering where
-- to allow opening this module in other files while there are still holes
{-# OPTIONS --allow-unsolved-metas #-}
module Semantics.Adequacy.Coinductive.DelayErrorOrdering where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.HLevels
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.Data.Sum
open import Cubical.Data.Unit renaming (Unit to ⊤ ; Unit* to ⊤*)
open import Cubical.Foundations.Structure
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Empty
open import Cubical.Relation.Binary
open import Semantics.Delay
open import Semantics.Adequacy.Coinductive.Delay
open import Common.Preorder.Base
open import Common.Preorder.Monotone
open import Cubical.Relation.Binary.Order.Poset
private
variable
ℓ ℓ' : Level
-- Lifting the relation on a preorder X to the relation on Delay' (X + 1)
module Ord (X : Preorder ℓ ℓ') where
-- Use propositional truncation (elimProp)
-- Lifting a Preorder X to a Preorder structure on (⟨ X ⟩ ⊎ ⊤)
module ResultPoset (X : Poset ℓ ℓ') where
open BinaryRelation
open Alternative (⟨ X ⟩ ⊎ ⊤)
-- Lifting the relation on X to an "error" relation on X ⊎ ⊤
module X = PosetStr (X .snd)
-- Lifting the relation on X to an "error" relation on X ⊎ ⊤
R-result : (⟨ X ⟩ ⊎ ⊤) -> (⟨ X ⟩ ⊎ ⊤) -> Type ℓ'
R-result (inl x) (inl y) = rel X x y
R-result (inl x) (inl y) = x X.≤ y
R-result (inl x) (inr tt) = ⊥* -- can't have a value be less than error
R-result (inr tt) y? = ⊤* -- error is the bottom element
R-result-refl : isRefl R-result
R-result-refl (inl x) = reflexive X x
R-result-refl (inl x) = X.is-refl x
R-result-refl (inr x) = _
R-result-trans : (x? y? z? : ⟨ X ⟩ ⊎ ⊤) -> R-result x? y? -> R-result y? z? -> R-result x? z?
R-result-trans (inr tt) y? z? x?≤y? y?≤z? = tt*
R-result-trans (inl x) (inl y) (inl z) x≤y y≤z = transitive X _ _ _ x≤y y≤z
R-result-trans (inl x) (inl y) (inl z) x≤y y≤z = X.is-trans _ _ _ x≤y y≤z
-- Agda can tell that the other cases are impossible!
R-result-antisym : (x? y? : ⟨ X ⟩ ⊎ ⊤) -> R-result x? y? -> R-result y? x? -> x? ≡ y?
R-result-antisym (inl x) (inl y) H1 H2 = cong inl {!!}
R-result-antisym (inr x) y? H1 H2 = {!!}
R-result-propValued : isPropValued R-result
R-result-propValued (inl x) (inl y) = X.is-prop-valued x y
R-result-propValued (inr tt) y? = isPropUnit*
-- Note that this is not the same as the usual preorder construction on sum types,
-- because there inr is related only to inr, whereas here error is related to everything.
ResultP : Poset ℓ ℓ'
ResultP = (⟨ X ⟩ ⊎ ⊤) , posetstr {!!} {!!}
{-preorderstr R-result
(ispreorder (isSet⊎ (IsPreorder.is-set X.isPreorder) isSetUnit)
R-result-propValued R-result-refl R-result-trans)
-}
-- Lifting the relation on a preorder X to the relation on Delay' (X + 1)
module Ord (X : Poset ℓ ℓ') where
open BinaryRelation
open Alternative (⟨ X ⟩ ⊎ ⊤) -- Definition of Delay as a function
open ResultPoset X -- Error ordering on results
-- private module X = PosetStr (X .snd)
_⊑'_ : PreDelay' -> PreDelay' -> Type (ℓ-max ℓ ℓ')
d ⊑' d' =
d ⊑' d' = ∥
-- If d terminates with a value x, then d' terminates with a related value y.
((x : ⟨ X ⟩) -> terminatesWith d (inl x) ->
Σ[ y ∈ ⟨ X ⟩ ] (terminatesWith d' (inl y) × (rel X x y))) ×
Σ[ y ∈ ⟨ X ⟩ ] (terminatesWith d' (inl y) × (x X.≤ y))) ×
-- If d' terminates with a result y?, then d terminates
-- with a related result x?.
((y? : ⟨ X ⟩ ⊎ ⊤) -> terminatesWith d' y? ->
Σ[ x? ∈ ⟨ X ⟩ ⊎ ⊤ ] (terminatesWith d x? × R-result x? y?))
Σ[ x? ∈ ⟨ X ⟩ ⊎ ⊤ ] (terminatesWith d x? × R-result x? y?)) ∥₁
-- Prop valued
⊑'-prop : (d d' : PreDelay') -> isProp (d ⊑' d')
⊑'-prop d d' = isPropPropTrunc
-- Reflexivity
⊑'-refl : (d : PreDelay') -> d ⊑' d
⊑'-refl d = ∣ aux ∣₁
where
aux : _ × _
aux .fst x d↓x = x , (d↓x , (X.is-refl _))
aux .snd y? d↓y? = y? , (d↓y? , R-result-refl y?)
{-
fst (⊑'-refl d) x d↓x = x , (d↓x , (reflexive X _))
snd (⊑'-refl d) y? d↓y? = y? , (d↓y? , R-result-refl y?)
-}
-- Transitivity
⊑'-trans : (d1 d2 d3 : PreDelay') -> d1 ⊑' d2 -> d2 ⊑' d3 -> d1 ⊑' d3
⊑'-trans d1 d2 d3 (d1≤d2-1 , d1≤d2-2) (d2≤d3-1 , d2≤d3-2) =
pt1 , pt2
⊑'-trans d1 d2 d3 H1 H2 = rec2 isPropPropTrunc aux H1 H2 where
aux : _
aux (d1≤d2-1 , d1≤d2-2) (d2≤d3-1 , d2≤d3-2) = ∣ pt1 , pt2 ∣₁
where
pt1 : (x1 : ⟨ X ⟩) →
terminatesWith d1 (inl x1) →
Σ-syntax ⟨ X ⟩ (λ y → terminatesWith d3 (inl y) × rel X x1 y)
Σ-syntax ⟨ X ⟩ (λ y → terminatesWith d3 (inl y) × x1 X.≤ y)
pt1 x1 d1↓x1 with d1≤d2-1 x1 d1↓x1
... | x2 , d2↓x2 , x1≤x2
with d2≤d3-1 x2 d2↓x2
... | x3 , d3↓x3 , x2≤x3 =
x3 , d3↓x3 , transitive X _ _ _ x1≤x2 x2≤x3
x3 , d3↓x3 , X.is-trans _ _ _ x1≤x2 x2≤x3
pt2 : (z? : ⟨ X ⟩ ⊎ ⊤) →
terminatesWith d3 z? →
......@@ -84,3 +139,19 @@ module Ord (X : Preorder ℓ ℓ') where
-- Now define the ordering on the original Delay type
_⊑_ : Delay (⟨ X ⟩ ⊎ ⊤) -> Delay (⟨ X ⟩ ⊎ ⊤) -> Type (ℓ-max ℓ ℓ')
d1 ⊑ d2 = fromDelay d1 ⊑' fromDelay d2
-- NTS: reflexive, transitive, prop-valued
-- This should follow becasue we have that Delay is a retract of
-- Delay'.
-- See pulledbackRel in Cubical.Relation.Binary.Properties
{-
-- Defining Delay as a Poset constructor, i.e., DelayP : Poset -> Poset
Delay℧P : Poset ℓ ℓ' -> Poset ℓ (ℓ-max ℓ ℓ')
Delay℧P X = (Delay (⟨ X ⟩ ⊎ ⊤)) , ?
where
open Ord X
module X = PosetStr (X .snd)
-}
formalizations/guarded-cubical/Semantics/Adequacy/Coinductive/DelayMonad.agda 0 → 100644
+ 268
− 0
View file @ 1d467b88
{-# OPTIONS --guardedness --rewriting --guarded #-}
-- to allow opening this module in other files while there are still holes
{-# OPTIONS --allow-unsolved-metas #-}
module Semantics.Adequacy.Coinductive.DelayMonad 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.Nat
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Monad.Base
open import Cubical.Categories.Instances.Sets
open import Cubical.Foundations.Structure
import Cubical.Data.Equality as Eq
open import Common.Preorder.Base
open import Semantics.Adequacy.Coinductive.Delay
open import Semantics.Adequacy.Coinductive.DelayErrorOrdering
private
variable
ℓ ℓ' : Level
-- ************************************
-- Utility functions
-- ************************************
private
S : Type ℓ -> Type ℓ
S X = State (X ⊎ ⊤)
T : Type ℓ -> Type ℓ
T X = Delay (X ⊎ ⊤)
-- DelayCod→StateCod
DFun→SFun : {Γ X Y : Type ℓ} -> (Γ -> X -> T Y) -> (Γ -> X -> S Y)
DFun→SFun f γ x = view (f γ x)
-- SFun→DFun
SFun→DFun : {Γ X Y : Type ℓ} -> (Γ -> X -> S Y) -> (Γ -> X -> T Y)
SFun→DFun f γ x = fromState (f γ x)
-- ************************************
-- Strong unit and bind
-- ************************************
unit-d : {X : Type ℓ} -> X -> T X
view (unit-d x) = done (inl x)
-- Unit of the strong monad
unitΓ-d : {Γ X : Type ℓ} -> Γ -> X -> T X
unitΓ-d γ x = unit-d x
unitΓ-s : {Γ X : Type ℓ} -> Γ -> X -> S X
unitΓ-s γ x = done (inl x)
strong-bind-d : ∀ {Γ X Y : Type ℓ} -> (Γ -> X -> T Y) -> (Γ -> T X -> T Y)
strong-bind-s : ∀ {Γ X Y : Type ℓ} -> (Γ -> X -> S Y) -> (Γ -> S X -> S Y)
strong-bind-s f γ (done (inl x)) = f γ x
strong-bind-s f γ (done (inr tt)) = done (inr tt)
strong-bind-s f γ (running d) =
running (strong-bind-d (λ γ' x' -> fromState (f γ' x')) γ d)
(strong-bind-d f γ d) .view = strong-bind-s (λ γ' x' -> view (f γ' x')) γ (view d)
{-
fromState-lem2 : ∀ {Γ X Y Z : Type ℓ} ->
(f : Γ -> Y -> State Z) -> (g : (Γ -> X -> State Y)) -> (γ : Γ) -> (x : X) ->
(fromState (strong-bind-s f γ (g γ x))) ≡ strong-bind-d (SFun→DFun f) γ (fromState (g γ x))
fromState-lem2 f g γ x i .view = strong-bind-s f γ (g γ x)
-}
-- ************************************
-- Properties
-- ************************************
-- Left unit
unitL-s : {Γ X : Type ℓ} -> (γ : Γ) -> (s : S X) ->
(strong-bind-s unitΓ-s) γ s ≡ s
unitL-d : {Γ X : Type ℓ} -> (γ : Γ) -> (d : T X) ->
(strong-bind-d unitΓ-d) γ d ≡ d
unitL-s γ (done (inl x)) = refl
unitL-s γ (done (inr tt)) = refl
unitL-s {Γ = Γ} γ (running d) i = running (goal _ (Eq.pathToEq fromState-lem) i)
-- cong running ((λ j -> strong-bind-d (fromState-lem j) γ d) ∙ unitL-d γ d)
where
fromState-lem : ∀ {Γ X : Type ℓ} -> (λ γ x -> fromState (unitΓ-s γ x)) ≡ unitΓ-d
fromState-lem {Γ = Γ} {X = X} = funExt λ γ -> funExt (λ x -> aux γ x)
where
aux : (γ : Γ) (x : X) -> fromState (unitΓ-s γ x) ≡ unitΓ-d γ x
aux γ x i .view = done (inl x)
goal : ∀ f -> f Eq.≡ unitΓ-d -> strong-bind-d f γ d ≡ d
goal .unitΓ-d Eq.refl = unitL-d γ d
-- NTS: strong-bind-d (λ γ' x' → fromState (unitΓ-s γ' x')) γ d ≡ d
unitL-d γ d i .view = unitL-s γ (view d) i
-- Right unit
unitR-s : {Γ X Y : Type ℓ} -> (f : Γ -> X -> S Y) -> (γ : Γ) -> (x : X) ->
strong-bind-s f γ (unitΓ-s γ x) ≡ f γ x
unitR-s f γ x = refl
unitR-d : {Γ X Y : Type ℓ} -> (f : Γ -> X -> T Y) -> (γ : Γ) -> (x : X) ->
strong-bind-d f γ (unitΓ-d γ x) ≡ f γ x
unitR-d f γ x i .view = unitR-s (λ γ' x' -> view (f γ' x')) γ x i
-- Composition
comp-s : {Γ X Y Z : Type ℓ} -> (f : Γ -> Y -> S Z) -> (g : (Γ -> X -> S Y)) ->
(γ : Γ) -> (x : X) -> (s : S X) ->
strong-bind-s f γ (strong-bind-s g γ s) ≡
strong-bind-s (λ γ' x' -> strong-bind-s f γ' (g γ' x')) γ s
comp-d : {Γ X Y Z : Type ℓ} -> (f : Γ -> Y -> T Z) -> (g : (Γ -> X -> T Y)) ->
(γ : Γ) -> (x : X) -> (d : T X) ->
strong-bind-d f γ (strong-bind-d g γ d) ≡
strong-bind-d (λ γ' x' -> strong-bind-d f γ' (g γ' x')) γ d
comp-s f g γ x (done (inl y)) = refl
comp-s f g γ x (done (inr tt)) = refl
comp-s {Γ = Γ} {X = X} {Z = Z} f g γ x (running d) i =
running (goal
(λ γ' x' -> fromState (strong-bind-s f γ' (g γ' x')))
(Eq.pathToEq (funExt (λ γ' -> funExt λ x' -> lem γ' x'))) i)
{- cong running (comp-d (SFun→DFun f) (SFun→DFun g) γ x d ∙
λ j -> strong-bind-d (λ γ' x' -> lem γ' x' j) γ d) -}
where
lem : ∀ γ' x' ->
fromState (strong-bind-s f γ' (g γ' x')) ≡
strong-bind-d (SFun→DFun f) γ' (SFun→DFun g γ' x')
(lem γ' x' i) .view = strong-bind-s f γ' (g γ' x')
goal : ∀ (f' : Γ -> X -> T Z) ->
f' Eq.≡ (λ γ' x' -> strong-bind-d (SFun→DFun f) γ' (SFun→DFun g γ' x')) ->
strong-bind-d (λ γ' x' -> fromState (f γ' x')) γ
(strong-bind-d (λ γ' x' -> fromState (g γ' x')) γ d) ≡
strong-bind-d f' γ d
goal .(λ γ' x' → strong-bind-d (SFun→DFun f) γ' (SFun→DFun g γ' x')) Eq.refl =
comp-d (SFun→DFun f) (SFun→DFun g) γ x d
{-
Know:
strong-bind-d (SFun→DFun f) γ (SFun→DFun g γ x) ≡
fromState (strong-bind-s f γ (g γ x))
Informally, we have the following chain of equalities:
strong-bind-d (λ γ' x' → fromState (f γ' x')) γ (strong-bind-d (λ γ' x' → fromState (g γ' x')) γ d) ≡ [by coind hyp]
strong-bind-d (λ γ' x' → strong-bind-d (SFun→DFun f) γ' (SFun→DFun g γ' x')) γ d ≡ [by lem]
^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^
strong-bind-d (λ γ' x' → fromState (strong-bind-s f γ' (g γ' x'))) γ d
^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^
-}
comp-d f g γ x d i .view = comp-s (DFun→SFun f) (DFun→SFun g) γ x (view d) i
-- ************************************
-- Monotonicity
-- ************************************
{-
-- The operations are monotone with respect to the ordering on Delay
module Monotone (X : Preorder ℓ ℓ') where
open ResultPreorder X -- Ordering on ⟨ X ⟩ ⊎ ⊤
open Ord X -- Ordering on Delay (⟨ X ⟩ ⊎ ⊤)
open Alternative (⟨ X ⟩ ⊎ ⊤) -- Function-based definition of Delay
fromDelay-unit : ∀ x? -> fromDelay (unit-d x?) zero ≡ {!!}
fromDelay-unit x? = refl
lem : ∀ x? y? -> terminatesWith (fromDelay (unit-d x?)) y? -> {!!}
lem x? y? (n , eq) = {!!}
unit-d-monotone : {Γ : Preorder ℓ ℓ'} -> {x y : ⟨ X ⟩} {γ : ⟨ Γ ⟩} ->
rel X x y -> (unitΓ-d γ x) ⊑ (unitΓ-d γ y)
unit-d-monotone x≤y = ∣ {!!} ∣₁
-- Need lemmas:
-- FromDelay (unit-d x?) terminates in zero steps.
--
-- If fromDelay (unit-d x?) n ≡ inl (inl x), then x? = inl x
-- More generally: If fromDelay (unit-d x?) ↓ y? , then x? ≡ y?
strong-bind-d-monotone : {Γ X Y : Preorder ℓ ℓ'} ->
{d d' : T ⟨ X ⟩} -> {γ γ' : ⟨ Γ ⟩} ->
{f : ⟨ Γ ⟩ -> (⟨ X ⟩) -> T (⟨ Y ⟩)} ->
rel Γ γ γ' ->
Ord._⊑_ X d d' ->
Ord._⊑_ Y (strong-bind-d f γ d) (strong-bind-d f γ d')
strong-bind-d-monotone {d = d} {d' = d'} {γ = γ} {γ' = γ'} {f = f}
γ≤γ' d≤d' with d .view | d' .view
... | done (inl x) | done (inl x₁) = {!!}
... | done (inl x) | done (inr x₁) = {!!}
... | done (inr x) | done (inl x₁) = {!!}
... | done (inr x) | done (inr x₁) = {!!}
... | done x | running x₁ = {!!}
... | running x | done x₁ = {!!}
... | running x | running x₁ = {!!}
-}
{-
-- Functor structure
mapState : {X Y : Type ℓ} -> (X -> Y) -> (State X -> State Y)
mapDelay : {X Y : Type ℓ} -> (X -> Y) -> (Delay X -> Delay Y)
mapState f (done x) = done (f x)
mapState f (running d') = running (mapDelay f d')
view (mapDelay f d) = mapState f (view d)
mapIdS : {X : Type ℓ} -> Path (State X -> State X) (mapState (λ x -> x)) (λ x -> x)
mapIdD : {X : Type ℓ} -> Path (Delay X -> Delay X) (mapDelay (λ x -> x)) (λ x -> x)
mapIdS i (done x) = done x
mapIdS i (running d) = running (mapIdD i d)
mapIdD i x .view = mapIdS i (x .view)
-- Monad on Set
DELAY : Monad (SET ℓ)
Functor.F-ob (fst DELAY) x = (Delay ⟨ x ⟩) , isSetDelay (x .snd)
Functor.F-hom (fst DELAY) = mapDelay
Functor.F-id (fst DELAY) = mapIdD
Functor.F-seq (fst DELAY) = {!!}
snd DELAY = {!!}
-}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment