Merge branch 'ralf/list-singleton' into 'master'

All list "map singleton" lemmas consistently use `singletonM` in their name

Closes #309

See merge request iris/iris!476

CHANGELOG.md

@@ -220,18 +220,17 @@ Coq 8.10, 8.11, and 8.12 are newly supported by this release, and Coq 8.7 and
   `sts_op_auth_frag` → `sts_auth_frag_op`,
   `sts_op_auth_frag_up` → `sts_auth_frag_up_op`,
   `sts_op_frag` → `sts_frag_op`,
-  `list_op_length` → `list_length_op`.
-* Make list singleton lemmas consistent with gmap by dropping the `M` suffix of
-  `singleton`:
-  `elem_of_list_singletonM` → `elem_of_list_singleton`,
-  `list_lookup_singletonM` → `list_lookup_singleton`,
-  `list_lookup_singletonM_lt` → `list_lookup_singleton_lt`,
-  `list_lookup_singletonM_gt` → `list_lookup_singleton_gt`,
-  `list_lookup_singletonM_ne` → `list_lookup_singleton_ne`,
-  `list_singletonM_validN` → `list_singleton_validN`,
-  `list_singletonM_length` → `list_singleton_length`,
-  `list_alter_singletonM` → `list_alter_singleton`,
-  `list_singletonM_included` → `list_singleton_included`.
+  `list_op_length` → `list_length_op`,
+  `list_core_singletonM` → `list_singletonM_core`,
+  `list_op_singletonM` → `list_singletonM_op`.
+* All list "map singleton" lemmas consistently use `singletonM` in their name:
+  `list_singleton_valid` → `list_singletonM_valid`,
+  `list_singleton_core_id` → `list_singletonM_core_id`,
+  `list_singleton_snoc` → `list_singletonM_snoc`,
+  `list_singleton_updateP` → `list_singletonM_updateP`,
+  `list_singleton_updateP'` → `list_singletonM_updateP'`,
+  `list_singleton_update` → `list_singletonM_update`,
+  `list_alloc_singleton_local_update` → `list_alloc_singletonM_local_update`.
 * Add `list_singletonM_included` and `list_lookup_singletonM_{lt,gt}` lemmas
   about singletons in the list RA.
 * Add `list_core_id'`, a stronger version of `list_core_id` which only talks
@@ -260,15 +259,16 @@ s/\bsingleton_included_exclusive\b/singleton_included_exclusive_l/g
 # f_op/f_core renames
 s/\b(op|core)_singleton\b/singleton_\1/g
 s/\bdiscrete_fun_(op|core)_singleton\b/discrete_fun_singleton_\1/g
-s/\blist_(op|core)_singletonM\b/list_singleton_\1/g
 s/\bsts_op_(auth_frag|auth_frag_up|frag)\b/sts_\1_op/g
+s/\blist_(op|core)_singletonM\b/list_singletonM_\1/g
 s/\blist_op_length\b/list_length_op/g
-# list singleton renames
-s/\belem_of_list_singletonM\b/elem_of_list_singleton/g
-s/\blist_lookup_singletonM(|_lt|_gt|_ne)\b/list_lookup_singleton\1/g
-s/\blist_singletonM_(validN|length)\b/list_singleton_\1/g
-s/\blist_alter_singletonM\b/list_alter_singleton/g
-s/\blist_singletonM_included\b/list_singleton_included/g
+# list "singleton map" renames
+s/\blist_singleton_valid\b/list_singletonM_valid/g
+s/\blist_singleton_core_id\b/list_singletonM_core_id/g
+s/\blist_singleton_snoc\b/list_singletonM_snoc/g
+s/\blist_singleton_updateP\b/list_singletonM_updateP/g
+s/\blist_singleton_update\b/list_singletonM_update/g
+s/\blist_alloc_singleton_local_update\b/list_alloc_singletonM_local_update/g
 # inv renames
 s/\binv_sep(|_1|_2)\b/inv_split\1/g
 s/\binv_acc\b/inv_alter/g

theories/algebra/list.v

@@ -365,79 +365,79 @@ Section properties.
   Global Instance list_singletonM_proper i :
     Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
 
