relations.v 3.1 KB
Newer Older
1 2 3 4
(** 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.
5 6 7 8
From iris Require Import options.

(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
Set Default Proof Using "Type*".
9

10 11
Definition bi_rtc_pre `{!BiInternalEq PROP}
    {A : ofeT} (R : A  A  PROP)
12 13 14
    (x2 : A) (rec : A  PROP) (x1 : A) : PROP :=
  (<affine> (x1  x2)   x', R x1 x'  rec x')%I.

15 16
Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
    {A : ofeT} (R : A  A  PROP) `{NonExpansive2 R} (x : A) :
17 18 19 20 21 22 23 24 25 26
  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.

27 28
Definition bi_rtc `{!BiInternalEq PROP}
    {A : ofeT} (R : A  A  PROP) (x1 x2 : A) : PROP :=
29 30 31 32 33
  bi_least_fixpoint (bi_rtc_pre R x2) x1.

Instance: Params (@bi_rtc) 3 := {}.
Typeclasses Opaque bi_rtc.

34
Instance bi_rtc_ne `{!BiInternalEq PROP} {A : ofeT} (R : A  A  PROP) :
35
  NonExpansive2 (bi_rtc R).
36 37 38 39 40
Proof.
  intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
  solve_proper.
Qed.

41
Instance bi_rtc_proper `{!BiInternalEq PROP} {A : ofeT} (R : A  A  PROP)
42 43 44 45
  : Proper (() ==> () ==> ()) (bi_rtc R).
Proof. apply ne_proper_2. apply _. Qed.

Section bi_rtc.
46
  Context `{!BiInternalEq PROP}.
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
  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.

Gregory Malecha's avatar
Gregory Malecha committed
72
  Lemma bi_rtc_refl x :  bi_rtc R x x.
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
  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.