From iris.proofmode Require Import base tactics classes.
From cgraphs.multiparty Require Export mutil.
From cgraphs.cgraphs Require Export util.
Definition session := nat. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=831235f9 *)
Definition participant := nat.
Definition endpoint := (session * participant)%type. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8a74f532 *)
(* ====================== *)
(* VALUES AND EXPRESSIONS *)
(* ====================== *)
Inductive val := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5a61b459 *)
| UnitV : val
| NatV : nat -> val
| PairV : val -> val -> val (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ae93847f *)
| InjV : bool -> val -> val (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f9cd562b *)
| InjNV : nat -> val -> val (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1c2c5e5d *)
| FunV : string -> expr -> val (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4698bf5a *)
| UFunV : string -> expr -> val (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1327f054 *)
| ChanV : endpoint -> (participant -> participant) -> val
with expr := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bfe44a27 *)
| Val : val -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=31a254e6 *)
| Var : string -> expr
| Pair : expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d97090d5 *)
| Inj : bool -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=95c30cc5 *)
| InjN : nat -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=671f65e3 *)
| App : expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6f23d4fd *)
| UApp : expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c0053564 *)
| Lam : string -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bedce7e8 *)
| ULam : string -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e50a8751 *)
| Send : participant -> expr -> nat -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c08ea362 *)
| Recv : participant -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b73fb057 *)
| Let : string -> expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d1341b4f *)
| LetUnit : expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2069579a *)
| LetProd : string -> string -> expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f50a2863 *)
| MatchVoid : expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2fbb0a41 *)
| MatchSum : expr -> string -> expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e3eeb024 *)
| MatchSumN n : expr -> (fin n -> expr) -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=07855502 *)
| If : expr -> expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=40586ad9 *)
| Spawn n : (fin n -> expr) -> expr
| Close : expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e6e85604 *)
| Relabel : (participant -> participant) -> expr -> expr. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=403332c4 *)
(* ===================== *)
(* OPERATIONAL SEMANTICS *)
(* ===================== *)
(* Our operational semantics uses substitution for variables *)
Fixpoint subst (x:string) (a:val) (e:expr) : expr := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c8b27361 *)
match e with
| Val _ => e
| Var x' => if decide (x = x') then Val a else e
| App e1 e2 => App (subst x a e1) (subst x a e2)
| Inj b e1 => Inj b (subst x a e1)
| Pair e1 e2 => Pair (subst x a e1) (subst x a e2)
| UApp e1 e2 => UApp (subst x a e1) (subst x a e2)
| Lam x' e1 => if decide (x = x') then e else Lam x' (subst x a e1)
| ULam x' e1 => if decide (x = x') then e else ULam x' (subst x a e1)
| Send p e1 i e2 => Send p (subst x a e1) i (subst x a e2)
| Recv p e1 => Recv p (subst x a e1)
| Let x' e1 e2 => Let x' (subst x a e1) (if decide (x = x') then e2 else subst x a e2)
| LetUnit e1 e2 => LetUnit (subst x a e1) (subst x a e2)
| LetProd x' y' e1 e2 =>
LetProd x' y' (subst x a e1) (if decide (x = x' ∨ x = y') then e2 else subst x a e2)
| MatchVoid e1 => MatchVoid (subst x a e1)
| MatchSum e1 x' eL eR =>
MatchSum (subst x a e1) x'
(if decide (x = x') then eL else subst x a eL)
(if decide (x = x') then eR else subst x a eR)
| InjN n e => InjN n (subst x a e)
| MatchSumN n e f => MatchSumN n (subst x a e) (λ i, subst x a (f i))
| If e1 e2 e3 => If (subst x a e1) (subst x a e2) (subst x a e3)
| Spawn ps f => Spawn ps (λ p, subst x a (f p))
| Close e1 => Close (subst x a e1)
| Relabel π e1 => Relabel π (subst x a e1)
end.
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=04de6946 *)
Inductive pure_step : expr -> expr -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=411f0d97 *)
| Pair_step : ∀ v1 v2, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=3b105acc *)
pure_step (Pair (Val v1) (Val v2)) (Val (PairV v1 v2)) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a1f5e7c4 *)
| Inj_step : ∀ v1 b, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a4bf5ceb *)
pure_step (Inj b (Val v1)) (Val (InjV b v1)) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=47939b6a *)
| App_step : ∀ x e a, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=89c51d22 *)
pure_step (App (Val (FunV x e)) (Val a)) (subst x a e) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=78bfe13e *)
| UApp_step : ∀ x e a, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c1eb1d58 *)
pure_step (UApp (Val (UFunV x e)) (Val a)) (subst x a e) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=95cad737 *)
| Lam_step : ∀ x e, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ec87986b *)
pure_step (Lam x e) (Val (FunV x e)) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a836c988 *)
| ULam_step : ∀ x e, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=253c7b48 *)
pure_step (ULam x e) (Val (UFunV x e)) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f2a704d3 *)
| If_step1 : ∀ n e1 e2,
n ≠ 0 ->
pure_step (If (Val (NatV n)) e1 e2) e1 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=06219868 *)
| If_step2 : ∀ e1 e2,
pure_step (If (Val (NatV 0)) e1 e2) e2 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d8985337 *)
| MatchSum_step : ∀ x v eL eR b, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=39aea32e *)
pure_step (MatchSum (Val (InjV b v)) x eL eR) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=cf8ead27 *)
(if b then subst x v eL else subst x v eR)
| InjN_step : ∀ n v, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b6aef92c *)
pure_step (InjN n (Val v)) (Val (InjNV n v)) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7a13f320 *)
| MatchSumN_step : ∀ n i v f, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7d55e26a *)
pure_step (MatchSumN n (Val (InjNV (fin_to_nat i) v)) f) (App (f i) (Val v)) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=52a7dd14 *)
| Let_step : ∀ x v e, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=3ce82401 *)
pure_step (Let x (Val v) e) (subst x v e) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=cbda3ed0 *)
| LetUnit_step : ∀ e, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8cc96606 *)
pure_step (LetUnit (Val UnitV) e) e (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1a12bb0e *)
| LetProd_step : ∀ x1 x2 v1 v2 e, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=97de0abc *)
pure_step (LetProd x1 x2 (Val (PairV v1 v2)) e) (subst x1 v1 $ subst x2 v2 e) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4ae5757d *)
| Relabel_step : ∀ π1 π2 c p, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=77d19a12 *)
pure_step (Relabel π1 (Val (ChanV (c,p) π2))) (Val (ChanV (c,p) (π2 ∘ π1))). (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=786dfef7 *)
(* Each multiparty channel has NxN buffers if there are N participants *)
(* We represent this as a nested finite map (gmap). *)
(* Each entry of the buffer stores a natural number,
indicating the branch chosen in the protocol,
and a payload message of type val. *) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f4f8f26a *)
Definition entryT := (nat * val)%type.
Notation bufsT A B V := (gmap B (gmap A (list V))).
Definition heap := bufsT participant endpoint entryT. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=55ea1ed0 *)
(* Pushing and popping of the buffer (p,q) for communicating from p to q. *)
Definition push `{Countable A, Countable B} {V} (p : A) (q : B) (x : V) (bufss : bufsT A B V) : bufsT A B V :=
alter (alter (λ buf, buf ++ [x]) p) q bufss.
Definition pop `{Countable A, Countable B} {V} (p : A) (q : B) (bufss : bufsT A B V) : option (V * bufsT A B V) :=
match bufss !! q with
| Some bufs =>
match bufs !! p with
| Some (v :: buf) => Some (v, <[ q := <[ p := buf ]> bufs ]> bufss)
| _ => None
end
| None => None
end.
(* We start with NxN empty buffers for N participants. *)
Definition init_chans {A} n : bufsT participant participant A :=
fin_gmap n (λ i, fin_gmap n (λ j, [])).
(* Initialization of the threads spawned by an N-ary fork. *)
Definition init_threads (c : session) (n : nat) (fv : fin n -> val) : list expr := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=42eb660a *)
fin_list n (λ i, App (Val (fv i)) (Val (ChanV (c, S (fin_to_nat i)) id))).
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0b3dea50 *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d9fe387d *)
Inductive head_step : expr -> heap -> expr -> heap -> list expr -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e3f6a221 *)
| Pure_step : ∀ e e' h, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=83315502 *)
pure_step e e' -> head_step e h e' h [] (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0c71ad99 *)
| Send_step : ∀ h c p q y i π, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b8dde2d4 *)
(* send puts the value in the bufs of the other *)
(* since we are participant p, we put it in that buffer *)
head_step (Send q (Val (ChanV (c,p) π)) i (Val y)) h (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=349dfc8c *)
(Val (ChanV (c,p) π)) (* Return the continuation channel *)
(push p (c,π q) (i,y) h) (* Push value onto the right buffer *)
[] (* no new threads spawned *)
| Recv_step : ∀ h c p q i y h' π, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8a28eae0 *)
pop (π p) (c,q) h = Some ((i,y), h') -> (* If there is a value in the buffer *)
head_step (Recv p (Val (ChanV (c,q) π))) h (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=dfabb166 *)
(Val (InjNV i (PairV (ChanV (c,q) π) y))) (* Return the message and continuation channel *)
h' (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=33bfef0d *)
[] (* no new threads spawned *)
| Close_step : ∀ c p h π, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0b255115 *)
head_step (Close (Val (ChanV (c,p) π))) h (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=cb662d06 *)
(Val UnitV) (* return value of the close call *)
(delete (c,p) h) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=70fe161c *)
[] (* no new threads spawned *)
| Spawn_step : ∀ (h : heap) c n f fv, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6bf28208 *)
(∀ p, h !! (c,p) = None) -> (* We must select fresh locations for the buffers *)
(∀ p, f p = Val (fv p)) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=607e5e35 *)
head_step
(Spawn n f) h
(Val (ChanV (c, 0) id)) (* The return value of the spawn call *)
(gmap_unslice (init_chans (S n)) c ∪ h) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=170e4c90 *)
(init_threads c n fv). (* The newly spawned threads *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2c2d82e7 *)
inside a nested expression. *)
Inductive ctx1 : (expr -> expr) -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d9522c3b *)
| Ctx_App_l e : ctx1 (λ x, App x e)
| Ctx_App_r v : ctx1 (λ x, App (Val v) x)
| Ctx_Pair_l e : ctx1 (λ x, Pair x e)
| Ctx_Pair_r v : ctx1 (λ x, Pair (Val v) x)
| Ctx_Inj b : ctx1 (λ x, Inj b x)
| Ctx_UApp_l e : ctx1 (λ x, UApp x e)
| Ctx_UApp_r v : ctx1 (λ x, UApp (Val v) x)
| Ctx_Send_l p e i : ctx1 (λ x, Send p x i e)
| Ctx_Send_r p v i : ctx1 (λ x, Send p (Val v) i x)
| Ctx_Recv p : ctx1 (λ x, Recv p x)
| Ctx_Let s e : ctx1 (λ x, Let s x e)
| Ctx_LetUnit e : ctx1 (λ x, LetUnit x e)
| Ctx_LetProd s1 s2 e : ctx1 (λ x, LetProd s1 s2 x e)
| Ctx_MatchVoid : ctx1 (λ x, MatchVoid x)
| Ctx_MatchSum s e1 e2 : ctx1 (λ x, MatchSum x s e1 e2)
| Ctx_InjN i : ctx1 (λ x, InjN i x)
| Ctx_MatchSumN n f : ctx1 (λ x, MatchSumN n x f)
| Ctx_If e1 e2 : ctx1 (λ x, If x e1 e2)
| Ctx_Spawn n (f : fin n -> expr) (p : fin n) :
ctx1 (λ x, Spawn n (λ q, if decide (p = q) then x else f q))
| Ctx_Close : ctx1 (λ x, Close x)
| Ctx_Relabel π : ctx1 (λ x, Relabel π x).
Inductive ctx : (expr -> expr) -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=27a07c99 *)
| Ctx_nil : ctx (λ x, x) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=39b87452 *)
| Ctx_cons : ∀ k1 k2, ctx1 k1 -> ctx k2 -> ctx (λ x, (k1 (k2 x))). (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a93094ec *)
Inductive ctx_step : expr -> heap -> expr -> heap -> list expr -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8ac2fd8d *)
| Ctx_step : ∀ k e h e' h' ts, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=de91b99b *)
ctx k -> head_step e h e' h' ts -> ctx_step (k e) h (k e') h' ts. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=cad028bb *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e0a0be6a *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6b93278c *)
the i-th thread can take a step, and this brings us to new thread pool [es'] and heap [h']. *) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b664b729 *)
Inductive stepi : nat -> list expr -> heap -> list expr -> heap -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bbb5c4c2 *)
| Head_step : ∀ e e' h h' i ts es, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=361c6961 *)
ctx_step e h e' h' ts -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d7374346 *)
es !! i = Some e ->
stepi i es h (<[i := e']> es ++ ts) h'.
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=55dc35db *)
Definition can_stepi i es h := ∃ es' h', stepi i es h es' h'.
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=fd8454cb *)
Definition step es h es' h' := ∃ i, stepi i es h es' h'. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0ef5cdc1 *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=31bb3fac *)
Inductive steps : list expr -> heap -> list expr -> heap -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b20933d5 *)
| Trans_step : ∀ e1 e2 e3 s1 s2 s3, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0f132ad2 *)
step e1 s1 e2 s2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b047a25f *)
steps e2 s2 e3 s3 ->
steps e1 s1 e3 s3
| Empty_step : ∀ e1 s1, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1abd3d33 *)
steps e1 s1 e1 s1.
(* =========== *)
(* TYPE SYSTEM *)
(* =========== *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ee27a570 *)
(* Unfortunately this requires some boilerplate. *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ff5723d5 *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=34b72539 *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f52e7c10 *)
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
CoInductive session_type' (T : Type) :=
| SendT n : participant -> (fin n -> T) -> (fin n -> session_type' T) -> session_type' T
| RecvT n : participant -> (fin n -> T) -> (fin n -> session_type' T) -> session_type' T
| EndT : session_type' T.
Arguments SendT {_} _ _ _.
Arguments RecvT {_} _ _ _.
Arguments EndT {_}.
Global Instance sendt_params : Params (@SendT) 1 := {}.
Global Instance recvt_params : Params (@RecvT) 1 := {}.
Global Instance finvec_equiv `{Equiv T} n : Equiv (fin n -> T) := λ f g, ∀ i, f i ≡ g i.
Global Instance finvec_reflexive `{Equiv T} n :
Reflexive (≡@{T}) -> Reflexive (≡@{fin n -> T}).
Proof.
intro. repeat intro; eauto.
Defined.
Global Instance finvec_symmetric `{Equiv T} n :
Symmetric (≡@{T}) -> Symmetric (≡@{fin n -> T}).
Proof.
intro. repeat intro; eauto.
Defined.
Global Instance finvec_transitive `{Equiv T} n :
Transitive (≡@{T}) -> Transitive (≡@{fin n -> T}).
Proof.
intro. repeat intro; eauto.
Defined.
Global Instance finvec_equivalence `{Equiv T} n :
Equivalence (≡@{T}) -> Equivalence (≡@{fin n -> T}).
Proof.
intros []. constructor; apply _.
Defined.
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=98a98e67 *)
CoInductive session_type_equiv `{Equiv T} : Equiv (session_type' T) :=
| cteq_EndT : EndT ≡ EndT
| cteq_SendT n t1 t2 f1 f2 p : t1 ≡ t2 -> f1 ≡ f2 -> SendT n p t1 f1 ≡ SendT n p t2 f2
| cteq_RecvT n t1 t2 f1 f2 p : t1 ≡ t2 -> f1 ≡ f2 -> RecvT n p t1 f1 ≡ RecvT n p t2 f2.
Global Existing Instance session_type_equiv.
Lemma session_type_reflexive `{Equiv T} :
Reflexive (≡@{T}) -> Reflexive (≡@{session_type' T}).
Proof.
intros ?. cofix IH. intros []; constructor; done.
Defined.
Lemma session_type_symmetric `{Equiv T} :
Symmetric (≡@{T}) -> Symmetric (≡@{session_type' T}).
Proof.
intros ?. cofix IH. intros ??[]; constructor; intro; done.
Defined.
Lemma session_type_transitive `{Equiv T} :
Transitive (≡@{T}) -> Transitive (≡@{session_type' T}).
Proof.
intros ?. cofix IH. intros ???[].
- inversion_clear 1. constructor.
- remember (SendT n p t2 f2).
inversion 1; simplify_eq.
constructor; etrans; eauto.
- remember (RecvT n p t2 f2).
inversion 1; simplify_eq.
constructor; etrans; eauto.
Defined.
Global Instance session_type_equivalence `{Equiv T} :
Equivalence (≡@{T}) -> Equivalence (≡@{session_type' T}).
Proof.
split.
- apply session_type_reflexive. apply _.
- apply session_type_symmetric. apply _.
- apply session_type_transitive. apply _.
Qed.
Global Instance sendt_proper `{Equiv T} n p : Proper ((≡) ==> (≡) ==> (≡)) (@SendT T n p).
Proof. by constructor. Qed.
Global Instance recvt_proper `{Equiv T} n p : Proper ((≡) ==> (≡) ==> (≡)) (@RecvT T n p).
Proof. by constructor. Qed.
Definition session_type_id {T} (s : session_type' T) : session_type' T :=
match s with
| SendT n p t s' => SendT n p t s'
| RecvT n p t s' => RecvT n p t s'
| EndT => EndT
end.
Lemma session_type_id_id {T} (s : session_type' T) :
session_type_id s = s.
Proof.
by destruct s.
Qed.
Lemma session_type_equiv_alt `{Equiv T} (s1 s2 : session_type' T) :
session_type_id s1 ≡ session_type_id s2 -> s1 ≡ s2.
Proof.
intros.
rewrite -(session_type_id_id s1).
rewrite -(session_type_id_id s2).
done.
Defined.
Lemma session_type_equiv_end_eq `{Equiv T} (s : session_type' T) :
s ≡ EndT -> s = EndT.
Proof.
by inversion 1.
Qed.
Canonical Structure session_type'O (T:ofe) := discreteO (session_type' T).
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=16c90e72 *)
CoInductive type := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=75c492dd *)
| UnitT : type
| VoidT : type
| NatT : type
| PairT : type -> type -> type (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a6816a9b *)
| SumT : type -> type -> type (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6082af24 *)
| SumNT n : (fin n -> type) -> type
| FunT : type -> type -> type (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=42974689 *)
| UFunT : type -> type -> type (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d3f0f15c *)
| ChanT : session_type' type -> type. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b683be22 *)
Definition type_id (t : type) :=
match t with
| UnitT => UnitT
| VoidT => VoidT
| NatT => NatT
| PairT t1 t2 => PairT t1 t2
| SumT t1 t2 => SumT t1 t2
| SumNT n f => SumNT n f
| FunT t1 t2 => FunT t1 t2
| UFunT t1 t2 => UFunT t1 t2
| ChanT s => ChanT s
end.
Lemma type_id_id t : type_id t = t.
Proof.
by destruct t.
Qed.
(* Coinductive bisimilarity equivalence on types. *)
CoInductive type_equiv : Equiv type := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4d1d9aef *)
| teq_UnitT : UnitT ≡ UnitT
| teq_VoidT : VoidT ≡ VoidT
| teq_NatT : NatT ≡ NatT
| teq_PairT t1 t2 t1' t2' : t1 ≡ t2 -> t1' ≡ t2' -> PairT t1 t1' ≡ PairT t2 t2'
| teq_SumT t1 t2 t1' t2' : t1 ≡ t2 -> t1' ≡ t2' -> SumT t1 t1' ≡ SumT t2 t2'
| teq_SumNT n f1 f2 : f1 ≡ f2 -> SumNT n f1 ≡ SumNT n f2
| teq_FunT t1 t2 t1' t2' : t1 ≡ t2 -> t1' ≡ t2' -> FunT t1 t1' ≡ FunT t2 t2'
| teq_UFunT t1 t2 t1' t2' : t1 ≡ t2 -> t1' ≡ t2' -> UFunT t1 t1' ≡ UFunT t2 t2'
| teq_ChanT s1 s2 : s1 ≡ s2 -> ChanT s1 ≡ ChanT s2.
Global Existing Instance type_equiv.
Global Instance type_equivalence : Equivalence (≡@{type}).
Proof.
split.
- cofix IH. intros []; constructor; done || apply session_type_reflexive, _.
- cofix IH. intros ??[]; constructor; done || by apply (session_type_symmetric _).
- cofix IH. intros ???[]; try solve [inversion_clear 1; constructor;
(by etrans || by eapply (session_type_transitive _))].
intros Q. remember (SumNT n f2) as X.
inversion Q; simplify_eq. constructor.
intro. etrans; eauto.
Qed.
Canonical Structure typeO := discreteO type.
Notation session_type := (session_type' type). (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=df6dd764 *)
Notation session_typeO := (session_type'O typeO).
CoFixpoint relabelT (π : participant -> participant) (σ : session_type) :=
match σ with
| SendT n p ts σs => SendT n (π p) ts (relabelT π ∘ σs)
| RecvT n p ts σs => RecvT n (π p) ts (relabelT π ∘ σs)
| EndT => EndT
end.
Notation envT := (gmap string type).
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=974d19e0 *)
CoInductive unrestricted : type -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c7bf4f13 *)
| Nat_unrestricted : unrestricted NatT (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=65f857c2 *)
| Unit_unrestricted : unrestricted UnitT (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6df3a3fc *)
| Void_unrestricted : unrestricted VoidT (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d9dd8a7b *)
| UFun_unrestricted t1 t2 : unrestricted (UFunT t1 t2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=65d7b397 *)
| Pair_unrestricted t1 t2 : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ded4020d *)
unrestricted t1 -> unrestricted t2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9162db1c *)
unrestricted (PairT t1 t2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a475cea8 *)
| Sum_unrestricted t1 t2 : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ca8a3da2 *)
unrestricted t1 -> unrestricted t2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b0278824 *)
unrestricted (SumT t1 t2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b50c1658 *)
| SumN_unrestricted n f : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=947d0d78 *)
(∀ i, unrestricted (f i)) -> unrestricted (SumNT n f). (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=561a5abd *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a8e5e592 *)
Definition disj (Γ1 Γ2 : envT) : Prop :=
∀ i t1 t2, Γ1 !! i = Some t1 -> Γ2 !! i = Some t2 -> t1 ≡ t2 ∧ unrestricted t1. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=904a0b27 *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e2fb8c9c *)
Definition Γunrestricted (Γ : envT) := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2cde60b7 *)
∀ x t, Γ !! x = Some t -> unrestricted t. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0388a973 *)
(* Disjoint union of N contexts *)
Record disj_union n (Γ : envT) (fΓ : fin n -> envT) : Prop := {
du_disj p q : p ≠ q -> disj (fΓ p) (fΓ q);
du_left p x t : (fΓ p) !! x ≡ Some t -> Γ !! x ≡ Some t;
du_right x t : Γ !! x ≡ Some t -> ∃ p, (fΓ p) !! x ≡ Some t
}.
Lemma disj_union_Proper_impl n Γ Γ' fΓ :
Γ ≡ Γ' -> disj_union n Γ fΓ → disj_union n Γ' fΓ.
Proof.
intros H []. split; eauto; setoid_rewrite <-H; eauto.
Qed.
Global Instance disj_union_Proper n : Proper ((≡) ==> (=) ==> (≡)) (disj_union n).
Proof.
intros ??????.
split; subst; eauto using disj_union_Proper_impl.
symmetry in H. eauto using disj_union_Proper_impl.
Qed.
Definition sentryT := (nat * type)%type.
Definition sbufsT := bufsT participant participant sentryT.
(* Says that if all participants are allowed to receive by their type,
then one of them has a value available in its buffer. *)
Definition can_progress {A}
(bufs : bufsT participant participant A)
(σs : gmap participant session_type) := ∃ q σ,
σs !! q = Some σ ∧
match σ with
| RecvT n p _ _ => ∃ y bufs', pop p q bufs = Some(y,bufs')
| _ => True
end.
Definition buf_empty (bufs : bufsT participant participant sentryT) (p : participant) :=
∀ bs, bufs !! p = Some bs ->
∀ q buf, bs !! q = Some buf -> buf = [].
Definition bufs_empty {A} (bufs : bufsT participant participant A) :=
∀ p q, pop p q bufs = None.
Definition is_present `{Countable A, Countable B} {V}
p q (bufss : bufsT A B V) :=
match bufss !! q with
| Some bufs => match bufs !! p with Some _ => True | None => False end
| None => False
end.
(* We define a stronger consistency notion here. *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=08849e4a *)
CoInductive sbufs_typed
(bufs : bufsT participant participant sentryT)
(σs : gmap participant session_type) : Prop := {
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=919296f7 *)
the message in must be present, and the new local types and buffers must be well-
typed after putting the message in. *) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1cf7a7fd *)
sbufs_typed_send
(n : nat) (p q : participant) ts ss (i : fin n) :
σs !! p = Some (SendT n q ts ss) ->
is_present p q bufs ∧
sbufs_typed (push p q (fin_to_nat i,ts i) bufs) (<[p:=ss i]> σs); (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2e1bbd4a *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d4e4f95d *)
the buffer, then the new local types and buffers must be well-typed after (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2823f30a *)
taking the message out of the buffer. *)
sbufs_typed_recv
(bufs' : bufsT participant participant sentryT)
(n : nat) (p q : participant) t i ts ss :
σs !! q = Some (RecvT n p ts ss) ->
pop p q bufs = Some((i,t),bufs') ->
∃ i', i = fin_to_nat i' ∧ t = ts i' ∧
sbufs_typed bufs' (<[ q := ss i' ]> σs); (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=47bc0c35 *)
(* https://apndx.org/pub/thesis/thesis.pdf#nameddest=fa350fad *)
be empty and the situation must still be well-typed after removing that participant's (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=73b733d5 *)
type and buffers. *) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9139ea1d *)
sbufs_typed_end p :
σs !! p = Some EndT ->
buf_empty bufs p ∧
sbufs_typed (delete p bufs) (delete p σs); (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=61f4f573 *)
(* If there are still buffers, there must be a participant that can make progress. *)
sbufs_typed_progress :
bufs = ∅ ∨ can_progress bufs σs;
(* The participants that have buffers must have local types and vice versa. *)
sbufs_typed_dom :
dom bufs = dom σs
}.
Definition consistent n (σs : fin n -> session_type) := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a495678f *)
sbufs_typed (init_chans n) (fin_gmap n σs). (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e9e2ceb7 *)
(* MPGV typing rules *)
Inductive typed : envT -> expr -> type -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d8292426 *)
| Unit_typed Γ : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=57f63f7b *)
Γunrestricted Γ -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d2abe238 *)
typed Γ (Val UnitV) UnitT (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2110c67a *)
| Nat_typed : ∀ Γ n, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ba3205de *)
Γunrestricted Γ -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=03ac3f4c *)
typed Γ (Val (NatV n)) NatT (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=304480f4 *)
| Var_typed : ∀ Γ x t t', (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=933534cd *)
Γ !! x = None ->
Γunrestricted Γ -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=073c39b5 *)
t ≡ t' ->
typed (Γ ∪ {[ x := t ]}) (Var x) t' (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=64920f8f *)
| Pair_typed : ∀ Γ1 Γ2 e1 e2 t1 t2, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ada7e78a *)
disj Γ1 Γ2 ->
typed Γ1 e1 t1 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=34d6df1e *)
typed Γ2 e2 t2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=25092d09 *)
typed (Γ1 ∪ Γ2) (Pair e1 e2) (PairT t1 t2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=3eca1b0a *)
| App_typed : ∀ Γ1 Γ2 e1 e2 t1 t2, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0f0da78c *)
disj Γ1 Γ2 ->
typed Γ1 e1 (FunT t1 t2) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9db1326e *)
typed Γ2 e2 t1 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4f239318 *)
typed (Γ1 ∪ Γ2) (App e1 e2) t2 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ad9160ca *)
| UApp_typed : ∀ Γ1 Γ2 e1 e2 t1 t2, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5228be30 *)
disj Γ1 Γ2 ->
typed Γ1 e1 (UFunT t1 t2) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1dc5fb97 *)
typed Γ2 e2 t1 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a0494455 *)
typed (Γ1 ∪ Γ2) (UApp e1 e2) t2 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=61530ef5 *)
| Lam_typed : ∀ Γ x e t1 t2, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a5228621 *)
Γ !! x = None ->
typed (Γ ∪ {[ x := t1 ]}) e t2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0aa2c7cc *)
typed Γ (Lam x e) (FunT t1 t2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6a5bb18e *)
| ULam_typed : ∀ Γ x e t1 t2, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e1af1654 *)
Γ !! x = None ->
Γunrestricted Γ -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0bfa74ff *)
typed (Γ ∪ {[ x := t1 ]}) e t2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e00db9d2 *)
typed Γ (ULam x e) (UFunT t1 t2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8b93451c *)
| Send_typed : ∀ Γ1 Γ2 e1 e2 n t r p i, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f6ddaf1f *)
disj Γ1 Γ2 ->
typed Γ1 e1 (ChanT (SendT n p t r)) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9d787c23 *)
typed Γ2 e2 (t i) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1460b017 *)
typed (Γ1 ∪ Γ2) (Send p e1 (fin_to_nat i) e2) (ChanT (r i)) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bf97d6f7 *)
| Recv_typed : ∀ Γ e n t r p, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a86154e7 *)
typed Γ e (ChanT (RecvT n p t r)) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=00f4912a *)
typed Γ (Recv p e) (SumNT n (λ i, PairT (ChanT (r i)) (t i))) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=810ca349 *)
| Let_typed : ∀ Γ1 Γ2 e1 e2 t1 t2 x, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0fd2dd4c *)
disj Γ1 Γ2 ->
Γ2 !! x = None ->
typed Γ1 e1 t1 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=409f125c *)
typed (Γ2 ∪ {[ x := t1 ]}) e2 t2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=082e0d1a *)
typed (Γ1 ∪ Γ2) (Let x e1 e2) t2 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=55439db7 *)
| LetUnit_typed : ∀ Γ1 Γ2 e1 e2 t, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=943da370 *)
disj Γ1 Γ2 ->
typed Γ1 e1 UnitT -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5792e3ae *)
typed Γ2 e2 t -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2b6eb513 *)
typed (Γ1 ∪ Γ2) (LetUnit e1 e2) t (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c5b4bd12 *)
| LetProd_typed : ∀ Γ1 Γ2 e1 e2 t11 t12 t2 x1 x2, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b3a32a0b *)
disj Γ1 Γ2 ->
x1 ≠ x2 ->
Γ2 !! x1 = None ->
Γ2 !! x2 = None ->
typed Γ1 e1 (PairT t11 t12) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=fb9b4be1 *)
typed (Γ2 ∪ {[ x1 := t11 ]} ∪ {[ x2 := t12 ]}) e2 t2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=15e35cc8 *)
typed (Γ1 ∪ Γ2) (LetProd x1 x2 e1 e2) t2 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6946ac5f *)
| MatchVoid_typed : ∀ Γ e t, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4d0de696 *)
typed Γ e VoidT -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1f840c9b *)
typed Γ (MatchVoid e) t (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9b3715d9 *)
| MatchSum_typed : ∀ Γ1 Γ2 e1 eL eR tL tR t x, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bb31192f *)
disj Γ1 Γ2 ->
Γ2 !! x = None ->
typed Γ1 e1 (SumT tL tR) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7f2397d7 *)
typed (Γ2 ∪ {[ x := tL ]}) eL t -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7a09f78b *)
typed (Γ2 ∪ {[ x := tR ]}) eR t -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f5823f8e *)
typed (Γ1 ∪ Γ2) (MatchSum e1 x eL eR) t (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1de80d95 *)
| InjN_typed : ∀ Γ n f i e, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=86e03e64 *)
typed Γ e (f i) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=292802a8 *)
typed Γ (InjN (fin_to_nat i) e) (SumNT n f) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d25223b0 *)
| MatchSumN_typed : ∀ n Γ1 Γ2 t (f : fin n -> type) fc e, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f178ea47 *)
disj Γ1 Γ2 ->
(n = 0 -> Γ2 = ∅) ->
typed Γ1 e (SumNT n f) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=addcd3f2 *)
(∀ i, typed Γ2 (fc i) (FunT (f i) t)) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9a06c888 *)
typed (Γ1 ∪ Γ2) (MatchSumN n e fc) t (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=92c7f0a9 *)
| If_typed : ∀ Γ1 Γ2 e1 e2 e3 t, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=419f0d4e *)
disj Γ1 Γ2 ->
typed Γ1 e1 NatT -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=de8bf616 *)
typed Γ2 e2 t -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=12258404 *)
typed Γ2 e3 t -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0da3e369 *)
typed (Γ1 ∪ Γ2) (If e1 e2 e3) t (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=de0fec68 *)
| Spawn_typed : ∀ n Γ (fΓ : fin n -> envT) (f : fin n -> expr) (σs : fin (S n) -> session_type), (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4daccd61 *)
consistent (S n) σs -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f6089a27 *)
disj_union n Γ fΓ ->
(∀ p, typed (fΓ p) (f p) (FunT (ChanT (σs (FS p))) UnitT)) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=95270432 *)
typed Γ (Spawn n f) (ChanT (σs 0%fin)) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=330cf0c9 *)
| Close_typed : ∀ Γ e, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4c6dfdde *)
typed Γ e (ChanT EndT) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=62774730 *)
typed Γ (Close e) UnitT (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=07362140 *)
| Relabel_typed : ∀ Γ π e σ, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0ed21b65 *)
typed Γ e (ChanT (relabelT π σ)) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=07d9af16 *)
typed Γ (Relabel π e) (ChanT σ) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d7f915c3 *)
| Iso_typed : ∀ Γ t t' e, (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c7323812 *)
t ≡ t' -> (* The ≡-relation is unfolding of recursive types *)
typed Γ e t -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9c918f45 *)
typed Γ e t'. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1c89c777 *)
(*
Coq's default notion of equality is not good enough for coinductive types:
the default equality is syntactic equality and not extensional equality.
We add an axiom to make equality extensional.
See https://coq.inria.fr/refman/language/core/coinductive.html:
"More generally, as in the case of positive coinductive types,
it is consistent to further identify extensional equality of coinductive (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b4a3f8b9 *)
types with propositional equality"
Such an axiom is similar to functional extensionality, but for coinductive types.
For extra guarantees, we have proved various properties about (≡) above,
for instance that it is an equivalence relation.
*)
Axiom session_type_extensionality : ∀ σ1 σ2 : session_type, σ1 ≡ σ2 -> σ1 = σ2.
(*
To show that it is possible to manually work around this limitation of Coq,
we have proved manually that our run-time type system is (≡)-invariant (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=620806d3 *)
(see rtyped_proper_impl in rtypesystem.v).
As you can see, this is very painful, and it also pollutes our definitions and proofs
and makes them less clear. So in certain cases we use this axiom.
*)