From 902f53055d9106a58da14fdab4dd7c9608b5b0dd Mon Sep 17 00:00:00 2001
From: Dmitry Khalanskiy <Dmitry.Khalanskiy@jetbrains.com>
Date: Tue, 21 Jan 2020 15:08:20 +0300
Subject: [PATCH] Add pair_op_1 and pair_op_2
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The two new lemmas allow splitting the resources in one component
of a pair when the other component has nothing. In combination
with `pair_split`, they allow to arbitrarily split the resource
`(a â‹… a', b â‹… b')`.

This is in line with `prod_local_update_1` and
`prod_local_update_2`, the lemmas that allow, in a sense, to only
consider one component of a pair.
---
 theories/algebra/cmra.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3ea70b65a..8a409fdbf 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1210,6 +1210,20 @@ Section prod_unit.
   Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
     (x, y) = (x, ε) ⋅ (ε, y).
   Proof. unfold_leibniz. apply pair_split. Qed.
+
+  Lemma pair_op_1 (a a': A) : (a ⋅ a', ε) ≡@{A*B} (a, ε) ⋅ (a', ε).
+  Proof. by rewrite -pair_op ucmra_unit_left_id. Qed.
+
+  Lemma pair_op_1_L `{!LeibnizEquiv A, !LeibnizEquiv B} (a a': A) :
+    (a ⋅ a', ε) =@{A*B} (a, ε) ⋅ (a', ε).
+  Proof. unfold_leibniz. apply pair_op_1. Qed.
+
+  Lemma pair_op_2 (b b': B) : (ε, b ⋅ b') ≡@{A*B} (ε, b) ⋅ (ε, b').
+  Proof. by rewrite -pair_op ucmra_unit_left_id. Qed.
+
+  Lemma pair_op_2_L `{!LeibnizEquiv A, !LeibnizEquiv B} (b b': B) :
+    (ε, b ⋅ b') =@{A*B} (ε, b) ⋅ (ε, b').
+  Proof. unfold_leibniz. apply pair_op_2. Qed.
 End prod_unit.
 
 Arguments prodUR : clear implicits.
-- 
GitLab