Commit 027f63a2 authored by Robbert Krebbers's avatar Robbert Krebbers

Make own_valid_[n] and own_update_[n] curried.

parent 85697195
Pipeline #3018 passed with stage
in 9 minutes and 59 seconds
......@@ -117,12 +117,12 @@ Section auth.
(a f t) φ t u b,
((f t, a) ~l~> (f u, b)) φ u ={E}= auth_inv γ f φ auth_own γ b.
Proof.
iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own.
iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
iDestruct "Hinv" as (t) "[>Hγa Hφ]".
iModIntro. iExists t.
iDestruct (own_valid_2 with "[$Hγa $Hγf]") as % [? ?]%auth_valid_discrete_2.
iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_valid_discrete_2.
iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
iMod (own_update_2 with "[$Hγa $Hγf]") as "[Hγa Hγf]".
iMod (own_update_2 with "Hγa Hγf") as "[Hγa Hγf]".
{ eapply auth_update; eassumption. }
iModIntro. iFrame. iExists u. iFrame.
Qed.
......
......@@ -57,7 +57,7 @@ Proof. apply _. Qed.
Lemma box_own_auth_agree γ b1 b2 :
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2) b1 = b2.
Proof.
rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_l.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
Qed.
......@@ -72,7 +72,7 @@ Qed.
Lemma box_own_agree γ Q1 Q2 :
(box_own_prop γ Q1 box_own_prop γ Q2) (Q1 Q2).
Proof.
rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_r.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
iIntros "#HQ". iNext. rewrite -{2}(iProp_fold_unfold Q1).
iRewrite "HQ". by rewrite iProp_fold_unfold.
......
......@@ -39,7 +39,7 @@ Section proofs.
Proof. by rewrite cinv_own_op Qp_div_2. Qed.
Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 cinv_own γ q2 (q1 + q2)%Qp.
Proof. rewrite /cinv_own own_valid_2. by iIntros "% !%". Qed.
Proof. rewrite /cinv_own -own_op own_valid. by iIntros "% !%". Qed.
Lemma cinv_own_1_l γ q : cinv_own γ 1 cinv_own γ q False.
Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed.
......
......@@ -68,11 +68,10 @@ Proof.
(* implicit arguments differ a bit *)
by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
Qed.
Lemma own_valid_2 γ a1 a2 : own γ a1 own γ a2 (a1 a2).
Proof. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 own γ a2 own γ a3 (a1 a2 a3).
Proof. by rewrite -!own_op assoc own_valid. Qed.
Lemma own_valid_2 γ a1 a2 : own γ a1 own γ a2 - (a1 a2).
Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 own γ a2 - own γ a3 - (a1 a2 a3).
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
Lemma own_valid_r γ a : own γ a own γ a a.
Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a a own γ a.
......@@ -122,11 +121,11 @@ Proof.
by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
Qed.
Lemma own_update_2 γ a1 a2 a' :
a1 a2 ~~> a' own γ a1 own γ a2 == own γ a'.
Proof. intros. rewrite -own_op. by apply own_update. Qed.
a1 a2 ~~> a' own γ a1 own γ a2 == own γ a'.
Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
Lemma own_update_3 γ a1 a2 a3 a' :
a1 a2 a3 ~~> a' own γ a1 own γ a2 own γ a3 == own γ a'.
Proof. intros. rewrite -!own_op assoc. by apply own_update. Qed.
a1 a2 a3 ~~> a' own γ a1 own γ a2 - own γ a3 == own γ a'.
Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
End global.
Arguments own_valid {_ _} [_] _ _.
......
......@@ -35,7 +35,7 @@ Section saved_prop.
Lemma saved_prop_agree γ x y :
saved_prop_own γ x saved_prop_own γ y (x y).
Proof.
rewrite own_valid_2 agree_validI agree_equivI later_equivI.
rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
assert ( z, G2 (G1 z) z) as help.
......
......@@ -57,7 +57,7 @@ Proof. by rewrite (own_empty (coPset_disjUR) enabled_name). Qed.
Lemma ownE_op E1 E2 : E1 E2 ownE (E1 E2) ⊣⊢ ownE E1 ownE E2.
Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
Lemma ownE_disjoint E1 E2 : ownE E1 ownE E2 E1 E2.
Proof. rewrite /ownE own_valid_2. by iIntros (?%coPset_disj_valid_op). Qed.
Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed.
Lemma ownE_op' E1 E2 : E1 E2 ownE (E1 E2) ⊣⊢ ownE E1 ownE E2.
Proof.
iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
......@@ -72,7 +72,7 @@ Proof. by rewrite (own_empty (gset_disjUR positive) disabled_name). Qed.
Lemma ownD_op E1 E2 : E1 E2 ownD (E1 E2) ⊣⊢ ownD E1 ownD E2.
Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
Lemma ownD_disjoint E1 E2 : ownD E1 ownD E2 E1 E2.
Proof. rewrite /ownD own_valid_2. by iIntros (?%gset_disj_valid_op). Qed.
Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
Lemma ownD_op' E1 E2 : E1 E2 ownD (E1 E2) ⊣⊢ ownD E1 ownD E2.
Proof.
iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
......@@ -87,7 +87,7 @@ Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
own invariant_name ( {[i := invariant_unfold P]})
Q, I !! i = Some Q (Q P).
Proof.
rewrite own_valid_2 auth_validI /=. iIntros "[#HI #HvI]".
rewrite -own_op own_valid auth_validI /=. iIntros "[#HI #HvI]".
iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
rewrite left_id_L lookup_fmap lookup_op lookup_singleton uPred.option_equivI.
......
......@@ -54,9 +54,9 @@ Section mono_proof.
iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "[$Hγ $Hγf]")
- iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. }
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
......@@ -74,9 +74,9 @@ Section mono_proof.
Proof.
iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]")
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ c); auto. }
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
......@@ -132,7 +132,7 @@ Section contrib_spec.
iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
- iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, option_local_update, prod_local_update_2.
apply (nat_local_update _ _ (S c) (S n)); omega. }
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
......@@ -149,7 +149,7 @@ Section contrib_spec.
Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]")
iDestruct (own_valid_2 with "Hγ Hγf")
as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
......@@ -161,7 +161,7 @@ Section contrib_spec.
Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]") as %[Hn _]%auth_valid_discrete_2.
iDestruct (own_valid_2 with "Hγ Hγf") as %[Hn _]%auth_valid_discrete_2.
apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
by iApply "HΦ".
......
......@@ -32,7 +32,7 @@ Section proof.
Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
Lemma locked_exclusive (γ : gname) : locked γ locked γ False.
Proof. rewrite /locked own_valid_2. by iIntros (?). Qed.
Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
Proof. solve_proper. Qed.
......
......@@ -101,7 +101,7 @@ Section proof.
iModIntro. wp_let. wp_op=>[_|[]] //.
wp_if.
iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
+ iDestruct (own_valid_2 with "[$Ht $Haown]") as % [_ ?%gset_disj_valid_op].
+ iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
set_solver.
- iMod ("Hclose" with "[Hlo Hln Ha]").
{ iNext. iExists o, n. by iFrame. }
......@@ -149,18 +149,18 @@ Section proof.
rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
wp_load.
iDestruct (own_valid_2 with "[$Hauth $Hγo]") as
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iMod ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
{ iNext. iExists o, n. by iFrame. }
iModIntro. wp_op.
iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
wp_store.
iDestruct (own_valid_2 with "[$Hauth $Hγo]") as
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iDestruct "Haown" as "[[Hγo' _]|?]".
{ iDestruct (own_valid_2 with "[$Hγo $Hγo']") as %[[] ?]. }
iMod (own_update_2 with "[$Hauth $Hγo]") as "[Hauth Hγo]".
{ iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
{ apply auth_update, prod_local_update_1.
by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
iMod ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last by iApply "HΦ".
......
......@@ -115,13 +115,13 @@ Implicit Types e : expr Λ.
(* Physical state *)
Lemma ownP_twice σ1 σ2 : ownP σ1 ownP σ2 False.
Proof. rewrite /ownP own_valid_2. by iIntros (?). Qed.
Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
Proof. rewrite /ownP; apply _. Qed.
Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ownP σ2 σ1 = σ2.
Proof.
rewrite /ownP /ownP_auth own_valid_2 -auth_both_op.
rewrite /ownP /ownP_auth -own_op own_valid -auth_both_op.
by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
Qed.
Lemma ownP_update σ1 σ2 : ownP_auth σ1 ownP σ1 == ownP_auth σ2 ownP σ2.
......
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