Commit 8f839433 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 0d88e833 695c9baa
...@@ -188,10 +188,10 @@ Section gmap. ...@@ -188,10 +188,10 @@ Section gmap.
by rewrite -big_sepM_delete. by rewrite -big_sepM_delete.
Qed. Qed.
Lemma big_sepM_fn_insert (Ψ : K A uPred M uPred M) (Φ : K uPred M) m i x P : Lemma big_sepM_fn_insert {B} (Ψ : K A B uPred M) (f : K B) m i x b :
m !! i = None m !! i = None
([ map] ky <[i:=x]> m, Ψ k y (<[i:=P]> Φ k)) ([ map] ky <[i:=x]> m, Ψ k y (<[i:=b]> f k))
⊣⊢ (Ψ i x P [ map] ky m, Ψ k y (Φ k)). ⊣⊢ (Ψ i x b [ map] ky m, Ψ k y (f k)).
Proof. Proof.
intros. rewrite big_sepM_insert // fn_lookup_insert. intros. rewrite big_sepM_insert // fn_lookup_insert.
apply sep_proper, big_sepM_proper; auto=> k y ??. apply sep_proper, big_sepM_proper; auto=> k y ??.
...@@ -301,10 +301,10 @@ Section gset. ...@@ -301,10 +301,10 @@ Section gset.
Lemma big_sepS_insert Φ X x : Lemma big_sepS_insert Φ X x :
x X ([ set] y {[ x ]} X, Φ y) ⊣⊢ (Φ x [ set] y X, Φ y). x X ([ set] y {[ x ]} X, Φ y) ⊣⊢ (Φ x [ set] y X, Φ y).
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed. Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_fn_insert (Ψ : A uPred M uPred M) Φ X x P : Lemma big_sepS_fn_insert {B} (Ψ : A B uPred M) f X x b :
x X x X
([ set] y {[ x ]} X, Ψ y (<[x:=P]> Φ y)) ([ set] y {[ x ]} X, Ψ y (<[x:=b]> f y))
⊣⊢ (Ψ x P [ set] y X, Ψ y (Φ y)). ⊣⊢ (Ψ x b [ set] y X, Ψ y (f y)).
Proof. Proof.
intros. rewrite big_sepS_insert // fn_lookup_insert. intros. rewrite big_sepS_insert // fn_lookup_insert.
apply sep_proper, big_sepS_proper; auto=> y ??. apply sep_proper, big_sepS_proper; auto=> y ??.
......
...@@ -110,7 +110,7 @@ Proof. ...@@ -110,7 +110,7 @@ Proof.
iAssert (barrier_ctx γ' l P)%I as "#?". iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. } { rewrite /barrier_ctx. by repeat iSplit. }
iAssert (sts_ownS γ' (i_states γ) {[Change γ]} iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
sts_ownS γ' low_states {[Send]})%I with "=>[-]" as "[Hr Hs]". sts_ownS γ' low_states {[Send]})%I with "|==>[-]" as "[Hr Hs]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver. + set_solver.
+ iApply (sts_own_weaken with "Hγ'"); + iApply (sts_own_weaken with "Hγ'");
...@@ -148,7 +148,7 @@ Proof. ...@@ -148,7 +148,7 @@ Proof.
iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"]. iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
{ iNext. rewrite {2}/barrier_inv /=. by iFrame. } { iNext. rewrite {2}/barrier_inv /=. by iFrame. }
iIntros "Hγ". iIntros "Hγ".
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "=>[Hγ]" as "Hγ". iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "|==>[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. } { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). auto. wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). auto.
- (* a High state: the comparison succeeds, and we perform a transition and - (* a High state: the comparison succeeds, and we perform a transition and
...@@ -185,7 +185,7 @@ Proof. ...@@ -185,7 +185,7 @@ Proof.
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto.
- iIntros "Hγ". - iIntros "Hγ".
iAssert (sts_ownS γ (i_states i1) {[Change i1]} iAssert (sts_ownS γ (i_states i1) {[Change i1]}
sts_ownS γ (i_states i2) {[Change i2]})%I with "=>[-]" as "[Hγ1 Hγ2]". sts_ownS γ (i_states i2) {[Change i2]})%I with "|==>[-]" as "[Hγ1 Hγ2]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver. + set_solver.
+ iApply (sts_own_weaken with "Hγ"); + iApply (sts_own_weaken with "Hγ");
......
...@@ -637,6 +637,11 @@ Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : C_scope. ...@@ -637,6 +637,11 @@ Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : C_scope.
Notation "( X ⊄ )" := (λ Y, X Y) (only parsing) : C_scope. Notation "( X ⊄ )" := (λ Y, X Y) (only parsing) : C_scope.
Notation "( ⊄ X )" := (λ Y, Y X) (only parsing) : C_scope. Notation "( ⊄ X )" := (λ Y, Y X) (only parsing) : C_scope.
Notation "X ⊆ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊆ Y ⊂ Z" := (X Y Y Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊂ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊂ Y ⊂ Z" := (X Y Y Z) (at level 70, Y at next level) : C_scope.
(** The class [Lexico A] is used for the lexicographic order on [A]. This order (** The class [Lexico A] is used for the lexicographic order on [A]. This order
is used to create finite maps, finite sets, etc, and is typically different from is used to create finite maps, finite sets, etc, and is typically different from
the order [()]. *) the order [()]. *)
......
...@@ -13,29 +13,31 @@ Section box_defs. ...@@ -13,29 +13,31 @@ Section box_defs.
Context `{boxG Λ Σ} (N : namespace). Context `{boxG Λ Σ} (N : namespace).
Notation iProp := (iPropG Λ Σ). Notation iProp := (iPropG Λ Σ).
Definition box_own_auth (γ : gname) (a : auth (option (excl bool))) : iProp := Definition slice_name := gname.
own γ (a, ).
Definition box_own_prop (γ : gname) (P : iProp) : iProp := Definition box_own_auth (γ : slice_name)
(a : auth (option (excl bool))) : iProp := own γ (a, ).
Definition box_own_prop (γ : slice_name) (P : iProp) : iProp :=
own γ (:auth _, Some (to_agree (Next (iProp_unfold P)))). own γ (:auth _, Some (to_agree (Next (iProp_unfold P)))).
Definition box_slice_inv (γ : gname) (P : iProp) : iProp := Definition slice_inv (γ : slice_name) (P : iProp) : iProp :=
( b, box_own_auth γ ( Excl' b) box_own_prop γ P if b then P else True)%I. ( b, box_own_auth γ ( Excl' b) box_own_prop γ P if b then P else True)%I.
Definition box_slice (γ : gname) (P : iProp) : iProp := Definition slice (γ : slice_name) (P : iProp) : iProp :=
inv N (box_slice_inv γ P). inv N (slice_inv γ P).
Definition box (f : gmap gname bool) (P : iProp) : iProp := Definition box (f : gmap slice_name bool) (P : iProp) : iProp :=
( Φ : gname iProp, ( Φ : slice_name iProp,
(P [ map] γ b f, Φ γ) (P [ map] γ b f, Φ γ)
[ map] γ b f, box_own_auth γ ( Excl' b) box_own_prop γ (Φ γ) [ map] γ b f, box_own_auth γ ( Excl' b) box_own_prop γ (Φ γ)
inv N (box_slice_inv γ (Φ γ)))%I. inv N (slice_inv γ (Φ γ)))%I.
End box_defs. End box_defs.
Instance: Params (@box_own_auth) 4. Instance: Params (@box_own_auth) 4.
Instance: Params (@box_own_prop) 4. Instance: Params (@box_own_prop) 4.
Instance: Params (@box_slice_inv) 4. Instance: Params (@slice_inv) 4.
Instance: Params (@box_slice) 5. Instance: Params (@slice) 5.
Instance: Params (@box) 5. Instance: Params (@box) 5.
Section box. Section box.
...@@ -46,13 +48,13 @@ Implicit Types P Q : iProp. ...@@ -46,13 +48,13 @@ Implicit Types P Q : iProp.
(* FIXME: solve_proper picks the eq ==> instance for Next. *) (* FIXME: solve_proper picks the eq ==> instance for Next. *)
Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ). Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (box_slice_inv γ). Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance box_slice_ne n γ : Proper (dist n ==> dist n) (box_slice N γ). Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f). Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance box_slice_persistent γ P : PersistentP (box_slice N γ P). Global Instance slice_persistent γ P : PersistentP (slice N γ P).
Proof. apply _. Qed. Proof. apply _. Qed.
(* This should go automatic *) (* This should go automatic *)
...@@ -95,7 +97,7 @@ Qed. ...@@ -95,7 +97,7 @@ Qed.
Lemma box_insert f P Q : Lemma box_insert f P Q :
box N f P ={N}=> γ, f !! γ = None box N f P ={N}=> γ, f !! γ = None
box_slice N γ Q box N (<[γ:=false]> f) (Q P). slice N γ Q box N (<[γ:=false]> f) (Q P).
Proof. Proof.
iIntros "H"; iDestruct "H" as {Φ} "[#HeqP Hf]". iIntros "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
iPvs (own_alloc_strong ( Excl' false Excl' false, iPvs (own_alloc_strong ( Excl' false Excl' false,
...@@ -103,7 +105,7 @@ Proof. ...@@ -103,7 +105,7 @@ Proof.
as {γ} "[Hdom Hγ]"; first done. as {γ} "[Hdom Hγ]"; first done.
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]". rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom. iDestruct "Hdom" as % ?%not_elem_of_dom.
iPvs (inv_alloc N _ (box_slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done. iPvs (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done.
{ iNext. iExists false; eauto. } { iNext. iExists false; eauto. }
iPvsIntro; iExists γ; repeat iSplit; auto. iPvsIntro; iExists γ; repeat iSplit; auto.
iNext. iExists (<[γ:=Q]> Φ); iSplit. iNext. iExists (<[γ:=Q]> Φ); iSplit.
...@@ -114,7 +116,7 @@ Qed. ...@@ -114,7 +116,7 @@ Qed.
Lemma box_delete f P Q γ : Lemma box_delete f P Q γ :
f !! γ = Some false f !! γ = Some false
box_slice N γ Q box N f P ={N}=> P', slice N γ Q box N f P ={N}=> P',
(P (Q P')) box N (delete γ f) P'. (P (Q P')) box N (delete γ f) P'.
Proof. Proof.
iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]". iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
...@@ -133,7 +135,7 @@ Qed. ...@@ -133,7 +135,7 @@ Qed.
Lemma box_fill f γ P Q : Lemma box_fill f γ P Q :
f !! γ = Some false f !! γ = Some false
box_slice N γ Q Q box N f P ={N}=> box N (<[γ:=true]> f) P. slice N γ Q Q box N f P ={N}=> box N (<[γ:=true]> f) P.
Proof. Proof.
iIntros {?} "(#Hinv & HQ & H)"; iDestruct "H" as {Φ} "[#HeqP Hf]". iIntros {?} "(#Hinv & HQ & H)"; iDestruct "H" as {Φ} "[#HeqP Hf]".
iInv N as {b'} "(Hγ & #HγQ & _)"; iTimeless "Hγ". iInv N as {b'} "(Hγ & #HγQ & _)"; iTimeless "Hγ".
...@@ -151,7 +153,7 @@ Qed. ...@@ -151,7 +153,7 @@ Qed.
Lemma box_empty f P Q γ : Lemma box_empty f P Q γ :
f !! γ = Some true f !! γ = Some true
box_slice N γ Q box N f P ={N}=> Q box N (<[γ:=false]> f) P. slice N γ Q box N f P ={N}=> Q box N (<[γ:=false]> f) P.
Proof. Proof.
iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]". iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
iInv N as {b} "(Hγ & #HγQ & HQ)"; iTimeless "Hγ". iInv N as {b} "(Hγ & #HγQ & HQ)"; iTimeless "Hγ".
...@@ -191,7 +193,7 @@ Lemma box_empty_all f P Q : ...@@ -191,7 +193,7 @@ Lemma box_empty_all f P Q :
Proof. Proof.
iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]". iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
iAssert ([ map] γ↦b f, Φ γ box_own_auth γ ( Excl' false) iAssert ([ map] γ↦b f, Φ γ box_own_auth γ ( Excl' false)
box_own_prop γ (Φ γ) inv N (box_slice_inv γ (Φ γ)))%I with "=>[Hf]" as "[HΦ ?]". box_own_prop γ (Φ γ) inv N (slice_inv γ (Φ γ)))%I with "|==>[Hf]" as "[HΦ ?]".
{ iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf". { iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
iAlways; iIntros {γ b ?} "(Hγ' & #$ & #$)". iAlways; iIntros {γ b ?} "(Hγ' & #$ & #$)".
assert (true = b) as <- by eauto. assert (true = b) as <- by eauto.
...@@ -207,4 +209,4 @@ Proof. ...@@ -207,4 +209,4 @@ Proof.
Qed. Qed.
End box. End box.
Typeclasses Opaque box_slice box. Typeclasses Opaque slice_name slice box.
...@@ -34,7 +34,7 @@ Qed. ...@@ -34,7 +34,7 @@ Qed.
(** Fairly explicit form of opening invariants *) (** Fairly explicit form of opening invariants *)
Lemma inv_open E N P : Lemma inv_open E N P :
nclose N E nclose N E
inv N P E', (E nclose N E' E' E) inv N P E', (E nclose N E' E)
|={E,E'}=> P ( P ={E',E}= True). |={E,E'}=> P ( P ={E',E}= True).
Proof. Proof.
rewrite /inv. iIntros {?} "Hinv". iDestruct "Hinv" as {i} "[% #Hi]". rewrite /inv. iIntros {?} "Hinv". iDestruct "Hinv" as {i} "[% #Hi]".
......
...@@ -41,11 +41,9 @@ Notation "|==> Q" := (pvs ⊤ ⊤ Q%I) ...@@ -41,11 +41,9 @@ Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
(at level 99, Q at level 200, format "|==> Q") : uPred_scope. (at level 99, Q at level 200, format "|==> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=> Q" := (P |={E1,E2}=> Q) Notation "P ={ E1 , E2 }=> Q" := (P |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200, (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
format "P ={ E1 , E2 }=> Q") : C_scope.
Notation "P ={ E }=> Q" := (P |={E}=> Q) Notation "P ={ E }=> Q" := (P |={E}=> Q)
(at level 99, E at level 50, Q at level 200, (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
format "P ={ E }=> Q") : C_scope.
Section pvs. Section pvs.
Context {Λ : language} {Σ : iFunctor}. Context {Λ : language} {Σ : iFunctor}.
......
...@@ -32,7 +32,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token := ...@@ -32,7 +32,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "#" s => tokenize_go s (TPersistent :: cons_name kn k) "" | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
| String "%" s => tokenize_go s (TPure :: cons_name kn k) "" | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
| String "*" s => tokenize_go s (TForall :: cons_name kn k) "" | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
| String "=" (String ">" s) => tokenize_go s (TPvs :: cons_name kn k) "" | String "|" (String "=" (String "=" (String ">" s))) =>
tokenize_go s (TPvs :: cons_name kn k) ""
| String a s => tokenize_go s k (String a kn) | String a s => tokenize_go s k (String a kn)
end. end.
Definition tokenize (s : string) : list token := tokenize_go s [] "". Definition tokenize (s : string) : list token := tokenize_go s [] "".
......
...@@ -100,7 +100,7 @@ Section iris. ...@@ -100,7 +100,7 @@ Section iris.
(True - P - inv N Q - True - R) P - Q - |={E}=> R. (True - P - inv N Q - True - R) P - Q - |={E}=> R.
Proof. Proof.
iIntros {?} "H HP HQ". iIntros {?} "H HP HQ".
iApply ("H" with "[#] HP =>[HQ] =>"). iApply ("H" with "[#] HP |==>[HQ] |==>").
- done. - done.
- by iApply inv_alloc. - by iApply inv_alloc.
- by iPvsIntro. - by iPvsIntro.
......
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