(* iris/algebra/mra.v *)
From iris.algebra Require Export cmra
From iris.algebra Require Import updates local_updates
From iris.prelude Require Import options
From this assumption it is not clear how to obtain witnesses [z1] and [z2]. *)

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 Argumentsmra_car {_ _} _.

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

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

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

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

Local Instancemra_valid : Valid (mra R) := λ x, True.

Local Instancemra_validN : ValidN (mra R) := λ n x, True.

Local ProgramInstance mra_op : Op (mra R) := λ x y,
    {| mra_car := mra_car x ++ mra_car y |}.

Local Instancemra_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 Instancemra_cmra_total : CmraTotal mraR.
  Proof. rewrite /CmraTotal; eauto. Qed.

Global Instancemra_core_id x : CoreId x.
  Proof. by constructor. Qed.

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

Local Instancemra_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_idempx : x ⋅ x ≡ x.
  Proof. intros a. set_solver. Qed.

Lemma mra_includedx y : x ≼ y ↔ y ≡ x ⋅ y.
  Proof using SI.
    split; [|by intros ?; exists 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 ?; exists (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.

Global ArgumentsmraO {_ _} _.

Global ArgumentsmraR {_ _} _.

Global ArgumentsmraUR {_ _} _.

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.

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

Global Instanceto_mra_proper {SI : sidx} `{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 Instanceto_mra_equiv_inj {SI : sidx} `{Equiv A} {R : relation A} :
  Reflexive R →
  AntiSymm (≡) R →
  Inj (≡) (≡@{mra R}) (to_mra) | 1.
Proof. intros. by apply (to_mra_rel_inj (≡)). Qed.