Library iris.base_logic.algebra

From iris.algebra Require Import cmra view auth agree csum list excl gmap.
From iris.algebra.lib Require Import excl_auth gmap_view dfrac_agree.
From iris.bi Require Import lib.cmra.
From iris.base_logic Require Import bi derived.
From iris.prelude Require Import options.

Internalized properties of our CMRA constructions.
Local Coercion uPred_holds : uPred >-> Funclass.

Section upred.
  Context {M : ucmra}.

  Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
  Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
  Notation "⊢ Q" := (bi_emp_valid (PROP:=uPredI M) Q).

  Lemma prod_validI {A B : cmra} (x : A × B) : x ⊣⊢ x.1 x.2.
  Proof. by uPred.unseal. Qed.
  Lemma option_validI {A : cmra} (mx : option A) :
     mx ⊣⊢ match mx with Some x x | NoneTrue : uPred M end.
  Proof. uPred.unseal. by destruct mx. Qed.
  Lemma discrete_fun_validI {A} {B : A ucmra} (g : discrete_fun B) :
     g ⊣⊢ i, g i.
  Proof. by uPred.unseal. Qed.

  Lemma id_freeI_r {A : cmra} (x y : A) :
    IdFree x x -∗ (x y) x -∗ False.
  Proof.
    intros ?. apply bi.wand_intro_l. rewrite bi.sep_and right_id.
    apply bi.wand_intro_r. rewrite bi.sep_and.
    uPred.unseal. splitn m Hm. case. by apply id_freeN_r.
  Qed.
  Lemma id_freeI_l {A : cmra} (x y : A) :
    IdFree x x -∗ (y x) x -∗ False.
  Proof.
    intros ?. apply bi.wand_intro_l. rewrite bi.sep_and right_id.
    apply bi.wand_intro_r. rewrite bi.sep_and.
    uPred.unseal. splitn m Hm. case. by apply id_freeN_l.
  Qed.

  Section gmap_ofe.
    Context `{Countable K} {A : ofe}.
    Implicit Types m : gmap K A.
    Implicit Types i : K.

    Lemma gmap_equivI m1 m2 : m1 m2 ⊣⊢ i, m1 !! i m2 !! i.
    Proof. by uPred.unseal. Qed.

    Lemma gmap_union_equiv_eqI m m1 m2 :
      m m1 m2 ⊣⊢ m1' m2', m = m1' m2' m1' m1 m2' m2.
    Proof. uPred.unseal; splitn x _. apply gmap_union_dist_eq. Qed.
  End gmap_ofe.

  Section gmap_cmra.
    Context `{Countable K} {A : cmra}.
    Implicit Types m : gmap K A.

    Lemma gmap_validI m : m ⊣⊢ i, (m !! i).
    Proof. by uPred.unseal. Qed.
    Lemma singleton_validI i x : ({[ i := x ]} : gmap K A) ⊣⊢ x.
    Proof.
      rewrite gmap_validI. apply: anti_symm.
      - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
      - apply bi.forall_introj. destruct (decide (i = j)) as [<-|Hne].
        + rewrite lookup_singleton option_validI. done.
        + rewrite lookup_singleton_ne // option_validI.
          apply bi.True_intro.
    Qed.
  End gmap_cmra.

  Section list_ofe.
    Context {A : ofe}.
    Implicit Types l : list A.

    Lemma list_equivI l1 l2 : l1 l2 ⊣⊢ i, l1 !! i l2 !! i.
    Proof. uPred.unseal; constructorn x ?. apply list_dist_lookup. Qed.
  End list_ofe.

  Section excl.
    Context {A : ofe}.
    Implicit Types x : excl A.

    Lemma excl_validI x :
       x ⊣⊢ if x is ExclBot then False else True.
    Proof. uPred.unseal. by destruct x. Qed.
  End excl.

  Section agree.
    Context {A : ofe}.
    Implicit Types a b : A.
    Implicit Types x y : agree A.

    Lemma agree_equivI a b : to_agree a to_agree b ⊣⊢ (a b).
    Proof.
      uPred.unseal. do 2 split.
      - intros Hx. exact: (inj to_agree).
      - intros Hx. exact: to_agree_ne.
    Qed.
    Lemma agree_validI x y : (x y) x y.
    Proof. uPred.unseal; splitr n _ ?; by apply: agree_op_invN. Qed.

    Lemma to_agree_validI a : to_agree a.
    Proof. uPred.unseal; done. Qed.
    Lemma to_agree_op_validI a b : (to_agree a to_agree b) ⊣⊢ a b.
    Proof.
      apply bi.entails_anti_sym.
      - rewrite agree_validI. by rewrite agree_equivI.
      - pose (Ψ := (λ x : A, (to_agree a to_agree x) : uPred M)%I).
        assert (NonExpansive Ψ) as ? by solve_proper.
        rewrite (internal_eq_rewrite a b Ψ).
        eapply bi.impl_elim; first reflexivity.
        etrans; first apply bi.True_intro.
        subst Ψ; simpl.
        rewrite agree_idemp. apply to_agree_validI.
    Qed.

    Lemma to_agree_uninjI x : x a, to_agree a x.
    Proof. uPred.unseal. splitn y _. exact: to_agree_uninjN. Qed.

