From 3ce80f37ec52828308bd46768acd098c4aa5d8f0 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 3 Sep 2020 13:17:20 +0200
Subject: [PATCH] Proven Amber-like rule

---
 theories/channel/proto.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 7eef5ce..4ebce7b 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -899,6 +899,17 @@ Section proto.
       iSplitL "H"; [iIntros "!>"; by iRewrite "Hp2d"|]. simpl; auto.
   Qed.
 
+  Lemma iProto_le_amber (p1 p2 : iProto Σ V → iProto Σ V)
+    `{Contractive p1, Contractive p2}:
+    □ (∀ rec1 rec2, ▷ (rec1 ⊑ rec2) → p1 rec1 ⊑ p2 rec2) -∗
+    fixpoint p1 ⊑ fixpoint p2.
+  Proof.
+    iIntros "#H". iLöb as "IH".
+    iEval (rewrite (fixpoint_unfold p1)).
+    iEval (rewrite (fixpoint_unfold p2)).
+    iApply "H". iApply "IH".
+  Qed.
+
   Lemma iProto_le_dual_l p1 p2 : iProto_dual p2 ⊑ p1 -∗ iProto_dual p1 ⊑ p2.
   Proof.
     iIntros "H". iEval (rewrite -(involutive iProto_dual p2)).
-- 
GitLab