### 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] k↦y ∈ h <\$> l, f k y) ≡ ([^o list] k↦y ∈ 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] k↦x ∈ l, f k x `o` g k x) ≡ ([^o list] k↦x ∈ l, f k x) `o` ([^o list] k↦x ∈ 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] k↦x ∈ m, f k x `o` g k x) ≡ ([^o map] k↦x ∈ m, f k x) `o` ([^o map] k↦x ∈ 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] k↦y ∈ f <\$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k (f y)). Proof. by rewrite big_opL_fmap. Qed. Lemma big_sepL_sepL Φ Ψ l : Lemma big_sepL_sep Φ Ψ l : ([∗ list] k↦x ∈ l, Φ k x ∗ Ψ k x) ⊣⊢ ([∗ list] k↦x ∈ l, Φ k x) ∗ ([∗ list] k↦x ∈ l, Ψ k x). Proof. by rewrite big_opL_opL. Qed. Proof. by rewrite big_opL_op. Qed. Lemma big_sepL_and Φ Ψ l : ([∗ list] k↦x ∈ 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] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2) ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ ([∗ list] k↦y1;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 _ _ ( _)%I). rewrite -(comm bi_sep ( _)%I). rewrite -assoc (assoc _ _ ( _)%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] k↦y ∈ f <\$> l, Φ k y) ⊣⊢ ([∧ list] k↦y ∈ l, Φ k (f y)). Proof. by rewrite big_opL_fmap. Qed. Lemma big_andL_andL Φ Ψ l : ([∧ list] k↦x ∈ l, Φ k x ∧ Ψ k x) ⊣⊢ ([∧ list] k↦x ∈ l, Φ k x) ∧ ([∧ list] k↦x ∈ l, Ψ k x). Proof. by rewrite big_opL_opL. Qed. Lemma big_andL_and Φ Ψ l : ([∧ list] k↦x ∈ l, Φ k x ∧ Ψ k x) ⊢ ([∧ list] k↦x ∈ l, Φ k x) ∧ ([∧ list] k↦x ∈ l, Ψ k x). Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed. ⊣⊢ ([∧ list] k↦x ∈ l, Φ k x) ∧ ([∧ list] k↦x ∈ l, Ψ k x). Proof. by rewrite big_opL_op. Qed. Lemma big_andL_persistently Φ l : ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, (Φ k x). ... ... @@ -667,10 +662,10 @@ Section map. ⊣⊢ ([∗ map] k↦y ∈ m1, Φ k y) ∗ ([∗ map] k↦y ∈ m2, Φ k y). Proof. apply big_opM_union. Qed. Lemma big_sepM_sepM Φ Ψ m : Lemma big_sepM_sep Φ Ψ m : ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x) ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x). Proof. apply big_opM_opM. Qed. Proof. apply big_opM_op. Qed. Lemma big_sepM_and Φ Ψ m : ([∗ map] k↦x ∈ m, Φ k x ∧ Ψ k x) ... ... @@ -962,7 +957,7 @@ Section map2. ⊣⊢ ([∗ map] k↦y1;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] k↦y1;y2 ∈ m1;m2, Φ k y1 y2 ∗ Ψ k y1 y2) ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∗ ([∗ map] k↦y1;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 _ ( _)%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] k↦x ∈ 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] k↦x ∈ 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!
{"ft_lang_label":"__label__en","ft_lang_prob":0.5448179,"math_prob":0.9389105,"size":237,"snap":"2021-43-2021-49","text_gpt3_token_len":72,"char_repetition_ratio":0.13304721,"word_repetition_ratio":0.0,"special_character_ratio":0.23628692,"punctuation_ratio":0.102564104,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.995373,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-12-07T14:42:07Z\",\"WARC-Record-ID\":\"<urn:uuid:9c2abdd9-1981-452a-89ae-700bcc853106>\",\"Content-Length\":\"450967\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:9f87dc02-a3c2-44b6-b2a6-2bff5a744045>\",\"WARC-Concurrent-To\":\"<urn:uuid:51501ea1-51e1-4aeb-92f1-825a7bf5a175>\",\"WARC-IP-Address\":\"139.19.205.205\",\"WARC-Target-URI\":\"https://gitlab.mpi-sws.org/gpirlea/iris/-/commit/84490edcea9c4636cbb89181bda3de41a900ba91\",\"WARC-Payload-Digest\":\"sha1:7IHCICBZB7CXBHGLQ42NJSYNIABHR5IM\",\"WARC-Block-Digest\":\"sha1:UVIE5SMFL6BG7J3M22SRWVRH3GEAQBW5\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-49/CC-MAIN-2021-49_segments_1637964363400.19_warc_CC-MAIN-20211207140255-20211207170255-00398.warc.gz\"}"}