Newer
Older
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
{-# OPTIONS --rewriting --guarded #-}
-- to allow opening this module in other files while there are still holes
{-# OPTIONS --allow-unsolved-metas #-}
module Semantics.GlobalBisim where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Nat hiding (_^_)
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Order.Poset
open import Cubical.HITs.PropositionalTruncation renaming (elim to PTelim ; rec to PTrec)
open import Common.Common
open import Common.Later
open import Common.LaterProperties
open import Common.ClockProperties
open import Semantics.Lift
open import Semantics.WeakBisimilarity
open import Semantics.GlobalLift
private
variable
ℓ ℓ' ℓR : Level
-- module WBSum {ℓ ℓR : Level} (X : Type ℓ) (R : X -> X -> Type ℓR) (k : Clock) = BisimSum k X R
module GlobalBisimSum (X : Type ℓ) (R : X -> X -> Type ℓR) where
-- open WBSum X R
--open module WBSum = BisimSum X R -- enaming (_≈_ to _≈S_)
--_≈[_]_ : {!L k X → (k : Clock) → L k X!}
--l ≈[ k ] l' = {!_≈_ k l l'!}
≈S : (k : Clock) → L k X → L k X → Type (ℓ-max ℓ ℓR)
≈S k = BisimSum._≈_ k X R
syntax ≈S k x y = x ≈[ k ] y
_≈g_ : L^gl X -> L^gl X -> Type (ℓ-max ℓ ℓR)
l1 ≈g l2 = ∀ k → (l1 k) ≈[ k ] (l2 k)
case1 : (l l' : L^gl X) -> Type (ℓ-max ℓ ℓR)
case1 l l' = Σ[ x ∈ X ] Σ[ y ∈ X ] (l ≡ ηL^gl x) × (l' ≡ ηL^gl y) × R x y
case2 : (l l' : L^gl X) -> Type (ℓ-max ℓ ℓR)
case2 l l' =
Σ[ x ∈ X ] ((l ≡ ηL^gl x)
× ∥ Σ[ n ∈ ℕ ] Σ[ y ∈ X ] ((l' ≡ (δL^gl ^ n) (ηL^gl y)) × R x y) ∥₁)
case3 : (l l' : L^gl X) -> Type (ℓ-max ℓ ℓR)
case3 l l' =
Σ[ y ∈ X ] ((l' ≡ ηL^gl y)
× ∥ Σ[ n ∈ ℕ ] Σ[ x ∈ X ] ((l ≡ (δL^gl ^ n) (ηL^gl x)) × R x y) ∥₁)
case4 : (l l' : L^gl X) -> Type (ℓ-max ℓ ℓR)
case4 l l' = Σ[ lx~ ∈ (∀ k -> ▹ k , L k X) ] Σ[ ly~ ∈ (∀ k -> ▹ k , (L^gl X)) ]
(l ≡ λ k → lx~ k {!!}) × (l' ≡ {!!}) × (▸ (λ t -> {!!}))
_≈g'_ : {!!}
l1 ≈g' l2 = {!!}
L^gl-R-iso : clock-irrel X -> (l l' : L^gl X) ->
Iso (l ≈g l') (case1 l l' ⊎ (case2 l l' ⊎ (case3 l l' ⊎ case4 l l')))
L^gl-R-iso X-irrel l l' =
(l ≈g l')
Iso⟨ {!!} ⟩
{!!} Iso⟨ {!!} ⟩ {!!}
(case1 l l' ⊎ (case2 l l' ⊎ (case3 l l' ⊎ case4 l l'))) ∎Iso