Commit d53af0f6 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/rename_op_core' into 'master'

make names of more `f_op`/`f_core` rewrite lemmas more consistent

See merge request iris/iris!403
parents 86b62616 63cc5199
......@@ -106,6 +106,48 @@ Coq development, but not every API-breaking change is listed. Changes marked
will fail. We provide one implementation using Ltac2 which works with Coq 8.11
and can be installed with opam; see
[iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
* Make names of `f_op`/`f_core` rewrite lemmas more consistent by always making
`_core`/`_op` the suffix:
`op_singleton` -> `singleton_op`, `core_singleton` -> `singleton_core`,
`discrete_fun_op_singleton` -> `discrete_fun_singleton_op`,
`discrete_fun_core_singleton` -> `discrete_fun_singleton_core`,
`list_core_singletonM` -> `list_singleton_core`,
`list_op_singletonM` -> `list_singleton_op`,
`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`.
The following `sed` script should perform most of the renaming (FIXME: incomplete)
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
```
sed -i -E '
# 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_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
' $(find theories -name "*.v")
```
**Changes in heap_lang:**
......
......@@ -84,7 +84,7 @@ Section cmra.
by apply ucmra_unit_validN.
Qed.
Lemma discrete_fun_core_singleton x (y : B x) :
Lemma discrete_fun_singleton_core x (y : B x) :
core (discrete_fun_singleton x y) discrete_fun_singleton x (core y).
Proof.
move=>x'; destruct (decide (x = x')) as [->|];
......@@ -94,9 +94,9 @@ Section cmra.
Global Instance discrete_fun_singleton_core_id x (y : B x) :
CoreId y CoreId (discrete_fun_singleton x y).
Proof. by rewrite !core_id_total discrete_fun_core_singleton=> ->. Qed.
Proof. by rewrite !core_id_total discrete_fun_singleton_core=> ->. Qed.
Lemma discrete_fun_op_singleton (x : A) (y1 y2 : B x) :
Lemma discrete_fun_singleton_op (x : A) (y1 y2 : B x) :
discrete_fun_singleton x y1 discrete_fun_singleton x y2 discrete_fun_singleton x (y1 y2).
Proof.
intros x'; destruct (decide (x' = x)) as [->|].
......
......@@ -284,23 +284,23 @@ Proof.
- by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id_L.
Qed.
Lemma core_singleton (i : K) (x : A) cx :
Lemma singleton_core (i : K) (x : A) cx :
pcore x = Some cx core {[ i := x ]} =@{gmap K A} {[ i := cx ]}.
Proof. apply omap_singleton. Qed.
Lemma core_singleton' (i : K) (x : A) cx :
Lemma singleton_core' (i : K) (x : A) cx :
pcore x Some cx core {[ i := x ]} @{gmap K A} {[ i := cx ]}.
Proof.
intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx').
intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (singleton_core _ _ cx').
Qed.
Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) :
core {[ i := x ]} =@{gmap K A} {[ i := core x ]}.
Proof. apply core_singleton. rewrite cmra_pcore_core //. Qed.
Lemma op_singleton (i : K) (x y : A) :
Proof. apply singleton_core. rewrite cmra_pcore_core //. Qed.
Lemma singleton_op (i : K) (x y : A) :
{[ i := x ]} {[ i := y ]} =@{gmap K A} {[ i := x y ]}.
Proof. by apply (merge_singleton _ _ _ x y). Qed.
Global Instance is_op_singleton i a a1 a2 :
IsOp a a1 a2 IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -op_singleton. Qed.
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -singleton_op. Qed.
Global Instance gmap_core_id m : ( x : A, CoreId x) CoreId m.
Proof.
......@@ -309,7 +309,7 @@ Proof.
Qed.
Global Instance gmap_singleton_core_id i (x : A) :
CoreId x CoreId {[ i := x ]}.
Proof. intros. by apply core_id_total, core_singleton'. Qed.
Proof. intros. by apply core_id_total, singleton_core'. Qed.
Lemma singleton_includedN_l n m i x :
{[ i := x ]} {n} m y, m !! i {n} Some y Some x {n} Some y.
......
......@@ -354,7 +354,7 @@ Section properties.
Lemma list_lookup_valid_Some l i x : l l !! i Some x x.
Proof. move=> /list_lookup_valid /(_ i)=> Hl Hi; move: Hl. by rewrite Hi. Qed.
Lemma list_op_length l1 l2 : length (l1 l2) = max (length l1) (length l2).
Lemma list_length_op l1 l2 : length (l1 l2) = max (length l1) (length l2).
Proof. revert l2. induction l1; intros [|??]; f_equal/=; auto. Qed.
Lemma replicate_valid n (x : A) : x replicate n x.
......@@ -365,75 +365,75 @@ Section properties.
Global Instance list_singletonM_proper i :
Proper (() ==> ()) (list_singletonM i) := ne_proper _.
Lemma elem_of_list_singletonM i z x : z ({[i := x]} : list A) z = ε z = x.
Lemma elem_of_list_singleton 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_singletonM i x : ({[ i := x ]} : list A) !! i = Some x.
Lemma list_lookup_singleton i x : ({[ i := x ]} : list A) !! i = Some x.
Proof. induction i; by f_equal/=. Qed.
Lemma list_lookup_singletonM_lt i i' x:
Lemma list_lookup_singleton_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_singletonM_gt i i' x:
Lemma list_lookup_singleton_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_singletonM_ne i j x :
Lemma list_lookup_singleton_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_singletonM_validN n i x : {n} ({[ i := x ]} : list A) {n} x.
Lemma list_singleton_validN n i x : {n} ({[ i := x ]} : list A) {n} x.
Proof.
rewrite list_lookup_validN. split.
{ move=> /(_ i). by rewrite list_lookup_singletonM. }
{ move=> /(_ i). by rewrite list_lookup_singleton. }
intros Hx j; destruct (decide (i = j)); subst.
- by rewrite list_lookup_singletonM.
- destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
- by rewrite list_lookup_singleton.
- destruct (list_lookup_singleton_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.
Proof.
rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
rewrite !cmra_valid_validN. by setoid_rewrite list_singleton_validN.
Qed.
Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
Lemma list_singleton_length i x : length {[ i := x ]} = S i.
Proof.
rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
Qed.
Lemma list_core_singletonM i (x : A) : core {[ i := x ]} @{list A} {[ i := core x ]}.
Lemma list_singleton_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_op_singletonM i (x y : A) :
Lemma list_singleton_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_singletonM f i x :
Lemma list_alter_singleton 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) :
CoreId x CoreId {[ i := x ]}.
Proof. by rewrite !core_id_total list_core_singletonM=> ->. Qed.
Proof. by rewrite !core_id_total list_singleton_core=> ->. Qed.
Lemma list_singleton_snoc l x:
{[length l := x]} l l ++ [x].
Proof. elim: l => //= ?? <-. by rewrite left_id. Qed.
Lemma list_singletonM_included i x l:
Lemma list_singleton_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_singletonM option_included_total.
{ move /(_ i). rewrite list_lookup_singleton option_included_total.
naive_solver. }
intros (y&Hi&?) j. destruct (Nat.lt_total j i) as [?|[->|?]].
- rewrite list_lookup_singletonM_lt //.
- rewrite list_lookup_singleton_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_singletonM Hi. by apply Some_included_2.
- rewrite list_lookup_singletonM_gt //. apply: ucmra_unit_least.
- rewrite list_lookup_singleton Hi. by apply Some_included_2.
- rewrite list_lookup_singleton_gt //. apply: ucmra_unit_least.
Qed.
(* Update *)
......
......@@ -213,7 +213,7 @@ Proof. rewrite namespace_map_valid_eq /=. split. done. by left. Qed.
Lemma namespace_map_data_op N a b :
namespace_map_data N (a b) = namespace_map_data N a namespace_map_data N b.
Proof.
by rewrite {2}/op /namespace_map_op /namespace_map_data /= -op_singleton left_id_L.
by rewrite {2}/op /namespace_map_op /namespace_map_data /= singleton_op left_id_L.
Qed.
Lemma namespace_map_data_mono N a b :
a b namespace_map_data N a namespace_map_data N b.
......
......@@ -327,14 +327,14 @@ Lemma sts_auth_frag_valid_inv s S T1 T2 :
Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
(** Op *)
Lemma sts_op_auth_frag s S T :
Lemma sts_auth_frag_op s S T :
s S closed S T sts_auth s sts_frag S T sts_auth s T.
Proof.
intros; split; [split|constructor; set_solver]; simpl.
- intros (?&?&?); by apply closed_disjoint with S.
- intros; split_and?; last constructor; set_solver.
Qed.
Lemma sts_op_auth_frag_up s T :
Lemma sts_auth_frag_up_op s T :
sts_auth s sts_frag_up s T sts_auth s T.
Proof.
intros; split; [split|constructor; set_solver]; simpl.
......@@ -346,7 +346,7 @@ Proof.
+ constructor; last set_solver. apply elem_of_up.
Qed.
Lemma sts_op_frag S1 S2 T1 T2 :
Lemma sts_frag_op S1 S2 T1 T2 :
T1 ## T2 sts.closed S1 T1 sts.closed S2 T2
sts_frag (S1 S2) (T1 T2) sts_frag S1 T1 sts_frag S2 T2.
Proof.
......@@ -357,7 +357,7 @@ Qed.
(* Notice that the following does *not* hold -- the composition of the
two closures is weaker than the closure with the itnersected token
set. Also see up_op.
Lemma sts_op_frag_up s T1 T2 :
Lemma sts_frag_up_op s T1 T2 :
T1 ## T2 → sts_frag_up s (T1 ∪ T2) ≡ sts_frag_up s T1 ⋅ sts_frag_up s T2.
*)
......
......@@ -190,7 +190,7 @@ Section gen_heap.
Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
Proof.
intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
op_singleton -pair_op agree_idemp.
singleton_op -pair_op agree_idemp.
Qed.
Global Instance mapsto_as_fractional l q v :
AsFractional (l {q} v) (λ q, l {q} v)%I q.
......@@ -200,7 +200,7 @@ Section gen_heap.
Proof.
apply wand_intro_r.
rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
f_equiv. rewrite auth_frag_valid op_singleton singleton_valid -pair_op.
f_equiv. rewrite auth_frag_valid singleton_op singleton_valid -pair_op.
by intros [_ ?%agree_op_invL'].
Qed.
......@@ -255,7 +255,7 @@ Section gen_heap.
iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
iAssert γm1 = γm2 %I as %->.
{ iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
rewrite singleton_valid. apply: agree_op_invL'. }
iDestruct (own_valid_2 with "Hm1 Hm2") as %?%namespace_map_token_valid_op.
iExists γm2. iFrame "Hγm2". rewrite namespace_map_token_union //. by iSplitL "Hm1".
......@@ -281,7 +281,7 @@ Section gen_heap.
iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
iAssert γm1 = γm2 %I as %->.
{ iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
rewrite singleton_valid. apply: agree_op_invL'. }
iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
......
......@@ -75,7 +75,7 @@ Proof. by intros n a a' Ha; apply discrete_fun_singleton_ne; rewrite Ha. Qed.
Lemma iRes_singleton_op γ a1 a2 :
iRes_singleton γ (a1 a2) iRes_singleton γ a1 iRes_singleton γ a2.
Proof.
by rewrite /iRes_singleton discrete_fun_op_singleton op_singleton cmra_transport_op.
rewrite /iRes_singleton discrete_fun_singleton_op singleton_op -cmra_transport_op //.
Qed.
(** ** Properties of [own] *)
......
......@@ -96,7 +96,7 @@ Section sts.
Lemma sts_ownS_op γ S1 S2 T1 T2 :
T1 ## T2 sts.closed S1 T1 sts.closed S2 T2
sts_ownS γ (S1 S2) (T1 T2) (sts_ownS γ S1 T1 sts_ownS γ S2 T2).
Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
Proof. intros. by rewrite /sts_ownS -own_op sts_frag_op. Qed.
Lemma sts_own_op γ s T1 T2 :
T1 ## T2 sts_own γ s (T1 T2) == sts_own γ s T1 sts_own γ s T2.
......@@ -104,7 +104,7 @@ Section sts.
Proof.
intros. rewrite /sts_own -own_op. iIntros "Hown".
iDestruct (own_valid with "Hown") as %Hval%sts_frag_up_valid.
rewrite -sts_op_frag.
rewrite -sts_frag_op.
- iApply (sts_own_weaken with "Hown"); first done.
+ split; apply sts.elem_of_up.
+ eapply sts.closed_op; apply sts.closed_up; set_solver.
......@@ -121,7 +121,7 @@ Section sts.
iIntros "Hφ". rewrite /sts_ctx /sts_own.
iMod (own_alloc (sts_auth s ( sts.tok s))) as (γ) "Hγ".
{ apply sts_auth_valid; set_solver. }
iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
iExists γ; iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
iMod (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
rewrite /sts_inv. iNext. iExists s. by iFrame.
Qed.
......@@ -139,8 +139,8 @@ Section sts.
iModIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
iIntros (s' T') "[% Hφ]".
iMod (own_update_2 with "Hγ Hγf") as "Hγ".
{ rewrite sts_op_auth_frag; [|done..]. by apply sts_update_auth. }
iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
{ rewrite sts_auth_frag_op; [|done..]. by apply sts_update_auth. }
iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
iModIntro. iNext. iExists s'; by iFrame.
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