Add transitive closure for bi

iris/bi/lib/relations.v

@@ -23,6 +23,16 @@ Section definitions.
   Global Instance: Params (@bi_rtc) 4 := {}.
   Typeclasses Opaque bi_rtc.
 
+  Definition bi_tc_pre (R : A → A → PROP)
+      (x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
+    R x1 x2 ∨ ∃ x', R x1 x' ∗ rec x'.
+
+  Definition bi_tc (R : A → A → PROP) (x1 x2 : A) : PROP :=
+    bi_least_fixpoint (bi_tc_pre R x2) x1.
+
+  Global Instance: Params (@bi_tc) 4 := {}.
+  Typeclasses Opaque bi_tc.
+
 End definitions.
 
 Global Instance bi_rtc_pre_mono {PROP : bi} `{!BiInternalEq PROP}
@@ -48,6 +58,31 @@ Global Instance bi_rtc_proper {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (R : A
   : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
 Proof. apply ne_proper_2. apply _. Qed.
 
+Global Instance bi_tc_pre_mono `{!BiInternalEq PROP}
+    {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
+  BiMonoPred (bi_tc_pre R x).
+Proof.
+  constructor; [|solve_proper].
+  iIntros (rec1 rec2 ??) "#H". iIntros (x1) "Hrec".
+  iDestruct "Hrec" as "[Hrec | Hrec]".
+  { by iLeft. }
+  iDestruct "Hrec" as (x') "[HR Hrec]".
+  iRight. iExists x'. iFrame "HR". by iApply "H".
+Qed.
+
+Global Instance bi_tc_ne `{!BiInternalEq PROP} {A : ofe}
+    (R : A → A → PROP) `{NonExpansive2 R} :
+  NonExpansive2 (bi_tc R).
+Proof.
+  intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_tc Hx. f_equiv=> rec z.
+  solve_proper.
+Qed.
+
+Global Instance bi_tc_proper `{!BiInternalEq PROP} {A : ofe}
+    (R : A → A → PROP) `{NonExpansive2 R}
+  : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_tc R).
+Proof. apply ne_proper_2. apply _. Qed.
+
 (** * General theorems *)
 Section general.
   Context {PROP : bi} `{!BiInternalEq PROP}.
@@ -102,4 +137,53 @@ Section general.
     by iApply "IH".
   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.
+  Proof. by rewrite /bi_tc; rewrite -least_fixpoint_unfold. Qed.
+
+  Lemma bi_tc_strong_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, (R x1 x2 ∨ (∃ x', R x1 x' ∗ (Φ x' ∧ bi_tc R x' x2))) -∗ Φ x1) -∗
+    ∀ x1, bi_tc R x1 x2 -∗ Φ x1.
+ Proof.
+    iIntros (?) "#IH". rewrite /bi_tc.
+    iApply (least_fixpoint_ind (bi_tc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_tc_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, (R x1 x2 ∨ (∃ x', R x1 x' ∗ Φ x')) -∗ Φ x1) -∗
+    ∀ x1, bi_tc R x1 x2 -∗ Φ x1.
+  Proof.
+    iIntros (?) "#IH". rewrite /bi_tc.
+    iApply (least_fixpoint_iter (bi_tc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_tc_l x1 x2 x3 : R x1 x2 -∗ bi_tc R x2 x3 -∗ bi_tc R x1 x3.
+  Proof.
+    iIntros "H1 H2".
+    iEval (rewrite bi_tc_unfold /bi_tc_pre).
+    iRight. iExists x2. iFrame.
+  Qed.
+
+  Lemma bi_tc_once x1 x2 : R x1 x2 -∗ bi_tc R x1 x2.
+  Proof.
+    iIntros "H".
+    iEval (rewrite bi_tc_unfold /bi_tc_pre).
+    by iLeft.
+  Qed.
+
+  Lemma bi_tc_trans x1 x2 x3 : bi_tc R x1 x2 -∗ bi_tc R x2 x3 -∗ bi_tc R x1 x3.
+  Proof.
+    iRevert (x1).
+    iApply bi_tc_ind_l.
+    { solve_proper. }
+    iIntros "!>" (x1) "H H2".
+    iDestruct "H" as "[H | H]".
+    { iApply (bi_tc_l with "H H2"). }
+    iDestruct "H" as (x') "[H IH]".
+    iApply (bi_tc_l with "H").
+    by iApply "IH".
+  Qed.
 End general.