Commit 1346ccb3 authored by Hai Dang's avatar Hai Dang
Browse files

Add internal algebra properties for siProp, and derive some of those for bi with siProp embedding

parent a8224a3c
......@@ -56,6 +56,7 @@ iris/algebra/lib/mono_nat.v
iris/algebra/lib/gset_bij.v
iris/si_logic/siprop.v
iris/si_logic/bi.v
iris/si_logic/algebra.v
iris/bi/notation.v
iris/bi/interface.v
iris/bi/derived_connectives.v
......
From iris.algebra Require Import cmra view auth agree csum list excl gmap.
From iris.algebra.lib Require Import excl_auth gmap_view.
From iris.base_logic Require Import bi derived.
From iris.si_logic Require Import algebra.
From iris.base_logic Require Import cmra_valid.
From iris.prelude Require Import options.
(** Internalized properties of our CMRA constructions. *)
Local Coercion uPred_holds : uPred >-> Funclass.
Local Coercion siProp_holds : siProp >-> Funclass.
Section upred.
Context {M : ucmra}.
Section bi_cmra_valid.
Context {PROP : bi} `{!BiEmbed siPropI PROP}.
(* Force implicit argument M *)
Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
Notation "P ⊢ Q" := (bi_entails (PROP:=PROP) P Q).
Notation "P ⊣⊢ Q" := (equiv (A:=PROP) P%I Q%I).
Local Definition unseal_eqs :=
(@embed_emp, @embed_pure,
@embed_and, @embed_or, @embed_impl, @embed_forall, @embed_exist,
@embed_sep, @embed_wand).
Local Ltac unseal_embed :=
bi_cmra_valid.unseal;
rewrite -?unseal_eqs;
first [apply embed_proper | apply embed_mono | idtac ].
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.
Proof. unseal_embed. exact: siProp_algebra.prod_validI. Qed.
Lemma option_validI `{!BiEmbedEmp siPropI PROP} {A : cmra} (mx : option A) :
mx match mx with Some x => x | None => emp end.
Proof. destruct mx; unseal_embed; exact: siProp_algebra.option_validI. Qed.
Lemma discrete_fun_validI {A} {B : A ucmra} (g : discrete_fun B) :
g i, g i.
Proof. by uPred.unseal. Qed.
Proof. unseal_embed. exact: siProp_algebra.discrete_fun_validI. Qed.
Lemma frac_validI (q : Qp) : q q 1%Qp.
Proof. rewrite uPred.discrete_valid frac_valid //. Qed.
Proof. unseal_embed. exact: siProp_algebra.frac_validI. Qed.
Section gmap_ofe.
(* 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.
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.
Proof. unseal_embed. exact: siProp_algebra.gmap_validI. 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.
Proof. unseal_embed. exact: siProp_algebra.singleton_validI. Qed.
End gmap_cmra.
Section list_ofe.
(* 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.
End list_ofe. *)
Section excl.
(* Section excl.
Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : excl A.
......@@ -78,9 +81,9 @@ Section excl.
Lemma excl_validI x :
✓ x ⊣⊢ if x is ExclBot then False else True.
Proof. uPred.unseal. by destruct x. Qed.
End excl.
End excl. *)
Section agree.
(* Section agree.
Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : agree A.
......@@ -114,7 +117,7 @@ Section csum_ofe.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; try destruct 1; try constructor.
Qed.
End csum_ofe.
End csum_ofe. *)
Section csum_cmra.
Context {A B : cmra}.
......@@ -127,7 +130,7 @@ Section csum_cmra.
| Cinr b => b
| CsumBot => False
end.
Proof. uPred.unseal. by destruct x. Qed.
Proof. destruct x; unseal_embed; exact: siProp_algebra.csum_validI. Qed.
End csum_cmra.
Section view.
......@@ -137,62 +140,45 @@ Section view.
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.
Lemma view_both_dfrac_validI_1 (relI : siProp) dq a b :
( n, rel n a b relI n)
(V{dq} a V b : view rel) ⌜✓dq relI .
Proof. intros. unseal_embed. exact: siProp_algebra.view_both_dfrac_validI_1. Qed.
Lemma view_both_dfrac_validI_2 (relI : siProp) dq a b :
( n, relI n rel n a b)
⌜✓dq relI (V{dq} a V b : view rel).
Proof. intros. unseal_embed. exact: siProp_algebra.view_both_dfrac_validI_2. Qed.
Lemma view_both_dfrac_validI (relI : siProp) dq a b :
( n, rel n a b relI n)
(V{dq} a V b : view rel) ⌜✓dq relI .
Proof. intros. unseal_embed. exact: siProp_algebra.view_both_dfrac_validI. Qed.
Lemma view_both_validI_1 (relI : siProp) a b :
( n, rel n a b relI n)
(V a V b : view rel) relI .
Proof. intros. unseal_embed. exact: siProp_algebra.view_both_validI_1. Qed.
Lemma view_both_validI_2 (relI : siProp) a b :
( n, relI n rel n a b)
relI (V a V b : view rel).
Proof. intros. unseal_embed. exact: siProp_algebra.view_both_validI_2. Qed.
Lemma view_both_validI (relI : siProp) a b :
( n, rel n a b relI n)
(V a V b : view rel) relI .
Proof. intros. unseal_embed. exact: siProp_algebra.view_both_validI. Qed.
Lemma view_auth_dfrac_validI (relI : siProp) dq a :
( n, relI n rel n a ε)
(V{dq} a : view rel) ⌜✓dq relI .
Proof. intros. unseal_embed. exact: siProp_algebra.view_auth_dfrac_validI. Qed.
Lemma view_auth_validI (relI : siProp) a :
( n, relI n rel n a ε)
(V a : view rel) relI .
Proof. intros. unseal_embed. exact: siProp_algebra.view_auth_validI. Qed.
Lemma view_frag_validI (relI : siProp) b :
( n, relI n a, rel n a b)
(V b : view rel) relI .
Proof. intros. unseal_embed. exact: siProp_algebra.view_frag_validI. Qed.
End view.
Section auth.
......@@ -201,33 +187,25 @@ Section auth.
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.
Proof. unseal_embed. exact: siProp_algebra.auth_auth_dfrac_validI. Qed.
Lemma auth_auth_validI a : ( a) a.
Proof.
by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
Qed.
Proof. unseal_embed. exact: siProp_algebra.auth_auth_validI. Qed.
Lemma auth_frag_validI a : ( a) a.
Proof.
apply view_frag_validI=> n x.
rewrite auth_view_rel_exists. by uPred.unseal.
Qed.
Proof. unseal_embed. exact: siProp_algebra.auth_frag_validI. Qed.
Lemma auth_both_dfrac_validI dq a b :
(* 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.
Qed. *)
End auth.
Section excl_auth.
(* Section excl_auth.
Context {A : ofe}.
Implicit Types a b : A.
......@@ -237,9 +215,9 @@ Section excl_auth.
apply bi.exist_elim=> -[[c|]|];
by rewrite option_equivI /= excl_equivI //= bi.False_elim.
Qed.
End excl_auth.
End excl_auth. *)
Section gmap_view.
(* Section gmap_view.
Context {K : Type} `{Countable K} {V : ofe}.
Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
......@@ -260,6 +238,6 @@ Section gmap_view.
rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
Qed.
End gmap_view.
End gmap_view. *)
End upred.
End bi_cmra_valid.
From iris.algebra Require Import cmra.
From iris.si_logic Require Export bi siprop.
From iris.si_logic Require Export bi.
From iris.prelude Require Import options.
Definition bi_cmra_valid_def
......@@ -16,7 +16,7 @@ Notation "✓ x" := (bi_cmra_valid x) (at level 20) : bi_scope.
Module bi_cmra_valid.
Ltac unseal :=
rewrite !bi_cmra_valid_eq /=.
rewrite !bi_cmra_valid_eq /bi_cmra_valid_def /=.
End bi_cmra_valid.
Section valid_props.
......@@ -27,7 +27,7 @@ Import bi_cmra_valid.
Global Instance cmra_valid_ne :
NonExpansive (@bi_cmra_valid _ _ A).
Proof. unseal => ????. by apply embed_ne, siProp_primitive.cmra_valid_ne. Qed.
Proof. unseal => ????. by apply embed_ne, siProp.cmra_valid_ne. Qed.
Global Instance cmra_valid_proper :
Proper (() ==> ()) (@bi_cmra_valid _ _ A) := ne_proper _.
......@@ -35,20 +35,19 @@ Global Instance cmra_valid_proper :
Lemma cmra_valid_intro P a : a P ( a).
Proof.
unseal => Ha.
rewrite /bi_cmra_valid_def -(siProp_primitive.cmra_valid_intro True%I) //.
rewrite embed_pure. apply bi.True_intro.
rewrite -(siProp.cmra_valid_intro True%I) // embed_pure. apply bi.True_intro.
Qed.
Lemma cmra_valid_elim (a : A) : ¬ {0} a a False.
Proof.
unseal=> ?. by rewrite /bi_cmra_valid_def siProp_primitive.cmra_valid_elim // embed_pure.
unseal=> ?. by rewrite siProp.cmra_valid_elim // embed_pure.
Qed.
Lemma cmra_valid_weaken (a b : A) : (a b) a.
Proof. unseal. apply embed_mono, siProp_primitive.cmra_valid_weaken. Qed.
Proof. unseal. apply embed_mono, siProp.cmra_valid_weaken. Qed.
Lemma discrete_valid `{!CmraDiscrete A} (a : A) : a ⌜✓ a.
Proof.
unseal. by rewrite /bi_cmra_valid_def siProp_primitive.discrete_valid embed_pure.
unseal. by rewrite siProp.discrete_valid embed_pure.
Qed.
Lemma valid_entails {B : cmra} (a : A) (b : B) :
......
From iris.algebra Require Import cmra view auth agree csum list excl gmap.
From iris.algebra.lib Require Import excl_auth gmap_view.
From iris.si_logic Require Import bi.
From iris.prelude Require Import options.
(** Internalized properties of our CMRA constructions. *)
Local Coercion siProp_holds : siProp >-> Funclass.
Module siProp_algebra.
Section siprop.
Notation "P ⊢ Q" := (bi_entails (PROP:=siPropI) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=siPropI) P%I Q%I).
Notation "✓ x" := (siProp_cmra_valid x) : bi_scope.
Lemma prod_validI {A B : cmra} (x : A * B) : x x.1 x.2.
Proof. by siProp.unseal. Qed.
Lemma option_validI {A : cmra} (mx : option A) :
mx match mx with Some x => x | None => True end.
Proof. siProp.unseal. by destruct mx. Qed.
Lemma discrete_fun_validI {A} {B : A ucmra} (g : discrete_fun B) :
g i, g i.
Proof. by siProp.unseal. Qed.
Lemma frac_validI (q : Qp) : q q 1%Qp.
Proof. rewrite siProp.discrete_valid frac_valid //. 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 siProp.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 siProp.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. siProp.unseal; constructor=> n. apply list_dist_lookup. Qed.
End list_ofe.
Section excl.
Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : excl A.
Lemma excl_equivI x y :
x y match x, y with
| Excl a, Excl b => a b
| ExclBot, ExclBot => True
| _, _ => False
end.
Proof.
siProp.unseal. do 2 split.
- by destruct 1.
- by destruct x, y; try constructor.
Qed.
Lemma excl_validI x :
x if x is ExclBot then False else True.
Proof. siProp.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.
siProp.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. siProp.unseal; split=> r n ; by apply: agree_op_invN. Qed.
Lemma to_agree_uninjI x : x a, to_agree a x.
Proof. siProp.unseal. split=> n. exact: to_agree_uninjN. Qed.
End agree.
Section csum_ofe.
Context {A B : ofe}.
Implicit Types a : A.
Implicit Types b : B.
Lemma csum_equivI (x y : csum A B) :
x y match x, y with
| Cinl a, Cinl a' => a a'
| Cinr b, Cinr b' => b b'
| CsumBot, CsumBot => True
| _, _ => False
end.
Proof.
siProp.unseal; do 2 split; first by destruct 1.
by destruct x, y; try destruct 1; try constructor.
Qed.
End csum_ofe.
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. siProp.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.
Local Arguments siProp_holds !_ _ /.
Lemma view_both_dfrac_validI_1 (relI : siProp) dq a b :
( n, rel n a b relI n)
(V{dq} a V b : view rel) ⌜✓dq relI.
Proof.
intros Hrel. siProp.unseal. split=> n /=.
rewrite /= view_both_dfrac_validN. by move=> [? /Hrel].
Qed.
Lemma view_both_dfrac_validI_2 (relI : siProp) dq a b :
( n, relI n rel n a b)
⌜✓dq relI (V{dq} a V b : view rel).
Proof.
intros Hrel. siProp.unseal. split=> n /=.
rewrite /= view_both_dfrac_validN. by move=> [? /Hrel].
Qed.
Lemma view_both_dfrac_validI (relI : siProp) dq a b :
( n, rel n a b relI n)
(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 : siProp) a b :
( n, rel n a b relI n)
(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 : siProp) a b :
( n, relI n 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 : siProp) a b :
( n, rel n a b relI n)
(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 : siProp) dq a :
( n, relI n 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 : siProp) a :
( n, relI n 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 : siProp) b :
( n, relI n a, rel n a b)
(V b : view rel) relI.
Proof. siProp.unseal=> Hrel. split=> n. 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. siProp.unseal; split; [|by intros [??]].
split; [|done]. apply ucmra_unit_leastN.
Qed.