Library iris.algebra.mra

From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Import options.

Given a preorder R on a type A we construct the "monotone" resource algebra mra R and an injection to_mra : A → mra R such that:

R x y iff to_mra x ≼ to_mra y

Here, ≼ is the extension order of the mra R resource algebra. This is exactly what the lemma to_mra_included shows.

This resource algebra is useful for reasoning about monotonicity. See the following paper for more details (to_mra is called "principal"):

Reasoning About Monotonicity in Separation Logic Amin Timany and Lars Birkedal in Certified Programs and Proofs (CPP) 2021

Note that unlike most Iris algebra constructions mra A works on A : Type, not on A : ofe. See the comment at mraO below for more information. If A has an Equiv A (i.e., is a setoid), there are some results at the bottom of this file.

Record mra {A} (R : relation A) := { mra_car : list A }.
Definition to_mra {A} {R : relation A} (a : A) : mra R :=
  {| mra_car := [a ] |}.
Global Arguments mra_car {_ _} _.

Section mra.
  Context {A} {R : relation A}.
  Implicit Types a b : A.
  Implicit Types x y : mra R.

Pronounced a is below x.

  Local Definition mra_below (a : A) (x : mra R) := ∃ b , b ∈ mra_car x ∧ R a b.

  Local Lemma mra_below_to_mra a b : mra_below a (to_mra b) ↔ R a b.
  Proof. set_solver. Qed.

  Local Instance mra_equiv : Equiv (mra R) := λ x y ,
    ∀ a , mra_below a x ↔ mra_below a y.

  Local Instance mra_equiv_equiv : Equivalence mra_equiv.
  Proof. unfold mra_equiv; split; intros ?; naive_solver. Qed.

Generalizing mra A to A : ofe and R : A -n> A -n> siProp is not obvious. It is not clear what axioms to impose on R for the "extension axiom" to hold:

cmra_extend : x ≡{n}≡ y1 ⋅ y2 → ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ y1 ≡{n}≡ z1 ∧ y2 ≡{n}≡ z2

To prove this, assume (⋅ is defined as ++, see mra_op):

x ≡{n}≡ y1 ++ y2

When defining dist as the step-indexed version of mra_equiv, this means:

∀ n' a, n' ≤ n → mra_below a x n' ↔ mra_below a y1 n' ∨ mra_below a y2 n'

From this assumption it is not clear how to obtain witnesses z1 and z2.

  Canonical Structure mraO := discreteO (mra R).

  Local Instance mra_valid : Valid (mra R) := λ x , True.
  Local Instance mra_validN : ValidN (mra R) := λ n x , True.
  Local Program Instance mra_op : Op (mra R) := λ x y ,
    {| mra_car := mra_car x ++ mra_car y |}.
  Local Instance mra_pcore : PCore (mra R) := Some.

  Lemma mra_cmra_mixin : CmraMixin (mra R).
  Proof.
    apply discrete_cmra_mixin; first apply _.
    apply ra_total_mixin; try done.
    - intros x y z Hyz a. specialize (Hyz a). set_solver.
    - apply _.
    - intros x y z a. set_solver.
    - intros x y a. set_solver.
    - intros x a. set_solver.
  Qed.

  Canonical Structure mraR : cmra := Cmra (mra R) mra_cmra_mixin.

  Global Instance mra_cmra_total : CmraTotal mraR.
  Proof. rewrite /CmraTotal; eauto. Qed.
  Global Instance mra_core_id x : CoreId x.
  Proof. by constructor. Qed.

  Global Instance mra_cmra_discrete : CmraDiscrete mraR.
  Proof. split; last done. intros ? ?; done. Qed.

  Local Instance mra_unit : Unit (mra R) := {| mra_car := [] |}.
  Lemma auth_ucmra_mixin : UcmraMixin (mra R).
  Proof. split; done. Qed.

  Canonical Structure mraUR := Ucmra (mra R) auth_ucmra_mixin.

  Lemma mra_idemp x : x ⋅ x ≡ x.
  Proof. intros a. set_solver. Qed.

  Lemma mra_included x y : x ≼ y ↔ y ≡ x ⋅ y.
  Proof.
    split; [|by intros ?; ∃ y].
    intros [z ->]; rewrite assoc mra_idemp; done.
  Qed.

  Lemma to_mra_R_op `{!Transitive R} a b :
    R a b →
    to_mra a ⋅ to_mra b ≡ to_mra b.
  Proof. intros Hab c. set_solver. Qed.

  Lemma to_mra_included `{!PreOrder R} a b :
    to_mra a ≼ to_mra b ↔ R a b.
  Proof.
    split.
    - move⇒ [z Hz]. specialize (Hz a). set_solver.
    - intros ?; ∃ (to_mra b). by rewrite to_mra_R_op.
  Qed.

  Lemma mra_local_update_grow `{!Transitive R} a x b:
    R a b →
    (to_mra a , x ) ¬l ~> (to_mra b , to_mra b ).
  Proof.
    intros Hana. apply local_update_unital_discrete⇒ z _ Habz.
    split; first done. intros c. specialize (Habz c). set_solver.
  Qed.

  Lemma mra_local_update_get_frag `{!PreOrder R} a b:
    R b a →
    (to_mra a , ε ) ¬l ~> (to_mra a , to_mra b ).
  Proof.
    intros Hana. apply local_update_unital_discrete⇒ z _.
    rewrite left_id. intros <-. split; first done.
    apply mra_included; by apply to_mra_included.
  Qed.
End mra.

Global Arguments mraO {_} _.
Global Arguments mraR {_} _.
Global Arguments mraUR {_} _.

If R is a partial order, relative to a reflexive relation S on the carrier A, then to_mra is proper and injective. The theory for arbitrary relations S is overly general, so we do not declare the results as instances. Below we provide instances for S being = and ≡.

Section mra_over_rel.
  Context {A} {R : relation A} (S : relation A).
  Implicit Types a b : A.
  Implicit Types x y : mra R.

  Lemma to_mra_rel_proper :
    Reflexive S →
    Proper (S ==> S ==> iff) R →
    Proper (S ==> (≡@{mra R })) (to_mra).
  Proof. intros ? HR a1 a2 Ha b. rewrite !mra_below_to_mra. by apply HR. Qed.

  Lemma to_mra_rel_inj :
    Reflexive R →
    AntiSymm S R →
    Inj S (≡@{mra R }) (to_mra).
  Proof.
    intros ?? a b Hab. move: (Hab a) (Hab b). rewrite !mra_below_to_mra.
    intros. apply (anti_symm R); naive_solver.
  Qed.
End mra_over_rel.

Global Instance to_mra_inj {A} {R : relation A} :
  Reflexive R →
  AntiSymm (=) R →
  Inj (=) (≡@{mra R }) (to_mra) | 0. Proof. intros. by apply (to_mra_rel_inj (=)). Qed.

Global Instance to_mra_proper `{Equiv A} {R : relation A} :
  Reflexive (≡@{A }) →
  Proper ((≡) ==> (≡) ==> iff) R →
  Proper ((≡) ==> (≡@{mra R })) (to_mra).
Proof. intros. by apply (to_mra_rel_proper (≡)). Qed.

Global Instance to_mra_equiv_inj `{Equiv A} {R : relation A} :
  Reflexive R →
  AntiSymm (≡) R →
  Inj (≡) (≡@{mra R }) (to_mra) | 1.
Proof. intros. by apply (to_mra_rel_inj (≡)). Qed.