Derived lemma: If two x y : agree O compose to some to_agree a, they are internally equal, and also equal to the to_agree a.
Empirically, x y to_agree a appears often when agreement comes up in CMRA validity terms, especially when views are involved. The desired simplification x y y to_agree a is also not straightforward to derive, so we have a special lemma to handle this common case.
    Lemma agree_op_equiv_to_agreeI x y a :
      x y to_agree a x y y to_agree a.
    Proof.
      assert (x y to_agree a x y) as Hxy_equiv.
      { rewrite -(agree_validI x y) internal_eq_sym.
        apply: (internal_eq_rewrite' _ _ (λ o, o)%I); first done.
        rewrite -to_agree_validI. apply bi.True_intro. }
      apply bi.and_intro; first done.
      rewrite -{1}(idemp bi_and (_ _)%I) {1}Hxy_equiv. apply bi.impl_elim_l'.
      apply: (internal_eq_rewrite' _ _
        (λ y', x y' to_agree a y' to_agree a)%I); [solve_proper|done|].
      rewrite agree_idemp. apply bi.impl_refl.
    Qed.

    Lemma to_agree_includedI a b :
      to_agree a to_agree b ⊣⊢ a b.
    Proof.
      apply (anti_symm _).
      - apply bi.exist_elimc. rewrite internal_eq_sym.
        rewrite agree_op_equiv_to_agreeI -agree_equivI.
        apply internal_eq_trans.
      - apply: (internal_eq_rewrite' _ _ (λ b, to_agree a to_agree b)%I);
          [solve_proper|done|].
        rewrite -internal_included_refl. apply bi.True_intro.
    Qed.

  End agree.

  Section csum_cmra.
    Context {A B : cmra}.
    Implicit Types a : A.
    Implicit Types b : B.

    Lemma csum_validI (x : csum A B) :
       x ⊣⊢ match x with
                        | Cinl a a
                        | Cinr b b
                        | CsumBotFalse
                        end.
    Proof. uPred.unseal. by destruct x. Qed.
  End csum_cmra.

  Section view.
    Context {A B} (rel : view_rel A B).
    Implicit Types a : A.
    Implicit Types ag : option (frac × agree A).
    Implicit Types b : B.
    Implicit Types x y : view rel.

    Lemma view_both_dfrac_validI_1 (relI : uPred M) dq a b :
      ( n (x : M), rel n a b relI n x)
       (V{dq} a V b : view rel) dq relI.
    Proof.
      intros Hrel. uPred.unseal. splitn x _ /=.
      rewrite /uPred_holds /= view_both_dfrac_validN. by move⇒ [? /Hrel].
    Qed.
    Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b :
      ( n (x : M), relI n x rel n a b)
      dq relI (V{dq} a V b : view rel).
    Proof.
      intros Hrel. uPred.unseal. splitn x _ /=.
      rewrite /uPred_holds /= view_both_dfrac_validN. by move⇒ [? /Hrel].
    Qed.
    Lemma view_both_dfrac_validI (relI : uPred M) dq a b :
      ( n (x : M), rel n a b relI n x)
       (V{dq} a V b : view rel) ⊣⊢ dq relI.
    Proof.
      intros. apply (anti_symm _);
        [apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
    Qed.

    Lemma view_both_validI_1 (relI : uPred M) a b :
      ( n (x : M), rel n a b relI n x)
       (V a V b : view rel) relI.
    Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.
    Lemma view_both_validI_2 (relI : uPred M) a b :
      ( n (x : M), relI n x rel n a b)
      relI (V a V b : view rel).
    Proof.
      intros. rewrite -view_both_dfrac_validI_2 //.
      apply bi.and_intro; [|done]. by apply bi.pure_intro.
    Qed.
    Lemma view_both_validI (relI : uPred M) a b :
      ( n (x : M), rel n a b relI n x)
       (V a V b : view rel) ⊣⊢ relI.
    Proof.
      intros. apply (anti_symm _);
        [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
    Qed.

    Lemma view_auth_dfrac_validI (relI : uPred M) dq a :
      ( n (x : M), relI n x rel n a ε)
       (V{dq} a : view rel) ⊣⊢ dq relI.
    Proof.
      intros. rewrite -(right_id ε op (V{dq} a)). by apply view_both_dfrac_validI.
    Qed.
    Lemma view_auth_validI (relI : uPred M) a :
      ( n (x : M), relI n x rel n a ε)
       (V a : view rel) ⊣⊢ relI.
    Proof. intros. rewrite -(right_id ε op (V a)). by apply view_both_validI. Qed.

    Lemma view_frag_validI (relI : uPred M) b :
      ( n (x : M), relI n x a, rel n a b)
       (V b : view rel) ⊣⊢ relI.
    Proof. uPred.unsealHrel. splitn x _. by rewrite Hrel. Qed.
  End view.

  Section auth.
    Context {A : ucmra}.
    Implicit Types a b : A.
    Implicit Types x y : auth A.

    Lemma auth_auth_dfrac_validI dq a : ({dq} a) ⊣⊢ dq a.
    Proof.
      apply view_auth_dfrac_validIn. uPred.unseal; split; [|by intros [??]].
      split; [|done]. apply ucmra_unit_leastN.
    Qed.
    Lemma auth_auth_validI a : ( a) ⊣⊢ a.
    Proof.
      by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
    Qed.
    Lemma auth_auth_dfrac_op_validI dq1 dq2 a1 a2 :
       ({dq1} a1 {dq2} a2) ⊣⊢ (dq1 dq2) (a1 a2) a1.
    Proof. uPred.unseal; splitn x _. apply auth_auth_dfrac_op_validN. Qed.

    Lemma auth_frag_validI a : ( a) ⊣⊢ a.
    Proof.
      apply view_frag_validIn x.
      rewrite auth_view_rel_exists. by uPred.unseal.
    Qed.

    Lemma auth_both_dfrac_validI dq a b :
       ({dq} a b) ⊣⊢ dq ( c, a b c) a.
    Proof. apply view_both_dfrac_validIn. by uPred.unseal. Qed.
    Lemma auth_both_validI a b :
       ( a b) ⊣⊢ ( c, a b c) a.
    Proof.
      by rewrite auth_both_dfrac_validI bi.pure_True // left_id.
    Qed.

  End auth.

  Section excl_auth.
    Context {A : ofe}.
    Implicit Types a b : A.

    Lemma excl_auth_agreeI a b : (E a E b) (a b).
    Proof.
      rewrite auth_both_validI bi.and_elim_l.
      apply bi.exist_elim⇒ -[[c|]|];
        by rewrite option_equivI /= excl_equivI //= bi.False_elim.
    Qed.
  End excl_auth.

  Section dfrac_agree.
    Context {A : ofe}.
    Implicit Types a b : A.

    Lemma dfrac_agree_validI dq a : (to_dfrac_agree dq a) ⊣⊢ dq.
    Proof.
      rewrite prod_validI /= uPred.discrete_valid. apply bi.entails_anti_sym.
      - by rewrite bi.and_elim_l.
      - apply bi.and_intro; first done. etrans; last apply to_agree_validI.
        apply bi.True_intro.
    Qed.

    Lemma dfrac_agree_validI_2 dq1 dq2 a b :
       (to_dfrac_agree dq1 a to_dfrac_agree dq2 b) ⊣⊢ (dq1 dq2) (a b).
    Proof.
      rewrite prod_validI /= uPred.discrete_valid to_agree_op_validI //.
    Qed.

    Lemma frac_agree_validI q a : (to_frac_agree q a) ⊣⊢ (q 1)%Qp.
    Proof.
      rewrite dfrac_agree_validI dfrac_valid_own //.
    Qed.

    Lemma frac_agree_validI_2 q1 q2 a b :
       (to_frac_agree q1 a to_frac_agree q2 b) ⊣⊢ (q1 + q2 1)%Qp (a b).
    Proof.
      rewrite dfrac_agree_validI_2 dfrac_valid_own //.
    Qed.
  End dfrac_agree.

  Section gmap_view.
    Context {K : Type} `{Countable K} {V : cmra}.
    Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).

    Lemma gmap_view_both_dfrac_validI dp m k dq v :
       (gmap_view_auth dp m gmap_view_frag k dq v) ⊣⊢
       v' dq', dp m !! k = Some v' (dq', v')
                Some (dq, v) Some (dq', v').
    Proof.
      unfold internal_included.
      uPred.unseal. splitn x _. apply: gmap_view_both_dfrac_validN.
    Qed.
    Lemma gmap_view_both_validI m dp k v :
       (gmap_view_auth dp m gmap_view_frag k (DfracOwn 1) v) ⊣⊢
       dp v m !! k Some v.
    Proof. uPred.unseal. splitn x _. apply: gmap_view_both_validN. Qed.
    Lemma gmap_view_both_validI_total `{!CmraTotal V} dp m k dq v :
       (gmap_view_auth dp m gmap_view_frag k dq v)
       v', dp dq m !! k = Some v' v' v v'.
    Proof.
      unfold internal_included.
      uPred.unseal. splitn x _. apply: gmap_view_both_dfrac_validN_total.
    Qed.

    Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
       (gmap_view_frag k dq1 v1 gmap_view_frag k dq2 v2) ⊣⊢
       (dq1 dq2) (v1 v2).
    Proof. uPred.unseal. splitn x _. apply: gmap_view_frag_op_validN. Qed.

  End gmap_view.
End upred.