From 55b62c3505e23039b620eede196a24b3d3b291c2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Oct 2020 18:00:40 +0200
Subject: [PATCH] =?UTF-8?q?Add=20injectivity=20instances=20for=20`?=
 =?UTF-8?q?=E2=97=8F`=20and=20`=E2=97=AF`=20for=20auth=20&=20view.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/algebra/auth.v | 14 +++++++++++---
 theories/algebra/view.v | 18 +++++++++++++++++-
 2 files changed, 28 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index cadb75d7f..f4e8cdadc 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -69,13 +69,21 @@ Section auth.
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_auth_proper q : Proper ((≡) ==> (≡)) (@auth_auth A q).
   Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_frag_ne: NonExpansive (@auth_frag A).
+  Global Instance auth_frag_ne : NonExpansive (@auth_frag A).
   Proof. rewrite /auth_frag. apply _. Qed.
   Global Instance auth_frag_proper : Proper ((≡) ==> (≡)) (@auth_frag A).
   Proof. rewrite /auth_frag. apply _. Qed.
 
-  Lemma auth_auth_frac_validN n q a :
-    ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
+  Global Instance auth_auth_dist_inj n : Inj2 (=) (dist n) (dist n) (@auth_auth A).
+  Proof. rewrite /auth_auth. apply _. Qed.
+  Global Instance auth_auth_inj : Inj2 (=) (≡) (≡) (@auth_auth A).
+  Proof. rewrite /auth_auth. apply _. Qed.
+  Global Instance auth_frag_dist_inj n : Inj (dist n) (dist n) (@auth_frag A).
+  Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_frag_inj : Inj (≡) (≡) (@auth_frag A).
+  Proof. rewrite /auth_frag. apply _. Qed.
+
+  Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
   Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
   Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index f18259973..b60729e2b 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -123,11 +123,27 @@ Section cmra.
   Proof. solve_proper. Qed.
   Global Instance view_auth_proper q : Proper ((≡) ==> (≡)) (@view_auth A B rel q).
   Proof. solve_proper. Qed.
-  Global Instance view_frag_ne: NonExpansive (@view_frag A B rel).
+  Global Instance view_frag_ne : NonExpansive (@view_frag A B rel).
   Proof. done. Qed.
   Global Instance view_frag_proper : Proper ((≡) ==> (≡)) (@view_frag A B rel).
   Proof. done. Qed.
 
+  Global Instance view_auth_dist_inj n :
+    Inj2 (=) (dist n) (dist n) (@view_auth A B rel).
+  Proof.
+    intros p1 a1 p2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
+    split; [done|]. by apply (inj to_agree).
+  Qed.
+  Global Instance view_auth_inj : Inj2 (=) (≡) (≡) (@view_auth A B rel).
+  Proof.
+    intros p1 a1 p2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
+    split; [done|]. by apply (inj to_agree).
+  Qed.
+  Global Instance view_frag_dist_inj n : Inj (dist n) (dist n) (@view_frag A B rel).
+  Proof. by intros ?? [??]. Qed.
+  Global Instance view_frag_inj : Inj (≡) (≡) (@view_frag A B rel).
+  Proof. by intros ?? [??]. Qed.
+
   Instance view_valid : Valid (view rel) := λ x,
     match view_auth_proj x with
     | Some (q, ag) =>
-- 
GitLab