From bd4b6aa2d9d122974cca54b83d4145617a620b88 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2023 16:05:19 +0100
Subject: [PATCH] More uses of `iCombine .. gives`.
---
theories/utils/contribution.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 2143b9d..24d5f38 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -63,8 +63,8 @@ Section contribution.
Lemma server_1_agree γ x y : server γ 1 x -∗ client γ y -∗ ⌜ x ≡ y âŒ.
Proof.
rewrite /server /client. case_decide=> //. iIntros "Hs Hc".
- iDestruct (own_valid_2 with "Hs Hc")
- as %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete; first done.
+ iCombine "Hs Hc"
+ gives %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete; first done.
move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[? _].
by destruct (Pos.lt_irrefl 1).
Qed.
@@ -88,8 +88,8 @@ Section contribution.
rewrite /server /client. iIntros "Hs Hc". case_decide; subst.
- iDestruct "Hs" as "(_ & _ & Hc')".
by iCombine "Hc Hc'" gives %?%auth_frag_op_valid_1.
- - iDestruct (own_valid_2 with "Hs Hc")
- as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
+ - iCombine "Hs Hc"
+ gives %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
{ setoid_subst. by destruct n. }
move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[??].
by destruct n.
--
GitLab