Adding a constructor for reflexive transitive closures into bi's

CHANGELOG.md

@@ -63,6 +63,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   To make this work we also had to rename `inv_acc` -> `inv_alter`.
   (Most developments should be unaffected as the typical way to invoke these
   lemmas is through `iInv`, and that does not change.)
+* Added a construction `bi_rtc` to create reflexive transitive closures of
+  PROP-level binary relations.
 
 ## Iris 3.2.0 (released 2019-08-29)
 

_CoqProject

@@ -63,6 +63,7 @@ theories/bi/lib/fractional.v
 theories/bi/lib/laterable.v
 theories/bi/lib/atomic.v
 theories/bi/lib/core.v
+theories/bi/lib/relations.v
 theories/base_logic/upred.v
 theories/base_logic/bi.v
 theories/base_logic/derived.v

theories/bi/lib/relations.v

+(** This file provides a construction to lift a PROP-level binary relation to
+its reflexive transitive closure. *)
+From iris.bi.lib Require Export fixpoint.
+From iris.proofmode Require Import tactics.
+
+Definition bi_rtc_pre
+    {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+    (x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
+  (<affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x')%I.
+
+Instance bi_rtc_pre_mono
+    {PROP : sbi} {A : ofeT} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
+  BiMonoPred (bi_rtc_pre R x).
+Proof.
+  constructor; [|solve_proper].
+  iIntros (rec1 rec2) "#H". iIntros (x1) "[Hrec | Hrec]".
+  { by iLeft. }
+  iRight.
+  iDestruct "Hrec" as (x') "[HP Hrec]".
+  iDestruct ("H" with "Hrec") as "Hrec". eauto with iFrame.
+Qed.
+
+Definition bi_rtc {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+    (x1 x2 : A) : PROP :=
+  bi_least_fixpoint (bi_rtc_pre R x2) x1.
+
+Instance: Params (@bi_rtc) 3 := {}.
+Typeclasses Opaque bi_rtc.
+
+Instance bi_rtc_ne
+    {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+  : NonExpansive2 (bi_rtc R).
+Proof.
+  intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
+  solve_proper.
+Qed.
+
+Instance bi_rtc_proper
+    {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+  : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
+Proof. apply ne_proper_2. apply _. Qed.
+
+Section bi_rtc.
+  Context {PROP : sbi}.
+  Context {A : ofeT}.
+  Context (R : A → A → PROP) `{NonExpansive2 R}.
+
+  Lemma bi_rtc_unfold (x1 x2 : A) :
+    bi_rtc R x1 x2 ≡ bi_rtc_pre R x2 (λ x1, bi_rtc R x1 x2) x1.
+  Proof. by rewrite /bi_rtc; rewrite -least_fixpoint_unfold. Qed.
+
+  Lemma bi_rtc_strong_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, <affine> (x1 ≡ x2) ∨ (∃ x', R x1 x' ∗ (Φ x' ∧ bi_rtc R x' x2)) -∗ Φ x1) -∗
+    ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
+ Proof.
+    iIntros (?) "#IH". rewrite /bi_rtc.
+    by iApply (least_fixpoint_strong_ind (bi_rtc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_rtc_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, <affine> (x1 ≡ x2) ∨ (∃ x', R x1 x' ∗ Φ x') -∗ Φ x1) -∗
+    ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
+  Proof.
+    iIntros (?) "#IH". rewrite /bi_rtc.
+    by iApply (least_fixpoint_ind (bi_rtc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_rtc_refl x : bi_rtc R x x.
+  Proof. rewrite bi_rtc_unfold. by iLeft. Qed.
+
+  Lemma bi_rtc_l x1 x2 x3 : R x1 x2 -∗ bi_rtc R x2 x3 -∗ bi_rtc R x1 x3.
+  Proof.
+    iIntros "H1 H2".
+    iEval (rewrite bi_rtc_unfold /bi_rtc_pre). iRight.
+    iExists x2. iFrame.
+  Qed.
+
+  Lemma bi_rtc_once x1 x2 : R x1 x2 -∗ bi_rtc R x1 x2.
+  Proof. iIntros "H". iApply (bi_rtc_l with "H"). iApply bi_rtc_refl. Qed.
+
+  Lemma bi_rtc_trans x1 x2 x3 : bi_rtc R x1 x2 -∗ bi_rtc R x2 x3 -∗ bi_rtc R x1 x3.
+  Proof.
+    iRevert (x1).
+    iApply bi_rtc_ind_l.
+    { solve_proper. }
+    iIntros "!>" (x1) "[H | H] H2".
+    { by iRewrite "H". }
+    iDestruct "H" as (x') "[H IH]".
+    iApply (bi_rtc_l with "H").
+    by iApply "IH".
+  Qed.
+
+End bi_rtc.