Commit 49f9097f authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'robbert/seal' into 'master'

Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.

See merge request !793
parents d080eb82 a3534b51
Pipeline #65899 passed with stage
in 9 minutes and 6 seconds
......@@ -5,6 +5,13 @@ lemma.
## Iris master
**General changes:**
- Rename "unsealing" lemmas from `_eq` to `_unseal`. This particularly
affects `envs_entails_eq`, which is commonly used in the definition of
custom proof mode tactics. All other unsealing lemmas should be internal, so
in principle you should not rely on them.
**Changes in `bi`:**
* Generalize `big_op` lemmas that were previously assuming `Absorbing`ness of
......
......@@ -28,7 +28,7 @@ tags: [
depends: [
"coq" { (>= "8.13" & < "8.16~") | (= "dev") }
"coq-stdpp" { (= "dev.2022-05-13.0.53c9d7f7") | (= "dev") }
"coq-stdpp" { (= "dev.2022-05-13.1.ebb89887") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
......
......@@ -35,12 +35,13 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
(at level 200, o at level 1, l at level 10, x at level 1, right associativity,
format "[^ o list] x ∈ l , P") : stdpp_scope.
Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K A M)
Local Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K A M)
(m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Local Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
Global Arguments big_opM {M} o {_ K _ _ A} _ _.
Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
Local Definition big_opM_unseal :
@big_opM = @big_opM_def := big_opM_aux.(seal_eq).
Global Instance: Params (@big_opM) 7 := {}.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
(at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
......@@ -49,23 +50,25 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
(at level 200, o at level 1, m at level 10, x at level 1, right associativity,
format "[^ o map] x ∈ m , P") : stdpp_scope.
Definition big_opS_def `{Monoid M o} `{Countable A} (f : A M)
Local Definition big_opS_def `{Monoid M o} `{Countable A} (f : A M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Local Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
Global Arguments big_opS {M} o {_ A _ _} _ _.
Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
Local Definition big_opS_unseal :
@big_opS = @big_opS_def := big_opS_aux.(seal_eq).
Global Instance: Params (@big_opS) 6 := {}.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o set] x ∈ X , P") : stdpp_scope.
Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A M)
Local Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Local Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Definition big_opMS := big_opMS_aux.(unseal).
Global Arguments big_opMS {M} o {_ A _ _} _ _.
Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
Local Definition big_opMS_unseal :
@big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
Global Instance: Params (@big_opMS) 6 := {}.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
......@@ -252,12 +255,12 @@ Proof. by apply big_opL_sep_zip_with. Qed.
Lemma big_opM_empty `{Countable K} {B} (f : K B M) :
([^o map] kx , f k x) = monoid_unit.
Proof. by rewrite big_opM_eq /big_opM_def map_to_list_empty. Qed.
Proof. by rewrite big_opM_unseal /big_opM_def map_to_list_empty. Qed.
Lemma big_opM_insert `{Countable K} {B} (f : K B M) (m : gmap K B) i x :
m !! i = None
([^o map] ky <[i:=x]> m, f k y) f i x `o` [^o map] ky m, f k y.
Proof. intros ?. by rewrite big_opM_eq /big_opM_def map_to_list_insert. Qed.
Proof. intros ?. by rewrite big_opM_unseal /big_opM_def map_to_list_insert. Qed.
Lemma big_opM_delete `{Countable K} {B} (f : K B M) (m : gmap K B) i x :
m !! i = Some x
......@@ -304,7 +307,7 @@ Section gmap.
( k x, m !! k = Some x R (f k x) (g k x))
R ([^o map] k x m, f k x) ([^o map] k x m, g k x).
Proof.
intros ?? Hf. rewrite big_opM_eq. apply (big_opL_gen_proper R); auto.
intros ?? Hf. rewrite big_opM_unseal. apply (big_opL_gen_proper R); auto.
intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list.
Qed.
......@@ -353,7 +356,7 @@ Section gmap.
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opM_map_to_list f m :
([^o map] kx m, f k x) [^o list] xk map_to_list m, f (xk.1) (xk.2).
Proof. rewrite big_opM_eq. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
Proof. rewrite big_opM_unseal. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
Lemma big_opM_singleton f i x : ([^o map] ky {[i:=x]}, f k y) f i x.
Proof.
......@@ -363,13 +366,13 @@ Section gmap.
Lemma big_opM_unit m : ([^o map] ky m, monoid_unit) (monoid_unit : M).
Proof.
by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_eq.
by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_unseal.
Qed.
Lemma big_opM_fmap {B} (h : A B) (f : K B M) m :
([^o map] ky h <$> m, f k y) ([^o map] ky m, f k (h y)).
Proof.
rewrite big_opM_eq /big_opM_def map_to_list_fmap big_opL_fmap.
rewrite big_opM_unseal /big_opM_def map_to_list_fmap big_opL_fmap.
by apply big_opL_proper=> ? [??].
Qed.
......@@ -445,7 +448,7 @@ Section gmap.
([^o map] kx m, f k x `o` g k x)
([^o map] kx m, f k x) `o` ([^o map] kx m, g k x).
Proof.
rewrite big_opM_eq /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??].
rewrite big_opM_unseal /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??].
Qed.
End gmap.
......@@ -483,7 +486,7 @@ Section gset.
( x, x X R (f x) (g x))
R ([^o set] x X, f x) ([^o set] x X, g x).
Proof.
rewrite big_opS_eq. intros ?? Hf. apply (big_opL_gen_proper R); auto.
rewrite big_opS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements.
Qed.
......@@ -514,10 +517,10 @@ Section gset.
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opS_elements f X :
([^o set] x X, f x) [^o list] x elements X, f x.
Proof. by rewrite big_opS_eq. Qed.
Proof. by rewrite big_opS_unseal. Qed.
Lemma big_opS_empty f : ([^o set] x , f x) = monoid_unit.
Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
Proof. by rewrite big_opS_unseal /big_opS_def elements_empty. Qed.
Lemma big_opS_insert f X x :
x X ([^o set] y {[ x ]} X, f y) (f x `o` [^o set] y X, f y).
......@@ -557,7 +560,7 @@ Section gset.
Lemma big_opS_unit X : ([^o set] y X, monoid_unit) (monoid_unit : M).
Proof.
by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_eq.
by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_unseal.
Qed.
Lemma big_opS_filter' (φ : A Prop) `{ x, Decision (φ x)} f X :
......@@ -605,7 +608,7 @@ Lemma big_opM_dom `{Countable K} {A} (f : K → M) (m : gmap K A) :
([^o map] k_ m, f k) ([^o set] k dom m, f k).
Proof.
induction m as [|i x ?? IH] using map_ind.
{ by rewrite big_opM_eq big_opS_eq dom_empty_L. }
{ by rewrite big_opM_unseal big_opS_unseal dom_empty_L. }
by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
Qed.
......@@ -620,7 +623,7 @@ Section gmultiset.
( x, x X R (f x) (g x))
R ([^o mset] x X, f x) ([^o mset] x X, g x).
Proof.
rewrite big_opMS_eq. intros ?? Hf. apply (big_opL_gen_proper R); auto.
rewrite big_opMS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements.
Qed.
......@@ -651,18 +654,18 @@ Section gmultiset.
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opMS_elements f X :
([^o mset] x X, f x) [^o list] x elements X, f x.
Proof. by rewrite big_opMS_eq. Qed.
Proof. by rewrite big_opMS_unseal. Qed.
Lemma big_opMS_empty f : ([^o mset] x , f x) = monoid_unit.
Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. Qed.
Proof. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_empty. Qed.
Lemma big_opMS_disj_union f X Y :
([^o mset] y X Y, f y) ([^o mset] y X, f y) `o` [^o mset] y Y, f y.
Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
Proof. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
Lemma big_opMS_singleton f x : ([^o mset] y {[+ x +]}, f y) f x.
Proof.
intros. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_singleton /= right_id.
intros. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_singleton /= right_id.
Qed.
Lemma big_opMS_insert f X x :
......@@ -679,12 +682,12 @@ Section gmultiset.
Lemma big_opMS_unit X : ([^o mset] y X, monoid_unit) (monoid_unit : M).
Proof.
by induction X using gmultiset_ind;
rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_eq.
rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_unseal.
Qed.
Lemma big_opMS_op f g X :
([^o mset] y X, f y `o` g y) ([^o mset] y X, f y) `o` ([^o mset] y X, g y).
Proof. by rewrite big_opMS_eq /big_opMS_def -big_opL_op. Qed.
Proof. by rewrite big_opMS_unseal /big_opMS_def -big_opL_op. Qed.
End gmultiset.
(** Commuting lemmas *)
......
......@@ -13,7 +13,8 @@ Qed.
Lemma big_opM_None {M : cmra} `{Countable K} {A} (f : K A option M) m :
([^op map] kx m, f k x) = None k x, m !! k = Some x f k x = None.
Proof.
induction m as [|i x m ? IH] using map_ind=> /=; first by rewrite big_opM_eq.
induction m as [|i x m ? IH] using map_ind=> /=.
{ by rewrite big_opM_empty. }
rewrite -None_equiv_eq big_opM_insert // None_equiv_eq op_None IH. split.
{ intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
intros Hm; split.
......@@ -23,7 +24,8 @@ Qed.
Lemma big_opS_None {M : cmra} `{Countable A} (f : A option M) X :
([^op set] x X, f x) = None x, x X f x = None.
Proof.
induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
induction X as [|x X ? IH] using set_ind_L.
{ by rewrite big_opS_empty. }
rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
Qed.
Lemma big_opMS_None {M : cmra} `{Countable A} (f : A option M) X :
......
......@@ -623,7 +623,7 @@ Proof.
right order, namely the order in which they appear in map_to_list. Here,
we achieve this by unfolding [big_opM] and doing induction over that list
instead. *)
rewrite big_opM_eq /big_opM_def -{2}(list_to_map_to_list m).
rewrite big_op.big_opM_unseal /big_op.big_opM_def -{2}(list_to_map_to_list m).
assert (NoDup (map_to_list m).*1) as Hnodup by apply NoDup_fst_map_to_list.
revert Hnodup. induction (map_to_list m) as [|[k x] l IH]; csimpl; first done.
intros [??]%NoDup_cons. rewrite IH //.
......
......@@ -330,12 +330,13 @@ Next Obligation.
- apply (contractive_S f), IH; auto with lia.
Qed.
Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A A)
Local Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A A)
`{!Contractive f} : A := compl (fixpoint_chain f).
Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
Local Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
Definition fixpoint := fixpoint_aux.(unseal).
Global Arguments fixpoint {A _ _} f {_}.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Local Definition fixpoint_unseal :
@fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Section fixpoint.
Context `{Cofe A, Inhabited A} (f : A A) `{!Contractive f}.
......@@ -346,7 +347,7 @@ Section fixpoint.
Lemma fixpoint_unfold : fixpoint f f (fixpoint f).
Proof.
apply equiv_dist=>n.
rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
rewrite fixpoint_unseal /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Qed.
......@@ -360,7 +361,7 @@ Section fixpoint.
Lemma fixpoint_ne (g : A A) `{!Contractive g} n :
( z, f z {n} g z) fixpoint f {n} fixpoint g.
Proof.
intros Hfg. rewrite fixpoint_eq /fixpoint_def
intros Hfg. rewrite fixpoint_unseal /fixpoint_def
(conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
rewrite Hfg; apply contractive_S, IH; auto using dist_S.
......
......@@ -7,54 +7,56 @@ From iris.prelude Require Import options.
Export invGS.
Import uPred.
Definition uPred_fupd_def `{!invGS Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
Local Definition uPred_fupd_def `{!invGS Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
wsat ownE E1 == (wsat ownE E2 P).
Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
Local Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
Definition uPred_fupd := uPred_fupd_aux.(unseal).
Global Arguments uPred_fupd {Σ _}.
Lemma uPred_fupd_eq `{!invGS Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
Local Lemma uPred_fupd_unseal `{!invGS Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
Lemma uPred_fupd_mixin `{!invGS Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
Proof.
split.
- rewrite uPred_fupd_eq. solve_proper.
- rewrite uPred_fupd_unseal. solve_proper.
- intros E1 E2 (E1''&->&?)%subseteq_disjoint_union_L.
rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
by iIntros "($ & $ & HE) !> !> [$ $] !> !>" .
- rewrite uPred_fupd_eq. iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
- rewrite uPred_fupd_eq. iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
- rewrite uPred_fupd_eq. iIntros (E1 E2 E3 P) "HP HwE".
- rewrite uPred_fupd_unseal.
iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
- rewrite uPred_fupd_unseal.
iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
- rewrite uPred_fupd_unseal. iIntros (E1 E2 E3 P) "HP HwE".
iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
- intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
- intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
iIntros "Hvs (Hw & HE1 &HEf)".
iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
iIntros "!> !>". by iApply "HP".
- rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
- rewrite uPred_fupd_unseal /uPred_fupd_def. by iIntros (????) "[HwP $]".
Qed.
Global Instance uPred_bi_fupd `{!invGS Σ} : BiFUpd (uPredI (iResUR Σ)) :=
{| bi_fupd_mixin := uPred_fupd_mixin |}.
Global Instance uPred_bi_bupd_fupd `{!invGS Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !> !>". Qed.
Global Instance uPred_bi_fupd_plainly `{!invGS Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
Proof.
split.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
- rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
iAssert ( P)%I as "#>HP".
{ by iMod ("H" with "[$]") as "(_ & _ & HP)". }
by iFrame.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q) "[H HQ] [Hw HE]".
- rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E P Q) "[H HQ] [Hw HE]".
iAssert ( P)%I as "#>HP".
{ by iMod ("H" with "HQ [$]") as "(_ & _ & HP)". }
by iFrame.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
- rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
iAssert ( P)%I as "#HP".
{ iNext. by iMod ("H" with "[$]") as "(_ & _ & HP)". }
iFrame. iIntros "!> !> !>". by iMod "HP".
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E A Φ) "HΦ [Hw HE]".
- rewrite uPred_fupd_unseal /uPred_fupd_def. iIntros (E A Φ) "HΦ [Hw HE]".
iAssert ( x : A, Φ x)%I as "#>HP".
{ iIntros (x). by iMod ("HΦ" with "[$Hw $HE]") as "(_&_&?)". }
by iFrame.
......@@ -66,7 +68,7 @@ Proof.
iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
iAssert (|={,E2}=> P)%I as "H".
{ iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd. }
rewrite uPred_fupd_eq /uPred_fupd_def.
rewrite uPred_fupd_unseal /uPred_fupd_def.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed.
......
......@@ -102,26 +102,27 @@ Section definitions.
ghost_map_auth (gen_heap_name hG) 1 σ
ghost_map_auth (gen_meta_name hG) 1 m.
Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
Local Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
l [gen_heap_name hG]{dq} v.
Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
Local Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
Definition mapsto := mapsto_aux.(unseal).
Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
Local Definition mapsto_unseal : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
Local Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
γm, l [gen_meta_name hG] γm own γm (reservation_map_token E).
Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
Local Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
Definition meta_token := meta_token_aux.(unseal).
Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
Local Definition meta_token_unseal :
@meta_token = @meta_token_def := meta_token_aux.(seal_eq).
(** TODO: The use of [positives_flatten] violates the namespace abstraction
(see the proof of [meta_set]. *)
Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
Local Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
γm, l [gen_meta_name hG] γm
own γm (reservation_map_data (positives_flatten N) (to_agree (encode x))).
Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
Local Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
Definition meta := meta_aux.(unseal).
Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
Local Definition meta_unseal : @meta = @meta_def := meta_aux.(seal_eq).
End definitions.
Global Arguments meta {L _ _ V Σ _ A _ _} l N x.
......@@ -147,37 +148,37 @@ Section gen_heap.
(** General properties of mapsto *)
Global Instance mapsto_timeless l dq v : Timeless (l {dq} v).
Proof. rewrite mapsto_eq. apply _. Qed.
Proof. rewrite mapsto_unseal. apply _. Qed.
Global Instance mapsto_fractional l v : Fractional (λ q, l {#q} v)%I.
Proof. rewrite mapsto_eq. apply _. Qed.
Proof. rewrite mapsto_unseal. apply _. Qed.
Global Instance mapsto_as_fractional l q v :
AsFractional (l {#q} v) (λ q, l {#q} v)%I q.
Proof. rewrite mapsto_eq. apply _. Qed.
Proof. rewrite mapsto_unseal. apply _. Qed.
Global Instance mapsto_persistent l v : Persistent (l ↦□ v).
Proof. rewrite mapsto_eq. apply _. Qed.
Proof. rewrite mapsto_unseal. apply _. Qed.
Lemma mapsto_valid l dq v : l {dq} v - ⌜✓ dq%Qp.
Proof. rewrite mapsto_eq. apply ghost_map_elem_valid. Qed.
Proof. rewrite mapsto_unseal. apply ghost_map_elem_valid. Qed.
Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l {dq1} v1 - l {dq2} v2 - ⌜✓ (dq1 dq2) v1 = v2.
Proof. rewrite mapsto_eq. apply ghost_map_elem_valid_2. Qed.
Proof. rewrite mapsto_unseal. apply ghost_map_elem_valid_2. Qed.
(** Almost all the time, this is all you really need. *)
Lemma mapsto_agree l dq1 dq2 v1 v2 : l {dq1} v1 - l {dq2} v2 - v1 = v2.
Proof. rewrite mapsto_eq. apply ghost_map_elem_agree. Qed.
Proof. rewrite mapsto_unseal. apply ghost_map_elem_agree. Qed.
Lemma mapsto_combine l dq1 dq2 v1 v2 :
l {dq1} v1 - l {dq2} v2 - l {dq1 dq2} v1 v1 = v2.
Proof. rewrite mapsto_eq. apply ghost_map_elem_combine. Qed.
Proof. rewrite mapsto_unseal. apply ghost_map_elem_combine. Qed.
Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
¬ (dq1 dq2) l1 {dq1} v1 - l2 {dq2} v2 - l1 l2.
Proof. rewrite mapsto_eq. apply ghost_map_elem_frac_ne. Qed.
Proof. rewrite mapsto_unseal. apply ghost_map_elem_frac_ne. Qed.
Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 v1 - l2 {dq2} v2 - l1 l2.
Proof. rewrite mapsto_eq. apply ghost_map_elem_ne. Qed.
Proof. rewrite mapsto_unseal. apply ghost_map_elem_ne. Qed.
(** Permanently turn any points-to predicate into a persistent
points-to predicate. *)
Lemma mapsto_persist l dq v : l {dq} v == l ↦□ v.
Proof. rewrite mapsto_eq. apply ghost_map_elem_persist. Qed.
Proof. rewrite mapsto_unseal. apply ghost_map_elem_persist. Qed.
(** Framing support *)
Global Instance frame_mapsto p l v q1 q2 RES :
......@@ -187,23 +188,23 @@ Section gen_heap.
(** General properties of [meta] and [meta_token] *)
Global Instance meta_token_timeless l N : Timeless (meta_token l N).
Proof. rewrite meta_token_eq. apply _. Qed.
Proof. rewrite meta_token_unseal. apply _. Qed.
Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
Proof. rewrite meta_eq. apply _. Qed.
Proof. rewrite meta_unseal. apply _. Qed.
Global Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
Proof. rewrite meta_eq. apply _. Qed.
Proof. rewrite meta_unseal. apply _. Qed.
Lemma meta_token_union_1 l E1 E2 :
E1 ## E2 meta_token l (E1 E2) - meta_token l E1 meta_token l E2.
Proof.
rewrite meta_token_eq /meta_token_def. intros ?. iDestruct 1 as (γm1) "[#Hγm Hm]".
rewrite meta_token_unseal /meta_token_def. intros ?. iDestruct 1 as (γm1) "[#Hγm Hm]".
rewrite reservation_map_token_union //. iDestruct "Hm" as "[Hm1 Hm2]".
iSplitL "Hm1"; eauto.
Qed.
Lemma meta_token_union_2 l E1 E2 :
meta_token l E1 - meta_token l E2 - meta_token l (E1 E2).
Proof.
rewrite meta_token_eq /meta_token_def.
rewrite meta_token_unseal /meta_token_def.
iIntros "(%γm1 & #Hγm1 & Hm1) (%γm2 & #Hγm2 & Hm2)".
iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
iDestruct (own_valid_2 with "Hm1 Hm2") as %?%reservation_map_token_valid_op.
......@@ -226,7 +227,7 @@ Section gen_heap.
Lemma meta_agree `{Countable A} l i (x1 x2 : A) :
meta l i x1 - meta l i x2 - x1 = x2.
Proof.
rewrite meta_eq /meta_def.
rewrite meta_unseal /meta_def.
iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)".
iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
......@@ -236,12 +237,13 @@ Section gen_heap.
Lemma meta_set `{Countable A} E l (x : A) N :
N E meta_token l E == meta l N x.
Proof.
rewrite meta_token_eq meta_eq /meta_token_def /meta_def.
rewrite meta_token_unseal meta_unseal /meta_token_def /meta_def.
iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
iApply (own_update with "Hm").
apply reservation_map_alloc; last done.
cut (positives_flatten N @{coPset} N); first by set_solver.
rewrite nclose_eq. apply elem_coPset_suffixes.
(* TODO: Avoid unsealing here. *)
rewrite namespaces.nclose_unseal. apply elem_coPset_suffixes.
exists 1%positive. by rewrite left_id_L.
Qed.
......@@ -250,7 +252,7 @@ Section gen_heap.
σ !! l = None
gen_heap_interp σ == gen_heap_interp (<[l:=v]>σ) l v meta_token l .
Proof.
iIntros (Hσl). rewrite /gen_heap_interp mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
iIntros (Hσl). rewrite /gen_heap_interp mapsto_unseal /mapsto_def meta_token_unseal /meta_token_def /=.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iMod (ghost_map_insert l with "Hσ") as "[Hσ Hl]"; first done.
iMod (own_alloc (reservation_map_token )) as (γm) "Hγm".
......@@ -279,7 +281,7 @@ Section gen_heap.
Lemma gen_heap_valid σ l dq v : gen_heap_interp σ - l {dq} v - ⌜σ !! l = Some v.
Proof.
iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
rewrite /gen_heap_interp mapsto_eq.
rewrite /gen_heap_interp mapsto_unseal.
by iDestruct (ghost_map_lookup with "Hσ Hl") as %?.
Qed.
......@@ -287,7 +289,7 @@ Section gen_heap.
gen_heap_interp σ - l v1 == gen_heap_interp (<[l:=v2]>σ) l v2.
Proof.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iIntros "Hl". rewrite /gen_heap_interp mapsto_eq /mapsto_def.