make use of Some inclusion in a few more places

iris/algebra/cmra.v

@@ -1524,6 +1524,27 @@ Section option.
   Lemma Some_included_is_Some x mb : Some x ≼ mb → is_Some mb.
   Proof. rewrite option_included. naive_solver. Qed.
 
+  Lemma Some_includedN_alt n a b : Some a ≼{n} Some b ↔ ∃ mc, b ≡{n}≡ a ⋅? mc.
+  Proof.
+    rewrite Some_includedN. split.
+    - intros [Heq|[c Heq]].
+      + exists None. auto.
+      + exists (Some c). auto.
+    - intros [[c|] Heq].
+      + right. exists c. auto.
+      + left. auto.
+  Qed.
+  Lemma Some_included_alt a b : Some a ≼ Some b ↔ ∃ mc, b ≡ a ⋅? mc.
+  Proof.
+    rewrite Some_included. split.
+    - intros [Heq|[c Heq]].
+      + exists None. auto.
+      + exists (Some c). auto.
+    - intros [[c|] Heq].
+      + right. exists c. auto.
+      + left. auto.
+  Qed.
+
   Lemma Some_includedN_total `{!CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
   Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.
   Lemma Some_included_total `{!CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.

iris/algebra/gmap.v

@@ -361,16 +361,18 @@ Proof.
   intros (y&?&->%(Some_included_exclusive _)); eauto using lookup_valid_Some.
 Qed.
 Lemma singleton_included i x y :
-  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≡ y ∨ x ≼ y.
+  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ Some x ≼ Some y.
 Proof.
   rewrite singleton_included_l. split.
-  - intros (y'&Hi&?). rewrite lookup_insert in Hi.
-    apply Some_included. by rewrite Hi.
-  - intros ?. exists y. by rewrite lookup_insert Some_included.
+  - intros (y'&Hi&?). rewrite lookup_insert in Hi. by rewrite Hi.
+  - intros ?. exists y. by rewrite lookup_insert.
 Qed.
+Lemma singleton_included_total `{!CmraTotal A}  i x y :
+  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≼ y.
+Proof. rewrite singleton_included Some_included_total. done. Qed.
 Lemma singleton_mono i x y :
   x ≼ y → {[ i := x ]} ≼ ({[ i := y ]} : gmap K A).
-Proof. intros Hincl. apply singleton_included. right. done. Qed.
+Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed.
 
 Global Instance singleton_cancelable i x :
   Cancelable (Some x) → Cancelable {[ i := x ]}.

iris/algebra/local_updates.v

@@ -76,30 +76,28 @@ Section updates.
   Qed.
 
   Lemma local_update_valid0 x y x' y' :
-    (✓{0} x → ✓{0} y → x ≡{0}≡ y ∨ y ≼{0} x → (x,y) ~l~> (x',y')) →
+    (✓{0} x → ✓{0} y → Some y ≼{0} Some x → (x,y) ~l~> (x',y')) →
     (x,y) ~l~> (x',y').
   Proof.
     intros Hup n mz Hmz Hz; simpl in *. apply Hup; auto.
     - by apply (cmra_validN_le n); last lia.
     - apply (cmra_validN_le n); last lia.
       move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l.
-    - destruct mz as [z|].
-      + right. exists z. apply dist_le with n; auto with lia.
-      + left. apply dist_le with n; auto with lia.
+    - eapply (cmra_includedN_le n); last lia.
+      apply Some_includedN_alt. eauto.
   Qed.
   Lemma local_update_valid `{!CmraDiscrete A} x y x' y' :
-    (✓ x → ✓ y → x ≡ y ∨ y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
+    (✓ x → ✓ y → Some y ≼ Some x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
   Proof.
-    rewrite !(cmra_discrete_valid_iff 0)
-      (cmra_discrete_included_iff 0) (discrete_iff 0).
+    rewrite !(cmra_discrete_valid_iff 0) (cmra_discrete_included_iff 0).
     apply local_update_valid0.
   Qed.
 
   Lemma local_update_total_valid0 `{!CmraTotal A} x y x' y' :
     (✓{0} x → ✓{0} y → y ≼{0} x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
   Proof.
-    intros Hup. apply local_update_valid0=> ?? [Hx|?]; apply Hup; auto.
-    by rewrite Hx.
+    intros Hup. apply local_update_valid0=> ?? Hincl. apply Hup; auto.
+    by apply Some_includedN_total.
   Qed.
   Lemma local_update_total_valid `{!CmraTotal A, !CmraDiscrete A} x y x' y' :
     (✓ x → ✓ y → y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').

iris/base_logic/lib/gen_inv_heap.v

@@ -219,8 +219,9 @@ Section inv_heap.
 
   Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦_I □.
   Proof.
-    iApply own_mono. apply auth_frag_mono. rewrite singleton_included pair_included.
-    right. split; [apply: ucmra_unit_least|done].
+    iApply own_mono. apply auth_frag_mono.
+    rewrite singleton_included_total pair_included.
+    split; [apply: ucmra_unit_least|done].
   Qed.
 
   (** An accessor to make use of [inv_mapsto_own].