Merge branch 'mono_list_auth_core_id' into 'master'

add mono_list_auth_core_id, mono_nat_auth_core_id

See merge request iris/iris!827

iris/algebra/auth.v

@@ -134,6 +134,8 @@ Section auth.
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
   Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_both_core_id a1 a2 : CoreId a2 → CoreId (●□ a1 ⋅ ◯ a2).
+  Proof. rewrite /auth_auth /auth_frag. apply _. Qed.
   Global Instance auth_frag_is_op a b1 b2 :
     IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
   Proof. rewrite /auth_frag. apply _. Qed.

iris/algebra/lib/mono_list.v

@@ -50,6 +50,8 @@ Section mono_list_props.
   (** * Operation *)
   Global Instance mono_list_lb_core_id l : CoreId (◯ML l).
   Proof. rewrite /mono_list_lb. apply _. Qed.
+  Global Instance mono_list_auth_core_id l : CoreId (●ML□ l).
+  Proof. rewrite /mono_list_auth. apply _. Qed.
 
   Lemma mono_list_auth_dfrac_op dq1 dq2 l :
     ●ML{dq1 ⋅ dq2} l ≡ ●ML{dq1} l ⋅ ●ML{dq2} l.

iris/algebra/lib/mono_nat.v

@@ -32,6 +32,8 @@ Section mono_nat.
 
   Global Instance mono_nat_lb_core_id n : CoreId (◯MN n).
   Proof. apply _. Qed.
+  Global Instance mono_nat_auth_core_id l : CoreId (●MN□ l).
+  Proof. apply _. Qed.
 
   Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
     ●MN{dq1 ⋅ dq2} n ≡ ●MN{dq1} n ⋅ ●MN{dq2} n.

iris/algebra/view.v

@@ -289,6 +289,8 @@ Section cmra.
   Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
   Global Instance view_frag_core_id b : CoreId b → CoreId (◯V b).
   Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
+  Global Instance view_both_core_id a b : CoreId b → CoreId (●V□ a ⋅ ◯V b).
+  Proof. do 2 constructor; simpl; auto. rewrite !left_id. apply: core_id_core. Qed.
   Global Instance view_frag_is_op b b1 b2 :
     IsOp b b1 b2 → IsOp' (◯V b) (◯V b1) (◯V b2).
   Proof. done. Qed.