Merge branch 'robbert/some_cmra_lemmas' into 'master'

Generalize `Excl_included` & more `singleton_included` lemmas

See merge request iris/iris!419

CHANGELOG.md

@@ -95,6 +95,12 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Better support for telescopes in the proof mode, i.e., all tactics should
   recognize and distribute telescopes now.
 * Remove namespace `N` from `is_lock`.
+* Make lemma `Excl_included` a bi-implication.
+* Add lemma `singleton_included : {[ i := x ]} ≼ ({[ i := y ]} ↔ x ≡ y ∨ x ≼ y`,
+  and rename existing asymmetric lemmas (with a singleton on just the LHS):
+  + `singleton_includedN` → `singleton_includedN_l`.
+  + `singleton_included` → `singleton_included_l`.
+  + `singleton_included_exclusive` → `singleton_included_exclusive_l`
 
 **Changes in heap_lang:**
 

theories/algebra/excl.v

@@ -118,10 +118,14 @@ Proof. by destruct mx. Qed.
 Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None.
 Proof. by destruct mx. Qed.
 
-Lemma Excl_includedN n a b  : Excl' a ≼{n} Excl' b → a ≡{n}≡ b.
-Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
-Lemma Excl_included a b : Excl' a ≼ Excl' b → a ≡ b.
-Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
+Lemma Excl_includedN n a b  : Excl' a ≼{n} Excl' b ↔ a ≡{n}≡ b.
+Proof.
+  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
+Qed.
+Lemma Excl_included a b : Excl' a ≼ Excl' b ↔ a ≡ b.
+Proof.
+  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
+Qed.
 End excl.
 
 Arguments exclO : clear implicits.

theories/algebra/gmap.v

@@ -308,7 +308,7 @@ Global Instance gmap_singleton_core_id i (x : A) :
   CoreId x → CoreId {[ i := x ]}.
 Proof. intros. by apply core_id_total, core_singleton'. Qed.
 
-Lemma singleton_includedN n m i x :
+Lemma singleton_includedN_l n m i x :
   {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ Some x ≼{n} Some y.
 Proof.
   split.
@@ -321,7 +321,7 @@ Proof.
     + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
 Qed.
 (* We do not have [x ≼ y ↔ ∀ n, x ≼{n} y], so we cannot use the previous lemma *)
-Lemma singleton_included m i x :
+Lemma singleton_included_l m i x :
   {[ i := x ]} ≼ m ↔ ∃ y, m !! i ≡ Some y ∧ Some x ≼ Some y.
 Proof.
   split.
@@ -333,13 +333,21 @@ Proof.
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
     + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
 Qed.
-Lemma singleton_included_exclusive m i x :
+Lemma singleton_included_exclusive_l m i x :
   Exclusive x → ✓ m →
   {[ i := x ]} ≼ m ↔ m !! i ≡ Some x.
 Proof.
-  intros ? Hm. rewrite singleton_included. split; last by eauto.
+  intros ? Hm. rewrite singleton_included_l. split; last by eauto.
   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.
+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.
+Qed.
 
 Global Instance singleton_cancelable i x :
   Cancelable (Some x) → Cancelable {[ i := x ]}.

theories/base_logic/lib/gen_heap.v

@@ -146,7 +146,7 @@ Section to_gen_heap.
   Lemma gen_heap_singleton_included σ l q v :
     {[l := (q, to_agree v)]} ≼ to_gen_heap σ → σ !! l = Some v.
   Proof.
-    rewrite singleton_included=> -[[q' av] []].
+    rewrite singleton_included_l=> -[[q' av] []].
     rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
     move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
   Qed.

theories/base_logic/lib/proph_map.v

@@ -102,7 +102,7 @@ Section to_proph_map.
   Lemma proph_map_singleton_included R p vs :
     {[p := Excl vs]} ≼ to_proph_map R → R !! p = Some vs.
   Proof.
-    rewrite singleton_included_exclusive; last by apply to_proph_map_valid.
+    rewrite singleton_included_exclusive_l; last by apply to_proph_map_valid.
     by rewrite leibniz_equiv_iff /to_proph_map lookup_fmap fmap_Some=> -[v' [-> [->]]].
   Qed.
 End to_proph_map.

theories/program_logic/ownp.v

@@ -90,8 +90,8 @@ Section lifting.
   Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
   Proof.
     iIntros "Hσ● Hσ◯". rewrite /ownP.
-    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_both_valid.
-    by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
+    by iDestruct (own_valid_2 with "Hσ● Hσ◯")
+      as %[->%Excl_included _]%auth_both_valid.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.