-  Lemma elem_of_list_singleton i z x : z ∈ ({[i := x]} : list A) → z = ε ∨ z = x.
+  Lemma elem_of_list_singletonM i z x : z ∈ ({[i := x]} : list A) → z = ε ∨ z = x.
   Proof.
     rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
   Qed.
-  Lemma list_lookup_singleton i x : ({[ i := x ]} : list A) !! i = Some x.
+  Lemma list_lookup_singletonM i x : ({[ i := x ]} : list A) !! i = Some x.
   Proof. induction i; by f_equal/=. Qed.
-  Lemma list_lookup_singleton_lt i i' x:
+  Lemma list_lookup_singletonM_lt i i' x:
     (i' < i)%nat → ({[ i := x ]} : list A) !! i' = Some ε.
   Proof. move: i'. induction i; intros [|i']; naive_solver auto with lia. Qed.
-  Lemma list_lookup_singleton_gt i i' x:
+  Lemma list_lookup_singletonM_gt i i' x:
     (i < i')%nat → ({[ i := x ]} : list A) !! i' = None.
   Proof. move: i'. induction i; intros [|i']; naive_solver auto with lia. Qed.
-  Lemma list_lookup_singleton_ne i j x :
+  Lemma list_lookup_singletonM_ne i j x :
     i ≠ j →
     ({[ i := x ]} : list A) !! j = None ∨ ({[ i := x ]} : list A) !! j = Some ε.
   Proof. revert j; induction i; intros [|j]; naive_solver auto with lia. Qed.
-  Lemma list_singleton_validN n i x : ✓{n} ({[ i := x ]} : list A) ↔ ✓{n} x.
+  Lemma list_singletonM_validN n i x : ✓{n} ({[ i := x ]} : list A) ↔ ✓{n} x.
   Proof.
     rewrite list_lookup_validN. split.
-    { move=> /(_ i). by rewrite list_lookup_singleton. }
+    { move=> /(_ i). by rewrite list_lookup_singletonM. }
     intros Hx j; destruct (decide (i = j)); subst.
-    - by rewrite list_lookup_singleton.
-    - destruct (list_lookup_singleton_ne i j x) as [Hi|Hi]; first done;
+    - by rewrite list_lookup_singletonM.
+    - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
         rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
   Qed.
-  Lemma list_singleton_valid  i x : ✓ ({[ i := x ]} : list A) ↔ ✓ x.
+  Lemma list_singletonM_valid  i x : ✓ ({[ i := x ]} : list A) ↔ ✓ x.
   Proof.
-    rewrite !cmra_valid_validN. by setoid_rewrite list_singleton_validN.
+    rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
   Qed.
-  Lemma list_singleton_length i x : length {[ i := x ]} = S i.
+  Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
   Proof.
     rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
   Qed.
 
-  Lemma list_singleton_core i (x : A) : core {[ i := x ]} ≡@{list A} {[ i := core x ]}.
+  Lemma list_singletonM_core i (x : A) : core {[ i := x ]} ≡@{list A} {[ i := core x ]}.
   Proof.
     rewrite /singletonM /list_singletonM.
     by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ∅).
   Qed.
-  Lemma list_singleton_op i (x y : A) :
+  Lemma list_singletonM_op i (x y : A) :
     {[ i := x ]} ⋅ {[ i := y ]} ≡@{list A} {[ i := x ⋅ y ]}.
   Proof.
     rewrite /singletonM /list_singletonM /=.
     induction i; constructor; rewrite ?left_id; auto.
   Qed.
-  Lemma list_alter_singleton f i x :
+  Lemma list_alter_singletonM f i x :
     alter f i ({[i := x]} : list A) = {[i := f x]}.
   Proof.
     rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
   Qed.
-  Global Instance list_singleton_core_id i (x : A) :
+  Global Instance list_singletonM_core_id i (x : A) :
     CoreId x → CoreId {[ i := x ]}.
-  Proof. by rewrite !core_id_total list_singleton_core=> ->. Qed.
-  Lemma list_singleton_snoc l x:
+  Proof. by rewrite !core_id_total list_singletonM_core=> ->. Qed.
+  Lemma list_singletonM_snoc l x:
     {[length l := x]} ⋅ l ≡ l ++ [x].
   Proof. elim: l => //= ?? <-. by rewrite left_id. Qed.
