diff --git a/theories/escrows.v b/theories/escrows.v
index 76752ec6c1ea4f060f3b00eeeda91ed5e791505e..7b7d25389632ff53b0d63719d517abe45e492941 100644
--- a/theories/escrows.v
+++ b/theories/escrows.v
@@ -76,7 +76,7 @@ Section proof.
let Q := if b then Q0 else P0 in
(P ∗ P → False) ⊢ ([ex P0 ↠Q0] V ∗ ▷ ⎡P V⎤ ={↑escrowN}=∗ ▷ ⎡Q V⎤).
Proof.
- intros. iStartProof (uPred _). iIntros (V') "ND".
+ intros P Q. iStartProof (uPred _). iIntros (V') "ND".
rewrite /exchange /tc_opaque. iIntros (V0 ?) "(#[% Inv] & P) /=".
iAssert (inv escrowN (monPred_at P V ∨ monPred_at Q V))%I with "[Inv]" as "#Inv'".
{ destruct b; subst P Q; auto. by rewrite bi.or_comm. }
diff --git a/theories/examples/kvnode.v b/theories/examples/kvnode.v
index 1f6f2d84889d0c57a11f4bdaf74ae899f7961161..18ce452afcf874adbda27a2124f25ff989350cab 100644
--- a/theories/examples/kvnode.v
+++ b/theories/examples/kvnode.v
@@ -134,7 +134,7 @@ Section Interpretation.
[∗ list] i↦x ∈ locs, [XP x in (fun l => nth i l 0) <$> L | dataP' version (fun _ _ => R)]_R)%I.*)
Definition map_nth {A} i (m : gmap nat (list A)) d := (λ l, nth i l d) <$> m.
-
+
Definition versionP_fun n γ : interpC Σ versionProtocol -> interpC Σ versionProtocol := (λ R _ _ s v,
⌜(Z.of_nat s = v)%Z⌠∗
∃ L : gmap nat (list Z), ⌜map_size L 8 /\ ∃ vs, log_latest L (if even s then s else (s - 1)%nat) vs⌠∗
@@ -144,24 +144,14 @@ Section Interpretation.
Instance versionP_contractive n γ : Contractive (versionP_fun n γ).
Proof.
- repeat intro.
- apply sep_ne; first done.
- apply exist_ne; intro.
- apply sep_ne; first done.
- apply sep_ne; first done.
- apply big_opL_ne; [repeat intro | done].
- apply vGPS_RSP_contractive.
- apply dist_dist_later.
- repeat intro.
- apply exist_ne; intro.
- apply sep_ne; first done.
- apply vGPS_RSP_contractive; done.
+ repeat intro. unfold versionP_fun. do 9 f_equiv.
+ apply dist_dist_later=>????. unfold dataP'. by do 4 f_equiv.
Qed.
-
+
Definition versionP n γ : interpC Σ versionProtocol := fixpoint (versionP_fun n γ).
Definition dataP n γ := dataP' n (versionP n γ).
-
+
Lemma versionP_eq' n γ: versionP n γ ≡ (fun _ _ s v =>
⌜(Z.of_nat s = v)%Z⌠∗
∃ L : gmap nat (list Z), ⌜map_size L 8 /\ ∃ vs, log_latest L (if even s then s else (s - 1)%nat) vs⌠∗
@@ -254,7 +244,7 @@ Section proof.
apply big_sepL_persistent; intros.
apply _.
Qed.
-
+
Instance node_state_R_persistent L v n g: Persistent (node_state_R L v n g).
Proof.
apply sep_persistent; first apply _.
@@ -265,7 +255,7 @@ Section proof.
Qed.
Opaque seq.
-
+
Lemma log_latest_ord: ∀ m1 m2 n1 n2 v1 v2, m1 ⊑ m2 -> log_latest m1 n1 v1 -> log_latest m2 n2 v2 ->
(n1 <= n2)%nat.
Proof.
@@ -279,14 +269,14 @@ Section proof.
induction a; auto.
by rewrite Nat2Z.inj_succ Nat.even_succ Z.even_succ Zodd_even_bool IHa Nat.negb_even.
Qed.
-
+
Lemma mod_even: ∀ a : nat, (a mod 2 = if even a then 0 else 1)%nat.
Proof.
intro; apply Nat2Z.inj.
rewrite Z2Nat_inj_mod Zmod_even Nat2Z_inj_even.
destruct (even a); auto.
Qed.
-
+
Lemma fmap_nth_log_latest : ∀ {A} m n (v : list A) i d, log_latest m n v ->
log_latest (map_nth i m d) n (nth i v d).
Proof.
@@ -298,7 +288,7 @@ Section proof.
Qed.
Require Import Recdef.
-
+
Function make_log {A} (n : nat) (d : A) { measure id n } : gmap nat A :=
<[n := d]>match n with O => ∅ | _ => (make_log (n - 2) d) end.
Proof.
@@ -320,7 +310,7 @@ Section proof.
destruct (decide (n' = n + 1)%nat); last omega.
subst; rewrite Nat.even_add Heven in H; done.
Qed.
-
+
Lemma make_log_latest {A} (n : nat) (d : A): even n = true -> log_latest (make_log n d) n d.
Proof.
functional induction (make_log n d); intros.
@@ -376,7 +366,7 @@ Section proof.
- subst; rewrite minus_diag; auto.
- rewrite !nth_overflow; auto; simpl; omega.
Qed.
-
+
Lemma map_nth_app {A} m1 n m2 i (d : A) (Hm1: map_size m1 n)
(Hdom: map_relation (fun _ _ => true) (fun _ => false) (fun _ => false) m1 m2):
map_nth i (map_app m1 m2) d = if decide (i = n) then m2 else map_nth i m1 d.
@@ -392,8 +382,8 @@ Section proof.
rewrite lookup_fmap Hj1; done.
- destruct (decide _); first done.
rewrite lookup_fmap Hj1; done.
- Qed.
-
+ Qed.
+
Lemma log_latest_comprehend: forall n g l L0 v vals, even v = true ->
(([∗ list] i↦x ∈ vals, ∃ Li, ⌜log_latest Li v x ∧ map_nth i L0 0 ⊆ Li⌠∗ [XP ZplusPos i l in Li | dataP n g ]_R) -∗ ∃ L, ⌜map_size L (length vals) /\ log_latest L v vals ∧
∀ i, (i < length vals)%nat -> map_nth i L0 0 ⊆ map_nth i L 0⌠∗
@@ -434,8 +424,8 @@ Section proof.
iApply big_sepL_mono; last done.
intros ???%lookup_lt_Some; simpl; erewrite map_nth_app; try eassumption.
destruct (decide _); auto; omega.
- Qed.
-
+ Qed.
+
Lemma node_state_ord L1 L2 v1 v2 n g E (Hv: (v1 ≤ v2)%nat) (HE: ↑persist_locN ⊆ E):
(⌜map_size L1 8 ∧ (∃ vs, log_latest L1 v1 vs)⌠∗
([∗ list] i ∈ seq 0 8, [XP ZplusPos (Z.of_nat i) (ZplusPos data n) in map_nth i L1 0 | dataP n g ]_R) -∗
@@ -446,8 +436,7 @@ Section proof.
iIntros "[% H1] [% H2]".
iCombine "H1 H2" as "H"; rewrite -big_sepL_sepL.
iPoseProof (big_sepL_mono with "H") as "H".
- { intros; simpl.
- iApply GPS_SW_Readers_agree.
+ { intros; simpl. apply @GPS_SW_Readers_agree.
etrans; [apply namespaces.nclose_subseteq | done]. }
rewrite fupd_big_sepL; iMod "H"; iModIntro.
rewrite big_sepL_forall.
@@ -465,8 +454,8 @@ Section proof.
rewrite HL2 in Hin2; destruct Hin2 as [_ Hin2]; apply is_Some_None in Hin2; first done.
destruct Hin1 as [[] _]; first by rewrite HL1; eauto.
split; auto; omega.
- Qed.
-
+ Qed.
+
Instance prots_persistent: Persistent ([∗ list] i ∈ seq 0 8, [XP ZplusPos (Z.of_nat i) l in map_nth i L 0 | prot]_R)%I.
Proof.
intros; apply big_sepL_persistent; intros; apply _.
@@ -531,7 +520,7 @@ Section proof.
([∗ list] i↦x ∈ vals, ∃ Li,
⌜(∃ vi, v1 <= vi <= v' /\ log_latest Li vi x /\ map_nth i L1 0 ⊆ Li)%nat⌠∗
[XP ZplusPos (Z.of_nat i) (ZplusPos data n) in Li | dataP n g]_R) ∗
- ([∗ list] i ∈ seq (Z.to_nat i) (8 - Z.to_nat i),
+ ([∗ list] i ∈ seq (Z.to_nat i) (8 - Z.to_nat i),
[XP ZplusPos (Z.of_nat i) (ZplusPos data n) in map_nth i L1 0 | dataP n g]_R))%I).
iIntros "!#" (i ?) "!# (% & _ & H) Hpost".
iDestruct "H" as (vals) "(% & Hout & Hrest & H)".
@@ -611,7 +600,7 @@ Section proof.
match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
wp_seq; clear Hclosed.
match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
- wp_bind ([_]_at)%E; clear Hclosed.
+ wp_bind ([_]_at)%E; clear Hclosed.
wp_op.
iMod ("Hshift" with "HP") as (L2) "[oL2 Hclose]".
iApply (GPS_SW_Read (s := (v' - 1)%nat) (versionP n g) emp%I (fun s v => ⌜Z.of_nat s = v⌠∗
@@ -860,7 +849,7 @@ Section proof.
Qed.
Opaque replicate write mult.
-
+
Lemma writer_spec n L v g N (HN : base_mask ## ↑N):
{{{ ⎡PSCtx⎤ ∗ node_state_W L v n g ∗ inv N (∃ L, ⎡own g (Master (1/2) L)⎤) }}} writer #n
{{{ RET #();
@@ -971,7 +960,7 @@ Section proof.
Qed.
Opaque read.
-
+
Lemma reader_spec n L v g N (HN : base_mask ## ↑N):
{{{ ⎡PSCtx⎤ ∗ node_state_R L v n g ∗ inv N (∃ L, ⎡own g (Master (1/2) L)⎤) }}} reader #n
{{{ RET #(); ∃ L' v', ⌜L ⊆ L'⌠∗ node_state_R L' v' n g }}}.
@@ -998,7 +987,7 @@ Section proof.
iDestruct "H" as (?) "(% & H)"; iSplit; first auto.
iDestruct "H" as (???) "((% & % & % & % & %) & ? & ?)"; eauto.
Qed.
-
+
End proof.
End kvnode.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 9e8981bc5fbf2385f06a8007da52e5a5ab3ad791..1acf8cbd6f6f5b78112a7145ae7399ced575055e 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -458,17 +458,9 @@ Section TicketLock.
Global Instance NSP'_contractive P γ:
Contractive (NSP' P γ).
Proof.
- intros ? ? ? H b ? ? ?.
- destruct b; [done|].
- apply bi.sep_ne; [done|].
- apply bi.persistently_ne, bi.forall_ne =>? /=.
- repeat apply bi.impl_ne;[done|].
- apply bi.exist_ne => ?.
- apply exchange_ne; [done| |done].
- destruct n; [done|cbn].
- apply bi.sep_ne; [done|].
- apply vGPS_WSP_contractive.
- destruct n; [done|]. eapply dist_le; [done|omega].
+ intros ? ? ? H b ? ? ?. rewrite /NSP' /ES /escrow. destruct b; [done|].
+ do 8 f_equiv. destruct n; [done|cbn]. do 2 f_equiv.
+ by apply dist_dist_later.
Qed.
Program Definition NSP P (γ: gname) : interpC Σ natProtocol :=
@@ -736,7 +728,7 @@ Section TicketLock.
wp_lam. wp_bind ([_]_at)%E. wp_op.
- iApply (GPS_SW_Read_ex with "[$kI $NSW]"); [done|done|..].
+ iApply (GPS_SW_Read_ex (NSP P γ) with "[$kI $NSW]"); [done|done|..].
{ iNext.
(* iIntros (? ?). iViewUp. iIntros "#?". iModIntro. by iSplitL. *)
admit.
diff --git a/theories/fork.v b/theories/fork.v
index ecc24357e591f22250e8bdb6aa64f43606b20b30..f5d63618bad1556433e04b44e67ae5ebbb2fee5c 100644
--- a/theories/fork.v
+++ b/theories/fork.v
@@ -9,9 +9,8 @@ Lemma wp_fork `{fG : foundationG Σ} E e Φ :
↑physN ⊆ E →
⎡PSCtx⎤ ∗ ▷ Φ #() ∗ ▷ WP e {{ _, True }} ⊢ WP base.Fork e @ E {{ Φ }}.
Proof.
- intros.
rewrite WP_Def.wp_eq /WP_Def.wp_def.
- iStartProof (uPred _); iIntros (?) "/=".
+ iStartProof (uPred _); iIntros (??) "/=".
iIntros "(? & ? & ?)" (???) "?".
iApply program_logic.weakestpre.wp_mask_mono; first done.
iApply f_fork; iFrame.
diff --git a/theories/fractor.v b/theories/fractor.v
index 87bb07bc16b1df55f5ee32789e5d178935e389cf..37b9d1813470f06f363bcff209dc1982a84b98ba 100644
--- a/theories/fractor.v
+++ b/theories/fractor.v
@@ -13,14 +13,40 @@ Definition fracN : namespace := nroot .@ "fractor".
Section Fractor.
Context `{!foundationG Σ, !cinvG Σ}.
- Implicit Types (l: loc) (φ: loc → InfoT → iProp Σ)
- (Ψ: loc → frac → InfoT -> iProp Σ).
+ Implicit Types (l: loc) (φ: loc -c> InfoT -c> iProp Σ)
+ (Ψ: loc -c> frac -c> InfoT -c> iProp Σ).
Definition fractored l φ Ψ p: iProp Σ :=
(∃ X, Ψ l p X
∗ ∃ γ, Info l p (DecAgree (encode (X,γ)))
∗ cinv_own γ p ∗ cinv (fracN .@ l) γ (φ l X))%I.
+ Global Instance fractored_proper l : Proper ((≡) ==> (≡) ==> (=) ==> (≡)) (fractored l).
+ Proof.
+ intros ? ? H1 ? ? H2 ??->. rewrite /fractored. repeat f_equiv. exact: H2. exact: H1.
+ Qed.
+ Global Instance fractored_ne l n :
+ Proper ((dist n) ==> (dist n) ==> (=) ==> (dist n)) (fractored l).
+ Proof.
+ intros ?? H1 ? ? H2 ??->. rewrite /fractored. repeat f_equiv. exact: H2. exact: H1.
+ Qed.
+ Global Instance fractored_contractive l n :
+ Proper (dist_later n ==> (=) ==> (=) ==> dist n) (fractored l).
+ Proof.
+ intros ?? H1 ??-> ??->. rewrite /fractored. repeat (f_contractive || f_equiv).
+ exact: H1.
+ Qed.
+ Global Instance fractored_mono l φ :
+ Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
+ ==> (=) ==> (⊢))
+ (fractored l φ).
+ Proof. unfold fractored, pointwise_relation=>?????->. repeat f_equiv. auto. Qed.
+ Global Instance fractored_mono_flip l φ :
+ Proper (flip (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢))))
+ ==> (=) ==> flip (⊢))
+ (fractored l φ).
+ Proof. solve_proper. Qed.
+
Lemma fractor_mono l φ Ψ Ψ' p:
(∀ X, Ψ l p X → Ψ' l p X) ∗ fractored l φ Ψ p ⊢ fractored l φ Ψ' p.
Proof.
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index 56bf83d6a96f6488c71e0a5fd87f50c367a21f95..e0aee6227945b9f23aeae95215bb6e6e93791b52 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -88,16 +88,14 @@ Section Fractional.
by iFrame "o1 o2".
Qed.
-
Lemma GPS_FP_Init l s v (E : coPset)
(HEN : ↑physN ⊆ E):
{{{ ⎡PSCtx⎤ ∗ own_loc l ∗ ▷ F l s v ∗ ▷ F_past l s v }}}
([ #(LitLoc l) ]_na <- #(LitInt v)) @ E
{{{ RET #() ; vGPS_FP l s 1%Qp }}}.
Proof.
- intros.
iStartProof (uPred _).
- iIntros (V); iIntros "(#kI & oL & F & Fp)" (V2 ?) "Post".
+ iIntros (? V); iIntros "(#kI & oL & F & Fp)" (V2 ?) "Post".
rewrite WP_Def.wp_eq /=; iIntros (V3 ??) "kS".
unfold own_loc, own_loc_prim.
iDestruct "oL" as (h i) "(Alloc & Hist & Info)".
@@ -134,9 +132,8 @@ Section Fractional.
([ #(LitLoc l) ]_at) @ E
{{{ s' v, RET #(LitInt v) ; ⌜s ⊑ s'⌠∗ Q s' v }}}.
Proof.
- intros.
iStartProof (uPred _).
- iIntros (V); iIntros "(#kI & VS & VSDup & oP & oR)" (V2 ?) "Post".
+ iIntros (? V); iIntros "(#kI & VS & VSDup & oP & oR)" (V2 ?) "Post".
rewrite WP_Def.wp_eq vGPS_FP_eq /=; iIntros (V3 ??) "kS".
iMod (fractor_open with "[$oR]")
as (X) "(gpsRaw & RRaw & HClose)"; first exact HNl.
@@ -209,9 +206,8 @@ Section Fractional.
{{{ s' v, RET #(LitInt v) ;
⌜s ⊑ s'⌠∗ Q s' v }}}.
Proof.
- intros.
iStartProof (uPred _).
- iIntros (V') "(#kI & VS & VSDup & oP & oR & %)"; iIntros (Vb ?) "Post".
+ iIntros (? V') "(#kI & VS & VSDup & oP & oR & %)"; iIntros (Vb ?) "Post".
rewrite WP_Def.wp_eq vGPS_FP_eq /=; iIntros (Vc ??) "kS".
iMod (fractor_open with "[$oR]") as (X) "(gpsRaw & RRaw & HClose)"; first exact HNl.
@@ -272,9 +268,8 @@ Section Fractional.
([ #(LitLoc l) ]_at <- #(LitInt v)) @ E
{{{ RET #() ; Q s' }}}.
Proof.
- intros.
iStartProof (uPred _).
- iIntros (V); iIntros "(#kI & VS & oP & oW)" (V2 ?) "Post".
+ iIntros (? V); iIntros "(#kI & VS & oP & oW)" (V2 ?) "Post".
rewrite WP_Def.wp_eq vGPS_FP_eq /=; iIntros (V3 ??) "kS".
iMod (fractor_open' with "[$oW]")
as (X) "(gpsRaw & RRaw & HT & HClose)"; first auto.
@@ -325,8 +320,7 @@ Section Fractional.
{{{ s'' (v: Z), RET #(LitInt v) ;
⌜s ⊑ s''⌠∗ vGPS_FP l s'' q ∗ Q s'' v }}}.
Proof.
- intros.
- iStartProof (uPred _).
+ intros. iStartProof (uPred _).
rewrite vGPS_FP_eq WP_Def.wp_eq /=.
iIntros (V); iIntros "(#kI & VS & oP & oW)" (V2 ?) "Post".
iIntros (V3 ??) "kS".
@@ -382,9 +376,8 @@ Section Fractional.
{{{ s'' (b: bool) v, RET #(lit_of_bool b) ;
⌜s ⊑ s''⌠∗ (if b then Q s'' else R s'' v) }}}.
Proof.
- intros.
iStartProof (uPred _).
- iIntros (V); iIntros "(#kI & VS & VSF & VSDup & oP & oW)" (V2 ?) "Post".
+ iIntros (? V); iIntros "(#kI & VS & VSF & VSDup & oP & oW)" (V2 ?) "Post".
rewrite WP_Def.wp_eq vGPS_FP_eq /=; iIntros (V3 ??) "kS".
iMod ((fractor_open) with "[$oW]")
as (X) "(gpsRaw & RRaw & HClose)"; first exact HNl.
@@ -505,7 +498,7 @@ Section Fractional.
vGPS_FP l s q1 ∗ vGPS_FP l s q2 ⊣⊢ vGPS_FP l s (q1 + q2).
Proof. by rewrite GPS_FP_fractional. Qed.
- Lemma GPS_FP_dealloc l s V (E: coPset) (HNl: ↑fracN .@ l ⊆ E):
+ Lemma GPS_FP_dealloc l s (E: coPset) (HNl: ↑fracN .@ l ⊆ E):
vGPS_FP l s 1%Qp ={E}=∗ own_loc l.
Proof.
rewrite vGPS_FP_eq /vGPS_FP_def /own_loc /own_loc_prim
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index 65e702755e4af15368ebe311eab744568b81a7a7..9f8a424b9e8c493ce861d8e727602ae17a3b0504 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -99,9 +99,8 @@ Section Plain.
([ #l ]_na <- #v) @ E
{{{ RET #() ; vGPS_PP l p s }}}.
Proof.
- intros.
iStartProof (uPred _).
- iIntros (V) "(#kI & #kIP & oL & F & Fp)"; iIntros (V1 ?) "Post".
+ iIntros (? V) "(#kI & #kIP & oL & F & Fp)"; iIntros (V1 ?) "Post".
rewrite /own_loc /own_loc_prim.
iDestruct "oL" as (h i) "(Alloc & Hist & Info)".
rewrite valloc_local_eq /valloc_local_def /=.
@@ -143,9 +142,8 @@ Section Plain.
[ #l ]_at @ E
{{{ s' v, RET #v ; ⌜s ⊑ s'⌠∗ Q s' v }}}.
Proof.
- intros.
iStartProof (uPred _).
- iIntros (V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V2 ?) "Post".
+ iIntros (? V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V2 ?) "Post".
rewrite WP_Def.wp_eq vGPS_PP_eq /=; iIntros (V3 ??) "kS".
iMod (persistor_open with "[$oR]")
as (X) "(gpsRaw & RRaw & HClose)"; first auto.
@@ -213,9 +211,8 @@ Section Plain.
([ #l ]_at <- #v) @ E
{{{ RET #() ; vGPS_PP l p s' ∗ Q s' }}}.
Proof.
- intros.
iStartProof (uPred _).
- iIntros (V); iIntros "(#kI & VS & oP & oW)" (V2 ?) "Post".
+ iIntros (? V); iIntros "(#kI & VS & oP & oW)" (V2 ?) "Post".
rewrite WP_Def.wp_eq vGPS_PP_eq /=; iIntros (V3 ??) "kS".
iMod ((persistor_open') with "oW")
as (X) "(gpsRaw & RRaw & #HT & HClose)"; [done|].
@@ -267,9 +264,8 @@ Section Plain.
{{{ s'' (b: bool) v, RET #(lit_of_bool b) ;
⌜s ⊑ s''⌠∗ (if b then Q s'' else R s'' v )}}}.
Proof.
- intros.
iStartProof (uPred _).
- iIntros (V); iIntros "(#kI & VS & VSF & VSDup & oP & oW)" (V2 ?) "Post".
+ iIntros (? V); iIntros "(#kI & VS & VSF & VSDup & oP & oW)" (V2 ?) "Post".
rewrite WP_Def.wp_eq vGPS_PP_eq /=; iIntros (V3 ??) "kS".
iMod ((persistor_open) with "[$oW]")
as (X) "(gpsRaw & RRaw & HClose)"; first exact HNl.
@@ -377,8 +373,7 @@ Section Plain.
{{{ s'' (v: Z), RET #v ;
⌜s ⊑ s''⌠∗ vGPS_PP l p s'' ∗ Q s'' v }}}.
Proof.
- intros.
- iStartProof (uPred _).
+ intros. iStartProof (uPred _).
iIntros (V); iIntros "(#kI & VS & oP & oW)" (V2 ?) "Post".
rewrite WP_Def.wp_eq vGPS_PP_eq /=; iIntros (V3 ??) "kS".
iMod ((persistor_open) with "[$oW]")
diff --git a/theories/gps/shared.v b/theories/gps/shared.v
index 871fc954746d028a2e1f653694f3b5a5e9061ecf..e4db3acf6a58fb0936a28838a3c07759fde11a1a 100644
--- a/theories/gps/shared.v
+++ b/theories/gps/shared.v
@@ -396,19 +396,18 @@ Section Setup.
End Setup.
-Global Instance gps_inv_ne {prtcl} `{fG : foundationG Σ} {pf : protocol_facts prtcl} {gpsG : gpsG Σ prtcl pf}:
- Proper (dist n ==> dist n) (λ F : interpC Σ prtcl, (gps_inv F l γ γx)).
+Global Instance gps_inv_ne `{foundationG Σ} `{gpsG Σ prtcl} :
+ Proper (dist n ==> (=) ==> (=) ==> (=) ==> dist n) gps_inv.
Proof.
- intros n ? ? ? f1 f2 H.
- repeat apply bi.exist_ne => ?. rewrite /= /gps_inv /ProtoInv.
- repeat (apply (_ : Proper (_ ==> dist n) _); repeat intro).
- repeat (apply (_ : Proper (_ ==> _ ==> dist n) _); repeat intro); auto;
- apply big_opS_ne; auto => ?; apply H.
+ intros n f1 f2 Hf ??-> ??-> ??->.
+ rewrite /= /gps_inv /ProtoInv /BE_Inv /All_Inv.
+ repeat f_equiv; apply Hf.
Qed.
Global Instance ProtoInv_proper {Σ Prtcl PF}:
Proper ((≡) ==> (=) ==> (≡) ==> (=) ==> (≡)) (@ProtoInv Σ Prtcl PF).
-Proof. rewrite /ProtoInv /All_Inv /BE_Inv /sEx /sBE.
+Proof.
+ rewrite /ProtoInv /All_Inv /BE_Inv /sEx /sBE.
intros ? ? H1 ? ? H2 ? ? H3 ? ? H4.
subst. apply bi.sep_proper.
- rewrite big_opS_proper; last first.
@@ -419,6 +418,6 @@ Proof. rewrite /ProtoInv /All_Inv /BE_Inv /sEx /sBE.
+ f_equiv; set_solver.
Qed.
-Global Instance gps_inv_proper {Σ fG Prtcl PF gpsG}:
- Proper ((≡) ==> (=) ==> (=) ==> (=) ==> (≡)) (@gps_inv Σ fG Prtcl PF gpsG).
+Global Instance gps_inv_proper `{foundationG Σ} `{gpsG Σ prtcl} :
+ Proper ((≡) ==> (=) ==> (=) ==> (=) ==> (≡)) gps_inv.
Proof. rewrite /gps_inv. solve_proper. Qed.
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 450bdb1764a4a13df3062dbd46304900503fd4da..0abd730b5f02f772973a5250229ff42ac7ee8608 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -84,10 +84,9 @@ Section Gname_StrongSW.
([ #l ]_na <- #v) @ E
{{{ γ, RET #() ; Q γ ∗ vGPS_nFWP γ l (s γ) 1%Qp }}}.
Proof.
- intros.
iStartProof (uPred _).
rewrite vGPS_nFWP_eq /vGPS_nFWP_def WP_Def.wp_eq /=.
- iIntros (V); iIntros "(#kI & oL & F)" (V2 ?) "Post".
+ iIntros (? V); iIntros "(#kI & oL & F)" (V2 ?) "Post".
iIntros (V3 ? ?) "kS".
rewrite /own_loc /own_loc_prim valloc_local_eq /valloc_local_def /=.
iDestruct "oL" as (h i) "(% & Hist & Info)".
@@ -123,10 +122,9 @@ Section Gname_StrongSW.
{{{ v, RET #v ;
vGPS_nFWP γ l s q ∗ F_past γ l s v }}}.
Proof.
- intros.
iStartProof (uPred _).
rewrite vGPS_nFWP_eq WP_Def.wp_eq /=.
- iIntros (V); iIntros "(#kI & VSDup & oW)" (V2 ?) "Post".
+ iIntros (? V); iIntros "(#kI & VSDup & oW)" (V2 ?) "Post".
iIntros (V3 ??) "kS".
iMod (fractor_open with "[$oW]")
as (X) "(gpsRaw & WRaw & HClose)"; first auto.
@@ -155,11 +153,8 @@ Section Gname_StrongSW.
vGPS_nFWP γ l s (q1 + q2) ⊢ vGPS_nFWP γ l s q1 ∗ vGPS_nFRP γ l s q2.
Proof.
rewrite vGPS_nFWP_eq vGPS_nFRP_eq /vGPS_nFWP_def /vGPS_nFRP_def /=.
- split => ?. iStartProof (uPred _).
+ iStartProof (uPred _). iIntros (V) "oW".
rewrite /gpsSWnRaw /WriterSWnRaw /=.
- iIntros "oW".
- unfold bi_sep; simpl; unfold sbi_sep; simpl.
- rewrite monPred_sep_eq /=.
iApply fractor_splitjoin.
iApply (fractor_mono with "[$oW]").
iIntros (X) "oW".
@@ -173,8 +168,7 @@ Section Gname_StrongSW.
Lemma GPS_nFWP_Writer_Reader_join γ l s1 s2 q1 q2:
vGPS_nFWP γ l s1 q1 ∗ vGPS_nFRP γ l s2 q2 ⊢ vGPS_nFWP γ l s1 (q1 + q2).
Proof.
- constructor => V.
- iIntros "(o1 & o2)". iCombine "o1" "o2" as "oW".
+ iStartProof (uPred _). iIntros (V) "(o1 & o2)". iCombine "o1" "o2" as "oW".
rewrite vGPS_nFWP_eq vGPS_nFRP_eq fractor_splitjoin; last auto.
iApply (fractor_mono with "[$oW]").
by iIntros (X) "(oW & _)".
@@ -183,8 +177,8 @@ Section Gname_StrongSW.
Lemma GPS_nFRP_gname_agree γ1 γ2 l s1 s2 q1 q2:
vGPS_nFRP γ1 l s1 q1 ∗ vGPS_nFRP γ2 l s2 q2 ⊢ ⌜γ1 = γ2âŒ.
Proof.
- constructor => V.
- rewrite vGPS_nFRP_eq /bi_sep /= /sbi_sep /= monPred_sep_eq /= fractor_join_l. iIntros "oR".
+ iStartProof (uPred _). iIntros (V) "oR".
+ rewrite vGPS_nFRP_eq /= fractor_join_l.
iDestruct (fractor_drop with "oR") as (X) "[oR1 oR2]".
iDestruct "oR1" as (γ_x1) "[% _]".
iDestruct "oR2" as (γ_x2) "[% _]".
@@ -194,21 +188,19 @@ Section Gname_StrongSW.
Lemma GPS_nFWP_gname_agree γ1 γ2 l s1 s2 q1 q2:
vGPS_nFWP γ1 l s1 q1 ∗ vGPS_nFRP γ2 l s2 q2 ⊢ ⌜γ1 = γ2âŒ.
Proof.
- constructor => V.
- rewrite vGPS_nFWP_eq vGPS_nFRP_eq /bi_sep /= /sbi_sep /= monPred_sep_eq /= fractor_join_l. iIntros "oW".
+ iStartProof (uPred _). iIntros (V) "oW".
+ rewrite vGPS_nFWP_eq vGPS_nFRP_eq /= fractor_join_l.
iDestruct (fractor_drop with "oW") as (X) "[oW oR]".
iDestruct "oW" as (γ_x1) "[% _]".
iDestruct "oR" as (γ_x2) "[% _]".
subst X. apply encode_inj in H0. by inversion H0.
Qed.
- Lemma GPS_nFRP_join_l γ l s1 s2 q1 q2 V:
- vGPS_nFRP γ l s1 q1 V ∗ vGPS_nFRP γ l s2 q2 V ⊢ vGPS_nFRP γ l s1 (q1 + q2) V.
+ Lemma GPS_nFRP_join_l γ l s1 s2 q1 q2 :
+ vGPS_nFRP γ l s1 q1 ∗ vGPS_nFRP γ l s2 q2 ⊢ vGPS_nFRP γ l s1 (q1 + q2).
Proof.
- iIntros "[oR1 oR2]". iCombine "oR1" "oR2" as "oR".
- rewrite vGPS_nFRP_eq fractor_join_l.
- iApply (fractor_mono with "[$oR]").
- by iIntros (X) "[R1 R2]".
+ iStartProof (uPred _). iIntros (V) "oR". rewrite vGPS_nFRP_eq fractor_join_l.
+ iApply (fractor_mono with "[$oR]"). by iIntros (X) "[R1 R2]".
Qed.
Lemma GPS_nFWP_join_writer γ l s1 s2 q1 q2:
@@ -217,10 +209,10 @@ Section Gname_StrongSW.
exact: GPS_nFWP_Writer_Reader_join.
Qed.
- Lemma GPS_nFWP_writer_exclusive γ1 γ2 l s1 s2 q1 q2 V:
- vGPS_nFWP γ1 l s1 q1 V ∗ vGPS_nFWP γ2 l s2 q2 V ⊢ False.
+ Lemma GPS_nFWP_writer_exclusive γ1 γ2 l s1 s2 q1 q2 :
+ vGPS_nFWP γ1 l s1 q1 ∗ vGPS_nFWP γ2 l s2 q2 ⊢ False.
Proof.
- rewrite vGPS_nFWP_eq fractor_join_l. iIntros "oW".
+ iStartProof (uPred _). iIntros (V) "oW". rewrite vGPS_nFWP_eq fractor_join_l.
iDestruct (fractor_drop with "oW") as (X) "[oW1 oW2]".
iDestruct "oW1" as (γ_x1) "[% oW1]".
iDestruct "oW2" as (γ_x2) "[% oW2]".
@@ -230,17 +222,18 @@ Section Gname_StrongSW.
iApply (Writer_Exclusive with "[$oW1 $oW2]").
Qed.
- Lemma GPS_nFWP_join_writer_2 γ1 γ2 l s1 s2 q1 q2 V:
- vGPS_nFWP γ1 l s1 q1 V ∗ vGPS_nFRP γ2 l s2 q2 V ⊢ vGPS_nFWP γ1 l s1 (q1 + q2) V.
+ Lemma GPS_nFWP_join_writer_2 γ1 γ2 l s1 s2 q1 q2:
+ vGPS_nFWP γ1 l s1 q1 ∗ vGPS_nFRP γ2 l s2 q2 ⊢ vGPS_nFWP γ1 l s1 (q1 + q2).
Proof.
- iIntros "oW". iDestruct (GPS_nFWP_gname_agree with "oW") as %?.
+ iStartProof (uPred _). iIntros (V) "oW".
+ iDestruct (GPS_nFWP_gname_agree with "oW") as %?.
subst γ2. iApply (GPS_nFWP_join_writer with "oW").
Qed.
- Global Instance GPS_nFRP_fractional' γ l s V:
- Fractional (λ q, vGPS_nFRP γ l s q V).
+ Global Instance GPS_nFRP_fractional γ l s:
+ Fractional (vGPS_nFRP γ l s).
Proof.
- intros q1 q2. rewrite vGPS_nFRP_eq. iSplit.
+ intros q1 q2. iStartProof (uPred _). iIntros (V). rewrite vGPS_nFRP_eq. iSplit.
- iIntros "oR". iApply fractor_splitjoin.
iApply (fractor_mono with "[$oR]").
iIntros (?) "#?". by iSplit.
@@ -250,17 +243,8 @@ Section Gname_StrongSW.
iApply (fractor_mono with "[$oR]"). by iIntros (X) "[R1 R2]".
Qed.
- Global Instance GPS_nFRP_fractional γ l s:
- Fractional (vGPS_nFRP γ l s).
- Proof.
- intros q1 q2. constructor => V.
- rewrite GPS_nFRP_fractional'.
- unfold bi_sep; simpl; unfold sbi_sep; simpl.
- rewrite monPred_sep_eq; done.
- Qed.
-
- Global Instance GPS_nFRP_exists_fractional' l γ V:
- Fractional (λ q, (∃ s, vGPS_nFRP γ l s q)%I V).
+ Global Instance GPS_nFRP_exists_fractional l γ:
+ Fractional (λ q, (∃ s, vGPS_nFRP γ l s q)%I).
Proof.
intros q1 q2. iSplit.
- iIntros "oR". iDestruct "oR" as (s) "oR".
@@ -269,24 +253,14 @@ Section Gname_StrongSW.
- iIntros "(oR1 & oR2)".
iDestruct "oR1" as (s1) "oR1".
iDestruct "oR2" as (s2) "oR2".
- iPoseProof (GPS_nFRP_join_l γ l s1 s2 q1 q2 V) as "HJ".
- iPoseProof ("HJ" with "[$oR1 $oR2]") as "oR".
+ iPoseProof (GPS_nFRP_join_l γ l s1 s2 q1 q2 with "[$oR1 $oR2]") as "oR".
by iExists _.
Qed.
- Global Instance GPS_nFRP_exists_fractional l γ:
- Fractional (λ q, (∃ s, vGPS_nFRP γ l s q)%I).
+ Lemma GPS_nFWP_dealloc γ l s (E: coPset) (HNl: ↑fracN .@ l ⊆ E):
+ vGPS_nFWP γ l s 1%Qp ={E}=∗ own_loc l.
Proof.
- intros q1 q2. constructor => V.
- rewrite GPS_nFRP_exists_fractional'.
- unfold bi_sep; simpl; unfold sbi_sep; simpl.
- rewrite monPred_sep_eq; done.
- Qed.
-
- Lemma GPS_nFWP_dealloc γ l s V (E: coPset) (HNl: ↑fracN .@ l ⊆ E):
- vGPS_nFWP γ l s 1%Qp V ={E}=∗ own_loc l V.
- Proof.
- iIntros "FP".
+ iStartProof (uPred _). iIntros (V) "FP".
rewrite vGPS_nFWP_eq.
iMod (fractor_dealloc with "FP") as (n i) "(Info & WR & Inv)"; first auto.
iDestruct "WR" as (γ_x) "(% & WA)".
@@ -303,9 +277,9 @@ Section Gname_StrongSW.
rewrite -H elem_of_map_gset. by exists (s, (v, Vr)).
Qed.
- Lemma GPS_nFRP_exists_mult_joinL l (n: positive) q γ V:
- ([∗ list] _ ∈ seq 0 (Pos.to_nat n), ∃ s, vGPS_nFRP γ l s q) V
- ⊢ ∃ s, vGPS_nFRP γ l s (Pos2Qp n * q) V.
+ Lemma GPS_nFRP_exists_mult_joinL l (n: positive) q γ:
+ ([∗ list] _ ∈ seq 0 (Pos.to_nat n), ∃ s, vGPS_nFRP γ l s q)
+ ⊢ ∃ s, vGPS_nFRP γ l s (Pos2Qp n * q).
Proof.
rewrite -(big_sepL_mult_fractional
(Φ := (λ q, (∃ s, vGPS_nFRP γ l s q)%I))); last lia.
@@ -314,31 +288,21 @@ Section Gname_StrongSW.
Lemma GPS_nFRP_join γ l s q1 q2:
vGPS_nFRP γ l s q1 ∗ vGPS_nFRP γ l s q2 ⊢ vGPS_nFRP γ l s (q1 + q2).
- Proof.
- by rewrite fractional.
- Qed.
+ Proof. by rewrite fractional. Qed.
Lemma GPS_nFRP_split γ l s q1 q2:
vGPS_nFRP γ l s (q1 + q2) ⊢ vGPS_nFRP γ l s q1 ∗ vGPS_nFRP γ l s q2.
- Proof.
- by rewrite fractional.
- Qed.
+ Proof. by rewrite fractional. Qed.
Lemma GPS_nFRP_mult_splitL γ l s (n: positive) q:
vGPS_nFRP γ l s (Pos2Qp n * q)
⊢ [∗ list] _ ∈ seq 0 (Pos.to_nat n), vGPS_nFRP γ l s q.
- Proof.
- rewrite -{1}(Pos2Nat.id n).
- rewrite big_sepL_mult_fractional; [auto|lia].
- Qed.
+ Proof. rewrite -{1}(Pos2Nat.id n) big_sepL_mult_fractional; [auto|lia]. Qed.
Lemma GPS_nFRP_mult_joinL γ l s (n: positive) q:
([∗ list] _ ∈ seq 0 (Pos.to_nat n), vGPS_nFRP γ l s q)
⊢ vGPS_nFRP γ l s (Pos2Qp n * q).
- Proof.
- rewrite -{2}(Pos2Nat.id n).
- rewrite big_sepL_mult_fractional; [auto|lia].
- Qed.
+ Proof. rewrite -{2}(Pos2Nat.id n) big_sepL_mult_fractional; [auto|lia]. Qed.
Lemma GPS_nFWP_mult_splitL_1 γ l s n:
vGPS_nFWP γ l s 1
@@ -360,9 +324,9 @@ Section Gname_StrongSW.
([ #l ]_at <- #v) @ E
{{{ RET #() ; vGPS_nFWP γ l s' q ∗ Q s' }}}.
Proof.
- intros. iStartProof (uPred _).
+ iStartProof (uPred _).
rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VS & oP & oW)"; iIntros (V1 ?) "Post"; iIntros (V2 ??) "kS".
+ iIntros (? V) "(#kI & VS & oP & oW)"; iIntros (V1 ?) "Post"; iIntros (V2 ??) "kS".
rewrite vGPS_nFWP_eq.
iMod (fractor_open with "[$oW]")
as (X) "(gpsRaw & WRaw & HClose)"; first auto.
@@ -391,17 +355,16 @@ Section Gname_StrongSW.
Lemma GPS_nFRP_PrtSeen γ l s q:
vGPS_nFRP γ l s q ⊢ PrtSeen γ s.
Proof.
- constructor => V.
+ iStartProof (uPred _). iIntros (V).
iIntros "oR". rewrite vGPS_nFRP_eq. iDestruct "oR" as (X) "[oR ?]".
- iDestruct "oR" as (γ_x) "[? $]".
+ iDestruct "oR" as (γ_x) "[? H]". iDestruct "H" as (V') "H". eauto.
Qed.
Lemma GPS_nFWP_PrtSeen γ l s q:
vGPS_nFWP γ l s q ⊢ PrtSeen γ s.
Proof.
- constructor => V.
- iIntros "oR". rewrite vGPS_nFWP_eq. iDestruct "oR" as (X) "[oR ?]".
- iDestruct "oR" as (γ_x) "[? WA]".
+ iStartProof (uPred _). iIntros (V) "oR". rewrite vGPS_nFWP_eq.
+ iDestruct "oR" as (X) "[oR ?]". iDestruct "oR" as (γ_x) "[? WA]".
iDestruct "WA" as (v V_0 ζ) "(vS & oW & _ & oW3 & oW4)".
iExists V_0, v. iFrame "vS oW3".
Qed.
@@ -409,11 +372,9 @@ Section Gname_StrongSW.
Lemma GPS_nFRP_PrtSeen_update γ l q s1 s2 (Le: s1 ⊑ s2):
vGPS_nFRP γ l s1 q ∗ PrtSeen γ s2 ⊢ vGPS_nFRP γ l s2 q.
Proof.
- constructor => V.
- iIntros "[oR oS]". rewrite vGPS_nFRP_eq. iDestruct "oR" as (X) "[oR Inv]".
- iDestruct "oR" as (γ_x) "[oX oS1]".
- iExists X. iFrame "Inv".
- iExists γ_x. by iSplit.
+ iStartProof (uPred _). iIntros (V) "[oR oS]". rewrite vGPS_nFRP_eq.
+ iDestruct "oR" as (X) "[oR Inv]". iDestruct "oR" as (γ_x) "[oX oS1]".
+ iExists X. iFrame "Inv". iExists γ_x. by iSplit.
Qed.
Lemma GPS_nFRP_Read' l γ q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -428,13 +389,11 @@ Section Gname_StrongSW.
{{{ s' v, RET #v ;
⌜s ⊑ s'⌠∗ Q s' v }}}.
Proof.
- intros.
iStartProof (uPred _).
rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ iIntros (? V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
setoid_rewrite H1; setoid_rewrite H2.
- rewrite vGPS_nFRP_eq.
- iMod (fractor_open with "[$oR]")
+ rewrite vGPS_nFRP_eq. iMod (fractor_open with "[$oR]")
as (X) "(gpsRaw & RRaw & HClose)"; first exact HNl.
iDestruct "RRaw" as (γ_x) "(% & RA)".
@@ -494,10 +453,10 @@ Section Gname_StrongSW.
{{{ s' v, RET #v ;
⌜s1 ⊑ s' ∧ s2 ⊑ s'⌠∗ Q s' v }}}.
Proof.
- intros.
iStartProof (uPred _).
- rewrite vGPS_nFRP_eq WP_Def.wp_eq /=.
- iIntros (V') "(#kI & VS & VSDup & oP & % & oR & oS2)"; iIntros (Vb ?) "Post"; iIntros (Vc ??) "kS".
+ rewrite WP_Def.wp_eq vGPS_nFRP_eq /=.
+ iIntros (? V'); iIntros "(#kI & VS & VSDup & oP & % & oR & oS2)" (Vb ?) "Post";
+ iIntros (Vc ??) "kS".
iMod (fractor_open with "[$oR]") as (X) "(gpsRaw & RRaw & HClose)"; first exact HNl.
@@ -587,10 +546,10 @@ Section Gname_StrongSW.
{{{ s' v, RET #v ;
⌜s ⊑ s'⌠∗ Q s' v }}}.
Proof.
- intros.
iStartProof (uPred _).
rewrite vGPS_nFRP_eq WP_Def.wp_eq /=.
- iIntros (V') "(#kI & VS & VSDup & oP & % & oR)"; iIntros (Vb ?) "Post"; iIntros (Vc ??) "kS".
+ iIntros (? V'); iIntros "(#kI & VS & VSDup & oP & % & oR)" (Vb ?) "Post";
+ iIntros (Vc ??) "kS".
iMod (fractor_open with "[$oR]")
as (X) "(gpsRaw & RRaw & HClose)"; first exact HNl.
@@ -640,7 +599,6 @@ Section Gname_StrongSW.
iApply (fupd_mask_mono _ _ (Q s' v)); last by iApply "VS"; iFrame.
solve_ndisj.
Qed.
-
End Gname_StrongSW.
Section Gname_StrongSW_2.
@@ -697,51 +655,34 @@ Section Gname_StrongSW_Param.
∃ (γ_x: gname),
⌜n = encode (p,γ,γ_x)⌠∗ gps_inv (IP γ) l γ γ_x.
- Definition ReaderSWpnRaw p γ s V l n : iProp :=
+ Definition ReaderSWpnRaw p γ s l n : vProp Σ :=
∃ (γ_x: gname),
- ⌜n = encode (p,γ,γ_x)⌠∗ PrtSeen γ s V.
+ ⌜n = encode (p,γ,γ_x)⌠∗ PrtSeen γ s.
- Definition WriterSWpnRaw p γ s V l n : iProp :=
+ Definition WriterSWpnRaw p γ s l n : vProp Σ :=
∃ (γ_x: gname),
- ⌜n = encode (p,γ,γ_x)⌠∗ WAEx l γ γ_x s V.
+ ⌜n = encode (p,γ,γ_x)⌠∗ WAEx l γ γ_x s.
- Definition GPS_nRSP γ l p s V : iProp :=
- persisted l (gpsSWpnRaw p γ) (ReaderSWpnRaw p γ s V).
-
- Definition GPS_nWSP γ l p s V : iProp :=
- persisted l (gpsSWpnRaw p γ) (WriterSWpnRaw p γ s V).
-
- Definition vPred_GPS_nRSP_mono γ l p s:
- Proper ((⊑) ==> (⊢)) (GPS_nRSP γ l p s).
- Proof.
- intros V V' Mono.
- iIntros "RP". iDestruct "RP" as (X) "(RPV & ?)".
- iDestruct "RPV" as (γ_x) "(? & RA)".
- iExists X. iFrame. iExists γ_x. by iFrame.
- Qed.
-
- Canonical Structure vGPS_nRSP γ l p s :=
- MonPred _ (vPred_GPS_nRSP_mono γ l p s).
+ Program Definition vGPS_nRSP_def γ l p s : vProp Σ :=
+ MonPred (λ V, persisted l (gpsSWpnRaw p γ) (λ l X, ReaderSWpnRaw p γ s l X V)) _.
+ Next Obligation. solve_proper. Qed.
+ Definition vGPS_nRSP_aux : seal vGPS_nRSP_def. by eexists. Qed.
+ Definition vGPS_nRSP := unseal vGPS_nRSP_aux.
+ Definition vGPS_nRSP_eq : vGPS_nRSP = _ := seal_eq _.
Global Instance vGPS_nRSP_persistent γ l p s
: Persistent (vGPS_nRSP γ l p s).
Proof.
- rewrite /Persistent /bi_persistently. split => ? /=.
- rewrite /sbi_persistently /= monPred_persistently_eq /=.
- apply persistor_persistent => ?. apply _.
+ rewrite /Persistent vGPS_nRSP_eq. iStartProof (uPred _). iIntros (V).
+ iApply persistent.
Qed.
- Definition vPred_GPS_nWSP_mono γ l p s:
- Proper ((⊑) ==> (⊢)) (GPS_nWSP γ l p s).
- Proof.
- intros V V' Mono.
- iIntros "WP". iDestruct "WP" as (X) "(WPV & ?)".
- iDestruct "WPV" as (γ_x) "(? & WA)".
- iExists X. iFrame. iExists γ_x. by iFrame.
- Qed.
-
- Canonical Structure vGPS_nWSP γ l p s :=
- MonPred _ (vPred_GPS_nWSP_mono γ l p s).
+ Program Definition vGPS_nWSP_def γ l p s : vProp Σ :=
+ MonPred (λ V, persisted l (gpsSWpnRaw p γ) (λ l X, WriterSWpnRaw p γ s l X V)) _.
+ Next Obligation. solve_proper. Qed.
+ Definition vGPS_nWSP_aux : seal vGPS_nWSP_def. by eexists. Qed.
+ Definition vGPS_nWSP := unseal vGPS_nWSP_aux.
+ Definition vGPS_nWSP_eq : vGPS_nWSP = _ := seal_eq _.
Lemma GPS_nSW_Init_strong l p (s: gname -> pr_state Prtcl) v
(Q : gname -> vPred) (E : coPset)
@@ -752,10 +693,9 @@ Section Gname_StrongSW_Param.
([ #l ]_na <- #v) @ E
{{{ γ, RET #() ; Q γ }}}%stdpp.
Proof.
- intros.
iStartProof (uPred _).
- rewrite valloc_local_eq WP_Def.wp_eq /=.
- iIntros (?) "(#kI & #kIp & oL & VS)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite valloc_local_eq WP_Def.wp_eq vGPS_nWSP_eq /=.
+ iIntros (Φ V) "(#kI & #kIp & oL & VS)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
setoid_rewrite H1; setoid_rewrite H2.
iDestruct "oL" as (h i) "(Alloc & Hist & Info)".
@@ -766,7 +706,7 @@ Section Gname_StrongSW_Param.
iNext.
iIntros (V' γ γ_x) "(#Le & kS & oI & ex & #oR & oW)".
iMod (persistor_inv_alloc' E i (encode (p,γ,γ_x)) l
- (gpsSWpnRaw p γ) (WriterSWpnRaw p γ (s γ) V')
+ (gpsSWpnRaw p γ) (λ l X, WriterSWpnRaw p γ (s γ) l X V')
with "[$Info $kI $kIp]") as "[WP HClose]"; [auto|auto|..].
iMod ("VS" $! γ _ with "Le [- Post HClose oI kS]") as "(F & Fp & Q)".
{ iApply "WP".
@@ -788,10 +728,9 @@ Section Gname_StrongSW_Param.
([ #l ]_at <- #v) @ E
{{{ RET #() ; vGPS_nRSP γ l p s' ∗ Q γ s' }}}%stdpp.
Proof.
- intros.
iStartProof (uPred _).
- rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VS & oP & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite WP_Def.wp_eq vGPS_nWSP_eq vGPS_nRSP_eq /=.
+ iIntros (? V) "(#kI & VS & oP & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
iMod ((persistor_open') with "[$oW]")
as (X) "(gpsRaw & WRaw & #HT & HClose)"; first auto.
iDestruct "WRaw" as (γ_x) "(% & WA)".
@@ -828,10 +767,9 @@ Section Gname_StrongSW_Param.
{{{ v, RET #v ;
vGPS_nWSP γ l p s ∗ F_past γ l s v }}}%stdpp.
Proof.
- intros.
iStartProof (uPred _).
- rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VSDup & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite WP_Def.wp_eq /= vGPS_nWSP_eq.
+ iIntros (? V) "(#kI & VSDup & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
iMod ((persistor_open) with "[$oW]")
as (X) "(gpsRaw & WRaw & HClose)"; first auto.
iDestruct "WRaw" as (γ_x) "(% & WA)".
@@ -868,10 +806,9 @@ Section Gname_StrongSW_Param.
{{{ s' v, RET #v ;
⌜s ⊑ s'⌠∗ Q s' v }}}%stdpp.
Proof.
- intros.
iStartProof (uPred _).
- rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite WP_Def.wp_eq /= vGPS_nRSP_eq.
+ iIntros (? V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
iMod ((persistor_open) with "[$oR]")
as (X) "(gpsRaw & RRaw & HClose)"; first auto.
iDestruct "RRaw" as (γ_x) "(% & RA)".
@@ -888,7 +825,7 @@ Section Gname_StrongSW_Param.
iDestruct ("VS" $! _ Hs' j with "[%]") as "[VS|VS]"; last by iRight.
{ etrans; eauto. }
iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
- iMod ("HClose" $! (ReaderSWpnRaw p γ s' j0) with "[oI oR']").
+ iMod ("HClose" $! (λ l X, ReaderSWpnRaw p γ s' l X j0) with "[oI oR']").
{ iSplit.
+ iNext. iExists γ_x. by iFrame "oI".
+ iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
@@ -921,10 +858,10 @@ Section Gname_StrongSW_Param.
solve_ndisj.
Qed.
- Lemma GPS_nSW_Writer_Reader γ l p s V:
- vGPS_nWSP γ l p s V ⊢ vGPS_nWSP γ l p s V ∗ vGPS_nRSP γ l p s V.
+ Lemma GPS_nSW_Writer_Reader γ l p s:
+ vGPS_nWSP γ l p s ⊢ vGPS_nWSP γ l p s ∗ vGPS_nRSP γ l p s.
Proof.
- iIntros "oW".
+ iStartProof (uPred _). iIntros (V) "oW". rewrite vGPS_nWSP_eq vGPS_nRSP_eq.
iDestruct "oW" as (X) "[oW #?]".
iDestruct "oW" as (γ_x) "[#? WA]".
iDestruct "WA" as (v V0 ζ) "(#? & ? & ? & #oR & #?)".
@@ -935,14 +872,14 @@ Section Gname_StrongSW_Param.
Qed.
Lemma GPS_nSW_nFRP_clash `{CInvG : cinvG Σ} {IP2 : gname → interpC Σ Prtcl}
- γ l p s1 s2 q V (E : coPset)
+ γ l p s1 s2 q (E : coPset)
(HNl1: ↑persist_locN .@ l ⊆ E) (HNl2: ↑fracN .@ l ⊆ E):
- vGPS_nRSP γ l p s1 V -∗ vGPS_nFRP (IP:=IP2) γ l s2 q V ={E}=∗ False.
+ vGPS_nRSP γ l p s1 -∗ vGPS_nFRP (IP:=IP2) γ l s2 q ={E}=∗ False.
Proof.
- iIntros "oR1 oR2".
+ rewrite vGPS_nFRP_eq vGPS_nRSP_eq. iStartProof (uPred _).
+ iIntros (?) "oR1 % -> oR2".
iMod (persistor_open with "oR1") as (X1) "(oI1 & oR1 & HClose1)";
first auto.
- rewrite vGPS_nFRP_eq /=.
iMod (fractor_open with "oR2")
as (X2) "(oI2 & oR2 & HClose2)"; first solve_ndisj.
iDestruct "oI1" as (?) "(_ & oI1)".
@@ -952,18 +889,18 @@ Section Gname_StrongSW_Param.
by iDestruct (Hist_Exclusive with "[$oH1 $oH2]") as %?.
Qed.
- Lemma GPS_nSW_Reader_PrtSeen γ l p s V:
- vGPS_nRSP γ l p s V ⊢ PrtSeen γ s V.
+ Lemma GPS_nSW_Reader_PrtSeen γ l p s:
+ vGPS_nRSP γ l p s ⊢ PrtSeen γ s.
Proof.
- iIntros "oR". iDestruct "oR" as (X) "[oR ?]".
- iDestruct "oR" as (γ_x) "[? $]".
+ iStartProof (uPred _). iIntros (V) "oR". rewrite vGPS_nRSP_eq.
+ iDestruct "oR" as (X) "[oR ?]". iDestruct "oR" as (γ_x) "[? $]".
Qed.
- Lemma GPS_nSW_Reader_PrtSeen_update γ l p s1 s2 (Le: s1 ⊑ s2) V:
- vGPS_nRSP γ l p s1 V ∗ PrtSeen γ s2 V ⊢ vGPS_nRSP γ l p s2 V.
+ Lemma GPS_nSW_Reader_PrtSeen_update γ l p s1 s2 (Le: s1 ⊑ s2):
+ vGPS_nRSP γ l p s1 ∗ PrtSeen γ s2 ⊢ vGPS_nRSP γ l p s2.
Proof.
- iIntros "[oR oS]". iDestruct "oR" as (X) "[oR Inv]".
- iDestruct "oR" as (γ_x) "[oX oS1]".
+ rewrite vGPS_nRSP_eq. iStartProof (uPred _). iIntros (V) "[oR oS]".
+ iDestruct "oR" as (X) "[oR Inv]". iDestruct "oR" as (γ_x) "[oX oS1]".
iExists X. iFrame "Inv". iExists γ_x. iFrame "oX oS".
Qed.
End Gname_StrongSW_Param.
@@ -1004,7 +941,7 @@ Lemma GPS_nSWs_param_agree
vGPS_nRSP (IP:=IP1) γ1 l p1 s1 V
∗ vGPS_nRSP (IP:=IP2) γ2 l p2 s2 V ⊢ ⌜p1 = p2 ∧ γ1 = γ2âŒ.
Proof.
- iIntros "RP". rewrite persistor_join_l persistor_drop.
+ iIntros "RP". rewrite !vGPS_nRSP_eq persistor_join_l persistor_drop.
iDestruct "RP" as (X) "[oR1 oR2]".
iDestruct "oR1" as (γx1) "(% & _)".
iDestruct "oR2" as (γx2) "(% & _)".
@@ -1041,93 +978,62 @@ Section SingleWriter.
∃ (γ γ_x: gname),
⌜n = encode (γ,γ_x)⌠∗ gps_inv IP l γ γ_x.
- Definition ReaderSWRaw s V l n : iProp :=
+ Definition ReaderSWRaw s l n : vProp Σ :=
∃ (γ γ_x: gname),
- ⌜n = encode (γ,γ_x)⌠∗ PrtSeen γ s V.
+ ⌜n = encode (γ,γ_x)⌠∗ PrtSeen γ s.
- Definition WriterSWRaw s V l n : iProp :=
+ Definition WriterSWRaw s l n : vProp Σ :=
∃ (γ γ_x: gname),
- ⌜n = encode (γ,γ_x)⌠∗ WAEx l γ γ_x s V.
-
- Definition GPS_RSP l s V : iProp :=
- persisted l (gpsSWRaw) (ReaderSWRaw s V).
-
- Definition GPS_WSP l s V : iProp :=
- persisted l (gpsSWRaw) (WriterSWRaw s V).
-
- Definition GPS_FRP l s (q: frac) V : iProp :=
- fractored l (gpsSWRaw) (λ l q, ReaderSWRaw s V l) q.
-
- Definition GPS_FWP l s (q: frac) V : iProp :=
- fractored l (gpsSWRaw) (λ l q, WriterSWRaw s V l) q.
-
+ ⌜n = encode (γ,γ_x)⌠∗ WAEx l γ γ_x s.
Local Close Scope I.
- Definition vPred_GPS_RSP_mono l s:
- Proper ((⊑) ==> (⊢)) (GPS_RSP l s).
- Proof.
- intros V V' Mono.
- iIntros "RP". iDestruct "RP" as (X) "(RPV & ?)".
- iDestruct "RPV" as (γ γ_x) "(? & RA)".
- iExists X. iFrame. iExists γ, γ_x. by iFrame.
- Qed.
-
- Canonical Structure vGPS_RSP l s :=
- MonPred _ (vPred_GPS_RSP_mono l s).
+ Program Definition vGPS_RSP_def l s : vProp Σ :=
+ MonPred (λ V, persisted l gpsSWRaw (λ l X, ReaderSWRaw s l X V)) _.
+ Next Obligation. solve_proper. Qed.
+ Definition vGPS_RSP_aux : seal vGPS_RSP_def. by eexists. Qed.
+ Definition vGPS_RSP := unseal vGPS_RSP_aux.
+ Definition vGPS_RSP_eq : vGPS_RSP = _ := seal_eq _.
Global Instance vGPS_RSP_persistent l s : Persistent (vGPS_RSP l s).
Proof.
- rewrite /Persistent /bi_persistently. split => ? /=.
- rewrite /sbi_persistently /= monPred_persistently_eq /=.
- apply persistor_persistent => ?. apply _.
+ rewrite /Persistent /bi_persistently vGPS_RSP_eq. iStartProof (uPred _).
+ iIntros (V). iApply persistent.
Qed.
- Definition vPred_GPS_WSP_mono l s:
- Proper ((⊑) ==> (⊢)) (GPS_WSP l s).
- Proof.
- intros V V' Mono.
- iIntros "WP". iDestruct "WP" as (X) "(WPV & ?)".
- iDestruct "WPV" as (γ γ_x) "(? & WA)".
- iExists X. iFrame. iExists γ, γ_x. by iFrame.
- Qed.
+ Program Definition vGPS_WSP_def l s : vProp Σ :=
+ MonPred (λ V, persisted l gpsSWRaw (λ l X, WriterSWRaw s l X V)) _.
+ Next Obligation. solve_proper. Qed.
+ Definition vGPS_WSP_aux : seal vGPS_WSP_def. by eexists. Qed.
+ Definition vGPS_WSP := unseal vGPS_WSP_aux.
+ Definition vGPS_WSP_eq : vGPS_WSP = _ := seal_eq _.
- Canonical Structure vGPS_WSP l s :=
- MonPred _ (vPred_GPS_WSP_mono l s).
+ Program Definition vGPS_FRP_def l s (q: frac) : vProp Σ :=
+ MonPred (λ V, fractored l gpsSWRaw (λ l q X, ReaderSWRaw s l X V) q) _.
+ Next Obligation. solve_proper. Qed.
+ Definition vGPS_FRP_aux : seal vGPS_FRP_def. by eexists. Qed.
+ Definition vGPS_FRP := unseal vGPS_FRP_aux.
+ Definition vGPS_FRP_eq : vGPS_FRP = _ := seal_eq _.
- Definition vPred_GPS_FRP_mono l s q:
- Proper ((⊑) ==> (⊢)) (GPS_FRP l s q).
- Proof.
- intros V V' Mono.
- iIntros "RP". iDestruct "RP" as (X) "(RPV & ?)".
- iDestruct "RPV" as (γ γ_x) "(? & RA)".
- iExists X. iFrame. iExists γ, γ_x. by iFrame.
- Qed.
-
- Canonical Structure vGPS_FRP l s q :=
- MonPred _ (vPred_GPS_FRP_mono l s q).
-
- Definition vPred_GPS_FWP_mono l s q:
- Proper ((⊑) ==> (⊢)) (GPS_FWP l s q).
- Proof.
- intros V V' Mono.
- iIntros "WP". iDestruct "WP" as (X) "(WPV & ?)".
- iDestruct "WPV" as (γ γ_x) "(? & WA)".
- iExists X. iFrame. iExists γ, γ_x. by iFrame.
- Qed.
-
- Canonical Structure vGPS_FWP l s q :=
- MonPred _ (vPred_GPS_FWP_mono l s q).
+ Program Definition vGPS_FWP_def l s (q: frac) : vProp Σ :=
+ MonPred (λ V, fractored l gpsSWRaw (λ l q X, WriterSWRaw s l X V) q) _.
+ Next Obligation. solve_proper. Qed.
+ Definition vGPS_FWP_aux : seal vGPS_FWP_def. by eexists. Qed.
+ Definition vGPS_FWP := unseal vGPS_FWP_aux.
+ Definition vGPS_FWP_eq : vGPS_FWP = _ := seal_eq _.
Local Instance :
Frame false (gps_inv IP l γ γ_x) (gpsSWRaw l (encode (γ, (γ_x)))) True.
- Proof. intros. unfold Frame, bi_affinely_if, bi_persistently_if.
- iIntros "[H _]". iExists _, _. by iFrame "∗". Qed.
+ Proof.
+ intros. unfold Frame, bi_affinely_if, bi_persistently_if.
+ iIntros "[H _]". iExists _, _. by iFrame "∗".
+ Qed.
+ Local Close Scope I.
Lemma GPS_SW_Readers_agree l s1 s2 (E : coPset) (HE: ↑persist_locN .@ l ⊆ E):
- (vGPS_RSP l s1 ∗ vGPS_RSP l s2 ={E}=∗ ⌜s1 ⊑ s2 ∨ s2 ⊑ s1âŒ)%stdpp.
+ vGPS_RSP l s1 ∗ vGPS_RSP l s2 ={E}=∗ ⌜s1 ⊑ s2 ∨ s2 ⊑ s1âŒ.
Proof.
iStartProof (uPred _).
- iIntros (V) "#RP".
+ iIntros (V) "#RP". rewrite vGPS_RSP_eq.
iDestruct (persistor_splitjoin with "RP") as "H".
iMod (persistor_open with "H") as (X) "(oI & (oR1 & oR2) & HClose)";
first auto.
@@ -1140,7 +1046,7 @@ Section SingleWriter.
iDestruct "RA2" as (V2 v2) "(? & #oR2)".
iMod (Reader_singleton_agree _ _ _ _ s1 _ _ s2 with "[$oI $oR1 $oR2]") as "[oI %]".
iMod ("HClose" $!
- (λ l0 X, ReaderSWRaw s1 _ l0 X ∗ ReaderSWRaw s2 _ l0 X)%I
+ (λ l0 X, ReaderSWRaw s1 l0 X V ∗ ReaderSWRaw s2 l0 X V)%I
with "[oI]") as "oR".
- iSplitL "oI"; last iSplitL ""; iExists γ, γ_x;
(iSplitL ""; first auto).
@@ -1151,10 +1057,10 @@ Section SingleWriter.
Qed.
Lemma GPS_SW_Writer_max l s s' (E : coPset) (HE: ↑persist_locN .@ l ⊆ E):
- (vGPS_RSP l s ∗ â–· vGPS_WSP l s' ={E}=∗ vGPS_WSP l s' ∗ ⌜s ⊑ s'âŒ)%stdpp.
+ vGPS_RSP l s ∗ â–· vGPS_WSP l s' ={E}=∗ vGPS_WSP l s' ∗ ⌜s ⊑ s'âŒ.
Proof.
iStartProof (uPred _).
- iIntros (V) "oRW".
+ iIntros (V) "oRW". rewrite vGPS_WSP_eq vGPS_RSP_eq.
iMod (persistor_join_later_rl with "oRW") as "oRW".
iMod (persistor_open with "oRW") as (X) "(oI & (oR & oW) & HClose)";
first auto.
@@ -1173,7 +1079,7 @@ Section SingleWriter.
assert (Le := H _ Ins).
iMod (Writer_sorted with "[$oI $oW]") as "(oI & oW & %)".
- iMod ("HClose" $! (λ l0 X, WriterSWRaw s' V l0 X)%I
+ iMod ("HClose" $! (λ l0 X, WriterSWRaw s' l0 X V)%I
with "[$oI oW ex]") as "oW".
{ iExists γ, γ_x. iSplitL ""; first auto.
iExists v2, V2, ζ. by iFrame (H) "oW ex oR2 vS". }
@@ -1182,8 +1088,6 @@ Section SingleWriter.
by apply (H2 _ _ Ins Ins').
Qed.
- Close Scope I.
-
Lemma GPS_SW_Read_ex l s (E : coPset)
(HN : ↑physN ⊆ E) (HNl: ↑persist_locN .@ l ⊆ E):
{{{ ⎡PSCtx⎤ ∗ â–· É (∀ v, F_past l s v ={E ∖ ↑persist_locN .@ l}=∗
@@ -1192,10 +1096,9 @@ Section SingleWriter.
{{{ v, RET #v ;
vGPS_WSP l s ∗ F_past l s v }}}.
Proof.
- intros.
iStartProof (uPred _).
- rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VSDup & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite WP_Def.wp_eq /= vGPS_WSP_eq.
+ iIntros (? V) "(#kI & VSDup & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
iMod ((persistor_open) with "[$oW]")
as (X) "(gpsRaw & WRaw & HClose)"; first auto.
iDestruct "WRaw" as (γ γ_x) "(% & WA)".
@@ -1226,10 +1129,9 @@ Section SingleWriter.
([ #l ]_na <- #v) @ E
{{{ RET #() ; Q }}}.
Proof.
- intros.
iStartProof (uPred _).
- rewrite valloc_local_eq WP_Def.wp_eq /=.
- iIntros (V) "(#kI & #kIp & oL & VS)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite valloc_local_eq WP_Def.wp_eq /= vGPS_WSP_eq.
+ iIntros (? V) "(#kI & #kIp & oL & VS)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
setoid_rewrite H1; setoid_rewrite H2.
iDestruct "oL" as (h i) "(Alloc & Hist & Info)".
@@ -1240,7 +1142,7 @@ Section SingleWriter.
iNext.
iIntros (V' γ γ_x) "(#Le & kS & oI & ex & #oR & oW)".
iMod (persistor_inv_alloc' E i (encode (γ,γ_x)) l
- (gpsSWRaw) (WriterSWRaw s V')
+ gpsSWRaw (λ l X, WriterSWRaw s l X V')
with "[$Info $kI $kIp]") as "[WP HClose]"; [auto|auto|..].
iMod ("VS" $! _ with "Le [- Post HClose oI kS]") as "(F & Fp & Q)".
{ iApply "WP".
@@ -1266,10 +1168,9 @@ Section SingleWriter.
{{{ s' v, RET #v ;
⌜s ⊑ s'⌠∗ Q s' v }}}.
Proof.
- intros.
iStartProof (uPred _).
- rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite WP_Def.wp_eq vGPS_RSP_eq /=.
+ iIntros (? V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
iMod ((persistor_open) with "[$oR]")
as (X) "(gpsRaw & RRaw & HClose)"; first auto.
iDestruct "RRaw" as (γ γ_x) "(% & RA)".
@@ -1286,7 +1187,7 @@ Section SingleWriter.
iDestruct ("VS" $! _ Hs' j with "[%]") as "[VS|VS]"; last by iRight.
{ etrans; eauto. }
iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
- iMod ("HClose" $! (ReaderSWRaw s' j0) with "[oI oR']").
+ iMod ("HClose" $! (λ l X, ReaderSWRaw s' l X j0) with "[oI oR']").
{ iSplit.
+ iNext. iExists γ, γ_x. by iFrame "oI".
+ iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
@@ -1330,10 +1231,9 @@ Section SingleWriter.
([ #l ]_at <- #v) @ E
{{{ RET #() ; vGPS_RSP l s' ∗ Q s' }}}.
Proof.
- intros.
iStartProof (uPred _).
- rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VS & oP & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite WP_Def.wp_eq vGPS_RSP_eq vGPS_WSP_eq /=.
+ iIntros (? V) "(#kI & VS & oP & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
iMod ((persistor_open') with "[$oW]")
as (X) "(gpsRaw & WRaw & #HT & HClose)"; first auto.
iDestruct "WRaw" as (γ γ_x) "(% & WA)".
@@ -1365,8 +1265,7 @@ Section SingleWriter.
Lemma GPS_SW_Writer_Reader l s:
vGPS_WSP l s ⊢ vGPS_WSP l s ∗ vGPS_RSP l s.
Proof.
- constructor => V.
- iIntros "oW".
+ iStartProof (uPred _). iIntros (V) "oW". rewrite vGPS_RSP_eq vGPS_WSP_eq.
iDestruct "oW" as (X) "[oW #?]".
iDestruct "oW" as (γ γ_x) "[#? WA]".
iDestruct "WA" as (v V0 ζ) "(#? & ? & ? & #oR & #?)".
@@ -1380,7 +1279,7 @@ Section SingleWriter.
(vGPS_FRP l s1 q1 ∗ vGPS_FRP l s2 q2
={E}=∗ ⌜s1 ⊑ s2 ∨ s2 ⊑ s1⌠∗ vGPS_FRP l s1 q1 ∗ vGPS_FRP l s2 q2)%stdpp.
Proof.
- iStartProof (uPred _).
+ iStartProof (uPred _). rewrite vGPS_FRP_eq.
iIntros (V) "[oR1 oR2]"; iCombine "oR1 oR2" as "RP".
iDestruct (fractor_splitjoin l with "RP") as "H".
iMod (fractor_open with "H") as (X) "(oI & (oR1 & oR2) & HClose)";
@@ -1394,7 +1293,7 @@ Section SingleWriter.
iDestruct "RA2" as (V2 v2) "(? & oR2)".
iMod (Reader_singleton_agree _ _ _ _ s1 _ _ s2 with "[$oI $oR1 $oR2]") as "[oI %]".
iMod ("HClose" $!
- (λ l0 _ X, ReaderSWRaw s1 _ l0 X ∗ ReaderSWRaw s2 _ l0 X)%I
+ (λ l0 _ X, ReaderSWRaw s1 l0 X V ∗ ReaderSWRaw s2 l0 X V)%I
with "[oI]") as "oR".
- iSplitL "oI"; last iSplitL ""; iExists γ, γ_x;
(iSplitL ""; first auto).
@@ -1402,8 +1301,8 @@ Section SingleWriter.
+ iExists V1, v1. by iFrame "oR1".
+ iExists V2, v2. by iFrame "oR2".
- iDestruct (fractor_splitjoin l _
- (λ l0 _ X, ReaderSWRaw s1 V l0 X)
- (λ l0 _ X, ReaderSWRaw s2 V l0 X)
+ (λ l0 _ X, ReaderSWRaw s1 l0 X V)
+ (λ l0 _ X, ReaderSWRaw s2 l0 X V)
with "oR") as "[o1 o2]".
iModIntro; iSplit; first auto.
iFrame "o1 o2".
@@ -1415,10 +1314,9 @@ Section SingleWriter.
([ #l ]_na <- #v) @ E
{{{ RET #() ; vGPS_FWP l s 1%Qp }}}%stdpp.
Proof.
- intros.
iStartProof (uPred _).
- rewrite valloc_local_eq WP_Def.wp_eq /=.
- iIntros (V) "(#kI & oL & F & Fp)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite valloc_local_eq WP_Def.wp_eq vGPS_FWP_eq /=.
+ iIntros (? V) "(#kI & oL & F & Fp)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
setoid_rewrite H1; setoid_rewrite H2.
iDestruct "oL" as (h i) "(Alloc & Hist & Info)".
iApply program_logic.weakestpre.wp_fupd.
@@ -1428,7 +1326,7 @@ Section SingleWriter.
iIntros (V' γ γ_x) "(#Le & kS' & oI & ex & #oR & oW)".
iMod (fractor_alloc E i (encode(γ,γ_x)) l
- (gpsSWRaw) (λ l q, WriterSWRaw s V' l)
+ gpsSWRaw (λ l q X, WriterSWRaw s l X V')
with "[-Post kS']") as "FP"; first auto.
{ iFrame "kI Info". iSplitL "oI"; iExists γ, γ_x.
- iSplitL ""; [by iNext|done].
@@ -1451,10 +1349,9 @@ Section SingleWriter.
{{{ s' v, RET #v ;
⌜s ⊑ s'⌠∗ Q s' v }}}%stdpp.
Proof.
- intros.
iStartProof (uPred _).
- rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite WP_Def.wp_eq vGPS_FRP_eq /=.
+ iIntros (? V) "(#kI & VS & VSDup & oP & oR)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
iMod (fractor_open with "[$oR]")
as (X) "(gpsRaw & RRaw & HClose)"; first exact HNl.
@@ -1472,7 +1369,7 @@ Section SingleWriter.
iDestruct ("VS" $! _ Hs' j with "[%]") as "[VS|VS]"; last by iRight.
{ etrans; eauto. }
iLeft; iIntros (v Vr j0 Hle') "(? & ? & % & % & oI & oR')".
- iMod ("HClose" $! (fun l _ => ReaderSWRaw s' j0 l) with "[oI oR']").
+ iMod ("HClose" $! (fun l _ X => ReaderSWRaw s' l X j0) with "[oI oR']").
{ iSplit.
+ iNext. iExists γ, γ_x. by iFrame "oI".
+ iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
@@ -1514,10 +1411,9 @@ Section SingleWriter.
{{{ v, RET #v ;
vGPS_FWP l s q ∗ F_past l s v }}}.
Proof.
- intros.
iStartProof (uPred _).
- rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VSDup & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite WP_Def.wp_eq vGPS_FWP_eq /=.
+ iIntros (? V) "(#kI & VSDup & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
iMod (fractor_open with "[$oW]")
as (X) "(gpsRaw & WRaw & HClose)"; first auto.
iDestruct "WRaw" as (γ γ_x) "(% & WA)".
@@ -1546,7 +1442,7 @@ Section SingleWriter.
vGPS_FRP l s q1 ∗ vGPS_FWP l s' q2 ∗ ⌜s ⊑ s'âŒ)%stdpp.
Proof.
iStartProof (uPred _).
- iIntros (V) "oRW".
+ iIntros (V) "oRW". rewrite vGPS_FWP_eq vGPS_FRP_eq.
iMod (fractor_join_later_rl with "oRW") as "oRW".
iMod (fractor_open with "oRW") as (X) "(oI & (oR & oW) & HClose)";
first auto.
@@ -1565,14 +1461,14 @@ Section SingleWriter.
assert (Le := H _ Ins).
iMod (Writer_sorted with "[$oI $oW]") as "(oI & oW & %)".
- iMod ("HClose" $! (λ l0 _ X, ReaderSWRaw s V l0 X ∗ WriterSWRaw s' V l0 X)%I
+ iMod ("HClose" $! (λ l0 _ X, ReaderSWRaw s l0 X V ∗ WriterSWRaw s' l0 X V)%I
with "[$oI oW ex]") as "oW".
{ iSplitL ""; iExists γ, γ_x; (iSplitL ""; first auto).
- iExists V1, v1. by iFrame "oR".
- iExists v2, V2, ζ. by iFrame "vS oW ex oR2". }
iDestruct (fractor_splitjoin l _
- (λ l0 _ X, ReaderSWRaw s V l0 X)
- (λ l0 _ X, WriterSWRaw s' V l0 X)
+ (λ l0 _ X, ReaderSWRaw s l0 X V)
+ (λ l0 _ X, WriterSWRaw s' l0 X V)
with "oW") as "[o1 o2]".
iFrame "o1 o2".
iPureIntro. by apply (H2 _ _ Ins Ins').
@@ -1581,9 +1477,7 @@ Section SingleWriter.
Lemma GPS_FWP_Writer_Reader l s q1 q2:
vGPS_FWP l s (q1 + q2) ⊢ vGPS_FWP l s q1 ∗ vGPS_FRP l s q2.
Proof.
- constructor => V.
- iIntros "oW".
- rewrite /bi_sep /= /sbi_sep /= monPred_sep_eq /=.
+ iStartProof (uPred _). iIntros (V) "oW". rewrite vGPS_FWP_eq vGPS_FRP_eq.
iApply fractor_splitjoin.
iApply (fractor_mono with "[$oW]").
iIntros (X) "oW".
@@ -1597,44 +1491,31 @@ Section SingleWriter.
Lemma GPS_FWP_Writer_Reader_join l s q1 q2:
vGPS_FWP l s q1 ∗ vGPS_FRP l s q2 ⊢ vGPS_FWP l s (q1 + q2).
Proof.
- constructor => V.
- iIntros "(o1 & o2)". iCombine "o1" "o2" as "oW".
- rewrite fractor_splitjoin; last auto.
+ iStartProof (uPred _). iIntros (V) "(o1 & o2)". iCombine "o1" "o2" as "oW".
+ rewrite vGPS_FWP_eq vGPS_FRP_eq fractor_splitjoin; last auto.
iApply (fractor_mono with "[$oW]").
by iIntros (X) "(oW & _)".
Qed.
- Global Instance GPS_FRP_fractional' l s V:
- Fractional (λ q, vGPS_FRP l s q V).
+ Global Instance GPS_FRP_fractional l s:
+ Fractional (vGPS_FRP l s).
Proof.
- intros q1 q2. rewrite /vGPS_FRP /= /GPS_FRP. iSplit.
- - iIntros "oR". iApply fractor_splitjoin.
+ intros q1 q2. iStartProof (uPred _). rewrite vGPS_FRP_eq.
+ iIntros (V). iSplit; iIntros "oR".
+ - iApply fractor_splitjoin.
iApply (fractor_mono with "[$oR]").
iIntros (?) "#?". by iSplit.
- - iIntros "(oR1 & oR2)".
- iCombine "oR1" "oR2" as "oR".
- rewrite fractor_splitjoin; last auto.
+ - rewrite fractor_splitjoin; last auto.
iApply (fractor_mono with "[$oR]"). by iIntros (X) "[R1 R2]".
Qed.
- Global Instance GPS_FRP_fractional l s:
- Fractional (vGPS_FRP l s).
- Proof.
- intros q1 q2. constructor => ?.
- rewrite /bi_sep /= /sbi_sep /= monPred_sep_eq GPS_FRP_fractional'; done.
- Qed.
-
Lemma GPS_FRP_join l s q1 q2:
vGPS_FRP l s q1 ∗ vGPS_FRP l s q2 ⊢ vGPS_FRP l s (q1 + q2).
- Proof.
- by rewrite fractional.
- Qed.
+ Proof. by rewrite fractional. Qed.
Lemma GPS_FRP_split l s q1 q2:
vGPS_FRP l s (q1 + q2) ⊢ vGPS_FRP l s q1 ∗ vGPS_FRP l s q2.
- Proof.
- by rewrite fractional.
- Qed.
+ Proof. by rewrite fractional. Qed.
Lemma GPS_FRP_mult_splitL l s (n: positive) q:
vGPS_FRP l s (Pos2Qp n * q)
@@ -1672,10 +1553,9 @@ Section SingleWriter.
([ #l ]_at <- #v) @ E
{{{ RET #() ; vGPS_FWP l s' q ∗ Q s' }}}.
Proof.
- intros.
iStartProof (uPred _).
- rewrite WP_Def.wp_eq /=.
- iIntros (V) "(#kI & VS & oP & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
+ rewrite WP_Def.wp_eq /= vGPS_FWP_eq.
+ iIntros (? V) "(#kI & VS & oP & oW)"; iIntros (V1 H1) "Post"; iIntros (V2 H2 ?) "kS".
iMod (fractor_open with "[$oW]")
as (X) "(gpsRaw & WRaw & HClose)"; first auto.
iDestruct "WRaw" as (γ γ_x) "(% & WA)".
@@ -1701,40 +1581,40 @@ Section SingleWriter.
End SingleWriter.
-Arguments vGPS_WSP [_ _ _ _ _ _] _ _ _.
-Arguments vGPS_RSP [_ _ _ _ _ _] _ _ _.
-Arguments GPS_SW_Init [_ _ _ _ _ _] _ [_] _ [_] _ [_] _ _ [_].
-Arguments GPS_SW_Read [_ _ _ _ _ _] _ [_] _ _ [_ _] _ _ [_].
-Arguments GPS_SW_Read_ex [_ _ _ _ _ _] _ [_ _ _] _ _ [_].
-Arguments GPS_SW_ExWrite [_ _ _ _ _ _] _ [_ _] _ [_ _] _ _ _ _ _ [_].
-(* Arguments GPS_SW_FAI [_ _] [_ _ _ _ _ _ _] [_] _ [_ _] _ _ _ _ [_ _ _]. *)
-(* Arguments GPS_SW_CAS [_ _] [_ _ _ _ _ _ _] [_] _ [_ _ _] _ _ _ _ _ [_ _ _]. *)
-Arguments GPS_SW_Writer_Reader [_ _] [_ _ _ _ _ _ _].
-Arguments GPS_SW_Readers_agree [_ _] [_ _ _ _ _ _ _ _ _] _.
-
-Arguments vGPS_FWP [_ _ _ _ _ _] _ _ _ _.
-Arguments vGPS_FRP [_ _ _ _ _ _] _ _ _ _.
-Arguments GPS_FWP_Init [_ _ _ _ _ _] _ [_] _ [_ _] _ [_].
-Arguments GPS_FRP_Read [_ _ _ _ _ _] _ [_ _] _ _ [_ _] _ _ [_].
-Arguments GPS_FWP_ExRead [_ _ _ _ _ _] _ [_ _ _ _] _ _ [_].
-Arguments GPS_FWP_ExWrite [_ _ _ _ _ _] _ [_ _] _ [_ _ _] _ _ _ _ _ [_].
-
-Arguments vGPS_nWSP [_ _ _ _ _ _ _ _ _] _ _ _ _.
-Arguments vGPS_nRSP [_ _ _ _ _ _ _ _ _] _ _ _ _.
-Arguments GPS_nSW_Init_strong [_ _ _ _ _ _ _ _ _] _ [_] _ _ [_] _ [_] _ _ [_].
-Arguments GPS_nSW_ExRead [_ _ _ _ _ _ _ _ _] _ [_ _] _ [ _ _] _ _ [_].
-Arguments GPS_nSW_ExWrite [_ _ _ _ _ _ _ _ _] _ [_ _] _ [_] _ [_ _] _ _ _ _ _ [_].
-Arguments GPS_nSW_Read [_ _ _ _ _ _ _ _ _] _ [_ _] _ _ _ [_ _] _ _ [_].
-Arguments GPS_nSW_Init_default [_ _ _ _ _ _] _ [ _] _ [_] _ [_] _ _ [_].
-Arguments GPS_nSWs_param_agree [_ _ _ _ _ _ _ _ _ _ _ _ _].
-Arguments GPS_nSW_nFRP_clash [_ _ _ _ _ _ _ _ _ _ _ _].
-
-Arguments vGPS_nFWP [_ _ _ _ _ _] _ _ _ _ _.
-Arguments vGPS_nFRP [_ _ _ _ _ _] _ _ _ _ _.
-Arguments GPS_nFWP_Init_strong [_ _ _ _ _ _] _ [_] _ [_] _ [_] _ [_].
-Arguments GPS_nFWP_ExRead [_ _ _ _ _ _] _ _ [_] _ [ _ _] _ _ [_].
-Arguments GPS_nFWP_ExWrite [_ _ _ _ _ _] _ _ [_ _] _ [_ _ _] _ _ _ _ _ [_].
-Arguments GPS_nFRP_Read [_ _ _ _ _ _] _ [_] _ [_] _ _ [_ _] _ _ [_].
+Arguments vGPS_WSP {_ _ _ _ _ _} _ _ _.
+Arguments vGPS_RSP {_ _ _ _ _ _} _ _ _.
+Arguments GPS_SW_Init {_ _ _ _ _ _} _ {_} _ {_} _ {_} _ _ {_}.
+Arguments GPS_SW_Read {_ _ _ _ _ _} _ {_} _ _ {_ _} _ _ {_}.
+Arguments GPS_SW_Read_ex {_ _ _ _ _ _} _ {_ _ _} _ _ {_}.
+Arguments GPS_SW_ExWrite {_ _ _ _ _ _} _ {_ _} _ {_ _} _ _ _ _ _ {_}.
+(* Arguments GPS_SW_FAI {_ _} {_ _ _ _ _ _ _} {_} _ {_ _} _ _ _ _ {_ _ _}. *)
+(* Arguments GPS_SW_CAS {_ _} {_ _ _ _ _ _ _} {_} _ {_ _ _} _ _ _ _ _ {_ _ _}. *)
+Arguments GPS_SW_Writer_Reader {_ _} {_ _ _ _ _ _ _}.
+Arguments GPS_SW_Readers_agree {_ _} {_ _ _ _ _ _ _ _ _} _.
+
+Arguments vGPS_FWP {_ _ _ _ _ _} _ _ _ _.
+Arguments vGPS_FRP {_ _ _ _ _ _} _ _ _ _.
+Arguments GPS_FWP_Init {_ _ _ _ _ _} _ {_} _ {_ _} _ {_}.
+Arguments GPS_FRP_Read {_ _ _ _ _ _} _ {_ _} _ _ {_ _} _ _ {_}.
+Arguments GPS_FWP_ExRead {_ _ _ _ _ _} _ {_ _ _ _} _ _ {_}.
+Arguments GPS_FWP_ExWrite {_ _ _ _ _ _} _ {_ _} _ {_ _ _} _ _ _ _ _ {_}.
+
+Arguments vGPS_nWSP {_ _ _ _ _ _ _ _ _} _ _ _ _.
+Arguments vGPS_nRSP {_ _ _ _ _ _ _ _ _} _ _ _ _.
+Arguments GPS_nSW_Init_strong {_ _ _ _ _ _ _ _ _} _ {_} _ _ {_} _ {_} _ _ {_}.
+Arguments GPS_nSW_ExRead {_ _ _ _ _ _ _ _ _} _ {_ _} _ { _ _} _ _ {_}.
+Arguments GPS_nSW_ExWrite {_ _ _ _ _ _ _ _ _} _ {_ _} _ {_} _ {_ _} _ _ _ _ _ {_}.
+Arguments GPS_nSW_Read {_ _ _ _ _ _ _ _ _} _ {_ _} _ _ _ {_ _} _ _ {_}.
+Arguments GPS_nSW_Init_default {_ _ _ _ _ _} _ { _} _ {_} _ {_} _ _ {_}.
+Arguments GPS_nSWs_param_agree {_ _ _ _ _ _ _ _ _ _ _ _ _}.
+Arguments GPS_nSW_nFRP_clash {_ _ _ _ _ _ _ _ _ _ _ _}.
+
+Arguments vGPS_nFWP {_ _ _ _ _ _} _ _ _ _ _.
+Arguments vGPS_nFRP {_ _ _ _ _ _} _ _ _ _ _.
+Arguments GPS_nFWP_Init_strong {_ _ _ _ _ _} _ {_} _ {_} _ {_} _ {_}.
+Arguments GPS_nFWP_ExRead {_ _ _ _ _ _} _ _ {_} _ { _ _} _ _ {_}.
+Arguments GPS_nFWP_ExWrite {_ _ _ _ _ _} _ _ {_ _} _ {_ _ _} _ _ _ _ _ {_}.
+Arguments GPS_nFRP_Read {_ _ _ _ _ _} _ {_} _ {_} _ _ {_ _} _ _ {_}.
Notation "'[XP' l 'in' s | p ']_W'" :=
(vGPS_WSP p l s)
@@ -1743,7 +1623,6 @@ Notation "'[XP' l 'in' s | p ']_R'" :=
(vGPS_RSP p l s)
(format "[XP l in s | p ]_R").
-
Notation "'[FXP' l 'in' s | p ']_W_' q" :=
(vGPS_FWP p l s q)
(at level 0,
@@ -1780,118 +1659,104 @@ Notation "'[nFXP' l 'in' s '@' γ | p ']_R_' q" :=
(at level 0,
format "[nFXP l in s @ γ | p ]_R_ q").
-
-Global Instance vGPS_RSP_contractive `{fG : foundationG Σ} `{pG : persistorG Σ} `{GPSG : gpsG Σ Prtcl}:
- Contractive (λ F : interpC _ _, [XP l in s1 | F ]_R).
-Proof.
- repeat intro. constructor => ?.
- apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|].
- apply bi.sep_ne; [|done].
- f_contractive. do 2 apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|by apply gps_inv_ne].
-Qed.
-
-Global Instance vGPS_WSP_contractive `{fG : foundationG Σ} `{pG : persistorG Σ} `{GPSG : gpsG Σ Prtcl}:
- Contractive (λ F : interpC _ _, [XP l in s1 | F ]_W).
-Proof.
- repeat intro. constructor => ?.
- apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|].
- apply bi.sep_ne; [|done].
- f_contractive. do 2 apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|by apply gps_inv_ne].
-Qed.
-
-Global Instance vGPS_FRP_contractive `{fG : foundationG Σ} `{aG : cinvG Σ} `{GPSG : gpsG Σ Prtcl}:
- Contractive (λ F : interpC _ _, [FXP l in s1 | F ]_R_q).
+Section proper.
+Context `{foundationG Σ, gpsG Σ Prtcl}.
+
+Global Instance gpsSWRaw_ne n :
+ Proper ((dist n) ==> (=) ==> (=) ==> (dist n)) (@gpsSWRaw _ _ _ _ _).
+Proof. solve_proper. Qed.
+Global Instance gpsSWnRaw_ne n :
+ Proper (pointwise_relation _ (dist n) ==> (=) ==> (=) ==> (=) ==> (dist n))
+ (@gpsSWnRaw _ _ _ _ _).
+Proof. rewrite /gpsSWnRaw. solve_proper. Qed.
+Global Instance gpsSWpnRaw_ne `{EqDecision Param, Countable Param} n :
+ Proper (pointwise_relation _ (dist n) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> (dist n)) (@gpsSWpnRaw _ _ _ _ _ _ _ _).
+Proof. rewrite /gpsSWpnRaw. solve_proper. Qed.
+
+Global Instance vGPS_RSP_contractive `{persistorG Σ} :
+ Proper (dist_later n ==> (=) ==> (=) ==> dist n) vGPS_RSP.
+Proof. split=>?. rewrite !vGPS_RSP_eq /=. solve_contractive. Qed.
+Global Instance vGPS_WSP_contractive `{persistorG Σ} :
+ Proper (dist_later n ==> (=) ==> (=) ==> dist n) vGPS_WSP.
+Proof. split=>?. rewrite !vGPS_WSP_eq /=. solve_contractive. Qed.
+
+Global Instance vGPS_FRP_contractive `{cinvG Σ} :
+ Proper (dist_later n ==> (=) ==> (=) ==> (=) ==> dist n) vGPS_FRP.
+Proof. split=>?. rewrite !vGPS_FRP_eq /=. solve_contractive. Qed.
+Global Instance vGPS_FWP_contractive `{cinvG Σ} :
+ Proper (dist_later n ==> (=) ==> (=) ==> (=) ==> dist n) vGPS_FWP.
+Proof. split=>?. rewrite !vGPS_FWP_eq /=. solve_contractive. Qed.
+
+Global Instance vGPS_nFRP_contractive `{cinvG Σ} :
+ Proper (pointwise_relation _ (dist_later n) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> dist n) vGPS_nFRP.
+Proof. split=>?. rewrite !vGPS_nFRP_eq /=. solve_contractive. Qed.
+Global Instance vGPS_nFWP_contractive `{cinvG Σ} :
+ Proper (pointwise_relation _ (dist_later n) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> dist n) vGPS_nFWP.
+Proof. split=>?. rewrite !vGPS_nFWP_eq /=. solve_contractive. Qed.
+
+Global Instance vGPS_nRSP_contractive `{persistorG Σ, EqDecision Param, Countable Param}:
+ Proper (pointwise_relation _ (dist_later n) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> dist n) vGPS_nRSP.
Proof.
- repeat intro. constructor => ?.
- apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|].
- apply bi.exist_ne => ?. repeat (apply bi.sep_ne; [done|]).
- f_contractive. do 2 apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|by apply gps_inv_ne].
+ split=>?. rewrite !vGPS_nRSP_eq /=. subst. f_contractive=>??.
+ by apply gpsSWpnRaw_ne.
Qed.
-
-Global Instance vGPS_FWP_contractive `{fG : foundationG Σ} `{aG : cinvG Σ} `{GPSG : gpsG Σ Prtcl}:
- Contractive (λ F : interpC _ _, [FXP l in s1 | F ]_W_q).
+Global Instance vGPS_nWSP_contractive `{persistorG Σ, EqDecision Param, Countable Param}:
+ Proper (pointwise_relation _ (dist_later n) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> dist n) vGPS_nWSP.
Proof.
- repeat intro. constructor => ?.
- apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|].
- apply bi.exist_ne => ?. repeat (apply bi.sep_ne; [done|]).
- f_contractive. do 2 apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|by apply gps_inv_ne].
+ split=>?. rewrite !vGPS_nWSP_eq /=. subst. f_contractive=>??.
+ by apply gpsSWpnRaw_ne.
Qed.
-Global Instance vGPS_nFRP_contractive `{fG : foundationG Σ} `{aG : cinvG Σ} `{GPSG : gpsG Σ Prtcl}:
- Contractive (λ F : gname -c> interpC _ _, [nFXP l in s @ γ | F ]_R_q).
+Global Instance gpsSWRaw_proper :
+ Proper ((≡) ==> (=) ==> (=) ==> (≡)) (@gpsSWRaw _ _ _ _ _).
+Proof. solve_proper. Qed.
+Global Instance gpsSWnRaw_proper :
+ Proper (pointwise_relation _ (≡) ==> (=) ==> (=) ==> (=) ==> (≡))
+ (@gpsSWnRaw _ _ _ _ _).
+Proof. rewrite /gpsSWnRaw. solve_proper. Qed.
+Global Instance gpsSWpnRaw_proper `{EqDecision Param, Countable Param} :
+ Proper (pointwise_relation _ (≡) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> (≡)) (@gpsSWpnRaw _ _ _ _ _ _ _ _).
+Proof. rewrite /gpsSWpnRaw. solve_proper. Qed.
+
+Global Instance vGPS_WSP_proper `{persistorG Σ} :
+ Proper ((≡) ==> (=) ==> (=) ==> (≡)) vGPS_WSP.
+Proof. split=>?. rewrite !vGPS_WSP_eq /=. solve_proper. Qed.
+Global Instance vGPS_RSP_proper `{persistorG Σ} :
+ Proper ((≡) ==> (=) ==> (=) ==> (≡)) vGPS_RSP.
+Proof. split=>?. rewrite !vGPS_RSP_eq /=. solve_proper. Qed.
+
+Global Instance vGPS_FRP_proper `{cinvG Σ} :
+ Proper ((≡) ==> (=) ==> (=) ==> (=) ==> (≡)) vGPS_FRP.
+Proof. split=>?. rewrite !vGPS_FRP_eq /=. solve_proper. Qed.
+Global Instance vGPS_FWP_proper `{cinvG Σ} :
+ Proper ((≡) ==> (=) ==> (=) ==> (=) ==> (≡)) vGPS_FWP.
+Proof. split=>?. rewrite !vGPS_FWP_eq /=. solve_proper. Qed.
+
+Global Instance vGPS_nFRP_proper `{cinvG Σ} :
+ Proper (pointwise_relation _ (≡) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> (≡)) vGPS_nFRP.
+Proof. split=>?. rewrite !vGPS_nFRP_eq /=. solve_proper. Qed.
+Global Instance vGPS_nFWP_proper `{cinvG Σ} :
+ Proper (pointwise_relation _ (≡) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> (≡)) vGPS_nFWP.
+Proof. split=>?. rewrite !vGPS_nFWP_eq /=. solve_proper. Qed.
+
+Global Instance vGPS_nRSP_proper `{persistorG Σ, EqDecision Param, Countable Param}:
+ Proper (pointwise_relation _ (≡) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> (≡)) vGPS_nRSP.
Proof.
- repeat intro. constructor => ?.
- rewrite !vGPS_nFRP_eq.
- apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|].
- apply bi.exist_ne => ?. repeat (apply bi.sep_ne; [done|]).
- f_contractive. apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|by apply gps_inv_ne].
+ split=>?. rewrite !vGPS_nRSP_eq /=. subst. f_equiv=>??. by apply gpsSWpnRaw_proper.
Qed.
-
-Global Instance vGPS_nFWP_contractive `{fG : foundationG Σ} `{aG : cinvG Σ} `{GPSG : gpsG Σ Prtcl}:
- Contractive (λ F : gname -c> interpC _ _, [nFXP l in s @ γ | F ]_W_q).
-Proof.
- repeat intro. constructor => ?.
- rewrite !vGPS_nFWP_eq.
- apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|].
- apply bi.exist_ne => ?. repeat (apply bi.sep_ne; [done|]).
- f_contractive. apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|by apply gps_inv_ne].
-Qed.
-
-Global Instance vGPS_nRSP_contractive `{fG : foundationG Σ} `{pG : persistorG Σ} `{GPSG : gpsG Σ Prtcl}:
- Contractive (λ F : gname -c> interpC _ _, [nXP l in s @ γ | F ]_R).
-Proof.
- repeat intro. constructor => ?.
- apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|].
- apply bi.sep_ne; [|done].
- f_contractive. apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|by apply gps_inv_ne].
-Qed.
-
-Global Instance vGPS_nWSP_contractive `{fG : foundationG Σ} `{pG : persistorG Σ} `{GPSG : gpsG Σ Prtcl}:
- Contractive (λ F : gname -c> interpC _ _, [nXP l in s @ γ | F ]_W).
-Proof.
- repeat intro. constructor => ?.
- apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|].
- apply bi.sep_ne; [|done].
- f_contractive. apply bi.exist_ne => ?.
- apply bi.sep_ne; [done|by apply gps_inv_ne].
-Qed.
-
-Global Instance gpsSWRaw_proper {Σ Prtcl fG PF gpsG}:
- Proper ((≡) ==> (=) ==> (=) ==> (≡)) (@gpsSWRaw Σ Prtcl fG PF gpsG).
-Proof.
- intros ? ? H1 ? ? H2 ? ? H3. subst.
- unfold gpsSWRaw.
- repeat (apply (_ : Proper (_ ==> (≡)) _); repeat intro).
- by apply gps_inv_proper.
-Qed.
-
-Global Instance vGPS_WSP_proper {Σ Prtcl fG PF gpsG persG}:
- Proper ((≡) ==> (=) ==> (=) ==> (≡)) (@vGPS_WSP Σ Prtcl fG PF gpsG persG).
-Proof.
- intros ? ? H1 ? ? H2 ? ? H3. constructor => ?. subst.
- unfold vGPS_WSP. rewrite /GPS_WSP /=.
- f_equiv. intros ? ?. by rewrite (gpsSWRaw_proper _ _ H1).
-Qed.
-
-Global Instance vGPS_RSP_proper {Σ Prtcl fG PF gpsG persG}:
- Proper ((≡) ==> (=) ==> (=) ==> (≡)) (@vGPS_RSP Σ Prtcl fG PF gpsG persG).
+Global Instance vGPS_nWSP_proper `{persistorG Σ, EqDecision Param, Countable Param}:
+ Proper (pointwise_relation _ (≡) ==>
+ (=) ==> (=) ==> (=) ==> (=) ==> (≡)) vGPS_nWSP.
Proof.
- intros ? ? H1 ? ? H2 ? ? H3. constructor => ?. subst.
- unfold vGPS_RSP. rewrite /GPS_RSP /=.
- f_equiv. intros ? ?. by rewrite (gpsSWRaw_proper _ _ H1).
+ split=>?. rewrite !vGPS_nWSP_eq /=. subst. f_equiv=>??. by apply gpsSWpnRaw_proper.
Qed.
+End proper.
\ No newline at end of file
diff --git a/theories/invariants.v b/theories/invariants.v
index aedb5230eb582d6b2ce206f4344142a16d1e43c7..117264c350c48245b23eb22d12afcf6331a77b4d 100644
--- a/theories/invariants.v
+++ b/theories/invariants.v
@@ -17,7 +17,6 @@ Section Invariants.
Lemma inv_alloc_open N (E : coPset) (P : vProp Σ) :
↑N ⊆ E → (|={E,E ∖ ↑N}=> inv N P ∗ (â–· (É P) ={E ∖ ↑N,E}=∗ True))%I.
Proof.
- intros.
iStartProof (uPred _). iIntros.
iPoseProof (invariants.inv_alloc_open) as "T"; [done|].
iMod "T" as "[$ T2]". iModIntro.
@@ -27,8 +26,7 @@ Section Invariants.
Lemma inv_open (E : coPset) N (P : vProp Σ) :
↑N ⊆ E → inv N P -∗ |={E,E ∖ ↑N}=> â–· (É P) ∗ (â–· (É P) ={E ∖ ↑N,E}=∗ True).
Proof.
- intros.
- iStartProof (uPred _). iIntros (?) "H".
+ iStartProof (uPred _). iIntros (??) "H".
iPoseProof (invariants.inv_open with "H") as "T"; [done|].
rewrite monPred_all_eq /=.
iMod "T" as "[$ T2]". iModIntro.
@@ -45,9 +43,9 @@ Section Invariants.
Global Instance all_timeless (P : vProp Σ) {_ : Timeless P} : Timeless (É P).
Proof.
- revert H; rewrite monPred_all_eq /monPred_all_def; intros.
+ revert H; rewrite monPred_all_eq /monPred_all_def.
rewrite /Timeless /=.
- iStartProof (uPred _); iIntros (V) "H /=".
+ iStartProof (uPred _); iIntros (H V) "H /=".
cut (Timeless (∀ i, P i)); [|].
{ by move => ->. }
apply bi.forall_timeless.
@@ -119,7 +117,7 @@ Section Invariants.
Lemma all_entails (P Q : vProp Σ) : (P -∗ Q) -> bi_valid (É (P -∗ Q))%I.
Proof.
- intro; iIntros.
+ iIntros.
iApply objective_all.
- apply wand_objective; auto.
- iApply H.
diff --git a/theories/lifting_vProp.v b/theories/lifting_vProp.v
index 107bac4a064ec4c9561e548258180c484bef93fc..63dc2559f9d11562996036ef82d77ebe70139824 100644
--- a/theories/lifting_vProp.v
+++ b/theories/lifting_vProp.v
@@ -45,7 +45,7 @@ Lemma wp_pure_step_later `{Inhabited (state)} E e1 e2 φ Φ :
φ →
▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
Proof.
- intros. iStartProof (uPred _). iIntros (V) "W".
+ iStartProof (uPred _). iIntros (?? V) "W".
rewrite WP_Def.wp_eq /WP_Def.wp_def /=. iIntros (V' HV' π) "G".
iApply program_logic.lifting.wp_pure_step_fupd; [apply pure_exec_view; eassumption|done|].
iIntros "!>". by iApply "W".
diff --git a/theories/malloc.v b/theories/malloc.v
index d6042e0ff0572e35844ca560bafe546c5d43df20..955e5237b14d8c68ae21fe6a75c5f504c6fb7a2a 100644
--- a/theories/malloc.v
+++ b/theories/malloc.v
@@ -43,19 +43,18 @@ Section proof.
Lemma alloc (E : coPset) :
↑physN ⊆ E →
{{{ ⎡PSCtx⎤ }}}
- (Alloc) @ E
+ (Alloc) @ E
{{{ (l: loc), RET (#l); (l ↦ A) }}}%stdpp.
Proof.
- intros.
rewrite /own_loc_na /own_loc_prim /= valloc_local_eq /valloc_local_def.
rewrite WP_Def.wp_eq /WP_Def.wp_def.
iStartProof (uPred _).
- iIntros (?) "#kI". iIntros (V2 HV2) "Post". iIntros (V3 HV3 π) "kS".
+ iIntros (???) "#kI". iIntros (V2 HV2) "Post". iIntros (V3 HV3 π) "kS".
iApply program_logic.weakestpre.wp_mask_mono;
last (iApply (f_alloc with "[$kI $kS]"));
first auto.
- iNext. iIntros (l V' h' i) "(% & $ & oH & oI & % & % & %)". subst.
- destruct H3; subst.
+ iNext. iIntros (l V' h' i) "(% & $ & oH & oI & % & % & %)".
+ destruct H2; subst.
iApply ("Post" $! _ _ with "[%]"); [etrans;done|].
iExists _, _. by iFrame "oH oI".
Qed.
@@ -65,11 +64,10 @@ Section proof.
(Dealloc #l) @ ↑physN
{{{ RET (#()); True }}}%stdpp.
Proof.
- intros.
rewrite /own_loc /own_loc_prim /= valloc_local_eq /valloc_local_def.
rewrite WP_Def.wp_eq /WP_Def.wp_def.
iStartProof (uPred _).
- iIntros (V1) "[#kI oL]". iIntros (V2 HV2) "Post". iIntros (V3 HV3 π) "kS".
+ iIntros (? V1) "[#kI oL]". iIntros (V2 HV2) "Post". iIntros (V3 HV3 π) "kS".
iDestruct "oL" as (h i) "(Alloc & oH & oI)".
rewrite HV2. rewrite {1}HV3.
iApply (f_dealloc with "[$kI $kS $oH $oI $Alloc]").
diff --git a/theories/na.v b/theories/na.v
index 2350907f615e314e15f400b471bfc64f824035d3..b682fc4050184d6607fe2aa12f20a5de36820f99 100644
--- a/theories/na.v
+++ b/theories/na.v
@@ -56,10 +56,10 @@ Section Exclusive.
(* ∀ V, IntoExist (own_loc_na l v V) (λ V0, (own_loc_prim l {[v, V0]}) V). *)
(* Proof. apply _. Qed. *)
- Global Instance Frame_na_ownloc:
+ Global Instance Frame_na_ownloc l v:
Frame false ((own_loc_na l v)) (own_loc l) (True%I) | 1.
Proof.
- intros. rewrite /own_loc_na /own_loc /Frame. iStartProof (uPred _).
+ rewrite /own_loc_na /own_loc /Frame. iStartProof (uPred _).
iIntros (?) "[H _] /=". iDestruct "H" as (?) "?". iExists _. eauto.
Qed.
@@ -162,10 +162,9 @@ Section ExclusiveRules.
([ #l]_na) @ E
{{{ z, RET (#z); ⌜z = v⌠∗ (l ↦ v) }}}.
Proof.
- intros.
rewrite /own_loc_na /own_loc_prim /= valloc_local_eq /valloc_local_def.
rewrite WP_Def.wp_eq /WP_Def.wp_def /bi_affinely.
- iStartProof (uPred _). iIntros (?) "[#kI oNA]".
+ iStartProof (uPred _). iIntros (???) "[#kI oNA]".
iDestruct "oNA" as (V_0 i) "(Halloc & oH & oI)".
iIntros (V ->) "Post". iIntros (? H1 π) "S".
setoid_rewrite H1.
@@ -177,7 +176,7 @@ Section ExclusiveRules.
apply alloc_local_singleton_value_init].
- iNext. iIntros (v_r V') "(% & $ & oH & % & H)".
iDestruct "H" as (V_1) "(% & % & %)".
- move: H6 => /value_at_hd_singleton [[->] ->].
+ move: H5 => /value_at_hd_singleton [[->] ->].
iApply ("Post" $! v_r).
iSplit; first done.
iExists _, _. iFrame "oH oI". iPureIntro.
@@ -190,10 +189,9 @@ Section ExclusiveRules.
([ #l]_na <- #v_w) @ E
{{{ RET (#()); (l ↦ v_w) }}}.
Proof.
- intros.
rewrite /own_loc /own_loc_na /own_loc_prim /= valloc_local_eq /valloc_local_def.
rewrite WP_Def.wp_eq /WP_Def.wp_def.
- iStartProof (uPred _). iIntros (?) "[#kI oL]".
+ iStartProof (uPred _). iIntros (???) "[#kI oL]".
iDestruct "oL" as (h) "oL".
iDestruct "oL" as (i) "(Halloc & oH & oI)".
iIntros (? ->) "Post". iIntros (? -> π) "S".
@@ -331,11 +329,10 @@ Section FractionalRules.
[ #l ]_na @ E
{{{ z, RET (#z); ⌜z = v⌠∗ l ↦{q} v }}}.
Proof.
- intros.
rewrite /own_loc_na_frac /own_loc_na /own_loc_prim /= valloc_local_eq /valloc_local_def.
rewrite WP_Def.wp_eq /WP_Def.wp_def.
iStartProof (uPred _).
- iIntros (?) "[#kI oNA]". iIntros (V H1) "Post". iIntros (V2 H2 π) "S".
+ iIntros (????) "[#kI oNA]". iIntros (V H1) "Post". iIntros (V2 H2 π) "S".
setoid_rewrite H1. setoid_rewrite H2.
iDestruct "oNA" as (V_0) "(% & oNA)".
iMod (fractor_open with "oNA") as (X) "(oH & HX & HClose)"; [solve_ndisj|].
@@ -346,7 +343,7 @@ Section FractionalRules.
apply alloc_local_singleton_value_init].
- iNext. iIntros (v_r V') "(% & $ & oH & % & H)".
iDestruct "H" as (V_1) "(% & % & %)".
- move: H8 => /value_at_hd_singleton [[->] ->].
+ move: H6 => /value_at_hd_singleton [[->] ->].
iApply ("Post").
iMod ("HClose" $! (λ _ _ X, ⌜X = encode (VInj v_r)âŒ)%I with "[$oH $HX]")
as "oNA".
@@ -362,12 +359,11 @@ Section FractionalRules.
[ #l ]_na @ E
{{{ z, RET (#z); ⌜z = v⌠∗ ⎡(l ↦{q} v) V⎤ }}}.
Proof.
- intros.
rewrite /own_loc_na_frac /own_loc_na /own_loc_prim /=
valloc_local_eq /valloc_local_def.
rewrite WP_Def.wp_eq /WP_Def.wp_def.
iStartProof (uPred _).
- iIntros (?) "[#kI (ol & %)]". simpl. iIntros (??) "Post". iIntros (V2 H2 π) "S".
+ iIntros (????) "[#kI (ol & %)] /=". iIntros (??) "Post". iIntros (V2 H2 π) "S".
iDestruct "ol" as (V0) "[% ol]".
iMod (fractor_open with "ol") as (X) "(oH & HX & HClose)"; [solve_ndisj|].
assert (V ⊑ V2) by solve_jsl.
@@ -379,7 +375,7 @@ Section FractionalRules.
by apply: (alloc_local_proper).
- iNext. iIntros (v_r V') "(% & $ & oH & % & H)".
iDestruct "H" as (V_1) "(% & % & %)".
- move: H9 => /value_at_hd_singleton [[?] ?]. subst v_r V_1.
+ move: H7 => /value_at_hd_singleton [[?] ?]. subst v_r V_1.
iApply ("Post" $! _ _ with "[%]"); [by etrans|].
iMod ("HClose" $! (λ _ _ X, ⌜X = encode (VInj v)âŒ)%I with "[$oH $HX]")
as "ol".
@@ -390,10 +386,9 @@ Section FractionalRules.
↑ physN ⊆ E →
(⎡PSCtx⎤ ∗ l ↦ v ={E}=∗ l ↦{1} v)%I.
Proof.
- intros.
rewrite /own_loc_na_frac /own_loc_na /own_loc_prim /= valloc_local_eq /valloc_local_def.
iStartProof (uPred _).
- iIntros (?) "[kI na]".
+ iIntros (??) "[kI na]".
iDestruct "na" as (V' i) "(Local & Hist & Info)".
iExists V'. iFrame "Local".
iApply (fractor_alloc _ _ (encode (VInj v))); [done|by iFrame].
@@ -418,7 +413,7 @@ Section FractionalRules.
([ #l]_na <- #v) @ E
{{{ RET (#()); (l ↦{1} v) }}}.
Proof.
- intros. iIntros "[#kI oL] Post".
+ iIntros (??) "[#kI oL] Post".
iApply wp_fupd.
iApply (na_write with "[$kI $oL]"); [done|].
iNext. iIntros "oL".
@@ -433,7 +428,7 @@ Section FractionalRules.
([ #l]_na <- #v_w) @ E
{{{ RET (#()); (l ↦{1} v_w) }}}.
Proof.
- intros. iIntros "[#kI oL] Post".
+ iIntros (???) "[#kI oL] Post".
iDestruct (na_frac_dealloc with "oL") as ">oL"; first done.
by iApply (na_write_frac_1 with "[$kI $oL]").
Qed.
diff --git a/theories/persistor.v b/theories/persistor.v
index 47947d08d44b492d362b55ff65ad919b8ea7e43f..876c865345ca21f7cba1a9f37209d7ec79920902 100644
--- a/theories/persistor.v
+++ b/theories/persistor.v
@@ -54,20 +54,25 @@ Section Persistor.
Global Instance persisted_proper l : Proper ((≡) ==> (≡) ==> (≡)) (persisted l).
Proof.
- intros ? ? H1 ? ? H2. apply bi.exist_proper => ? /=.
- apply bi.sep_proper; [exact: H2|].
- apply bi.sep_proper; [|auto].
- f_equiv. exact: H1.
+ intros ? ? H1 ? ? H2. rewrite /persisted. repeat f_equiv. exact: H2. exact: H1.
Qed.
-
- Lemma persistor_mono l φ Ψ Ψ':
- (∀ X, Ψ l X → Ψ' l X) ∗ persisted l φ Ψ ⊢ persisted l φ Ψ'.
+ Global Instance persisted_ne l : NonExpansive2 (persisted l).
+ Proof.
+ intros ??? H1 ? ? H2. rewrite /persisted. repeat f_equiv. exact: H2. exact: H1.
+ Qed.
+ Global Instance persisted_contractive l n :
+ Proper (dist_later n ==> (=) ==> dist n) (persisted l).
Proof.
- iIntros "[Imp Per]".
- iDestruct "Per" as (X) "[Pre #Pers]".
- iExists X. iFrame "Pers".
- by iApply "Imp".
+ intros ?? H1 ?? ->. rewrite /persisted. repeat (f_contractive || f_equiv).
+ exact: H1.
Qed.
+ Global Instance persistor_mono l φ :
+ Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢)) (persisted l φ).
+ Proof. unfold persisted, pointwise_relation=>???. repeat f_equiv. auto. Qed.
+ Global Instance persistor_mono_flip l φ :
+ Proper ((flip (pointwise_relation _ (pointwise_relation _ (⊢)))) ==> flip (⊢))
+ (persisted l φ).
+ Proof. solve_proper. Qed.
Lemma persistor_drop l φ Ψ:
persisted l φ Ψ ⊢ ∃ X, Ψ l X.
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index fdb7002378bd5f44976473b0db5f504c8f203b4a..d100fd263583172d8015d69a49d77a1247bc671a 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -159,8 +159,8 @@ Qed.
Lemma wp_strong_mono E1 E2 e Φ Ψ :
E1 ⊆ E2 → (∀ v, Φ v ={E2}=∗ Ψ v) ∗ WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Ψ }}.
Proof.
- intros. iStartProof (uPred _). rewrite wp_eq /wp_def /=.
- iIntros (Vo) "[VS WP]". iIntros (V HV). iSpecialize ("WP" $! V with "[//]").
+ iStartProof (uPred _). rewrite wp_eq /wp_def /=.
+ iIntros (? Vo) "[VS WP]". iIntros (V HV). iSpecialize ("WP" $! V with "[//]").
iIntros (π) "S". iSpecialize ("WP" $! π with "S").
iApply (wp_strong_mono_iris with "[-$WP]"); first done.
iIntros (? V' HV'). iIntros "[$ HΦ]".
@@ -184,7 +184,7 @@ Lemma wp_atomic E1 E2 e Φ :
(∀ V, Atomic WeaklyAtomic ((e ,V) : ra_lang.expr)) →
(|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
Proof.
- intros Hatomic. iStartProof (uPred _). iIntros (?) "H".
+ iStartProof (uPred _). iIntros (Hatomic ?) "H".
rewrite wp_eq /wp_def /=. iIntros (?? π) "S".
iApply (weakestpre.wp_atomic _ E1 E2) => //. iMod "H". iModIntro.
iApply (weakestpre.wp_strong_mono _ _ E2 with "[-]"); [done..|by iApply "H"|].
@@ -196,7 +196,7 @@ Lemma wp_step_fupd E1 E2 e P Φ :
base.to_val e = None → E2 ⊆ E1 →
(|={E1,E2}▷=> P) -∗ WP e @ E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ E1 {{ Φ }}.
Proof.
- move => H1 H2. iStartProof (uPred _). iIntros (V) "HR". iIntros (V' ->).
+ iStartProof (uPred _). iIntros (H1 H2 V) "HR". iIntros (V' ->).
move: H1 H2. rewrite wp_eq /wp_def /=.
do !setoid_rewrite weakestpre.wp_unfold. rewrite /weakestpre.wp_pre.
rewrite /to_val /= /ra_lang.to_val /=.
@@ -416,9 +416,8 @@ Section proofmode_classes_embedding.
ElimModal (⎡|={E1,E2}=> A⎤) ⎡A⎤
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof.
- intros.
rewrite /ElimModal.
- iStartProof (upred.uPredSI _). iIntros (?) "[U WP]".
+ iStartProof (upred.uPredSI _). iIntros (??) "[U WP]".
iIntros (V -> π) "kS".
iMod "U".
iSpecialize ("WP" with "[U //]").
diff --git a/theories/wp_tactics_vProp.v b/theories/wp_tactics_vProp.v
index e5aca333de6aef77f2dd1f5dce0a9bf3ae221129..1f64da172620c9f356f90112bd699008642d4529 100644
--- a/theories/wp_tactics_vProp.v
+++ b/theories/wp_tactics_vProp.v
@@ -11,8 +11,7 @@ Lemma tac_wp_expr_eval `{foundationG Σ} Δ E Φ e e' :
Proof. by intros ->. Qed.
Ltac wp_expr_eval t :=
- try iStartProof;
- try (eapply tac_wp_expr_eval; [t; reflexivity|]).
+ try (iStartProof; eapply tac_wp_expr_eval; [t; reflexivity|]).
Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.