From c66ceaed74c6254cef628fad45725113b22662cb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Oct 2020 14:59:30 +0200
Subject: [PATCH] Remove lemma `view_equivI` and document that.

---
 theories/algebra/auth.v |  3 +++
 theories/algebra/view.v | 12 ++++++------
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 1284f10c8..7eb644ac4 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -62,6 +62,9 @@ Notation "●{ q } a" := (auth_auth q a) (at level 20, format "●{ q }  a").
 Notation "● a" := (auth_auth 1 a) (at level 20).
 
 (** * Laws of the authoritative camera *)
+(** We omit the usual [equivI] lemma because it is hard to state a suitably
+general version in terms of [●] and [◯], and because such a lemma has never
+been needed in practice. *)
 Section auth.
   Context {A : ucmraT}.
   Implicit Types a b : A.
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index a0bae0dc4..f4dcad122 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -71,6 +71,9 @@ Class ViewRelDiscrete {A B} (rel : view_rel A B) :=
   view_rel_discrete n a b : rel 0 a b → rel n a b.
 
 (** * Definition of the view camera *)
+(** To make use of the lemmas provided in this file, elements of [view] should
+always be constructed using [●V] and [◯V], and never using the constructor
+[View]. *)
 Record view {A B} (rel : nat → A → B → Prop) :=
   View { view_auth_proj : option (frac * agree A) ; view_frag_proj : B }.
 Add Printing Constructor view.
@@ -94,6 +97,9 @@ Notation "●V a" := (view_auth 1 a) (at level 20).
 Notation "â—¯V a" := (view_frag a) (at level 20).
 
 (** * The OFE structure *)
+(** We omit the usual [equivI] lemma because it is hard to state a suitably
+general version in terms of [●V] and [◯V], and because such a lemma has never
+been needed in practice. *)
 Section ofe.
   Context {A B : ofeT} (rel : nat → A → B → Prop).
   Implicit Types a : A.
@@ -132,12 +138,6 @@ Section ofe.
   Global Instance view_ofe_discrete :
     OfeDiscrete A → OfeDiscrete B → OfeDiscrete viewO.
   Proof. intros ?? [??]; apply _. Qed.
-
-  (** Internalized properties *)
-  Lemma view_equivI {M} x y :
-    x ≡ y ⊣⊢@{uPredI M}
-      view_auth_proj x ≡ view_auth_proj y ∧ view_frag_proj x ≡ view_frag_proj y.
-  Proof. by uPred.unseal. Qed.
 End ofe.
 
 (** * The camera structure *)
-- 
GitLab