diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v index 5a0ca25351f8c0f95496dfe34520c797feb3a45f..9b95dd1b1ca4395cbce2aedf111fec500873e635 100644 --- a/theories/bi/big_op.v +++ b/theories/bi/big_op.v @@ -167,6 +167,10 @@ Section sep_list. Global Instance big_sepL_persistent_id Ps : TCForall Persistent Ps → Persistent ([∗] Ps). Proof. induction 1; simpl; apply _. Qed. + + Global Instance big_sepL_affine Φ l : + (∀ k x, Affine (Φ k x)) → Affine ([∗ list] k↦x ∈ l, Φ k x). + Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed. End sep_list. Section sep_list2. @@ -429,6 +433,12 @@ Section gmap. Global Instance big_sepM_persistent Φ m : (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x). Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed. + + Global Instance big_sepM_affine Φ m : + (∀ k x, Affine (Φ k x)) → Affine ([∗ map] k↦x ∈ m, Φ k x). + Proof. + intros. apply big_sepL_affine=> _ [??]; apply _. + Qed. End gmap. (** ** Big ops over finite sets *) @@ -580,6 +590,10 @@ Section gset. Global Instance big_sepS_persistent Φ X : (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x). Proof. rewrite /big_opS. apply _. Qed. + + Global Instance big_sepS_affine Φ X : + (∀ x, Affine (Φ x)) → Affine ([∗ set] x ∈ X, Φ x). + Proof. rewrite /big_opS. apply _. Qed. End gset. Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) : @@ -654,6 +668,10 @@ Section gmultiset. Global Instance big_sepMS_persistent Φ X : (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x). Proof. rewrite /big_opMS. apply _. Qed. + + Global Instance big_sepMS_affine Φ X : + (∀ x, Affine (Φ x)) → Affine ([∗ mset] x ∈ X, Φ x). + Proof. rewrite /big_opMS. apply _. Qed. End gmultiset. End bi_big_op.