diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v index 89210107e2947013d86cc2d8b0e3e38526a64e3d..d92c6fa88b13497c3095761e50fe624388536e56 100644 --- a/algebra/upred_tactics.v +++ b/algebra/upred_tactics.v @@ -1,3 +1,4 @@ +From iris.prelude Require Import gmap. From iris.algebra Require Export upred. From iris.algebra Require Export upred_big_op. Import uPred. @@ -227,6 +228,21 @@ Global Instance strip_later_r_sep P1 P2 Q1 Q2 : StripLaterR P1 Q1 → StripLaterR P2 Q2 → StripLaterR (P1 ★ P2) (Q1 ★ Q2). Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed. +Global Instance strip_later_r_big_sepM `{Countable K} {A} + (Φ Ψ : K → A → uPred M) (m : gmap K A) : + (∀ x k, StripLaterR (Φ k x) (Ψ k x)) → + StripLaterR ([★ map] k ↦ x ∈ m, Φ k x) ([★ map] k ↦ x ∈ m, Ψ k x). +Proof. + rewrite /StripLaterR=> ?. rewrite big_sepM_later; by apply big_sepM_mono. +Qed. +Global Instance strip_later_r_big_sepS `{Countable A} + (Φ Ψ : A → uPred M) (X : gset A) : + (∀ x, StripLaterR (Φ x) (Ψ x)) → + StripLaterR ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ x). +Proof. + rewrite /StripLaterR=> ?. rewrite big_sepS_later; by apply big_sepS_mono. +Qed. + Global Instance strip_later_l_later P : StripLaterL (▷ P) P. Proof. done. Qed. Global Instance strip_later_l_and P1 P2 Q1 Q2 :