-
Notifications
You must be signed in to change notification settings - Fork 0
/
ProtoRep.v
117 lines (97 loc) · 3.68 KB
/
ProtoRep.v
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
Require Import Crypto.
Inductive protoType : Type :=
| Send : type -> protoType -> protoType
| Receive : type -> protoType -> protoType
| Choice : protoType -> protoType -> protoType
| Offer : protoType -> protoType -> protoType
| Eps : type -> protoType.
Inductive protoExp : protoType -> Type :=
| SendC {t:type} {p':protoType} : (message t) -> (protoExp p')
-> protoExp (Send t p')
| ReceiveC {t:type} {p':protoType} : ((message t)->(protoExp p'))
-> protoExp (Receive t p')
| ChoiceC (b:bool) {r s:protoType} : (protoExp r) -> (protoExp s)
-> (protoExp (Choice r s))
| OfferC {r s : protoType} : (protoExp r) -> (protoExp s)
-> protoExp (Offer r s)
| ReturnC {t:type} : (message t) -> protoExp (Eps t).
Fixpoint returnType (pt : protoType) : type :=
match pt with
| Eps t => t
| Send _ pt' => returnType pt'
| Receive _ pt' => returnType pt'
| Choice pt' pt'' => Either (returnType pt') (returnType pt'')
| Offer pt' pt'' => Either (returnType pt') (returnType pt'')
end.
Notation "x :!: y" := (Send x y)
(at level 50, left associativity).
Notation "x :!: y" := (protoExp (Send x y))
(at level 50, left associativity).
Notation "x :?: y" := (Receive x y)
(at level 50, left associativity).
Notation "x :?: y" := (protoExp (Receive x y))
(at level 50, left associativity).
Notation "x :+: y" := (Choice x y)
(at level 50, left associativity).
Notation "x :+: y" := (protoExp (Choice x y))
(at level 50, left associativity).
Notation "x :&: y" := (Offer x y)
(at level 50, left associativity).
Notation "x :&: y" := (protoExp (Offer x y))
(at level 50, left associativity).
Notation "'send' n ; p" := (SendC n p)
(right associativity, at level 60).
Notation "x <- 'receive' ; p " := (ReceiveC (fun x => p))
(right associativity, at level 60).
Notation "'offer'" := OfferC.
Notation "'choice'" := ChoiceC.
Definition EpsC := ReturnC (basic 0).
Fixpoint DualT (t t':protoType) : Prop :=
match t with
| Send p1T p1' =>
match t' with
| Receive p2T p2' => (p1T = p2T) /\ (DualT p1' p2')
| _ => False
end
| Receive p1T p1' =>
match t' with
| Send p2T p2' => (p1T = p2T) /\ (DualT p1' p2')
| _ => False
end
| Choice p1' p1'' =>
match t' with
| Offer p2' p2'' => (DualT p1' p2') /\ (DualT p1'' p2'')
| _ => False
end
| Offer p1' p1'' =>
match t' with
| Choice p2' p2'' => (DualT p1' p2') /\ (DualT p1'' p2'')
| _ => False
end
| Eps _ =>
match t' with
| Eps _ => True
| _ => False
end
end.
Fixpoint DualT_dec (t t':protoType) : {DualT t t'} + {~ DualT t t'}.
Proof.
destruct t; destruct t';
(* Eliminate all un-interesting cases *)
try (right; unfold not; intros; inversion H; contradiction);
(* For the Send/Receive, Receive/Send cases *)
try (
destruct (eq_type_dec t t1); destruct (DualT_dec t0 t');
try (right; unfold not; intros; inversion H; contradiction);
try (left; split; assumption)
);
(* For the Choice/Offer, Offer/Choice cases *)
try (
destruct (DualT_dec t1 t'1); destruct (DualT_dec t2 t'2);
try (right; unfold not; intros; inversion H; contradiction);
try( left; split; assumption)
).
(* Eps/Eps case *)
left. simpl. trivial.
Defined.
Definition Dual {t t':protoType} (p1:protoExp t) (p2:protoExp t') : Prop := DualT t t'.