From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Thu, 19 Jan 2017 19:34:26 +0000 (+0300)
Subject: Replace context's constructors and add new theorems.
X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=d435954772cd531775f203c71c9753e68a527c85;p=jolie.agda.git

Replace context's constructors and add new theorems.
---

diff --git a/src/Type.agda b/src/Type.agda
index 153acd3..255f3e2 100644
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -2,7 +2,7 @@ module Type where
 
 open import Data.Nat using (ℕ)
 open import Data.String using (String)
-open import Data.Vec using (Vec) renaming (_∷_ to _∷-Vec_)
+open import Data.Vec using (Vec; _∷_)
 open import Variable
 
 
@@ -27,16 +27,16 @@ Ctx : ℕ → Set
 Ctx = Vec TypeDecl
 
 data Context : Set where
-  ◆ : ∀ {n} → Ctx n → Context
-  ■ : Context → Context → Context
+  ⋆ : ∀ {n} → Ctx n → Context
+  & : Context → Context → Context
 
 infix 4 _∈_
 
 data _∈_ : TypeDecl → Context → Set where
-  here-◆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ◆ (x ∷-Vec xs)
-  there-◆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ◆ xs) → x ∈ ◆ (y ∷-Vec xs)
-  here-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■  (◆ (x ∷-Vec xs)) (◆ ys)
-  here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
-  there-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ (◆ xs) (◆ ys)) → x ∈ ■ (◆ (x ∷-Vec xs)) (◆ ys)
-  there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ (◆ xs) (◆ ys)) → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
+  here-⋆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ⋆ (x ∷ xs)
+  there-⋆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ⋆ xs) → x ∈ ⋆ (y ∷ xs)
+  here-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ & (⋆ (x ∷ xs)) (⋆ ys)
+  here-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
+  there-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ (x ∷ xs)) (⋆ ys)
+  there-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
 
diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 4cab90f..f4c1915 100644
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -53,7 +53,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
         → Γ₁ ⊢B b1 ▹ Γ₁'
         → Γ₂ ⊢B b2 ▹ Γ₂'
         ------------------------------------
-        → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
+        → (& Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (& Γ₁' Γ₂')
 
   t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour}
         → Γ ⊢B b₁ ▹ Γ₁
@@ -69,22 +69,22 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                  → Γ ⊢B output (o at l [ var e ]) ▹ Γ
 
   t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
-               → ◆ Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
-               → ¬ (var x Tₓ ∈ ◆ Γ) -- x ∉ Γ
+               → ⋆ Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
+               → ¬ (var x Tₓ ∈ ⋆ Γ) -- x ∉ Γ
                ---------------------------------
-               → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ)
+               → ⋆ Γ ⊢B x ≃ e ▹ ⋆ (var x Tₑ ∷ Γ)
 
   t-assign-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m}  {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
-                    → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
-                    → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ
+                    → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
+                    → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) -- x ∉ Γ
                     -------------------------------------------------------
-                    → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ (var x Tₑ ∷ Γ)) (◆ Γ₁)
+                    → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ (var x Tₑ ∷ Γ)) (⋆ Γ₁)
 
   t-assign-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m}  {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
-                     → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
-                     → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ
+                     → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
+                     → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) -- x ∉ Γ
                      ------------------------------------------------------
-                     → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ Γ) (◆ (var x Tₑ ∷ Γ₁))
+                     → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ Γ) (⋆ (var x Tₑ ∷ Γ₁))
 
   t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e ∶ Tₑ
@@ -94,22 +94,22 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                   → Γ ⊢B x ≃ e ▹ Γ
 
   t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
-               → inOneWay o Tᵢ ∈ ◆ Γ
-               → ¬ (var x Tₓ ∈ ◆ Γ)
+               → inOneWay o Tᵢ ∈ ⋆ Γ
+               → ¬ (var x Tₓ ∈ ⋆ Γ)
                -------------------------------------------
