Commit 9833e872 authored by Ralf Jung's avatar Ralf Jung

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

parent fea0c2de
......@@ -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
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment