Skip to content
GitLab
Commit 7fd895dd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use generic big op lemmas instead of uPred specific ones when possible.

parent 6fbff46e
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/boxes.v
View file @ 7fd895dd
......@@ -97,9 +97,8 @@ Qed.
Lemma box_alloc : box N ∅ True%I.
Proof.
iIntros; iExists (λ _, True)%I; iSplit.
- iNext. by rewrite big_sepM_empty.
- by rewrite big_sepM_empty.
iIntros; iExists (λ _, True)%I; iSplit; last done.
iNext. by rewrite big_opM_empty.
Qed.
Lemma slice_insert_empty E q f Q P :
......@@ -116,8 +115,8 @@ Proof.
{ iNext. iExists false; eauto. }
iModIntro; iExists γ; repeat iSplit; auto.
iNext. iExists (<[γ:=Q]> Φ); iSplit.
- iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'.
- rewrite (big_sepM_fn_insert (λ _ _ P', _ ∗ _ _ P' ∗ _ _ (_ _ P')))%I //.
- iNext. iRewrite "HeqP". by rewrite big_opM_fn_insert'.
- rewrite (big_opM_fn_insert (λ _ _ P', _ ∗ _ _ P' ∗ _ _ (_ _ P')))%I //.
iFrame; eauto.
Qed.
......@@ -130,13 +129,13 @@ Proof.
iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
iInv N as (b) "[>Hγ _]" "Hclose".
iDestruct (big_sepM_delete _ f _ false with "Hf")
iDestruct (big_opM_delete _ f _ false with "Hf")
as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
iMod ("Hclose" with "[Hγ]"); first iExists false; eauto.
iModIntro. iNext. iSplit.
- iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
- iExists Φ; eauto.
Qed.
......@@ -147,13 +146,13 @@ Lemma slice_fill E q f γ P Q :
Proof.
iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b') "[>Hγ _]" "Hclose".
iDestruct (big_sepM_delete _ f _ false with "Hf")
iDestruct (big_opM_delete _ f _ false with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
iMod ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
- by rewrite big_opM_insert_override.
- rewrite -insert_delete big_opM_insert ?lookup_delete //.
iFrame; eauto.
Qed.
......@@ -164,15 +163,15 @@ Lemma slice_empty E q f P Q γ :
Proof.
iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b) "[>Hγ HQ]" "Hclose".
iDestruct (big_sepM_delete _ f with "Hf")
iDestruct (big_opM_delete _ f with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iFrame "HQ".
iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
- by rewrite big_opM_insert_override.
- rewrite -insert_delete big_opM_insert ?lookup_delete //.
iFrame; eauto.
Qed.
......@@ -205,11 +204,11 @@ Lemma box_fill E f P :
box N f P -∗ ▷ P ={E}=∗ box N (const true <$> f) P.
Proof.
iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
rewrite internal_eq_iff later_iff big_sepM_later.
iExists Φ; iSplitR; first by rewrite big_opM_fmap.
rewrite internal_eq_iff later_iff big_opM_commute.
iDestruct ("HeqP" with "HP") as "HP".
iCombine "Hf" "HP" as "Hf".
rewrite -big_sepM_sepM big_sepM_fmap; iApply (fupd_big_sepM _ _ f).
rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
iApply (@big_sepM_impl with "[$Hf]").
iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]" "Hclose".
......@@ -226,7 +225,7 @@ Proof.
iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ) ∗
[∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' false) ∗ box_own_prop γ (Φ γ) ∗
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
{ rewrite -big_sepM_sepM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
{ rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto.
iInv N as (b) "[>Hγ HΦ]" "Hclose".
......@@ -235,8 +234,8 @@ Proof.
iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
iFrame "HγΦ Hinv". by iApply "HΦ". }
iModIntro; iSplitL "HΦ".
- rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
- iExists Φ; iSplit; by rewrite big_sepM_fmap.
- rewrite internal_eq_iff later_iff big_opM_commute. by iApply "HeqP".
- iExists Φ; iSplit; by rewrite big_opM_fmap.
Qed.
Lemma slice_iff E q f P Q Q' γ b :
......
theories/base_logic/lib/fractional.v
View file @ 7fd895dd
......@@ -63,30 +63,22 @@ Section fractional.
Global Instance fractional_big_sepL {A} l Ψ :
(∀ k (x : A), Fractional (Ψ k x)) →
Fractional (M:=M) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I.
Proof.
intros ? q q'. rewrite -big_sepL_sepL. by setoid_rewrite fractional.
Qed.
Proof. intros ? q q'. rewrite -big_opL_opL. by setoid_rewrite fractional. Qed.
Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
(∀ k (x : A), Fractional (Ψ k x)) →
Fractional (M:=M) (λ q, [∗ map] k↦x ∈ m, Ψ k x q)%I.
Proof.
intros ? q q'. rewrite -big_sepM_sepM. by setoid_rewrite fractional.
Qed.
Proof. intros ? q q'. rewrite -big_opM_opM. by setoid_rewrite fractional. Qed.
Global Instance fractional_big_sepS `{Countable A} (X : gset A) Ψ :
(∀ x, Fractional (Ψ x)) →
Fractional (M:=M) (λ q, [∗ set] x ∈ X, Ψ x q)%I.
Proof.
intros ? q q'. rewrite -big_sepS_sepS. by setoid_rewrite fractional.
Qed.
Proof. intros ? q q'. rewrite -big_opS_opS. by setoid_rewrite fractional. Qed.
Global Instance fractional_big_sepMS `{Countable A} (X : gmultiset A) Ψ :
(∀ x, Fractional (Ψ x)) →
Fractional (M:=M) (λ q, [∗ mset] x ∈ X, Ψ x q)%I.
Proof.
intros ? q q'. rewrite -big_sepMS_sepMS. by setoid_rewrite fractional.
Qed.
Proof. intros ? q q'. rewrite -big_opMS_opMS. by setoid_rewrite fractional. Qed.
(** Mult instances *)
......
theories/base_logic/lib/wsat.v
View file @ 7fd895dd
......@@ -105,9 +105,9 @@ Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ow
Proof.
rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
iDestruct (invariant_lookup I i P with "[$]") as (Q) "[% #HPQ]".
iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
- iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
iFrame "HI"; eauto.
- iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
Qed.
......@@ -115,9 +115,9 @@ Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ o
Proof.
rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
iDestruct (invariant_lookup with "[$]") as (Q) "[% #HPQ]".
iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
- iDestruct (ownD_singleton_twice with "[$]") as %[].
- iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
- iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
Qed.
......@@ -139,7 +139,7 @@ Proof.
iModIntro; iExists i; iSplit; [done|]. rewrite /ownI; iFrame "HiP".
iExists (<[i:=P]>I); iSplitL "Hw".
{ by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
iApply (big_sepM_insert _ I); first done.
iApply (big_opM_insert _ I); first done.
iFrame "HI". iLeft. by rewrite /ownD; iFrame.
Qed.
......@@ -162,7 +162,7 @@ Proof.
rewrite -/(ownD _). iFrame "HD".
iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
{ by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
iApply (big_sepM_insert _ I); first done.
iApply (big_opM_insert _ I); first done.
iFrame "HI". by iRight.
Qed.
End wsat.
theories/base_logic/tactics.v
View file @ 7fd895dd
......@@ -28,7 +28,7 @@ Module uPred_reflection. Section uPred_reflection.
Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
Proof.
induction e as [| |e1 IH1 e2 IH2];
rewrite /= ?right_id ?big_sepL_app ?IH1 ?IH2 //.
rewrite /= ?right_id ?big_opL_app ?IH1 ?IH2 //.
Qed.
Lemma flatten_entails Σ e1 e2 :
flatten e2 ⊆+ flatten e1 → eval Σ e1 ⊢ eval Σ e2.
......@@ -89,7 +89,7 @@ Module uPred_reflection. Section uPred_reflection.
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
rewrite !big_sepL_app. apply sep_mono_r.
rewrite !big_opL_app. apply sep_mono_r.
Qed.
Fixpoint to_expr (l : list nat) : expr :=
......@@ -109,7 +109,7 @@ Module uPred_reflection. Section uPred_reflection.
cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ (to_expr ns) ∗ eval Σ e').
Proof.
intros He%flatten_cancel.
by rewrite eval_flatten He big_sepL_app eval_to_expr eval_flatten.
by rewrite eval_flatten He big_opL_app eval_to_expr eval_flatten.
Qed.
Lemma split_r Σ e ns e' :
cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ e' ∗ eval Σ (to_expr ns)).
......
theories/heap_lang/lib/barrier/proof.v
View file @ 7fd895dd
......@@ -76,15 +76,15 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
ress P ({[i1;i2]} ∪ I ∖ {[i]}).
Proof.
iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
iDestruct (big_opS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
iDestruct (big_opS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
rewrite -assoc_L !big_sepS_fn_insert'; [|abstract set_solver ..].
rewrite -assoc_L !big_opS_fn_insert'; [|abstract set_solver ..].
by iFrame.
- rewrite -assoc_L !big_sepS_fn_insert; [|abstract set_solver ..]. eauto.
- rewrite -assoc_L !big_opS_fn_insert; [|abstract set_solver ..]. eauto.
Qed.
(** Actual proofs *)
......@@ -98,7 +98,7 @@ Proof.
iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as (γ') "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame.
iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
iExists (const P). rewrite !big_opS_singleton /=. eauto. }
iAssert (barrier_ctx γ' l P)%I as "#?".
{ done. }
iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
......@@ -147,9 +147,9 @@ Proof.
- (* a High state: the comparison succeeds, and we perform a transition and
return to the client *)
iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iDestruct (big_opS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iAssert (▷ Ψ i ∗ ▷ [∗ set] j ∈ I ∖ {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
{ iNext. iApply (big_opS_delete _ _ i); first done. by iApply "HΨ". }
iMod ("Hclose" $! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]").
{ iSplit; [iPureIntro; by eauto using wait_step|].
rewrite /barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
......
theories/program_logic/adequacy.v
View file @ 7fd895dd
......@@ -30,7 +30,7 @@ Proof.
iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
rewrite /wsat /ownE; iFrame.
iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
Qed.
(* Program logic adequacy *)
......
theories/proofmode/class_instances.v
View file @ 7fd895dd
......@@ -181,7 +181,7 @@ Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat → A → uPred M) (l: l
IntoLaterN' n ([∗ list] k ↦ x ∈ l, Φ k x) ([∗ list] k ↦ x ∈ l, Ψ k x).
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ?.
rewrite big_sepL_laterN. by apply big_sepL_mono.
rewrite big_opL_commute. by apply big_sepL_mono.
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
(Φ Ψ : K → A → uPred M) (m : gmap K A) :
......@@ -189,7 +189,7 @@ Global Instance into_laterN_big_sepM n `{Countable K} {A}
IntoLaterN' n ([∗ map] k ↦ x ∈ m, Φ k x) ([∗ map] k ↦ x ∈ m, Ψ k x).
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ?.
rewrite big_sepM_laterN; by apply big_sepM_mono.
rewrite big_opM_commute; by apply big_sepM_mono.
Qed.
Global Instance into_laterN_big_sepS n `{Countable A}
(Φ Ψ : A → uPred M) (X : gset A) :
......@@ -197,7 +197,7 @@ Global Instance into_laterN_big_sepS n `{Countable A}
IntoLaterN' n ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ x).
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ?.
rewrite big_sepS_laterN; by apply big_sepS_mono.
rewrite big_opS_commute; by apply big_sepS_mono.
Qed.
Global Instance into_laterN_big_sepMS n `{Countable A}
(Φ Ψ : A → uPred M) (X : gmultiset A) :
......@@ -205,7 +205,7 @@ Global Instance into_laterN_big_sepMS n `{Countable A}
IntoLaterN' n ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ x).
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ?.
rewrite big_sepMS_laterN; by apply big_sepMS_mono.
rewrite big_opMS_commute; by apply big_sepMS_mono.
Qed.
(* FromLater *)
......@@ -464,7 +464,7 @@ Global Instance frame_big_sepL_app {A} p (Φ : nat → A → uPred M) R Q l l1 l
Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
[∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ.
Global Instance make_and_true_l P : MakeAnd True P P.
......
theories/proofmode/coq_tactics.v
View file @ 7fd895dd
......@@ -234,14 +234,14 @@ Proof.
intros j. apply (env_app_disjoint _ _ _ j) in Happ.
naive_solver eauto using env_app_fresh.
+ rewrite (env_app_perm _ _ Γp') //.
rewrite big_sepL_app always_sep. solve_sep_entails.
rewrite big_opL_app always_sep. solve_sep_entails.
- destruct (env_app Γ Γp) eqn:Happ,
(env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using env_app_wf.
intros j. apply (env_app_disjoint _ _ _ j) in Happ.
naive_solver eauto using env_app_fresh.
+ rewrite (env_app_perm _ _ Γs') // big_sepL_app. solve_sep_entails.
+ rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Qed.
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
......@@ -257,14 +257,14 @@ Proof.
intros j. apply (env_app_disjoint _ _ _ j) in Happ.
destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
+ rewrite (env_replace_perm _ _ Γp') //.
rewrite big_sepL_app always_sep. solve_sep_entails.
rewrite big_opL_app always_sep. solve_sep_entails.
- destruct (env_app Γ Γp) eqn:Happ,
(env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using env_replace_wf.
intros j. apply (env_app_disjoint _ _ _ j) in Happ.
destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
+ rewrite (env_replace_perm _ _ Γs') // big_sepL_app. solve_sep_entails.
+ rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Qed.
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
......
Supports Markdown
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