relations.v 2.91 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
(** 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.