From 5b83879e8b52088567a38d3ba02fb8ef9e56ea69 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 14 Sep 2020 17:29:22 +0200
Subject: [PATCH] Reintroduced contractiveness of lty_choice

---
 theories/logrel/session_types.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index c932551..f319581 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -107,6 +107,19 @@ Section session_types.
   Proof. solve_proper. Qed.
   Global Instance lty_choice_proper a : Proper ((≡) ==> (≡)) (@lty_choice Σ a).
   Proof. apply ne_proper, _. Qed.
+  Global Instance lty_choice_contractive a :
+    Proper (map_relation (dist_later n) (λ _, False) (λ _, False) ==> dist n)
+           (@lty_choice Σ a).
+  Proof.
+    intros n Ss Ts Heq. rewrite /lty_choice.
+    do 4 f_equiv.
+    rewrite !lookup_total_alt.
+    specialize (Heq a0).
+    destruct (Ss !! a0), (Ts !! a0);
+      [ f_contractive | contradiction | contradiction | done ].
+    - f_equiv. split; intros H; eauto.
+    - by rewrite Heq.
+  Qed.
   Global Instance lty_dual_ne : NonExpansive (@lty_dual Σ).
   Proof. solve_proper. Qed.
   Global Instance lty_dual_proper : Proper ((≡) ==> (≡)) (@lty_dual Σ).
-- 
GitLab