Commit 032f365f authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:iris/iris into master.2

parents 95433e05 6b570757
......@@ -100,6 +100,9 @@ Changes in Coq:
steps that would require unlocking subterms. Every impure wp_ tactic executes
this tactic before doing anything else.
* Add `big_sepM_insert_acc`.
* The `_strong` lemmas (e.g. `own_alloc_strong`) work for all infinite
sets, instead of just for cofinite sets. The versions with cofinite
sets have been renamed to use the `_cofinite` suffix.
## Iris 3.1.0 (released 2017-12-19)
......
From iris.algebra Require Export cmra.
From stdpp Require Export gmap.
From stdpp Require Export list gmap.
From iris.algebra Require Import updates local_updates.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import proofmode_classes.
......@@ -354,29 +354,48 @@ Qed.
Section freshness.
Local Set Default Proof Using "Type*".
Context `{!Infinite K}.
Lemma alloc_updateP_strong (Q : gmap K A Prop) (I : gset K) m x :
x ( i, m !! i = None i I Q (<[i:=x]>m)) m ~~>: Q.
Lemma alloc_updateP_strong (Q : gmap K A Prop) (I : K Prop) m x :
pred_infinite I
x ( i, m !! i = None I i Q (<[i:=x]>m)) m ~~>: Q.
Proof.
intros ? HQ. apply cmra_total_updateP.
intros n mf Hm. set (i := fresh (I dom (gset K) (m mf))).
assert (i I i dom (gset K) m i dom (gset K) mf) as [?[??]].
{ rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ.
apply cmra_total_updateP. intros n mf Hm.
destruct (HP (dom (gset K) (m mf))) as [i [Hi1 Hi2]].
assert (m !! i = None).
{ eapply (not_elem_of_dom (D:=gset K)). revert Hi2.
rewrite dom_op not_elem_of_union. naive_solver. }
exists (<[i:=x]>m); split.
{ apply HQ; last done. by eapply not_elem_of_dom. }
rewrite insert_singleton_op; last by eapply not_elem_of_dom.
rewrite -assoc -insert_singleton_op;
last by eapply (not_elem_of_dom (D:=gset K)); rewrite dom_op not_elem_of_union.
- by apply HQ.
- rewrite insert_singleton_op //.
rewrite -assoc -insert_singleton_op;
last by eapply (not_elem_of_dom (D:=gset K)).
by apply insert_validN; [apply cmra_valid_validN|].
Qed.
Lemma alloc_updateP (Q : gmap K A Prop) m x :
x ( i, m !! i = None Q (<[i:=x]>m)) m ~~>: Q.
Proof. move=>??. eapply alloc_updateP_strong with (I:=); by eauto. Qed.
Lemma alloc_updateP_strong' m x (I : gset K) :
x m ~~>: λ m', i, i I m' = <[i:=x]>m m !! i = None.
Proof.
move=>??.
eapply alloc_updateP_strong with (I:=λ _, True);
eauto using pred_infinite_True.
Qed.
Lemma alloc_updateP_strong' m x (I : K Prop) :
pred_infinite I
x m ~~>: λ m', i, I i m' = <[i:=x]>m m !! i = None.
Proof. eauto using alloc_updateP_strong. Qed.
Lemma alloc_updateP' m x :
x m ~~>: λ m', i, m' = <[i:=x]>m m !! i = None.
Proof. eauto using alloc_updateP. Qed.
Lemma alloc_updateP_cofinite (Q : gmap K A Prop) (J : gset K) m x :
x ( i, m !! i = None i J Q (<[i:=x]>m)) m ~~>: Q.
Proof.
eapply alloc_updateP_strong.
apply (pred_infinite_set (C:=gset K)).
intros E. exists (fresh (J E)).
apply not_elem_of_union, is_fresh.
Qed.
Lemma alloc_updateP_cofinite' m x (J : gset K) :
x m ~~>: λ m', i, i J m' = <[i:=x]>m m !! i = None.
Proof. eauto using alloc_updateP_cofinite. Qed.
End freshness.
Lemma alloc_unit_singleton_updateP (P : A Prop) (Q : gmap K A Prop) u i :
......
......@@ -102,22 +102,31 @@ Section auth.
Global Instance own_mono' γ : Proper (flip () ==> ()) (auth_own γ).
Proof. intros a1 a2. apply auth_own_mono. Qed.
Lemma auth_alloc_strong N E t (G : gset gname) :
(f t) φ t ={E}= γ, ⌜γ G auth_ctx γ N f φ auth_own γ (f t).
Lemma auth_alloc_strong N E t (I : gname Prop) :
pred_infinite I
(f t) φ t ={E}= γ, I γ⌝ auth_ctx γ N f φ auth_own γ (f t).
Proof.
iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) I) as (γ) "[% Hγ]"; [done|done|].
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
{ iNext. rewrite /auth_inv. iExists t. by iFrame. }
eauto.
Qed.
Lemma auth_alloc_cofinite N E t (G : gset gname) :
(f t) φ t ={E}= γ, ⌜γ G auth_ctx γ N f φ auth_own γ (f t).
Proof.
intros ?. apply auth_alloc_strong=>//.
apply (pred_infinite_set (C:=gset gname)) => E'.
exists (fresh (G E')). apply not_elem_of_union, is_fresh.
Qed.
Lemma auth_alloc N E t :
(f t) φ t ={E}= γ, auth_ctx γ N f φ auth_own γ (f t).
Proof.
iIntros (?) "Hφ".
iMod (auth_alloc_strong N E t with "Hφ") as (γ) "[_ ?]"; eauto.
iMod (auth_alloc_cofinite N E t with "Hφ") as (γ) "[_ ?]"; eauto.
Qed.
Lemma auth_empty γ : (|==> auth_own γ ε)%I.
......
......@@ -108,7 +108,7 @@ Lemma slice_insert_empty E q f Q P :
slice N γ Q ?q box N (<[γ:=false]> f) (Q P).
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_strong ( Excl' false Excl' false,
iMod (own_alloc_cofinite ( Excl' false Excl' false,
Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
as (γ) "[Hdom Hγ]"; first done.
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
......
......@@ -62,15 +62,23 @@ Section proofs.
- iIntros "?". iApply "HP'". iApply "HP''". done.
Qed.
Lemma cinv_alloc_strong (G : gset gname) E N :
(|={E}=> γ, γ G cinv_own γ 1 P, P ={E}= cinv N γ P)%I.
Lemma cinv_alloc_strong (I : gname Prop) E N :
pred_infinite I
(|={E}=> γ, I γ cinv_own γ 1 P, P ={E}= cinv N γ P)%I.
Proof.
iMod (own_alloc_strong 1%Qp G) as (γ) "[Hfresh Hγ]"; first done.
iIntros (?). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|].
iExists γ; iIntros "!> {$Hγ $Hfresh}" (P) "HP".
iMod (inv_alloc N _ (P own γ 1%Qp)%I with "[HP]"); first by eauto.
iIntros "!>". iExists P. iSplit; last done. iIntros "!# !>"; iSplit; auto.
Qed.
Lemma cinv_alloc_cofinite (G : gset gname) E N :
(|={E}=> γ, γ G cinv_own γ 1 P, P ={E}= cinv N γ P)%I.
Proof.
apply cinv_alloc_strong. apply (pred_infinite_set (C:=gset gname))=> E'.
exists (fresh (G E')). apply not_elem_of_union, is_fresh.
Qed.
Lemma cinv_open_strong E N γ p P :
N E
cinv N γ P - cinv_own γ p ={E,E∖↑N}=
......@@ -88,7 +96,7 @@ Section proofs.
Lemma cinv_alloc E N P : P ={E}= γ, cinv N γ P cinv_own γ 1.
Proof.
iIntros "HP". iMod (cinv_alloc_strong E N) as (γ _) "[Hγ Halloc]".
iIntros "HP". iMod (cinv_alloc_cofinite E N) as (γ _) "[Hγ Halloc]".
iExists γ. iFrame "Hγ". by iApply "Halloc".
Qed.
......
......@@ -143,11 +143,12 @@ Qed.
(** ** Allocation *)
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc_strong a (G : gset gname) :
a (|==> γ, ⌜γ G own γ a)%I.
Lemma own_alloc_strong a (P : gname Prop) :
pred_infinite P
a (|==> γ, P γ⌝ own γ a)%I.
Proof.
intros Ha.
rewrite -(bupd_mono ( m, γ, γ G m = iRes_singleton γ a uPred_ownM m)%I).
intros HP Ha.
rewrite -(bupd_mono ( m, γ, P γ m = iRes_singleton γ a uPred_ownM m)%I).
- rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
......@@ -155,9 +156,18 @@ Proof.
- apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
Qed.
Lemma own_alloc_cofinite a (G : gset gname) :
a (|==> γ, ⌜γ G own γ a)%I.
Proof.
intros Ha.
apply (own_alloc_strong a (λ γ, γ G))=> //.
apply (pred_infinite_set (C:=gset gname)).
intros E. set (i := fresh (G E)).
exists i. apply not_elem_of_union, is_fresh.
Qed.
Lemma own_alloc a : a (|==> γ, own γ a)%I.
Proof.
intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_strong a ) //; [].
intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_cofinite a ) //; [].
apply bupd_mono, exist_mono=>?. eauto using and_elim_r.
Qed.
......
......@@ -37,9 +37,14 @@ Section saved_anything.
Global Instance saved_anything_proper γ : Proper (() ==> ()) (saved_anything_own γ).
Proof. solve_proper. Qed.
Lemma saved_anything_alloc_strong x (G : gset gname) :
Lemma saved_anything_alloc_strong x (I : gname Prop) :
pred_infinite I
(|==> γ, I γ⌝ saved_anything_own γ x)%I.
Proof. intros ?. by apply own_alloc_strong. Qed.
Lemma saved_anything_alloc_cofinite x (G : gset gname) :
(|==> γ, ⌜γ G saved_anything_own γ x)%I.
Proof. by apply own_alloc_strong. Qed.
Proof. by apply own_alloc_cofinite. Qed.
Lemma saved_anything_alloc x : (|==> γ, saved_anything_own γ x)%I.
Proof. by apply own_alloc. Qed.
......@@ -72,9 +77,14 @@ Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
Contractive (saved_prop_own γ).
Proof. solve_contractive. Qed.
Lemma saved_prop_alloc_strong `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
Lemma saved_prop_alloc_strong `{!savedPropG Σ} (I : gname Prop) (P: iProp Σ) :
pred_infinite I
(|==> γ, I γ⌝ saved_prop_own γ P)%I.
Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
Lemma saved_prop_alloc_cofinite `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
(|==> γ, ⌜γ G saved_prop_own γ P)%I.
Proof. iApply saved_anything_alloc_strong. Qed.
Proof. iApply saved_anything_alloc_cofinite. Qed.
Lemma saved_prop_alloc `{!savedPropG Σ} (P: iProp Σ) :
(|==> γ, saved_prop_own γ P)%I.
......@@ -99,9 +109,14 @@ Proof.
solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
Qed.
Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (G : gset gname) (Φ : A iProp Σ) :
Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (I : gname Prop) (Φ : A iProp Σ) :
pred_infinite I
(|==> γ, I γ⌝ saved_pred_own γ Φ)%I.
Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
Lemma saved_pred_alloc_cofinite `{!savedPredG Σ A} (G : gset gname) (Φ : A iProp Σ) :
(|==> γ, ⌜γ G saved_pred_own γ Φ)%I.
Proof. iApply saved_anything_alloc_strong. Qed.
Proof. iApply saved_anything_alloc_cofinite. Qed.
Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A iProp Σ) :
(|==> γ, saved_pred_own γ Φ)%I.
......
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