-               → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
+               → ⋆ Γ ⊢B input (o [ x ]) ▹ ⋆ (var x Tᵢ ∷ Γ)
 
   t-oneway-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
-                    → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
-                    → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
+                    → inOneWay o Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
+                    → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
                     -----------------------------------------------------------------
-                    → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
+                    → & (⋆ Γ) (⋆ Γ₁) ⊢B input (o [ x ]) ▹ & (⋆ (var x Tᵢ ∷ Γ)) (⋆ Γ₁)
 
   t-oneway-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
-                     → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
-                     → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
+                     → inOneWay o Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
+                     → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
                      -----------------------------------------------------------------
-                     → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
+                     → & (⋆ Γ) (⋆ Γ₁) ⊢B input (o [ x ]) ▹ & (⋆ Γ) (⋆ (var x Tᵢ ∷ Γ₁))
 
   t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                   → inOneWay o Tᵢ ∈ Γ
@@ -119,25 +119,25 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                   → Γ ⊢B input (o [ x ]) ▹ Γ
 
   t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
-                → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
+                → outSolRes o l Tₒ Tᵢ ∈ ⋆ Γ
                 → Tₑ ⊆ Tₒ
-                → ¬ (var x Tₓ ∈ ◆ Γ)
+                → ¬ (var x Tₓ ∈ ⋆ Γ)
                 ------------------------------------------------------
-                → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
+                → ⋆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ⋆ (var x Tᵢ ∷ Γ)
 
   t-solresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
-                     → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
+                     → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
                      → Tₑ ⊆ Tₒ
-                     → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
+                     → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
                      ----------------------------------------------------------------------------
