Merge branch 'generalize-gmap-equivI' into 'master'

Generalize the type of gmap_equivI.

See merge request iris/iris!495

theories/algebra/auth.v

@@ -69,6 +69,11 @@ Global Instance Auth_discrete a b :
 Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
 Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete authO.
 Proof. intros ? [??]; apply _. Qed.
+
+(** Internalized properties *)
+Lemma auth_equivI {M} x y :
+  x ≡ y ⊣⊢@{uPredI M} auth_auth_proj x ≡ auth_auth_proj y ∧ auth_frag_proj x ≡ auth_frag_proj y.
+Proof. by uPred.unseal. Qed.
 End ofe.
 
 Arguments authO : clear implicits.
@@ -329,9 +334,6 @@ Lemma auth_auth_frac_op_invL `{!LeibnizEquiv A} q a p b :
 Proof. by intros ?%auth_auth_frac_op_inv%leibniz_equiv. Qed.
 
 (** Internalized properties *)
-Lemma auth_equivI {M} x y :
-  x ≡ y ⊣⊢@{uPredI M} auth_auth_proj x ≡ auth_auth_proj y ∧ auth_frag_proj x ≡ auth_frag_proj y.
-Proof. by uPred.unseal. Qed.
 Lemma auth_validI {M} x :
   ✓ x ⊣⊢@{uPredI M} match auth_auth_proj x with
                     | Some (q, ag) => ✓ q ∧

theories/algebra/csum.v

@@ -107,6 +107,19 @@ Global Instance Cinl_discrete a : Discrete a → Discrete (Cinl a).
 Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
 Global Instance Cinr_discrete b : Discrete b → Discrete (Cinr b).
 Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
+
+(** Internalized properties *)
+Lemma csum_equivI {M} (x y : csum A B) :
+  x ≡ y ⊣⊢@{uPredI M} match x, y with
+                      | Cinl a, Cinl a' => a ≡ a'
+                      | Cinr b, Cinr b' => b ≡ b'
+                      | CsumBot, CsumBot => True
+                      | _, _ => False
+                      end.
+Proof.
+  uPred.unseal; do 2 split; first by destruct 1.
+  by destruct x, y; try destruct 1; try constructor.
+Qed.
 End cofe.
 
 Arguments csumO : clear implicits.
@@ -287,17 +300,6 @@ Global Instance Cinr_id_free b : IdFree b → IdFree (Cinr b).
 Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
 
 (** Internalized properties *)
-Lemma csum_equivI {M} (x y : csum A B) :
-  x ≡ y ⊣⊢@{uPredI M} match x, y with
-                      | Cinl a, Cinl a' => a ≡ a'
-                      | Cinr b, Cinr b' => b ≡ b'
-                      | CsumBot, CsumBot => True
-                      | _, _ => False
-                      end.
-Proof.
-  uPred.unseal; do 2 split; first by destruct 1.
-  by destruct x, y; try destruct 1; try constructor.
-Qed.
 Lemma csum_validI {M} (x : csum A B) :
   ✓ x ⊣⊢@{uPredI M} match x with
                     | Cinl a => ✓ a

theories/algebra/gmap.v

@@ -94,6 +94,10 @@ Global Instance gmap_singleton_discrete i x :
 Lemma insert_idN n m i x :
   m !! i ≡{n}≡ Some x → <[i:=x]>m ≡{n}≡ m.
 Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
+
+(** Internalized properties *)
+Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢@{uPredI M} ∀ i, m1 !! i ≡ m2 !! i.
+Proof. by uPred.unseal. Qed.
 End cofe.
 
 Arguments gmapO _ {_ _} _.
@@ -232,8 +236,6 @@ Qed.
 Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
 
 (** Internalized properties *)
-Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢@{uPredI M} ∀ i, m1 !! i ≡ m2 !! i.
-Proof. by uPred.unseal. Qed.
 Lemma gmap_validI {M} m : ✓ m ⊣⊢@{uPredI M} ∀ i, ✓ (m !! i).
 Proof. by uPred.unseal. Qed.
 End cmra.

theories/algebra/list.v

@@ -93,6 +93,10 @@ Global Instance nil_discrete : Discrete (@nil A).
 Proof. inversion_clear 1; constructor. Qed.
 Global Instance cons_discrete x l : Discrete x → Discrete l → Discrete (x :: l).
 Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
+
+(** Internalized properties *)
+Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢@{uPredI M} ∀ i, l1 !! i ≡ l2 !! i.
+Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
 End cofe.
 
 Arguments listO : clear implicits.
@@ -311,8 +315,6 @@ Section cmra.
   Proof. intros Hyp; by apply list_core_id'. Qed.
 
   (** Internalized properties *)
-  Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢@{uPredI M} ∀ i, l1 !! i ≡ l2 !! i.
-  Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
   Lemma list_validI {M} l : ✓ l ⊣⊢@{uPredI M} ∀ i, ✓ (l !! i).
   Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
 End cmra.