From fcf2343c0b49df8642243fe2d8b04859cf678b77 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 30 Apr 2020 19:54:54 +0200
Subject: [PATCH] Proved contractiveness of lty_msg_base.
---
theories/logrel/session_types.v | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 46eeacd..cb8dcc2 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -69,10 +69,14 @@ Section session_types.
Global Instance lty_msg_base_proper a :
Proper ((≡) ==> (≡) ==> (≡)) (@lty_msg_base Σ a).
Proof. rewrite /lty_msg_base. apply ne_proper_2, _. Qed.
- (* FIXME: Not contractive since lty_msg_exist is not contractive *)
- (* Global Instance lty_msg_base_contractive n a : *)
- (* Proper (dist n ==> dist_later n ==> dist n) (@lty_msg_base Σ a). *)
- (* Proof. rewrite /lty_msg_base. solve_contractive. Qed. *)
+ Global Instance lty_msg_base_contractive n :
+ Proper (dist_later n ==> dist_later n ==> dist n) (@lty_msg_base Σ).
+ Proof.
+ intros A1 A2 HA S1 S2 HS.
+ rewrite /lty_msg_base.
+ f_equiv=> w.
+ by repeat f_contractive.
+ Qed.
Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
Proof. solve_proper. Qed.
--
GitLab