-                     → ■ (◆ Γ) (◆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
+                     → & (⋆ Γ) (⋆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ & (⋆ (var x Tᵢ ∷ Γ)) (⋆ Γ₁)
 
   t-solresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
-                      → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
+                      → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
                       → Tₑ ⊆ Tₒ
-                      → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
+                      → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
                       ----------------------------------------------------------------------------
-                      → ■ (◆ Γ) (◆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
+                      → & (⋆ Γ) (⋆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ & (⋆ Γ) (⋆ (var x Tᵢ ∷ Γ₁))
 
   t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                    → outSolRes o l Tₒ Tᵢ ∈ Γ
@@ -148,31 +148,31 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    → Γ ⊢B output (o at l [ e ][ x ]) ▹ Γ
 
   t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
-                → inReqRes o Tᵢ Tₒ ∈ ◆ Γ
-                → ¬ (var x Tₓ ∈ ◆ Γ)
-                → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
-                → var a Tₐ ∈ ◆ Γ₁
+                → inReqRes o Tᵢ Tₒ ∈ ⋆ Γ
+                → ¬ (var x Tₓ ∈ ⋆ Γ)
+                → ⋆ (var x Tₓ ∷ Γ) ⊢B b ▹ ⋆ Γ₁
+                → var a Tₐ ∈ ⋆ Γ₁
                 → Tₐ ⊆ Tₒ
                 --------------------------------------
-                → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
+                → ⋆ Γ ⊢B input (o [ x ][ a ] b) ▹ ⋆ Γ₁
 
   t-reqresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
-                     → inReqRes o Tᵢ Tₒ ∈ ■ (◆ Γ) (◆ Γ₁)
-                     → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
-                     → ■ (◆ (var x Tₓ ∷ Γ)) (◆ Γ₁) ⊢B b ▹ Γ₂
+                     → inReqRes o Tᵢ Tₒ ∈ & (⋆ Γ) (⋆ Γ₁)
+                     → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
+                     → & (⋆ (var x Tₓ ∷ Γ)) (⋆ Γ₁) ⊢B b ▹ Γ₂
                      → var a Tₐ ∈ Γ₂
                      → Tₐ ⊆ Tₒ
                      ------------------------------------
-                     → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
+                     → ⋆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
 
   t-reqresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
-                      → inReqRes o Tᵢ Tₒ ∈ ■ (◆ Γ) (◆ Γ₁)
-                      → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
-                      → ■ (◆ Γ) (◆ (var x Tₓ ∷ Γ₁)) ⊢B b ▹ Γ₂
+                      → inReqRes o Tᵢ Tₒ ∈ & (⋆ Γ) (⋆ Γ₁)
+                      → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
+                      → & (⋆ Γ) (⋆ (var x Tₓ ∷ Γ₁)) ⊢B b ▹ Γ₂
                       → var a Tₐ ∈ Γ₂
                       → Tₐ ⊆ Tₒ
                       ------------------------------------
-                      → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
+                      → ⋆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
 
   t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
                    → (inReqRes o Tᵢ Tₒ) ∈ Γ
@@ -185,22 +185,22 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
 
   t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
-             → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
-             → ¬ (var x Tₓ ∈ ◆ Γ)
+             → outSolRes o l Tₒ Tᵢ ∈ ⋆ Γ
+             → ¬ (var x Tₓ ∈ ⋆ Γ)
              ----------------------------------------
-             → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ)
+             → ⋆ Γ ⊢B wait r o l x ▹ ⋆ (var x Tᵢ ∷ Γ)
 
   t-wait-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
-                  → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
-                  → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
+                  → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
+                  → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
                   --------------------------------------------------------------
-                  → ■ (◆ Γ) (◆ Γ₁) ⊢B wait r o l x ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
+                  → & (⋆ Γ) (⋆ Γ₁) ⊢B wait r o l x ▹ & (⋆ (var x Tᵢ ∷ Γ)) (⋆ Γ₁)
 
   t-wait-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
-                   → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
-                   → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
+                   → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
+                   → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
                    --------------------------------------------------------------
-                   → ■ (◆ Γ) (◆ Γ₁) ⊢B wait r o l x ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
+                   → & (⋆ Γ) (⋆ Γ₁) ⊢B wait r o l x ▹ & (⋆ Γ) (⋆ (var x Tᵢ ∷ Γ₁))
 
   t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
                 → outSolRes o l Tₒ Tᵢ ∈ Γ
@@ -223,12 +223,22 @@ struct-congruence : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour}
                   → Γ ⊢B b₂ ▹ Γ₁
 struct-congruence t refl = t
 
+struct-cong-seq-nil : {Γ Γ₁ : Context} {b : Behaviour}
+                    → Γ ⊢B nil ∶ b ▹ Γ₁
+                    → Γ ⊢B b ▹ Γ₁
+struct-cong-seq-nil (t-seq t-nil x) = x
+
 struct-cong-par-nil : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b : Behaviour}
-                    → ■ Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ ■ Γ₁' Γ₂'
+                    → & Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ & Γ₁' Γ₂'
                     → Γ₁ ⊢B b ▹ Γ₁'
 struct-cong-par-nil (t-par x _) = x
 
 struct-cong-par-sym : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}
-                    → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂'
-                    → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁'
+                    → & Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ & Γ₁' Γ₂'
+                    → & Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ & Γ₂' Γ₁'
 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
+
+struct-cong-par-assoc : {Γ₁ Γ₂ Γ₃ Γ₁' Γ₂' Γ₃' : Context} {b₁ b₂ b₃ : Behaviour}
+                      → & (& Γ₁ Γ₂) Γ₃ ⊢B (b₁ ∥ b₂) ∥ b₃ ▹ & (& Γ₁' Γ₂') Γ₃'
+                      → & Γ₁ (& Γ₂ Γ₃) ⊢B b₁ ∥ (b₂ ∥ b₃) ▹ & Γ₁' (& Γ₂' Γ₃')
+struct-cong-par-assoc (t-par (t-par t1 t2) t3) = t-par t1 (t-par t2 t3)