- commit
- d435954
- parent
- 07111ae
- author
- Eugene Akentyev
- date
- 2017-01-19 23:34:26 +0400 +04
Replace context's constructors and add new theorems.
2 files changed,
+72,
-62
+9,
-9
1@@ -2,7 +2,7 @@ module Type where
2
3 open import Data.Nat using (ℕ)
4 open import Data.String using (String)
5-open import Data.Vec using (Vec) renaming (_∷_ to _∷-Vec_)
6+open import Data.Vec using (Vec; _∷_)
7 open import Variable
8
9
10@@ -27,16 +27,16 @@ Ctx : ℕ → Set
11 Ctx = Vec TypeDecl
12
13 data Context : Set where
14- ◆ : ∀ {n} → Ctx n → Context
15- ■ : Context → Context → Context
16+ ⋆ : ∀ {n} → Ctx n → Context
17+ & : Context → Context → Context
18
19 infix 4 _∈_
20
21 data _∈_ : TypeDecl → Context → Set where
22- here-◆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ◆ (x ∷-Vec xs)
23- there-◆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ◆ xs) → x ∈ ◆ (y ∷-Vec xs)
24- here-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (◆ (x ∷-Vec xs)) (◆ ys)
25- here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
26- there-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ (◆ xs) (◆ ys)) → x ∈ ■ (◆ (x ∷-Vec xs)) (◆ ys)
27- there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ (◆ xs) (◆ ys)) → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
28+ here-⋆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ⋆ (x ∷ xs)
29+ there-⋆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ⋆ xs) → x ∈ ⋆ (y ∷ xs)
30+ here-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ & (⋆ (x ∷ xs)) (⋆ ys)
31+ here-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
32+ there-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ (x ∷ xs)) (⋆ ys)
33+ there-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
34
+63,
-53
1@@ -53,7 +53,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
2 → Γ₁ ⊢B b1 ▹ Γ₁'
3 → Γ₂ ⊢B b2 ▹ Γ₂'
4 ------------------------------------
5- → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
6+ → (& Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (& Γ₁' Γ₂')
7
8 t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour}
9 → Γ ⊢B b₁ ▹ Γ₁
10@@ -69,22 +69,22 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
11 → Γ ⊢B output (o at l [ var e ]) ▹ Γ
12
13 t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
14- → ◆ Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
15- → ¬ (var x Tₓ ∈ ◆ Γ) -- x ∉ Γ
16+ → ⋆ Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
17+ → ¬ (var x Tₓ ∈ ⋆ Γ) -- x ∉ Γ
18 ---------------------------------
19- → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ)
20+ → ⋆ Γ ⊢B x ≃ e ▹ ⋆ (var x Tₑ ∷ Γ)
21
22 t-assign-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
23- → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
24- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ
25+ → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
26+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) -- x ∉ Γ
27 -------------------------------------------------------
28- → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ (var x Tₑ ∷ Γ)) (◆ Γ₁)
29+ → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ (var x Tₑ ∷ Γ)) (⋆ Γ₁)
30
31 t-assign-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
32- → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
33- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ
34+ → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
35+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) -- x ∉ Γ
36 ------------------------------------------------------
37- → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ Γ) (◆ (var x Tₑ ∷ Γ₁))
38+ → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ Γ) (⋆ (var x Tₑ ∷ Γ₁))
39
40 t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
41 → Γ ⊢ₑ e ∶ Tₑ
42@@ -94,22 +94,22 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
43 → Γ ⊢B x ≃ e ▹ Γ
44
45 t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
46- → inOneWay o Tᵢ ∈ ◆ Γ
47- → ¬ (var x Tₓ ∈ ◆ Γ)
48+ → inOneWay o Tᵢ ∈ ⋆ Γ
49+ → ¬ (var x Tₓ ∈ ⋆ Γ)
50 -------------------------------------------
51- → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
52+ → ⋆ Γ ⊢B input (o [ x ]) ▹ ⋆ (var x Tᵢ ∷ Γ)
53
54 t-oneway-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
55- → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
56- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
57+ → inOneWay o Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
58+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
59 -----------------------------------------------------------------
60- → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
61+ → & (⋆ Γ) (⋆ Γ₁) ⊢B input (o [ x ]) ▹ & (⋆ (var x Tᵢ ∷ Γ)) (⋆ Γ₁)
62
63 t-oneway-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
64- → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
65- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
66+ → inOneWay o Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
67+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
68 -----------------------------------------------------------------
69- → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
70+ → & (⋆ Γ) (⋆ Γ₁) ⊢B input (o [ x ]) ▹ & (⋆ Γ) (⋆ (var x Tᵢ ∷ Γ₁))
71
72 t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
73 → inOneWay o Tᵢ ∈ Γ
74@@ -119,25 +119,25 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
75 → Γ ⊢B input (o [ x ]) ▹ Γ
76
77 t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
78- → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
79+ → outSolRes o l Tₒ Tᵢ ∈ ⋆ Γ
80 → Tₑ ⊆ Tₒ
81- → ¬ (var x Tₓ ∈ ◆ Γ)
82+ → ¬ (var x Tₓ ∈ ⋆ Γ)
83 ------------------------------------------------------
84- → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
85+ → ⋆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ⋆ (var x Tᵢ ∷ Γ)
86
87 t-solresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
88- → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
89+ → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
90 → Tₑ ⊆ Tₒ
91- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
92+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
93 ----------------------------------------------------------------------------
94- → ■ (◆ Γ) (◆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
95+ → & (⋆ Γ) (⋆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ & (⋆ (var x Tᵢ ∷ Γ)) (⋆ Γ₁)
96
97 t-solresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
98- → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
99+ → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
100 → Tₑ ⊆ Tₒ
101- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
102+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
103 ----------------------------------------------------------------------------
104- → ■ (◆ Γ) (◆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
105+ → & (⋆ Γ) (⋆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ & (⋆ Γ) (⋆ (var x Tᵢ ∷ Γ₁))
106
107 t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
108 → outSolRes o l Tₒ Tᵢ ∈ Γ
109@@ -148,31 +148,31 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
110 → Γ ⊢B output (o at l [ e ][ x ]) ▹ Γ
111
112 t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
113- → inReqRes o Tᵢ Tₒ ∈ ◆ Γ
114- → ¬ (var x Tₓ ∈ ◆ Γ)
115- → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
116- → var a Tₐ ∈ ◆ Γ₁
117+ → inReqRes o Tᵢ Tₒ ∈ ⋆ Γ
118+ → ¬ (var x Tₓ ∈ ⋆ Γ)
119+ → ⋆ (var x Tₓ ∷ Γ) ⊢B b ▹ ⋆ Γ₁
120+ → var a Tₐ ∈ ⋆ Γ₁
121 → Tₐ ⊆ Tₒ
122 --------------------------------------
123- → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
124+ → ⋆ Γ ⊢B input (o [ x ][ a ] b) ▹ ⋆ Γ₁
125
126 t-reqresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
127- → inReqRes o Tᵢ Tₒ ∈ ■ (◆ Γ) (◆ Γ₁)
128- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
129- → ■ (◆ (var x Tₓ ∷ Γ)) (◆ Γ₁) ⊢B b ▹ Γ₂
130+ → inReqRes o Tᵢ Tₒ ∈ & (⋆ Γ) (⋆ Γ₁)
131+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
132+ → & (⋆ (var x Tₓ ∷ Γ)) (⋆ Γ₁) ⊢B b ▹ Γ₂
133 → var a Tₐ ∈ Γ₂
134 → Tₐ ⊆ Tₒ
135 ------------------------------------
136- → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
137+ → ⋆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
138
139 t-reqresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
140- → inReqRes o Tᵢ Tₒ ∈ ■ (◆ Γ) (◆ Γ₁)
141- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
142- → ■ (◆ Γ) (◆ (var x Tₓ ∷ Γ₁)) ⊢B b ▹ Γ₂
143+ → inReqRes o Tᵢ Tₒ ∈ & (⋆ Γ) (⋆ Γ₁)
144+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
145+ → & (⋆ Γ) (⋆ (var x Tₓ ∷ Γ₁)) ⊢B b ▹ Γ₂
146 → var a Tₐ ∈ Γ₂
147 → Tₐ ⊆ Tₒ
148 ------------------------------------
149- → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
150+ → ⋆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
151
152 t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
153 → (inReqRes o Tᵢ Tₒ) ∈ Γ
154@@ -185,22 +185,22 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
155 → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
156
157 t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
158- → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
159- → ¬ (var x Tₓ ∈ ◆ Γ)
160+ → outSolRes o l Tₒ Tᵢ ∈ ⋆ Γ
161+ → ¬ (var x Tₓ ∈ ⋆ Γ)
162 ----------------------------------------
163- → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ)
164+ → ⋆ Γ ⊢B wait r o l x ▹ ⋆ (var x Tᵢ ∷ Γ)
165
166 t-wait-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
167- → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
168- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
169+ → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
170+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
171 --------------------------------------------------------------
172- → ■ (◆ Γ) (◆ Γ₁) ⊢B wait r o l x ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
173+ → & (⋆ Γ) (⋆ Γ₁) ⊢B wait r o l x ▹ & (⋆ (var x Tᵢ ∷ Γ)) (⋆ Γ₁)
174
175 t-wait-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
176- → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
177- → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
178+ → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
179+ → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
180 --------------------------------------------------------------
181- → ■ (◆ Γ) (◆ Γ₁) ⊢B wait r o l x ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
182+ → & (⋆ Γ) (⋆ Γ₁) ⊢B wait r o l x ▹ & (⋆ Γ) (⋆ (var x Tᵢ ∷ Γ₁))
183
184 t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
185 → outSolRes o l Tₒ Tᵢ ∈ Γ
186@@ -223,12 +223,22 @@ struct-congruence : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour}
187 → Γ ⊢B b₂ ▹ Γ₁
188 struct-congruence t refl = t
189
190+struct-cong-seq-nil : {Γ Γ₁ : Context} {b : Behaviour}
191+ → Γ ⊢B nil ∶ b ▹ Γ₁
192+ → Γ ⊢B b ▹ Γ₁
193+struct-cong-seq-nil (t-seq t-nil x) = x
194+
195 struct-cong-par-nil : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b : Behaviour}
196- → ■ Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ ■ Γ₁' Γ₂'
197+ → & Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ & Γ₁' Γ₂'
198 → Γ₁ ⊢B b ▹ Γ₁'
199 struct-cong-par-nil (t-par x _) = x
200
201 struct-cong-par-sym : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}
202- → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂'
203- → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁'
204+ → & Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ & Γ₁' Γ₂'
205+ → & Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ & Γ₂' Γ₁'
206 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
207+
208+struct-cong-par-assoc : {Γ₁ Γ₂ Γ₃ Γ₁' Γ₂' Γ₃' : Context} {b₁ b₂ b₃ : Behaviour}
209+ → & (& Γ₁ Γ₂) Γ₃ ⊢B (b₁ ∥ b₂) ∥ b₃ ▹ & (& Γ₁' Γ₂') Γ₃'
210+ → & Γ₁ (& Γ₂ Γ₃) ⊢B b₁ ∥ (b₂ ∥ b₃) ▹ & Γ₁' (& Γ₂' Γ₃')
211+struct-cong-par-assoc (t-par (t-par t1 t2) t3) = t-par t1 (t-par t2 t3)