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.base_logic Require Import bi derived.
From iris.prelude Require Import options.
From iris.algebra.lib Require Import excl_auth gmap_view dfrac_agree.
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_entails (PROP:=uPredI M) True 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 | None ⇒ True : 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.
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.
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_intro⇒j. 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; constructor⇒ n 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; split⇒ r 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. split⇒ n y _. exact: to_agree_uninjN. Qed.
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_entails (PROP:=uPredI M) True 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 | None ⇒ True : 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.
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.
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_intro⇒j. 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; constructor⇒ n 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; split⇒ r 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. split⇒ n 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.
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
| CsumBot ⇒ False
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. split⇒ n 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. split⇒ n 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.unseal⇒ Hrel. split⇒ n 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_validI⇒ n. 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; split ⇒ n x _. apply auth_auth_dfrac_op_validN. Qed.
Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
Proof.
apply view_frag_validI⇒ n 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_validI⇒ n. 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 : ofe}.
Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
Lemma gmap_view_both_validI m k dq v :
✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ⊢
✓ dq ∧ m !! k ≡ Some v.
Proof.
rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
intros n a. uPred.unseal. apply gmap_view.gmap_view_rel_lookup.
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.
rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI⇒ n x.
rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
Qed.
End gmap_view.
End upred.
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.
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
| CsumBot ⇒ False
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. split⇒ n 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. split⇒ n 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.unseal⇒ Hrel. split⇒ n 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_validI⇒ n. 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; split ⇒ n x _. apply auth_auth_dfrac_op_validN. Qed.
Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
Proof.
apply view_frag_validI⇒ n 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_validI⇒ n. 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 : ofe}.
Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
Lemma gmap_view_both_validI m k dq v :
✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ⊢
✓ dq ∧ m !! k ≡ Some v.
Proof.
rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
intros n a. uPred.unseal. apply gmap_view.gmap_view_rel_lookup.
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.
rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI⇒ n x.
rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
Qed.
End gmap_view.
End upred.