-  Lemma list_singleton_included i x l:
+  Lemma list_singletonM_included i x l:
     {[i := x]} ≼ l ↔ (∃ x', l !! i = Some x' ∧ x ≼ x').
   Proof.
     rewrite list_lookup_included. split.
-    { move /(_ i). rewrite list_lookup_singleton option_included_total.
+    { move /(_ i). rewrite list_lookup_singletonM option_included_total.
       naive_solver. }
     intros (y&Hi&?) j. destruct (Nat.lt_total j i) as [?|[->|?]].
-    - rewrite list_lookup_singleton_lt //.
+    - rewrite list_lookup_singletonM_lt //.
       destruct (lookup_lt_is_Some_2 l j) as [z Hz].
       { trans i; eauto using lookup_lt_Some. }
       rewrite Hz. by apply Some_included_2, ucmra_unit_least.
-    - rewrite list_lookup_singleton Hi. by apply Some_included_2.
-    - rewrite list_lookup_singleton_gt //. apply: ucmra_unit_least.
+    - rewrite list_lookup_singletonM Hi. by apply Some_included_2.
+    - rewrite list_lookup_singletonM_gt //. apply: ucmra_unit_least.
   Qed.
 
   (* Update *)
-  Lemma list_singleton_updateP (P : A → Prop) (Q : list A → Prop) x :
+  Lemma list_singletonM_updateP (P : A → Prop) (Q : list A → Prop) x :
     x ~~>: P → (∀ y, P y → Q [y]) → [x] ~~>: Q.
   Proof.
     rewrite !cmra_total_updateP=> Hup HQ n lf /list_lookup_validN Hv.
@@ -447,12 +447,12 @@ Section properties.
     apply list_lookup_validN=> i.
     move: (Hv i) Hv'. by destruct i, lf; rewrite /= ?right_id.
   Qed.
-  Lemma list_singleton_updateP' (P : A → Prop) x :
+  Lemma list_singletonM_updateP' (P : A → Prop) x :
     x ~~>: P → [x] ~~>: λ k, ∃ y, k = [y] ∧ P y.
-  Proof. eauto using list_singleton_updateP. Qed.
-  Lemma list_singleton_update x y : x ~~> y → [x] ~~> [y].
+  Proof. eauto using list_singletonM_updateP. Qed.
+  Lemma list_singletonM_update x y : x ~~> y → [x] ~~> [y].
   Proof.
-    rewrite !cmra_update_updateP; eauto using list_singleton_updateP with subst.
+    rewrite !cmra_update_updateP; eauto using list_singletonM_updateP with subst.
   Qed.
 
   Lemma app_updateP (P1 P2 Q : list A → Prop) l1 l2 :
@@ -476,7 +476,7 @@ Section properties.
     x ~~>: P1 → l ~~>: P2 → (∀ y k, P1 y → P2 k → Q (y :: k)) → x :: l ~~>: Q.
   Proof.
     intros. eapply (app_updateP _ _ _ [x]);
-      naive_solver eauto using list_singleton_updateP'.
+      naive_solver eauto using list_singletonM_updateP'.
   Qed.
   Lemma cons_updateP' (P1 : A → Prop) (P2 : list A → Prop) x l :
     x ~~>: P1 → l ~~>: P2 → x :: l ~~>: λ k, ∃ y k', k = y :: k' ∧ P1 y ∧ P2 k'.
@@ -523,13 +523,13 @@ Section properties.
   Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
 *)
 
-  Lemma list_alloc_singleton_local_update x l :
+  Lemma list_alloc_singletonM_local_update x l :
     ✓ x → (l, ε) ~l~> (l ++ [x], {[length l := x]}).
   Proof.
     move => ?.
     have -> : ({[length l := x]} ≡ {[length l := x]} ⋅ ε) by rewrite right_id.
-    rewrite -list_singleton_snoc. apply op_local_update => ??.
-    rewrite list_singleton_snoc app_validN cons_validN. split_and? => //; [| constructor].
+    rewrite -list_singletonM_snoc. apply op_local_update => ??.
+    rewrite list_singletonM_snoc app_validN cons_validN. split_and? => //; [| constructor].
     by apply cmra_valid_validN.
   Qed.