Commit 84490edc authored by Robbert Krebbers's avatar Robbert Krebbers

Fix inconsistent names for bigop lemmas.

Notably, `big_andL_andL` and `big_andL_and` where a ⊣⊢ and ⊢ version
of the same lemma. I favored the `big_opL_op` naming scheme.
parent d62f14ed
......@@ -145,7 +145,7 @@ Section list.
([^o list] ky h <$> l, f k y) ([^o list] ky l, f k (h y)).
Proof. revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite IH. Qed.
Lemma big_opL_opL f g l :
Lemma big_opL_op f g l :
([^o list] kx l, f k x `o` g k x)
([^o list] kx l, f k x) `o` ([^o list] kx l, g k x).
Proof.
......@@ -253,10 +253,10 @@ Section gmap.
rewrite -assoc IH //.
Qed.
Lemma big_opM_opM f g m :
Lemma big_opM_op f g m :
([^o map] kx m, f k x `o` g k x)
([^o map] kx m, f k x) `o` ([^o map] kx m, g k x).
Proof. rewrite /big_opM -big_opL_opL. by apply big_opL_proper=> ? [??]. Qed.
Proof. rewrite /big_opM -big_opL_op. by apply big_opL_proper=> ? [??]. Qed.
End gmap.
......@@ -335,9 +335,9 @@ Section gset.
induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id //.
Qed.
Lemma big_opS_opS f g X :
Lemma big_opS_op f g X :
([^o set] y X, f y `o` g y) ([^o set] y X, f y) `o` ([^o set] y X, g y).
Proof. by rewrite /big_opS -big_opL_opL. Qed.
Proof. by rewrite /big_opS -big_opL_op. Qed.
End gset.
Lemma big_opM_dom `{Countable K} {A} (f : K M) (m : gmap K A) :
......@@ -403,9 +403,9 @@ Section gmultiset.
rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id //.
Qed.
Lemma big_opMS_opMS f g X :
Lemma big_opMS_op f g X :
([^o mset] y X, f y `o` g y) ([^o mset] y X, f y) `o` ([^o mset] y X, g y).
Proof. by rewrite /big_opMS -big_opL_opL. Qed.
Proof. by rewrite /big_opMS -big_opL_op. Qed.
End gmultiset.
End big_op.
......
......@@ -210,7 +210,7 @@ Proof.
iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
iDestruct ("HeqP" with "HP") as "HP".
iCombine "Hf" "HP" as "Hf".
rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
rewrite -big_sepM_sep big_opM_fmap; iApply (fupd_big_sepM _ _ f).
iApply (@big_sepM_impl with "Hf").
iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]".
......@@ -227,7 +227,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_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
{ rewrite -big_sepM_sep -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto.
iInv N as (b) "[>Hγ HΦ]".
......
......@@ -132,10 +132,10 @@ Section sep_list.
([ list] ky f <$> l, Φ k y) ([ list] ky l, Φ k (f y)).
Proof. by rewrite big_opL_fmap. Qed.
Lemma big_sepL_sepL Φ Ψ l :
Lemma big_sepL_sep Φ Ψ l :
([ list] kx l, Φ k x Ψ k x)
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. by rewrite big_opL_opL. Qed.
Proof. by rewrite big_opL_op. Qed.
Lemma big_sepL_and Φ Ψ l :
([ list] kx l, Φ k x Ψ k x)
......@@ -392,11 +392,11 @@ Section sep_list2.
by f_equiv; f_equiv=> k [??].
Qed.
Lemma big_sepL2_sepL2 Φ Ψ l1 l2 :
Lemma big_sepL2_sep Φ Ψ l1 l2 :
([ list] ky1;y2 l1;l2, Φ k y1 y2 Ψ k y1 y2)
([ list] ky1;y2 l1;l2, Φ k y1 y2) ([ list] ky1;y2 l1;l2, Ψ k y1 y2).
Proof.
rewrite !big_sepL2_alt big_sepL_sepL !persistent_and_affinely_sep_l.
rewrite !big_sepL2_alt big_sepL_sep !persistent_and_affinely_sep_l.
rewrite -assoc (assoc _ _ (<affine> _)%I). rewrite -(comm bi_sep (<affine> _)%I).
rewrite -assoc (assoc _ _ (<affine> _)%I) -!persistent_and_affinely_sep_l.
by rewrite affinely_and_r persistent_and_affinely_sep_l idemp.
......@@ -507,15 +507,10 @@ Section and_list.
([ list] ky f <$> l, Φ k y) ([ list] ky l, Φ k (f y)).
Proof. by rewrite big_opL_fmap. Qed.
Lemma big_andL_andL Φ Ψ l :
([ list] kx l, Φ k x Ψ k x)
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. by rewrite big_opL_opL. Qed.
Lemma big_andL_and Φ Ψ l :
([ list] kx l, Φ k x Ψ k x)
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. by rewrite big_opL_op. Qed.
Lemma big_andL_persistently Φ l :
<pers> ([ list] kx l, Φ k x) [ list] kx l, <pers> (Φ k x).
......@@ -667,10 +662,10 @@ Section map.
([ map] ky m1, Φ k y) ([ map] ky m2, Φ k y).
Proof. apply big_opM_union. Qed.
Lemma big_sepM_sepM Φ Ψ m :
Lemma big_sepM_sep Φ Ψ m :
([ map] kx m, Φ k x Ψ k x)
([ map] kx m, Φ k x) ([ map] kx m, Ψ k x).
Proof. apply big_opM_opM. Qed.
Proof. apply big_opM_op. Qed.
Lemma big_sepM_and Φ Ψ m :
([ map] kx m, Φ k x Ψ k x)
......@@ -962,7 +957,7 @@ Section map2.
([ map] ky1;y2 m1;m2, Φ k y1 (g y2)).
Proof. rewrite -{1}(map_fmap_id m1). apply big_sepM2_fmap. Qed.
Lemma big_sepM2_sepM2 Φ Ψ m1 m2 :
Lemma big_sepM2_sep Φ Ψ m1 m2 :
([ map] ky1;y2 m1;m2, Φ k y1 y2 Ψ k y1 y2)
([ map] ky1;y2 m1;m2, Φ k y1 y2) ([ map] ky1;y2 m1;m2, Ψ k y1 y2).
Proof.
......@@ -972,7 +967,7 @@ Section map2.
rewrite !persistent_and_affinely_sep_l /=.
rewrite -sep_assoc. apply sep_proper=>//.
rewrite sep_assoc (sep_comm _ (<affine> _)%I) -sep_assoc.
apply sep_proper=>//. apply big_sepM_sepM.
apply sep_proper=>//. apply big_sepM_sep.
Qed.
Lemma big_sepM2_and Φ Ψ m1 m2 :
......@@ -1148,9 +1143,9 @@ Section gset.
(([ set] y Y, P y Φ y) - [ set] y X, Φ y).
Proof. intros. setoid_rewrite <-decide_emp. by apply big_sepS_filter_acc'. Qed.
Lemma big_sepS_sepS Φ Ψ X :
Lemma big_sepS_sep Φ Ψ X :
([ set] y X, Φ y Ψ y) ([ set] y X, Φ y) ([ set] y X, Ψ y).
Proof. apply big_opS_opS. Qed.
Proof. apply big_opS_op. Qed.
Lemma big_sepS_and Φ Ψ X :
([ set] y X, Φ y Ψ y) ([ set] y X, Φ y) ([ set] y X, Ψ y).
......@@ -1256,9 +1251,9 @@ Section gmultiset.
Lemma big_sepMS_singleton Φ x : ([ mset] y {[ x ]}, Φ y) Φ x.
Proof. apply big_opMS_singleton. Qed.
Lemma big_sepMS_sepMS Φ Ψ X :
Lemma big_sepMS_sep Φ Ψ X :
([ mset] y X, Φ y Ψ y) ([ mset] y X, Φ y) ([ mset] y X, Ψ y).
Proof. apply big_opMS_opMS. Qed.
Proof. apply big_opMS_op. Qed.
Lemma big_sepMS_and Φ Ψ X :
([ mset] y X, Φ y Ψ y) ([ mset] y X, Φ y) ([ mset] y X, Ψ y).
......
......@@ -64,22 +64,22 @@ Section fractional.
Global Instance fractional_big_sepL {A} l Ψ :
( k (x : A), Fractional (Ψ k x))
Fractional (PROP:=PROP) (λ q, [ list] kx l, Ψ k x q)%I.
Proof. intros ? q q'. rewrite -big_opL_opL. by setoid_rewrite fractional. Qed.
Proof. intros ? q q'. rewrite -big_sepL_sep. by setoid_rewrite fractional. Qed.
Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
( k (x : A), Fractional (Ψ k x))
Fractional (PROP:=PROP) (λ q, [ map] kx m, Ψ k x q)%I.
Proof. intros ? q q'. rewrite -big_opM_opM. by setoid_rewrite fractional. Qed.
Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed.
Global Instance fractional_big_sepS `{Countable A} (X : gset A) Ψ :
( x, Fractional (Ψ x))
Fractional (PROP:=PROP) (λ q, [ set] x X, Ψ x q)%I.
Proof. intros ? q q'. rewrite -big_opS_opS. by setoid_rewrite fractional. Qed.
Proof. intros ? q q'. rewrite -big_sepS_sep. by setoid_rewrite fractional. Qed.
Global Instance fractional_big_sepMS `{Countable A} (X : gmultiset A) Ψ :
( x, Fractional (Ψ x))
Fractional (PROP:=PROP) (λ q, [ mset] x X, Ψ x q)%I.
Proof. intros ? q q'. rewrite -big_opMS_opMS. by setoid_rewrite fractional. Qed.
Proof. intros ? q q'. rewrite -big_sepMS_sep. by setoid_rewrite fractional. Qed.
(** Mult instances *)
......
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