Add persistency lemmas/instances for bi_tc, bi_rtc

iris/bi/lib/relations.v

@@ -149,6 +149,14 @@ Section general.
     bi_rtc R x z -∗ <affine> (x ≡ z) ∨ ∃ y, R x y ∗ bi_rtc R y z.
   Proof. rewrite bi_rtc_unfold. iIntros "[H | H]"; eauto. Qed.
 
+  Global Instance bi_rtc_persistent_affine :
+    (∀ x y, Affine (R x y)) →
+    (∀ x y, Persistent (R x y)) →
+    ∀ x y, Persistent (bi_rtc R x y).
+  Proof.
+    intros ????. apply least_fixpoint_persistent_affine; apply _.
+  Qed.
+
   (** ** Results about the transitive closure [bi_tc] *)
   Lemma bi_tc_unfold (x1 x2 : A) :
     bi_tc R x1 x2 ≡ bi_tc_pre R x2 (λ x1, bi_tc R x1 x2) x1.
@@ -237,6 +245,22 @@ Section general.
     iApply (bi_rtc_l with "H H'").
   Qed.
 
+  Lemma bi_tc_persistent_absorbing :
+    (∀ x y, Absorbing (R x y)) →
+    (∀ x y, Persistent (R x y)) →
+    ∀ x y, Persistent (bi_tc R x y).
+  Proof.
+    intros ????. apply least_fixpoint_persistent_absorbing; apply _.
+  Qed.
+
+  Lemma bi_tc_persistent_affine :
+    (∀ x y, Affine (R x y)) →
+    (∀ x y, Persistent (R x y)) →
+    ∀ x y, Persistent (bi_tc R x y).
+  Proof.
+    intros ????. apply least_fixpoint_persistent_affine; apply _.
+  Qed.
+
   (** ** Equivalences between closure operators *)
   Lemma bi_rtc_bi_tc x y : bi_rtc R x y ⊣⊢ <affine> (x ≡ y) ∨ bi_tc R x y.
   Proof.