Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/iris
  • jeehoon.kang/iris-coq
  • amintimany/iris-coq
  • dfrumin/iris-coq
  • Villetaneuse/iris
  • gares/iris
  • shiatsumat/iris
  • Blaisorblade/iris
  • jihgfee/iris-coq
  • mrhaandi/iris
  • tlsomers/iris
  • Quarkbeast/iris-coq
  • janno/iris
  • amaurremi/iris-coq
  • proux/iris
  • tchajed/iris
  • herbelin/iris-coq
  • msammler/iris-coq
  • maximedenes/iris-coq
  • bpeters/iris
  • haidang/iris
  • lepigre/iris
  • lczch/iris
  • simonspies/iris
  • gpirlea/iris
  • dkhalanskiyjb/iris
  • gmalecha/iris
  • germanD/iris
  • aa755/iris
  • jules/iris
  • abeln/iris
  • simonfv/iris
  • atrieu/iris
  • arthuraa/iris
  • simonh/iris
  • jung/iris
  • mattam82/iris
  • Armael/iris
  • adamAndMath/iris
  • gmevel/iris
  • snyke7/iris
  • johannes/iris
  • NiklasM/iris
  • simonspies/iris-parametric-index
  • svancollem/iris
  • proux1/iris
  • wmansky/iris
  • LukeXuan/iris
  • ivanbakel/iris
  • SkySkimmer/iris
  • tjhance/iris
  • yiyunliu/iris
  • Lee-Janggun/iris
  • thomas-lamiaux/iris
  • dongjae/iris
  • dnezam/iris
  • Tragicus/iris
  • clef-men/iris
  • ffengyu/iris
59 results
Show changes
Showing
with 4667 additions and 75 deletions
From stdpp Require Import gmap gmultiset.
From iris.algebra Require Export big_op cmra.
From iris.prelude Require Import options.
(** Option *)
Lemma big_opL_None {SI : sidx} {M : cmra} {A} (f : nat A option M) l :
([^op list] kx l, f k x) = None k x, l !! k = Some x f k x = None.
Proof.
revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
- intros [??] [|k] y ?; naive_solver.
- intros Hl. split; [by apply (Hl 0)|]. intros k. apply (Hl (S k)).
Qed.
Lemma big_opM_None {SI : sidx}
{M : cmra} `{Countable K} {A} (f : K A option M) m :
([^op map] kx m, f k x) = None k x, m !! k = Some x f k x = None.
Proof.
induction m as [|i x m ? IH] using map_ind=> /=.
{ by rewrite big_opM_empty. }
rewrite -None_equiv_eq big_opM_insert // None_equiv_eq op_None IH. split.
{ intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
intros Hm; split.
- apply (Hm i). by simplify_map_eq.
- intros k y ?. apply (Hm k). by simplify_map_eq.
Qed.
Lemma big_opS_None {SI : sidx} {M : cmra} `{Countable A} (f : A option M) X :
([^op set] x X, f x) = None x, x X f x = None.
Proof.
induction X as [|x X ? IH] using set_ind_L.
{ by rewrite big_opS_empty. }
rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
Qed.
Lemma big_opMS_None {SI : sidx} {M : cmra} `{Countable A} (f : A option M) X :
([^op mset] x X, f x) = None x, x X f x = None.
Proof.
induction X as [|x X IH] using gmultiset_ind.
{ rewrite big_opMS_empty. multiset_solver. }
rewrite -None_equiv_eq big_opMS_disj_union big_opMS_singleton None_equiv_eq op_None IH.
multiset_solver.
Qed.
From stdpp Require Export sets coPset.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Import options.
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)
(* The union CMRA *)
Section coPset.
Context {SI : sidx}.
Implicit Types X Y : coPset.
Canonical Structure coPsetO := discreteO coPset.
Local Instance coPset_valid_instance : Valid coPset := λ _, True.
Local Instance coPset_unit_instance : Unit coPset := ( : coPset).
Local Instance coPset_op_instance : Op coPset := union.
Local Instance coPset_pcore_instance : PCore coPset := Some.
Lemma coPset_op X Y : X Y = X Y.
Proof. done. Qed.
Lemma coPset_core X : core X = X.
Proof. done. Qed.
Lemma coPset_included X Y : X Y X Y.
Proof.
split.
- intros [Z ->]. rewrite coPset_op. set_solver.
- intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
Qed.
Lemma coPset_ra_mixin : RAMixin coPset.
Proof.
apply ra_total_mixin; eauto.
- solve_proper.
- solve_proper.
- solve_proper.
- intros X1 X2 X3. by rewrite !coPset_op assoc_L.
- intros X1 X2. by rewrite !coPset_op comm_L.
- intros X. by rewrite coPset_core idemp_L.
Qed.
Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.
Global Instance coPset_cmra_discrete : CmraDiscrete coPsetR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma coPset_ucmra_mixin : UcmraMixin coPset.
Proof. split; [done | | done]. intros X. by rewrite coPset_op left_id_L. Qed.
Canonical Structure coPsetUR := Ucmra coPset coPset_ucmra_mixin.
Lemma coPset_opM X mY : X ? mY = X default mY.
Proof using SI. destruct mY; by rewrite /= ?right_id_L. Qed.
Lemma coPset_update X Y : X ~~> Y.
Proof. done. Qed.
Lemma coPset_local_update X Y X' : X X' (X,Y) ~l~> (X',X').
Proof.
intros (Z&->&?)%subseteq_disjoint_union_L.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
split; first done. rewrite coPset_op. set_solver.
Qed.
End coPset.
(* The disjoint union CMRA *)
Inductive coPset_disj :=
| CoPset : coPset coPset_disj
| CoPsetInvalid : coPset_disj.
Section coPset_disj.
Context {SI : sidx}.
Local Arguments op _ _ !_ !_ /.
Canonical Structure coPset_disjO := leibnizO coPset_disj.
Local Instance coPset_disj_valid_instance : Valid coPset_disj := λ X,
match X with CoPset _ => True | CoPsetInvalid => False end.
Local Instance coPset_disj_unit_instance : Unit coPset_disj := CoPset ∅.
Local Instance coPset_disj_op_instance : Op coPset_disj := λ X Y,
match X, Y with
| CoPset X, CoPset Y => if decide (X ## Y) then CoPset (X Y) else CoPsetInvalid
| _, _ => CoPsetInvalid
end.
Local Instance coPset_disj_pcore_instance : PCore coPset_disj := λ _, Some ε.
Ltac coPset_disj_solve :=
repeat (simpl || case_decide);
first [apply (f_equal CoPset)|done|exfalso]; set_solver by eauto.
Lemma coPset_disj_included X Y : CoPset X CoPset Y X Y.
Proof.
split.
- move=> [[Z|]]; simpl; try case_decide; set_solver.
- intros (Z&->&?)%subseteq_disjoint_union_L.
exists (CoPset Z). coPset_disj_solve.
Qed.
Lemma coPset_disj_valid_inv_l X Y :
(CoPset X Y) Y', Y = CoPset Y' X ## Y'.
Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
Lemma coPset_disj_union X Y : X ## Y CoPset X CoPset Y = CoPset (X Y).
Proof. intros. by rewrite /= decide_True. Qed.
Lemma coPset_disj_valid_op X Y : (CoPset X CoPset Y) X ## Y.
Proof. simpl. case_decide; by split. Qed.
Lemma coPset_disj_ra_mixin : RAMixin coPset_disj.
Proof.
apply ra_total_mixin; eauto.
- intros [?|]; destruct 1; coPset_disj_solve.
- by constructor.
- by destruct 1.
- intros [X1|] [X2|] [X3|]; coPset_disj_solve.
- intros [X1|] [X2|]; coPset_disj_solve.
- intros [X|]; coPset_disj_solve.
- exists (CoPset ); coPset_disj_solve.
- intros [X1|] [X2|]; coPset_disj_solve.
Qed.
Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.
Global Instance coPset_disj_cmra_discrete : CmraDiscrete coPset_disjR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma coPset_disj_ucmra_mixin : UcmraMixin coPset_disj.
Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
Canonical Structure coPset_disjUR := Ucmra coPset_disj coPset_disj_ucmra_mixin.
End coPset_disj.
From iris.algebra Require Export cofe. From iris.algebra Require Export ofe.
From iris.algebra Require Export stepindex_finite.
Record solution (F : cFunctor) := Solution { From iris.prelude Require Import options.
solution_car :> cofeT;
solution_unfold : solution_car -n> F solution_car; (** * Solver for recursive domain equations over Cofes for FINITE step-indices *)
solution_fold : F solution_car -n> solution_car; (** This file implements a solver for recursive equations of the form [F X ≃ X],
solution_fold_unfold X : solution_fold (solution_unfold X) X; where [F] is a locally contractive functor of Cofes. As such, it is an
solution_unfold_fold X : solution_unfold (solution_fold X) X implementation of America and Rutten's theorem. More details can be found in the
Iris Reference.
This implementation only works for the [nat] index type. Importing this file
will globally fix the index type to [nat]. *)
(* Note that [Inhabited] is not derivable. Take [F X := ▶ X], then a possible
solution is [Empty_set]. *)
Record solution (F : oFunctor) := Solution {
solution_car :> ofe;
solution_inhabited : Inhabited solution_car;
solution_cofe : Cofe solution_car;
solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
}. }.
Arguments solution_unfold {_} _. Global Existing Instances solution_inhabited solution_cofe.
Arguments solution_fold {_} _.
Module solver. Section solver. Module solver. Section solver.
Context (F : cFunctor) `{Fcontr : cFunctorContractive F} Context (F : oFunctor) `{Fcontr : !oFunctorContractive F}.
`{Finhab : Inhabited (F unitC)}. Context `{Fcofe : (T : ofe) `{!Cofe T}, Cofe (oFunctor_apply F T)}.
Notation map := (cFunctor_map F). Context `{Finh : Inhabited (oFunctor_apply F unitO)}.
Notation map := (oFunctor_map F).
Fixpoint A' (k : nat) : { C : ofe & Cofe C } :=
match k with
| 0 => existT (P:=Cofe) unitO _
| S k => existT (P:=Cofe) (@oFunctor_apply _ F (projT1 (A' k)) (projT2 (A' k))) _
end.
Notation A k := (projT1 (A' k)).
Local Instance A_cofe k : Cofe (A k) := projT2 (A' k).
Fixpoint A (k : nat) : cofeT :=
match k with 0 => unitC | S k => F (A k) end.
Fixpoint f (k : nat) : A k -n> A (S k) := Fixpoint f (k : nat) : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end match k with 0 => OfeMor (λ _, inhabitant) | S k => map (g k,f k) end
with g (k : nat) : A (S k) -n> A k := with g (k : nat) : A (S k) -n> A k :=
match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end. match k with 0 => OfeMor (λ _, ()) | S k => map (f k,g k) end.
Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl. Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl. Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
Arguments A : simpl never. Global Arguments f : simpl never.
Arguments f : simpl never. Global Arguments g : simpl never.
Arguments g : simpl never.
Lemma gf {k} (x : A k) : g k (f k x) x. Lemma gf {k} (x : A k) : g k (f k x) x.
Proof. Proof using Fcontr.
induction k as [|k IH]; simpl in *; [by destruct x|]. induction k as [|k IH]; simpl in *; [by destruct x|].
rewrite -cFunctor_compose -{2}[x]cFunctor_id. by apply (contractive_proper map). rewrite -oFunctor_map_compose -{2}[x]oFunctor_map_id.
by apply (contractive_proper map).
Qed. Qed.
Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) {k} x. Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) {k} x.
Proof. Proof using Fcontr.
induction k as [|k IH]; simpl. induction k as [|k IH]; simpl.
- rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose. - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
apply (contractive_0 map). apply (contractive_0 map).
- rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose. - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
by apply (contractive_S map). by apply (contractive_S map).
Qed. Qed.
...@@ -45,53 +63,57 @@ Record tower := { ...@@ -45,53 +63,57 @@ Record tower := {
tower_car k :> A k; tower_car k :> A k;
g_tower k : g k (tower_car (S k)) tower_car k g_tower k : g k (tower_car (S k)) tower_car k
}. }.
Instance tower_equiv : Equiv tower := λ X Y, k, X k Y k. Global Instance tower_equiv : Equiv tower := λ X Y, k, X k Y k.
Instance tower_dist : Dist tower := λ n X Y, k, X k {n} Y k. Global Instance tower_dist : Dist tower := λ n X Y, k, X k {n} Y k.
Program Definition tower_chain (c : chain tower) (k : nat) : chain (A k) := Definition tower_ofe_mixin : OfeMixin tower.
{| chain_car i := c i k |}.
Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
Program Instance tower_compl : Compl tower := λ c,
{| tower_car n := compl (tower_chain c n) |}.
Next Obligation.
intros c k; apply equiv_dist=> n.
by rewrite (conv_compl n (tower_chain c k))
(conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k).
Qed.
Definition tower_cofe_mixin : CofeMixin tower.
Proof. Proof.
split. apply ofe_mixin_finite.
- intros X Y; split; [by intros HXY n k; apply equiv_dist|]. - intros X Y; split; [by intros HXY n k; apply equiv_dist|].
intros HXY k; apply equiv_dist; intros n; apply HXY. intros HXY k; apply equiv_dist; intros n; apply HXY.
- intros k; split. - intros k; split.
+ by intros X n. + by intros X n.
+ by intros X Y ? n. + by intros X Y ? n.
+ by intros X Y Z ?? n; trans (Y n). + by intros X Y Z ?? n; trans (Y n).
- intros k X Y HXY n; apply dist_S. - intros k X Y HXY n. specialize (HXY (S n)).
by rewrite -(g_tower X) (HXY (S n)) g_tower. apply (dist_le _ k) in HXY; [|apply SIdx.le_succ_diag_r].
- intros n c k; rewrite /= (conv_compl n (tower_chain c k)). by rewrite -(g_tower X) HXY g_tower.
apply (chain_cauchy c); lia. Qed.
Definition T : ofe := Ofe tower tower_ofe_mixin.
Program Definition tower_chain (c : chain T) (k : nat) : chain (A k) :=
{| chain_car i := c i k |}.
Next Obligation. intros c k n i ?; by apply (chain_cauchy c n). Qed.
Program Definition tower_compl : Compl T := λ c,
{| tower_car n := compl (tower_chain c n) |}.
Next Obligation.
intros c k; apply equiv_dist=> n.
by rewrite (conv_compl n (tower_chain c k))
(conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k).
Qed.
Global Program Instance tower_cofe : Cofe T := cofe_finite tower_compl _.
Next Obligation.
intros n c k; rewrite /= (conv_compl n (tower_chain c k)). done.
Qed. Qed.
Definition T : cofeT := CofeT tower tower_cofe_mixin.
Fixpoint ff {k} (i : nat) : A k -n> A (i + k) := Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
match i with 0 => cid | S i => f (i + k) ff i end. match i with 0 => cid | S i => f (i + k) ff i end.
Fixpoint gg {k} (i : nat) : A (i + k) -n> A k := Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
match i with 0 => cid | S i => gg i g (i + k) end. match i with 0 => cid | S i => gg i g (i + k) end.
Lemma ggff {k i} (x : A k) : gg i (ff i x) x. Lemma ggff {k i} (x : A k) : gg i (ff i x) x.
Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed. Proof using Fcontr. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
Lemma f_tower k (X : tower) : f (S k) (X (S k)) {k} X (S (S k)). Lemma f_tower k (X : tower) : f (S k) (X (S k)) {k} X (S (S k)).
Proof. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed. Proof using Fcontr. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
Lemma ff_tower k i (X : tower) : ff i (X (S k)) {k} X (i + S k). Lemma ff_tower k i (X : tower) : ff i (X (S k)) {k} X (i + S k).
Proof. Proof using Fcontr.
intros; induction i as [|i IH]; simpl; [done|]. intros; induction i as [|i IH]; simpl; [done|].
by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega. by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last lia.
Qed. Qed.
Lemma gg_tower k i (X : tower) : gg i (X (i + k)) X k. Lemma gg_tower k i (X : tower) : gg i (X (i + k)) X k.
Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed. Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
Instance tower_car_ne n k : Proper (dist n ==> dist n) (λ X, tower_car X k). Global Instance tower_car_ne k : NonExpansive (λ X, tower_car X k).
Proof. by intros X Y HX. Qed. Proof. by intros X Y HX. Qed.
Definition project (k : nat) : T -n> A k := CofeMor (λ X : T, tower_car X k). Definition project (k : nat) : T -n> A k := OfeMor (λ X : T, tower_car X k).
Definition coerce {i j} (H : i = j) : A i -n> A j := Definition coerce {i j} (H : i = j) : A i -n> A j :=
eq_rect _ (λ i', A i -n> A i') cid _ H. eq_rect _ (λ i', A i -n> A i') cid _ H.
...@@ -106,17 +128,17 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed. ...@@ -106,17 +128,17 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma coerce_f {k j} (H : S k = S j) (x : A k) : Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x). coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x).
Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed. Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) : Lemma gg_gg {k i i1 i2 j} : (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k),
gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)). gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
Proof. Proof.
assert (i = i2 + i1) by lia; simplify_eq/=. revert j x H1. intros Hij -> x. assert (i = i2 + i1) as -> by lia. revert j x Hij.
induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=; induction i2 as [|i2 IH]; intros j X Hij; simplify_eq/=;
[by rewrite coerce_id|by rewrite g_coerce IH]. [by rewrite coerce_id|by rewrite g_coerce IH].
Qed. Qed.
Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) : Lemma ff_ff {k i i1 i2 j} : (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k),
coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)). coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
Proof. Proof.
assert (i = i1 + i2) by lia; simplify_eq/=. intros ? <- x. assert (i = i1 + i2) as -> by lia.
induction i1 as [|i1 IH]; simplify_eq/=; induction i1 as [|i1 IH]; simplify_eq/=;
[by rewrite coerce_id|by rewrite coerce_f IH]. [by rewrite coerce_id|by rewrite coerce_f IH].
Qed. Qed.
...@@ -128,7 +150,7 @@ Definition embed_coerce {k} (i : nat) : A k -n> A i := ...@@ -128,7 +150,7 @@ Definition embed_coerce {k} (i : nat) : A k -n> A i :=
end. end.
Lemma g_embed_coerce {k i} (x : A k) : Lemma g_embed_coerce {k i} (x : A k) :
g i (embed_coerce (S i) x) embed_coerce i x. g i (embed_coerce (S i) x) embed_coerce i x.
Proof. Proof using Fcontr.
unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl. unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
- symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl. - symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
- exfalso; lia. - exfalso; lia.
...@@ -142,10 +164,10 @@ Qed. ...@@ -142,10 +164,10 @@ Qed.
Program Definition embed (k : nat) (x : A k) : T := Program Definition embed (k : nat) (x : A k) : T :=
{| tower_car n := embed_coerce n x |}. {| tower_car n := embed_coerce n x |}.
Next Obligation. intros k x i. apply g_embed_coerce. Qed. Next Obligation. intros k x i. apply g_embed_coerce. Qed.
Instance: Params (@embed) 1. Global Instance: Params (@embed) 1 := {}.
Instance embed_ne k n : Proper (dist n ==> dist n) (embed k). Global Instance embed_ne k : NonExpansive (embed k).
Proof. by intros x y Hxy i; rewrite /= Hxy. Qed. Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed.
Definition embed' (k : nat) : A k -n> T := CofeMor (embed k). Definition embed' (k : nat) : A k -n> T := OfeMor (embed k).
Lemma embed_f k (x : A k) : embed (S k) (f k x) embed k x. Lemma embed_f k (x : A k) : embed (S k) (f k x) embed k x.
Proof. Proof.
rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce. rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce.
...@@ -168,43 +190,45 @@ Proof. ...@@ -168,43 +190,45 @@ Proof.
- rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _). - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
Qed. Qed.
Program Definition unfold_chain (X : T) : chain (F T) := Global Instance tower_inhabited : Inhabited tower := populate (embed 0 ()).
Program Definition unfold_chain (X : T) : chain (oFunctor_apply F T) :=
{| chain_car n := map (project n,embed' n) (X (S n)) |}. {| chain_car n := map (project n,embed' n) (X (S n)) |}.
Next Obligation. Next Obligation.
intros X n i Hi. simpl; intros X n i Hi.
assert ( k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi. assert ( k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
induction k as [|k IH]; simpl; first done. induction k as [|k IH]; simpl; first done.
rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia. rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
rewrite f_S -cFunctor_compose. rewrite f_S -oFunctor_map_compose.
by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f. by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
Qed. Qed.
Definition unfold (X : T) : F T := compl (unfold_chain X). Definition unfold (X : T) : oFunctor_apply F T := compl (unfold_chain X).
Instance unfold_ne : Proper (dist n ==> dist n) unfold. Global Instance unfold_ne : NonExpansive unfold.
Proof. Proof.
intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X)) intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
(conv_compl n (unfold_chain Y)) /= (HXY (S n)). (conv_compl n (unfold_chain Y)) /= (HXY (S n)).
Qed. Qed.
Program Definition fold (X : F T) : T := Program Definition fold (X : oFunctor_apply F T) : T :=
{| tower_car n := g n (map (embed' n,project n) X) |}. {| tower_car n := g n (map (embed' n,project n) X) |}.
Next Obligation. Next Obligation.
intros X k. apply (_ : Proper (() ==> ()) (g k)). intros X k. apply (_ : Proper (() ==> ()) (g k)).
rewrite g_S -cFunctor_compose. rewrite g_S -oFunctor_map_compose.
apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower]. apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
Qed. Qed.
Instance fold_ne : Proper (dist n ==> dist n) fold. Global Instance fold_ne : NonExpansive fold.
Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed. Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Theorem result : solution F. Theorem result : solution F.
Proof. Proof using Type*.
apply (Solution F T (CofeMor unfold) (CofeMor fold)). refine (Solution F T _ _ (OfeIso (OfeMor fold) (OfeMor unfold) _ _)).
- move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=. - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)). rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
trans (map (ff n, gg n) (X (S (n + k)))). trans (map (ff n, gg n) (X (S (n + k)))).
{ rewrite /unfold (conv_compl n (unfold_chain X)). { rewrite /unfold (conv_compl n (unfold_chain X)).
rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia. rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia. rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
rewrite f_S -!cFunctor_compose; apply (contractive_ne map); split=> Y. rewrite f_S -!oFunctor_map_compose; apply (contractive_ne map); split=> Y.
+ rewrite /embed' /= /embed_coerce. + rewrite /embed' /= /embed_coerce.
destruct (le_lt_dec _ _); simpl; [exfalso; lia|]. destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf. by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
...@@ -214,14 +238,14 @@ Proof. ...@@ -214,14 +238,14 @@ Proof.
assert ( i k (x : A (S i + k)) (H : S i + k = i + S k), assert ( i k (x : A (S i + k)) (H : S i + k = i + S k),
map (ff i, gg i) x gg i (coerce H x)) as map_ff_gg. map (ff i, gg i) x gg i (coerce H x)) as map_ff_gg.
{ intros i; induction i as [|i IH]; intros k' x H; simpl. { intros i; induction i as [|i IH]; intros k' x H; simpl.
{ by rewrite coerce_id cFunctor_id. } { by rewrite coerce_id oFunctor_map_id. }
rewrite cFunctor_compose g_coerce; apply IH. } rewrite oFunctor_map_compose g_coerce; apply IH. }
assert (H: S n + k = n + S k) by lia. assert (H: S n + k = n + S k) by lia.
rewrite (map_ff_gg _ _ _ H). rewrite (map_ff_gg _ _ _ H).
apply (_ : Proper (_ ==> _) (gg _)); by destruct H. apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
- intros X; rewrite equiv_dist=> n /=. - intros X; rewrite equiv_dist=> n /=.
rewrite /unfold /= (conv_compl' n (unfold_chain (fold X))) /=. rewrite /unfold /= (conv_compl_S n (unfold_chain (fold X))) /=.
rewrite g_S -!cFunctor_compose -{2}[X]cFunctor_id. rewrite g_S -!oFunctor_map_compose -{2}[X]oFunctor_map_id.
apply (contractive_ne map); split => Y /=. apply (contractive_ne map); split => Y /=.
+ rewrite f_tower. apply dist_S. by rewrite embed_tower. + rewrite f_tower. apply dist_S. by rewrite embed_tower.
+ etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower]. + etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
......
From iris.algebra Require Export cmra updates. From iris.algebra Require Export cmra.
From iris.algebra Require Import upred. From iris.algebra Require Import updates local_updates.
From iris.prelude Require Import options.
Local Arguments pcore _ _ !_ /. Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /. Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /. Local Arguments validN _ _ _ _ !_ /.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
Local Arguments cmra_validN _ _ !_ /. Local Arguments cmra_validN _ _ _ !_ /.
Local Arguments cmra_valid _ !_ /. Local Arguments cmra_valid _ !_ /.
Inductive csum (A B : Type) := Inductive csum (A B : Type) :=
| Cinl : A csum A B | Cinl : A csum A B
| Cinr : B csum A B | Cinr : B csum A B
| CsumBot : csum A B. | CsumInvalid : csum A B.
Arguments Cinl {_ _} _. Global Arguments Cinl {_ _} _.
Arguments Cinr {_ _} _. Global Arguments Cinr {_ _} _.
Arguments CsumBot {_ _}. Global Arguments CsumInvalid {_ _}.
Section cofe. Global Instance: Params (@Cinl) 2 := {}.
Context {A B : cofeT}. Global Instance: Params (@Cinr) 2 := {}.
Global Instance: Params (@CsumInvalid) 2 := {}.
Global Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
match x with Cinl a => Some a | _ => None end.
Global Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
match x with Cinr b => Some b | _ => None end.
Section ofe.
Context {SI : sidx} {A B : ofe}.
Implicit Types a : A. Implicit Types a : A.
Implicit Types b : B. Implicit Types b : B.
(* Cofe *) (* Cofe *)
Inductive csum_equiv : Equiv (csum A B) := Inductive csum_equiv : Equiv (csum A B) :=
| Cinl_equiv a a' : a a' Cinl a Cinl a' | Cinl_equiv a a' : a a' Cinl a Cinl a'
| Cinlr_equiv b b' : b b' Cinr b Cinr b' | Cinr_equiv b b' : b b' Cinr b Cinr b'
| CsumBot_equiv : CsumBot CsumBot. | CsumInvalid_equiv : CsumInvalid CsumInvalid.
Existing Instance csum_equiv. Local Existing Instance csum_equiv.
Inductive csum_dist : Dist (csum A B) := Inductive csum_dist : Dist (csum A B) :=
| Cinl_dist n a a' : a {n} a' Cinl a {n} Cinl a' | Cinl_dist n a a' : a {n} a' Cinl a {n} Cinl a'
| Cinlr_dist n b b' : b {n} b' Cinr b {n} Cinr b' | Cinr_dist n b b' : b {n} b' Cinr b {n} Cinr b'
| CsumBot_dist n : CsumBot {n} CsumBot. | CsumInvalid_dist n : CsumInvalid {n} CsumInvalid.
Existing Instance csum_dist. Local Existing Instance csum_dist.
Global Instance Cinl_ne n : Proper (dist n ==> dist n) (@Cinl A B). Global Instance Cinl_ne : NonExpansive (@Cinl A B).
Proof. by constructor. Qed. Proof. by constructor. Qed.
Global Instance Cinl_proper : Proper (() ==> ()) (@Cinl A B). Global Instance Cinl_proper : Proper (() ==> ()) (@Cinl A B).
Proof. by constructor. Qed. Proof. by constructor. Qed.
...@@ -40,7 +51,7 @@ Global Instance Cinl_inj : Inj (≡) (≡) (@Cinl A B). ...@@ -40,7 +51,7 @@ Global Instance Cinl_inj : Inj (≡) (≡) (@Cinl A B).
Proof. by inversion_clear 1. Qed. Proof. by inversion_clear 1. Qed.
Global Instance Cinl_inj_dist n : Inj (dist n) (dist n) (@Cinl A B). Global Instance Cinl_inj_dist n : Inj (dist n) (dist n) (@Cinl A B).
Proof. by inversion_clear 1. Qed. Proof. by inversion_clear 1. Qed.
Global Instance Cinr_ne n : Proper (dist n ==> dist n) (@Cinr A B). Global Instance Cinr_ne : NonExpansive (@Cinr A B).
Proof. by constructor. Qed. Proof. by constructor. Qed.
Global Instance Cinr_proper : Proper (() ==> ()) (@Cinr A B). Global Instance Cinr_proper : Proper (() ==> ()) (@Cinr A B).
Proof. by constructor. Qed. Proof. by constructor. Qed.
...@@ -49,49 +60,92 @@ Proof. by inversion_clear 1. Qed. ...@@ -49,49 +60,92 @@ Proof. by inversion_clear 1. Qed.
Global Instance Cinr_inj_dist n : Inj (dist n) (dist n) (@Cinr A B). Global Instance Cinr_inj_dist n : Inj (dist n) (dist n) (@Cinr A B).
Proof. by inversion_clear 1. Qed. Proof. by inversion_clear 1. Qed.
Program Definition csum_chain_l (c : chain (csum A B)) (a : A) : chain A := Definition csum_ofe_mixin : OfeMixin (csum A B).
{| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Program Definition csum_chain_r (c : chain (csum A B)) (b : B) : chain B :=
{| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Instance csum_compl : Compl (csum A B) := λ c,
match c 0 with
| Cinl a => Cinl (compl (csum_chain_l c a))
| Cinr b => Cinr (compl (csum_chain_r c b))
| CsumBot => CsumBot
end.
Definition csum_cofe_mixin : CofeMixin (csum A B).
Proof. Proof.
split. split.
- intros mx my; split. - intros mx my; split.
+ by destruct 1; constructor; try apply equiv_dist. + by destruct 1; constructor; try apply equiv_dist.
+ intros Hxy; feed inversion (Hxy 0); subst; constructor; try done; + intros Hxy; oinversion (Hxy 0); subst; constructor; try done;
apply equiv_dist=> n; by feed inversion (Hxy n). apply equiv_dist=> n; by oinversion (Hxy n).
- intros n; split. - intros n; split.
+ by intros [|a|]; constructor. + by intros [|a|]; constructor.
+ by destruct 1; constructor. + by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto. + destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S. - inversion_clear 1; intros Hlt; constructor; eauto using dist_le.
- intros n c; rewrite /compl /csum_compl. Qed.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. Canonical Structure csumO : ofe := Ofe (csum A B) csum_ofe_mixin.
+ rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver.
+ rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver. Program Definition csum_chain_l (c : chain csumO) (a : A) : chain A :=
{| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Program Definition csum_chain_r (c : chain csumO) (b : B) : chain B :=
{| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Definition csum_compl `{!Cofe A, !Cofe B} : Compl csumO := λ c,
match c 0 with
| Cinl a => Cinl (compl (csum_chain_l c a))
| Cinr b => Cinr (compl (csum_chain_r c b))
| CsumInvalid => CsumInvalid
end.
Program Definition csum_bchain_l {α} (c : bchain csumO α) (a : A) : bchain A α :=
{| bchain_car β := match c β return _ with Cinl a' => a' | _ => a end |}.
Next Obligation.
intros α c a β γ Hle . simpl.
by destruct (bchain_cauchy _ c β γ Hle ).
Qed.
Program Definition csum_bchain_r {α} (c : bchain csumO α) (b : B) : bchain B α :=
{| bchain_car β := match c β return _ with Cinr b' => b' | _ => b end |}.
Next Obligation.
intros α c b β γ Hle . simpl.
by destruct (bchain_cauchy _ c β γ Hle ).
Qed.
Definition csum_lbcompl `{!Cofe A, !Cofe B} : LBCompl csumO := λ n Hn c,
match c _ (SIdx.limit_lt_0 _ Hn) with
| Cinl a => Cinl (lbcompl Hn (csum_bchain_l c a))
| Cinr b => Cinr (lbcompl Hn (csum_bchain_r c b))
| CsumInvalid => CsumInvalid
end.
Global Program Instance csum_cofe `{!Cofe A, !Cofe B} : Cofe csumO :=
{| compl := csum_compl; lbcompl := csum_lbcompl |}.
Next Obligation.
intros ?? n c; rewrite /compl /csum_compl.
oinversion (chain_cauchy c 0 n); first apply SIdx.le_0_l; constructor.
- rewrite (conv_compl n (csum_chain_l c _)) /=. destruct (c n); naive_solver.
- rewrite (conv_compl n (csum_chain_r c _)) /=. destruct (c n); naive_solver.
Qed.
Next Obligation.
intros ?? n Hn c m Hm. rewrite /lbcompl /csum_lbcompl.
oinversion (bchain_cauchy _ c 0 m (SIdx.limit_lt_0 _ Hn) Hm);
[apply SIdx.le_0_l|..]; f_equiv.
- rewrite (conv_lbcompl Hn (csum_bchain_l c _) Hm) /=.
destruct (c m); naive_solver.
- rewrite (conv_lbcompl Hn (csum_bchain_r c _) Hm) /=.
destruct (c m); naive_solver.
Qed. Qed.
Canonical Structure csumC : cofeT := CofeT (csum A B) csum_cofe_mixin. Next Obligation.
Global Instance csum_discrete : Discrete A Discrete B Discrete csumC. intros ?? n Hn c1 c2 m Hc. rewrite /lbcompl /csum_lbcompl.
Proof. by inversion_clear 3; constructor; apply (timeless _). Qed. destruct (Hc 0 (SIdx.limit_lt_0 _ Hn)); f_equiv.
- apply lbcompl_ne=> p Hp /=. by destruct (Hc p Hp).
- apply lbcompl_ne=> p Hp /=. by destruct (Hc p Hp).
Qed.
Global Instance csum_ofe_discrete :
OfeDiscrete A OfeDiscrete B OfeDiscrete csumO.
Proof. by inversion_clear 3; constructor; apply (discrete_0 _). Qed.
Global Instance csum_leibniz : Global Instance csum_leibniz :
LeibnizEquiv A LeibnizEquiv B LeibnizEquiv (csumC A B). LeibnizEquiv A LeibnizEquiv B LeibnizEquiv csumO.
Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed. Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
Global Instance Cinl_timeless a : Timeless a Timeless (Cinl a). Global Instance Cinl_discrete a : Discrete a Discrete (Cinl a).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
Global Instance Cinr_timeless b : Timeless b Timeless (Cinr b). Global Instance Cinr_discrete b : Discrete b Discrete (Cinr b).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
End cofe.
End ofe.
Arguments csumC : clear implicits. Global Arguments csumO {_} _ _.
(* Functor on COFEs *) (* Functor on COFEs *)
Definition csum_map {A A' B B'} (fA : A A') (fB : B B') Definition csum_map {A A' B B'} (fA : A A') (fB : B B')
...@@ -99,9 +153,9 @@ Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B') ...@@ -99,9 +153,9 @@ Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
match x with match x with
| Cinl a => Cinl (fA a) | Cinl a => Cinl (fA a)
| Cinr b => Cinr (fB b) | Cinr b => Cinr (fB b)
| CsumBot => CsumBot | CsumInvalid => CsumInvalid
end. end.
Instance: Params (@csum_map) 4. Global Instance: Params (@csum_map) 4 := {}.
Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x. Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x.
Proof. by destruct x. Qed. Proof. by destruct x. Qed.
...@@ -109,74 +163,98 @@ Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'') ...@@ -109,74 +163,98 @@ Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
(g : B B') (g' : B' B'') (x : csum A B) : (g : B B') (g' : B' B'') (x : csum A B) :
csum_map (f' f) (g' g) x = csum_map f' g' (csum_map f g x). csum_map (f' f) (g' g) x = csum_map f' g' (csum_map f g x).
Proof. by destruct x. Qed. Proof. by destruct x. Qed.
Lemma csum_map_ext {A A' B B' : cofeT} (f f' : A A') (g g' : B B') x : Lemma csum_map_ext {SI : sidx} {A A' B B' : ofe} (f f' : A A') (g g' : B B') x :
( x, f x f' x) ( x, g x g' x) csum_map f g x csum_map f' g' x. ( x, f x f' x) ( x, g x g' x) csum_map f g x csum_map f' g' x.
Proof. by destruct x; constructor. Qed. Proof. by destruct x; constructor. Qed.
Instance csum_map_cmra_ne {A A' B B' : cofeT} n : Global Instance csum_map_cmra_ne {SI : sidx} {A A' B B' : ofe} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n) Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
(@csum_map A A' B B'). (@csum_map A A' B B').
Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed. Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
Definition csumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') : Definition csumO_map {SI : sidx} {A A' B B'} (f : A -n> A') (g : B -n> B') :
csumC A B -n> csumC A' B' := csumO A B -n> csumO A' B' :=
CofeMor (csum_map f g). OfeMor (csum_map f g).
Instance csumC_map_ne A A' B B' n : Global Instance csumO_map_ne {SI : sidx} A A' B B' :
Proper (dist n ==> dist n ==> dist n) (@csumC_map A A' B B'). NonExpansive2 (@csumO_map SI A A' B B').
Proof. by intros f f' Hf g g' Hg []; constructor. Qed. Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
Section cmra. Section cmra.
Context {A B : cmraT}. Context {SI : sidx} {A B : cmra}.
Implicit Types a : A. Implicit Types a : A.
Implicit Types b : B. Implicit Types b : B.
(* CMRA *) (* CMRA *)
Instance csum_valid : Valid (csum A B) := λ x, Local Instance csum_valid_instance : Valid (csum A B) := λ x,
match x with match x with
| Cinl a => a | Cinl a => a
| Cinr b => b | Cinr b => b
| CsumBot => False | CsumInvalid => False
end. end.
Instance csum_validN : ValidN (csum A B) := λ n x, Local Instance csum_validN_instance : ValidN (csum A B) := λ n x,
match x with match x with
| Cinl a => {n} a | Cinl a => {n} a
| Cinr b => {n} b | Cinr b => {n} b
| CsumBot => False | CsumInvalid => False
end. end.
Instance csum_pcore : PCore (csum A B) := λ x, Local Instance csum_pcore_instance : PCore (csum A B) := λ x,
match x with match x with
| Cinl a => Cinl <$> pcore a | Cinl a => Cinl <$> pcore a
| Cinr b => Cinr <$> pcore b | Cinr b => Cinr <$> pcore b
| CsumBot => Some CsumBot | CsumInvalid => Some CsumInvalid
end. end.
Instance csum_op : Op (csum A B) := λ x y, Local Instance csum_op_instance : Op (csum A B) := λ x y,
match x, y with match x, y with
| Cinl a, Cinl a' => Cinl (a a') | Cinl a, Cinl a' => Cinl (a a')
| Cinr b, Cinr b' => Cinr (b b') | Cinr b, Cinr b' => Cinr (b b')
| _, _ => CsumBot | _, _ => CsumInvalid
end. end.
Lemma Cinl_op a a' : Cinl a Cinl a' = Cinl (a a'). Lemma Cinl_op a a' : Cinl (a a') = Cinl a Cinl a'.
Proof. done. Qed. Proof. done. Qed.
Lemma Cinr_op b b' : Cinr b Cinr b' = Cinr (b b'). Lemma Cinr_op b b' : Cinr (b b') = Cinr b Cinr b'.
Proof. done. Qed.
Lemma Cinl_valid a : (Cinl a) a.
Proof. done. Qed.
Lemma Cinr_valid b : (Cinr b) b.
Proof. done. Qed. Proof. done. Qed.
Lemma csum_included x y : Lemma csum_included x y :
x y y = CsumBot ( a a', x = Cinl a y = Cinl a' a a') x y y = CsumInvalid ( a a', x = Cinl a y = Cinl a' a a')
( b b', x = Cinr b y = Cinr b' b b'). ( b b', x = Cinr b y = Cinr b' b b').
Proof. Proof.
split. split.
- intros [z Hy]; destruct x as [a|b|], z as [a'|b'|]; inversion_clear Hy; auto. - unfold included. intros [[a'|b'|] Hy]; destruct x as [a|b|];
+ right; left; eexists _, _; split_and!; eauto. eexists; eauto. inversion_clear Hy; eauto 10.
+ right; right; eexists _, _; split_and!; eauto. eexists; eauto.
- intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]]. - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
+ destruct x; exists CsumBot; constructor. + destruct x; exists CsumInvalid; constructor.
+ exists (Cinl c); by constructor. + exists (Cinl c); by constructor.
+ exists (Cinr c); by constructor. + exists (Cinr c); by constructor.
Qed. Qed.
Lemma Cinl_included a a' : Cinl a Cinl a' a a'.
Proof. rewrite csum_included. naive_solver. Qed.
Lemma Cinr_included b b' : Cinr b Cinr b' b b'.
Proof. rewrite csum_included. naive_solver. Qed.
Lemma CsumInvalid_included x : x CsumInvalid.
Proof. exists CsumInvalid. by destruct x. Qed.
(** We register a hint for [CsumInvalid_included] below. *)
Lemma csum_cmra_mixin : CMRAMixin (csum A B). Lemma csum_includedN n x y :
x {n} y y = CsumInvalid ( a a', x = Cinl a y = Cinl a' a {n} a')
( b b', x = Cinr b y = Cinr b' b {n} b').
Proof. Proof.
split. split.
- intros n []; destruct 1; constructor; by cofe_subst. - unfold includedN. intros [[a'|b'|] Hy]; destruct x as [a|b|];
inversion_clear Hy; eauto 10.
- intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
+ destruct x; exists CsumInvalid; constructor.
+ exists (Cinl c); by constructor.
+ exists (Cinr c); by constructor.
Qed.
Lemma csum_cmra_mixin : CmraMixin (csum A B).
Proof.
split.
- intros [] n; destruct 1; constructor; by ofe_subst.
- intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto. - intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto. destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto.
...@@ -184,9 +262,9 @@ Proof. ...@@ -184,9 +262,9 @@ Proof.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq. + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_ne n b b' cb) as (cb'&->&?); auto. destruct (cmra_pcore_ne n b b' cb) as (cb'&->&?); auto.
exists (Cinr cb'); by repeat constructor. exists (Cinr cb'); by repeat constructor.
- intros ? [a|b|] [a'|b'|] H; inversion_clear H; cofe_subst; done. - intros ? [a|b|] [a'|b'|] H; inversion_clear H; ofe_subst; done.
- intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O. - pose 0. intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver.
- intros n [a|b|]; simpl; auto using cmra_validN_S. - intros n m [a|b|]; simpl; eauto using cmra_validN_le.
- intros [a1|b1|] [a2|b2|] [a3|b3|]; constructor; by rewrite ?assoc. - intros [a1|b1|] [a2|b2|] [a3|b3|]; constructor; by rewrite ?assoc.
- intros [a1|b1|] [a2|b2|]; constructor; by rewrite 1?comm. - intros [a1|b1|] [a2|b2|]; constructor; by rewrite 1?comm.
- intros [a|b|] ? [=]; subst; auto. - intros [a|b|] ? [=]; subst; auto.
...@@ -196,68 +274,83 @@ Proof. ...@@ -196,68 +274,83 @@ Proof.
constructor; eauto using cmra_pcore_l. constructor; eauto using cmra_pcore_l.
- intros [a|b|] ? [=]; subst; auto. - intros [a|b|] ? [=]; subst; auto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
feed inversion (cmra_pcore_idemp a ca); repeat constructor; auto. oinversion (cmra_pcore_idemp a ca); repeat constructor; auto.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq. + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
feed inversion (cmra_pcore_idemp b cb); repeat constructor; auto. oinversion (cmra_pcore_idemp b cb); repeat constructor; auto.
- intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=]. - intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
+ exists CsumBot. rewrite csum_included; eauto. + exists CsumInvalid. rewrite csum_included; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_preserving a a' ca) as (ca'&->&?); auto. destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
exists (Cinl ca'). rewrite csum_included; eauto 10. exists (Cinl ca'). rewrite csum_included; eauto 10.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq. + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_preserving b b' cb) as (cb'&->&?); auto. destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto.
exists (Cinr cb'). rewrite csum_included; eauto 10. exists (Cinr cb'). rewrite csum_included; eauto 10.
- intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done. - intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
- intros n [a|b|] y1 y2 Hx Hx'. - intros n [a|b|] y1 y2 Hx Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx'). + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'.
apply (inj Cinl) in Hx'. destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); [done|apply (inj Cinl), Hx'|].
destruct (cmra_extend n a a1 a2) as ([z1 z2]&?&?&?); auto. exists (Cinl z1), (Cinl z2). by repeat constructor.
exists (Cinl z1, Cinl z2). by repeat constructor. + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx'). destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); [done|apply (inj Cinr), Hx'|].
apply (inj Cinr) in Hx'. exists (Cinr z1), (Cinr z2). by repeat constructor.
destruct (cmra_extend n b b1 b2) as ([z1 z2]&?&?&?); auto. + by exists CsumInvalid, CsumInvalid; destruct y1, y2; inversion_clear Hx'.
exists (Cinr z1, Cinr z2). by repeat constructor.
+ by exists (CsumBot, CsumBot); destruct y1, y2; inversion_clear Hx'.
Qed. Qed.
Canonical Structure csumR := Canonical Structure csumR := Cmra (csum A B) csum_cmra_mixin.
CMRAT (csum A B) csum_cofe_mixin csum_cmra_mixin.
Global Instance csum_cmra_discrete : Global Instance csum_cmra_discrete :
CMRADiscrete A CMRADiscrete B CMRADiscrete csumR. CmraDiscrete A CmraDiscrete B CmraDiscrete csumR.
Proof. Proof.
split; first apply _. split; first apply _.
by move=>[a|b|] HH /=; try apply cmra_discrete_valid. by move=>[a|b|] HH /=; try apply cmra_discrete_valid.
Qed. Qed.
Global Instance Cinl_persistent a : Persistent a Persistent (Cinl a). Global Instance Cinl_core_id a : CoreId a CoreId (Cinl a).
Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed. Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinr_persistent b : Persistent b Persistent (Cinr b). Global Instance Cinr_core_id b : CoreId b CoreId (Cinr b).
Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed. Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinl_exclusive a : Exclusive a Exclusive (Cinl a). Global Instance Cinl_exclusive a : Exclusive a Exclusive (Cinl a).
Proof. by move=> H[]? =>[/H||]. Qed. Proof. by move=> H[]? =>[/H||]. Qed.
Global Instance Cinr_exclusive b : Exclusive b Exclusive (Cinr b). Global Instance Cinr_exclusive b : Exclusive b Exclusive (Cinr b).
Proof. by move=> H[]? =>[|/H|]. Qed. Proof. by move=> H[]? =>[|/H|]. Qed.
(** Internalized properties *) Global Instance Cinl_cancelable a : Cancelable a Cancelable (Cinl a).
Lemma csum_equivI {M} (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 : uPred M).
Proof. Proof.
uPred.unseal; do 2 split; first by destruct 1. move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ.
by destruct x, y; try destruct 1; try constructor. constructor. by eapply (cancelableN a).
Qed.
Global Instance Cinr_cancelable b : Cancelable b Cancelable (Cinr b).
Proof.
move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ.
constructor. by eapply (cancelableN b).
Qed.
Global Instance Cinl_id_free a : IdFree a IdFree (Cinl a).
Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
Global Instance Cinr_id_free b : IdFree b IdFree (Cinr b).
Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
(** Interaction with [option] *)
Lemma Some_csum_includedN x y n :
Some x {n} Some y
y = CsumInvalid
( a a', x = Cinl a y = Cinl a' Some a {n} Some a')
( b b', x = Cinr b y = Cinr b' Some b {n} Some b').
Proof.
repeat setoid_rewrite Some_includedN. rewrite csum_includedN. split.
- intros [Hxy|?]; [inversion Hxy|]; naive_solver.
- naive_solver by f_equiv.
Qed.
Lemma Some_csum_included x y :
Some x Some y
y = CsumInvalid
( a a', x = Cinl a y = Cinl a' Some a Some a')
( b b', x = Cinr b y = Cinr b' Some b Some b').
Proof.
repeat setoid_rewrite Some_included. rewrite csum_included. split.
- intros [Hxy|?]; [inversion Hxy|]; naive_solver.
- naive_solver by f_equiv.
Qed. Qed.
Lemma csum_validI {M} (x : csum A B) :
x ⊣⊢ (match x with
| Cinl a => a
| Cinr b => b
| CsumBot => False
end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** Updates *) (** Updates *)
Lemma csum_update_l (a1 a2 : A) : a1 ~~> a2 Cinl a1 ~~> Cinl a2. Lemma csum_update_l (a1 a2 : A) : a1 ~~> a2 Cinl a1 ~~> Cinl a2.
...@@ -292,66 +385,66 @@ Proof. eauto using csum_updateP_l. Qed. ...@@ -292,66 +385,66 @@ Proof. eauto using csum_updateP_l. Qed.
Lemma csum_updateP'_r (P : B Prop) b : Lemma csum_updateP'_r (P : B Prop) b :
b ~~>: P Cinr b ~~>: λ m', b', m' = Cinr b' P b'. b ~~>: P Cinr b ~~>: λ m', b', m' = Cinr b' P b'.
Proof. eauto using csum_updateP_r. Qed. Proof. eauto using csum_updateP_r. Qed.
Lemma csum_local_update_l (a1 a2 : A) af :
( af', af = Cinl <$> af' a1 ~l~> a2 @ af') Cinl a1 ~l~> Cinl a2 @ af. Lemma csum_local_update_l (a1 a2 a1' a2' : A) :
(a1,a2) ~l~> (a1',a2') (Cinl a1,Cinl a2) ~l~> (Cinl a1',Cinl a2').
Proof. Proof.
intros Ha. split; destruct af as [[af'| |]|]=>//=. intros Hup n mf ? Ha1; simpl in *.
- by eapply (Ha (Some af')). destruct (Hup n (mf ≫= maybe Cinl)); auto.
- by eapply (Ha None). { by destruct mf as [[]|]; inversion_clear Ha1. }
- destruct (Ha (Some af') (reflexivity _)) as [_ Ha']. split; first done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Ha' n (Some mz)). by apply (Ha' n None).
- destruct (Ha None (reflexivity _)) as [_ Ha'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Ha' n (Some mz)). by apply (Ha' n None).
Qed. Qed.
Lemma csum_local_update_r (b1 b2 : B) bf : Lemma csum_local_update_r (b1 b2 b1' b2' : B) :
( bf', bf = Cinr <$> bf' b1 ~l~> b2 @ bf') Cinr b1 ~l~> Cinr b2 @ bf. (b1,b2) ~l~> (b1',b2') (Cinr b1,Cinr b2) ~l~> (Cinr b1',Cinr b2').
Proof. Proof.
intros Hb. split; destruct bf as [[|bf'|]|]=>//=. intros Hup n mf ? Ha1; simpl in *.
- by eapply (Hb (Some bf')). destruct (Hup n (mf ≫= maybe Cinr)); auto.
- by eapply (Hb None). { by destruct mf as [[]|]; inversion_clear Ha1. }
- destruct (Hb (Some bf') (reflexivity _)) as [_ Hb']. split; first done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Hb' n (Some mz)). by apply (Hb' n None).
- destruct (Hb None (reflexivity _)) as [_ Hb'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Hb' n (Some mz)). by apply (Hb' n None).
Qed. Qed.
End cmra. End cmra.
Arguments csumR : clear implicits. (* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
the new unification algorithm. The old unification algorithm sometimes gets
confused by going from [ucmra]'s to [cmra]'s and back. *)
Global Hint Extern 0 (_ CsumInvalid) => apply: CsumInvalid_included : core.
Global Arguments csumR {_} _ _.
(* Functor *) (* Functor *)
Instance csum_map_cmra_monotone {A A' B B' : cmraT} (f : A A') (g : B B') : Global Instance csum_map_cmra_morphism {SI : sidx} {A A' B B' : cmra}
CMRAMonotone f CMRAMonotone g CMRAMonotone (csum_map f g). (f : A A') (g : B B') :
CmraMorphism f CmraMorphism g CmraMorphism (csum_map f g).
Proof. Proof.
split; try apply _. split; try apply _.
- intros n [a|b|]; simpl; auto using validN_preserving. - intros n [a|b|]; simpl; auto using cmra_morphism_validN.
- intros x y; rewrite !csum_included. - move=> [a|b|]=>//=; rewrite -cmra_morphism_pcore; by destruct pcore.
intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl; - intros [xa|ya|] [xb|yb|]=>//=; by rewrite cmra_morphism_op.
eauto 10 using included_preserving.
Qed. Qed.
Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {| Program Definition csumRF {SI : sidx} (Fa Fb : rFunctor) : rFunctor := {|
rFunctor_car A B := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B); rFunctor_car A _ B _ := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
rFunctor_map A1 A2 B1 B2 fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg) rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
csumO_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
|}. |}.
Next Obligation. Next Obligation.
by intros Fa Fb A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne. intros ? Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg;
by apply csumO_map_ne; try apply rFunctor_map_ne.
Qed. Qed.
Next Obligation. Next Obligation.
intros Fa Fb A B x. rewrite /= -{2}(csum_map_id x). intros ? Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
apply csum_map_ext=>y; apply rFunctor_id. apply csum_map_ext=>y; apply rFunctor_map_id.
Qed. Qed.
Next Obligation. Next Obligation.
intros Fa Fb A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -csum_map_compose. intros ? Fa Fb A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x.
apply csum_map_ext=>y; apply rFunctor_compose. rewrite /= -csum_map_compose.
apply csum_map_ext=>y; apply rFunctor_map_compose.
Qed. Qed.
Instance csumRF_contractive Fa Fb : Global Instance csumRF_contractive {SI : sidx} Fa Fb :
rFunctorContractive Fa rFunctorContractive Fb rFunctorContractive Fa rFunctorContractive Fb
rFunctorContractive (csumRF Fa Fb). rFunctorContractive (csumRF Fa Fb).
Proof. Proof.
by intros ?? A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_contractive. intros ??? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
by apply csumO_map_ne; try apply rFunctor_map_contractive.
Qed. Qed.
(** Camera of discardable fractions.
This is a generalisation of the fractional camera where elements can
represent both ownership of a fraction (as in the fractional camera) and the
knowledge that a fraction has been discarded.
Ownership of a fraction is denoted [DfracOwn q] and behaves identically to
[q] of the fractional camera.
Knowledge that a fraction has been discarded is denoted [DfracDiscarded].
This elements is its own core, making ownership persistent.
One can make a frame preserving update from _owning_ a fraction to _knowing_
that the fraction has been discarded.
Crucially, ownership over 1 is an exclusive element just as it is in the
fractional camera. Hence owning 1 implies that no fraction has been
discarded. Conversely, knowing that a fraction has been discarded implies
that no one can own 1. And, since discarding is an irreversible operation,
it also implies that no one can own 1 in the future *)
From stdpp Require Import countable.
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes updates frac.
From iris.prelude Require Import options.
(** An element of dfrac denotes ownership of a fraction, knowledge that a
fraction has been discarded, or both. Note that [DfracBoth] can be written
as [DfracOwn q ⋅ DfracDiscarded]. This should be used instead
of [DfracBoth] which is for internal use only. *)
Inductive dfrac :=
| DfracOwn : Qp dfrac
| DfracDiscarded : dfrac
| DfracBoth : Qp dfrac.
(* This notation is intended to be used as a component in other notations that
include discardable fractions. The notation provides shorthands for the
constructors and the commonly used full fraction. For an example
demonstrating how this can be used see the notation in [gen_heap.v]. *)
Declare Custom Entry dfrac.
Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
Notation "□" := DfracDiscarded (in custom dfrac).
Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
Notation "" := (DfracOwn 1) (in custom dfrac).
Section dfrac.
Context {SI : sidx}.
Canonical Structure dfracO := leibnizO dfrac.
Implicit Types p q : Qp.
Implicit Types dp dq : dfrac.
Global Instance dfrac_inhabited : Inhabited dfrac := populate DfracDiscarded.
Global Instance dfrac_eq_dec : EqDecision dfrac.
Proof. solve_decision. Defined.
Global Instance dfrac_countable : Countable dfrac.
Proof.
set (enc dq := match dq with
| DfracOwn q => inl q
| DfracDiscarded => inr (inl ())
| DfracBoth q => inr (inr q)
end).
set (dec y := Some match y with
| inl q => DfracOwn q
| inr (inl ()) => DfracDiscarded
| inr (inr q) => DfracBoth q
end).
refine (inj_countable enc dec _). by intros [].
Qed.
Global Instance DfracOwn_inj : Inj (=) (=) DfracOwn.
Proof. by injection 1. Qed.
Global Instance DfracBoth_inj : Inj (=) (=) DfracBoth.
Proof. by injection 1. Qed.
(** An element is valid as long as the sum of its content is less than one. *)
Local Instance dfrac_valid_instance : Valid dfrac := λ dq,
match dq with
| DfracOwn q => q 1
| DfracDiscarded => True
| DfracBoth q => q < 1
end%Qp.
(** As in the fractional camera the core is undefined for elements denoting
ownership of a fraction. For elements denoting the knowledge that a fraction has
been discarded the core is the identity function. *)
Local Instance dfrac_pcore_instance : PCore dfrac := λ dq,
match dq with
| DfracOwn q => None
| DfracDiscarded => Some DfracDiscarded
| DfracBoth q => Some DfracDiscarded
end.
(** When elements are combined, ownership is added together and knowledge of
discarded fractions is preserved. *)
Local Instance dfrac_op_instance : Op dfrac := λ dq dp,
match dq, dp with
| DfracOwn q, DfracOwn q' => DfracOwn (q + q')
| DfracOwn q, DfracDiscarded => DfracBoth q
| DfracOwn q, DfracBoth q' => DfracBoth (q + q')
| DfracDiscarded, DfracOwn q' => DfracBoth q'
| DfracDiscarded, DfracDiscarded => DfracDiscarded
| DfracDiscarded, DfracBoth q' => DfracBoth q'
| DfracBoth q, DfracOwn q' => DfracBoth (q + q')
| DfracBoth q, DfracDiscarded => DfracBoth q
| DfracBoth q, DfracBoth q' => DfracBoth (q + q')
end.
Lemma dfrac_valid dq :
dq match dq with
| DfracOwn q => q 1
| DfracDiscarded => True
| DfracBoth q => q < 1
end%Qp.
Proof. done. Qed.
Lemma dfrac_op_own q p : DfracOwn p DfracOwn q = DfracOwn (p + q).
Proof. done. Qed.
Lemma dfrac_op_discarded :
DfracDiscarded DfracDiscarded = DfracDiscarded.
Proof. done. Qed.
Lemma dfrac_own_included q p : DfracOwn q DfracOwn p (q < p)%Qp.
Proof.
rewrite Qp.lt_sum. split.
- rewrite /included /op /dfrac_op_instance. intros [[o| |?] [= ->]]. by exists o.
- intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
Qed.
(* [dfrac] does not have a unit so reflexivity is not for granted! *)
Lemma dfrac_discarded_included :
DfracDiscarded DfracDiscarded.
Proof. exists DfracDiscarded. done. Qed.
Definition dfrac_ra_mixin : RAMixin dfrac.
Proof.
split; try apply _.
- intros [?| |?] ? dq <-; intros [= <-]; eexists _; done.
- intros [?| |?] [?| |?] [?| |?];
rewrite /op /dfrac_op_instance 1?assoc_L 1?assoc_L; done.
- intros [?| |?] [?| |?];
rewrite /op /dfrac_op_instance 1?(comm_L Qp.add); done.
- intros [?| |?] dq; rewrite /pcore /dfrac_pcore_instance; intros [= <-];
rewrite /op /dfrac_op_instance; done.
- intros [?| |?] ? [= <-]; done.
- intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
apply dfrac_discarded_included.
- intros [q| |q] [q'| |q']; rewrite /op /dfrac_op_instance /valid /dfrac_valid_instance //.
+ intros. trans (q + q')%Qp; [|done]. apply Qp.le_add_l.
+ apply Qp.lt_le_incl.
+ intros. trans (q + q')%Qp; [|by apply Qp.lt_le_incl]. apply Qp.le_add_l.
+ intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
+ intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
Qed.
Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.
Global Instance dfrac_cmra_discrete : CmraDiscrete dfracR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance dfrac_full_exclusive : Exclusive (DfracOwn 1).
Proof.
intros [q| |q];
rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid //=.
- apply Qp.not_add_le_l.
- move=> /Qp.lt_le_incl. apply Qp.not_add_le_l.
Qed.
Global Instance dfrac_cancelable q : Cancelable (DfracOwn q).
Proof.
apply: discrete_cancelable.
intros [q1| |q1][q2| |q2] _ [=]; simplify_eq/=; try done.
- by destruct (Qp.add_id_free q q2).
- by destruct (Qp.add_id_free q q1).
Qed.
Global Instance dfrac_own_id_free q : IdFree (DfracOwn q).
Proof. intros [q'| |q'] _ [=]. by apply (Qp.add_id_free q q'). Qed.
Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
Proof. by constructor. Qed.
Lemma dfrac_valid_own p : DfracOwn p (p 1)%Qp.
Proof. done. Qed.
Lemma dfrac_valid_own_1 : DfracOwn 1.
Proof. done. Qed.
Lemma dfrac_valid_own_r dq q : (dq DfracOwn q) (q < 1)%Qp.
Proof.
destruct dq as [q'| |q']; [|done|].
- apply Qp.lt_le_trans, Qp.lt_add_r.
- intro Hlt. etrans; last apply Hlt. apply Qp.lt_add_r.
Qed.
Lemma dfrac_valid_own_l dq q : (DfracOwn q dq) (q < 1)%Qp.
Proof using SI. rewrite comm. apply dfrac_valid_own_r. Qed.
Lemma dfrac_valid_discarded : DfracDiscarded.
Proof. done. Qed.
Lemma dfrac_valid_own_discarded q :
(DfracOwn q DfracDiscarded) (q < 1)%Qp.
Proof. done. Qed.
Global Instance dfrac_is_op q q1 q2 :
IsOp q q1 q2
IsOp' (DfracOwn q) (DfracOwn q1) (DfracOwn q2).
Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.
(** Discarding a fraction is a frame preserving update. *)
Lemma dfrac_discard_update dq : dq ~~> DfracDiscarded.
Proof.
intros n [[q'| |q']|]; rewrite -!cmra_discrete_valid_iff //=.
- apply dfrac_valid_own_r.
- apply cmra_valid_op_r.
Qed.
Lemma dfrac_undiscard_update : DfracDiscarded ~~>: λ k, q, k = DfracOwn q.
Proof.
apply cmra_discrete_updateP. intros [[q'| |q']|].
- intros [qd Hqd]%Qp.lt_sum. exists (DfracOwn (qd/2)%Qp).
split; first by eexists. apply dfrac_valid_own.
rewrite Hqd Qp.add_comm -Qp.add_le_mono_l.
by apply Qp.div_le.
- intros _. exists (DfracOwn (1/2)); split; first by eexists.
by apply dfrac_valid_own_discarded.
- intros [qd Hqd]%Qp.lt_sum. exists (DfracOwn (qd/2)%Qp).
split; first by eexists. rewrite /= /op /valid /cmra_op /cmra_valid /=.
rewrite Hqd Qp.add_comm -Qp.add_lt_mono_l.
by apply Qp.div_lt.
- intros _. exists (DfracOwn 1); split; first by eexists.
by apply dfrac_valid_own.
Qed.
End dfrac.
From iris.algebra Require Export gmap coPset local_updates.
From iris.algebra Require Import reservation_map updates proofmode_classes.
From iris.prelude Require Import options.
(** The camera [dyn_reservation_map A] over a camera [A] extends [gmap positive
A] with a notion of "reservation tokens" for a (potentially infinite) set [E :
coPset] which represent the right to allocate a map entry at any position [k ∈
E]. Unlike [reservation_map], [dyn_reservation_map] supports dynamically
allocating these tokens, including infinite sets of them. This is useful when
syncing the keys of this map with another API that dynamically allocates names:
we can first reserve a fresh infinite set [E] of tokens here, then allocate a
new name *in [E]* with the other API (assuming it offers the usual "allocate a
fresh name in an infinite set" API), and then use our tokens to allocate the
same name here. In effect, we have performed synchronized allocation of the
same name across two maps, without the other API having to have dedicated
support for this.
The key connectives are [dyn_reservation_map_data k a] (the "points-to"
assertion of this map), which associates data [a : A] with a key [k : positive],
and [dyn_reservation_map_token E] (the reservation token), which says
that no data has been associated with the indices in the mask [E]. The important
properties of this camera are:
- The lemma [dyn_reservation_map_reserve] provides a frame-preserving update to
obtain ownership of [dyn_reservation_map_token E] for some fresh infinite [E].
- The lemma [dyn_reservation_map_alloc] provides a frame preserving update to
associate data to a key: [dyn_reservation_map_token E ~~> dyn_reservation_map_data k a]
provided [k ∈ E] and [✓ a].
In the future, it could be interesting to generalize this map to arbitrary key
types instead of hard-coding [positive]. *)
Record dyn_reservation_map (A : Type) := DynReservationMap {
dyn_reservation_map_data_proj : gmap positive A;
dyn_reservation_map_token_proj : coPset_disj
}.
Add Printing Constructor dyn_reservation_map.
Global Arguments DynReservationMap {_} _ _.
Global Arguments dyn_reservation_map_data_proj {_} _.
Global Arguments dyn_reservation_map_token_proj {_} _.
Global Instance: Params (@DynReservationMap) 1 := {}.
Global Instance: Params (@dyn_reservation_map_data_proj) 1 := {}.
Global Instance: Params (@dyn_reservation_map_token_proj) 1 := {}.
Definition dyn_reservation_map_data {SI : sidx} {A : cmra}
(k : positive) (a : A) : dyn_reservation_map A :=
DynReservationMap {[ k := a ]} ε.
Definition dyn_reservation_map_token {SI : sidx} {A : cmra}
(E : coPset) : dyn_reservation_map A :=
DynReservationMap (CoPset E).
Global Instance: Params (@dyn_reservation_map_data) 3 := {}.
(** We consruct the OFE and CMRA structure via an isomorphism with
[reservation_map]. *)
Section ofe.
Context {SI : sidx} {A : ofe}.
Implicit Types x y : dyn_reservation_map A.
Local Definition to_reservation_map x : reservation_map A :=
ReservationMap (dyn_reservation_map_data_proj x) (dyn_reservation_map_token_proj x).
Local Definition from_reservation_map (x : reservation_map A) : dyn_reservation_map A :=
DynReservationMap (reservation_map_data_proj x) (reservation_map_token_proj x).
Local Instance dyn_reservation_map_equiv : Equiv (dyn_reservation_map A) := λ x y,
dyn_reservation_map_data_proj x dyn_reservation_map_data_proj y
dyn_reservation_map_token_proj x = dyn_reservation_map_token_proj y.
Local Instance dyn_reservation_map_dist : Dist (dyn_reservation_map A) := λ n x y,
dyn_reservation_map_data_proj x {n} dyn_reservation_map_data_proj y
dyn_reservation_map_token_proj x = dyn_reservation_map_token_proj y.
Global Instance DynReservationMap_ne :
NonExpansive2 (@DynReservationMap A).
Proof. by split. Qed.
Global Instance DynReservationMap_proper :
Proper (() ==> (=) ==> ()) (@DynReservationMap A).
Proof. by split. Qed.
Global Instance dyn_reservation_map_data_proj_ne :
NonExpansive (@dyn_reservation_map_data_proj A).
Proof. by destruct 1. Qed.
Global Instance dyn_reservation_map_data_proj_proper :
Proper (() ==> ()) (@dyn_reservation_map_data_proj A).
Proof. by destruct 1. Qed.
Definition dyn_reservation_map_ofe_mixin : OfeMixin (dyn_reservation_map A).
Proof.
by apply (iso_ofe_mixin to_reservation_map).
Qed.
Canonical Structure dyn_reservation_mapO :=
Ofe (dyn_reservation_map A) dyn_reservation_map_ofe_mixin.
Global Instance DynReservationMap_discrete a b :
Discrete a Discrete b Discrete (DynReservationMap a b).
Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete_0. Qed.
Global Instance dyn_reservation_map_ofe_discrete :
OfeDiscrete A OfeDiscrete dyn_reservation_mapO.
Proof. intros ? [??]; apply _. Qed.
End ofe.
Global Arguments dyn_reservation_mapO {_} _.
Section cmra.
Context {SI : sidx} {A : cmra}.
Implicit Types a b : A.
Implicit Types x y : dyn_reservation_map A.
Implicit Types k : positive.
Global Instance dyn_reservation_map_data_ne i :
NonExpansive (@dyn_reservation_map_data SI A i).
Proof. intros ? ???. rewrite /dyn_reservation_map_data. solve_proper. Qed.
Global Instance dyn_reservation_map_data_proper N :
Proper (() ==> ()) (@dyn_reservation_map_data SI A N).
Proof. solve_proper. Qed.
Global Instance dyn_reservation_map_data_discrete N a :
Discrete a Discrete (dyn_reservation_map_data N a).
Proof. intros. apply DynReservationMap_discrete; apply _. Qed.
Global Instance dyn_reservation_map_token_discrete E :
Discrete (@dyn_reservation_map_token SI A E).
Proof. intros. apply DynReservationMap_discrete; apply _. Qed.
Local Instance dyn_reservation_map_valid_instance : Valid (dyn_reservation_map A) := λ x,
match dyn_reservation_map_token_proj x with
| CoPset E =>
(dyn_reservation_map_data_proj x) set_infinite ( E)
(* dom (dyn_reservation_map_data_proj x) ⊥ E *)
( i, dyn_reservation_map_data_proj x !! i = None i E)
| CoPsetInvalid => False
end.
Global Arguments dyn_reservation_map_valid_instance !_ /.
Local Instance dyn_reservation_map_validN_instance : ValidN (dyn_reservation_map A) := λ n x,
match dyn_reservation_map_token_proj x with
| CoPset E =>
{n} (dyn_reservation_map_data_proj x) set_infinite ( E)
(* dom (dyn_reservation_map_data_proj x) ⊥ E *)
( i, dyn_reservation_map_data_proj x !! i = None i E)
| CoPsetInvalid => False
end.
Global Arguments dyn_reservation_map_validN_instance !_ /.
Local Instance dyn_reservation_map_pcore_instance : PCore (dyn_reservation_map A) := λ x,
Some (DynReservationMap (core (dyn_reservation_map_data_proj x)) ε).
Local Instance dyn_reservation_map_op_instance : Op (dyn_reservation_map A) := λ x y,
DynReservationMap (dyn_reservation_map_data_proj x dyn_reservation_map_data_proj y)
(dyn_reservation_map_token_proj x dyn_reservation_map_token_proj y).
Definition dyn_reservation_map_valid_eq :
valid = λ x, match dyn_reservation_map_token_proj x with
| CoPset E =>
(dyn_reservation_map_data_proj x) set_infinite ( E)
(* dom (dyn_reservation_map_data_proj x) ⊥ E *)
i, dyn_reservation_map_data_proj x !! i = None i E
| CoPsetInvalid => False
end := eq_refl _.
Definition dyn_reservation_map_validN_eq :
validN = λ n x, match dyn_reservation_map_token_proj x with
| CoPset E =>
{n} (dyn_reservation_map_data_proj x) set_infinite ( E)
(* dom (dyn_reservation_map_data_proj x) ⊥ E *)
i, dyn_reservation_map_data_proj x !! i = None i E
| CoPsetInvalid => False
end := eq_refl _.
Lemma dyn_reservation_map_included x y :
x y
dyn_reservation_map_data_proj x dyn_reservation_map_data_proj y
dyn_reservation_map_token_proj x dyn_reservation_map_token_proj y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (DynReservationMap z1 z2); split; auto.
Qed.
Lemma dyn_reservation_map_data_proj_validN n x : {n} x {n} dyn_reservation_map_data_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
Lemma dyn_reservation_map_token_proj_validN n x : {n} x {n} dyn_reservation_map_token_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
Lemma dyn_reservation_map_cmra_mixin : CmraMixin (dyn_reservation_map A).
Proof.
apply (iso_cmra_mixin_restrict_validity from_reservation_map to_reservation_map); try done.
- intros n [m [E|]];
rewrite dyn_reservation_map_validN_eq reservation_map_validN_eq /=;
naive_solver.
- intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[?[??]]; split; simplify_eq/=.
+ by rewrite -Hm.
+ split; first done. intros i. by rewrite -(dist_None n) -Hm dist_None.
- pose 0.
intros [m [E|]]; rewrite dyn_reservation_map_valid_eq
dyn_reservation_map_validN_eq /= ?cmra_valid_validN; naive_solver.
- intros n m [r [E|]]; rewrite dyn_reservation_map_validN_eq /=;
naive_solver eauto using cmra_validN_le.
- intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite dyn_reservation_map_validN_eq /=.
rewrite {1}/op /cmra_op /=. case_decide; last done.
intros [Hm [Hinf Hdisj]]; split; first by eauto using cmra_validN_op_l.
split.
+ rewrite ->difference_union_distr_r_L in Hinf.
eapply set_infinite_subseteq, Hinf. set_solver.
+ intros i. move: (Hdisj i). rewrite lookup_op.
case: (m1 !! i); case: (m2 !! i); set_solver.
Qed.
Canonical Structure dyn_reservation_mapR :=
Cmra (dyn_reservation_map A) dyn_reservation_map_cmra_mixin.
Global Instance dyn_reservation_map_cmra_discrete :
CmraDiscrete A CmraDiscrete dyn_reservation_mapR.
Proof.
split; first apply _.
intros [m [E|]]; rewrite dyn_reservation_map_validN_eq dyn_reservation_map_valid_eq //=.
by intros [?%cmra_discrete_valid ?].
Qed.
Local Instance dyn_reservation_map_empty_instance : Unit (dyn_reservation_map A) :=
DynReservationMap ε ε.
Lemma dyn_reservation_map_ucmra_mixin : UcmraMixin (dyn_reservation_map A).
Proof.
split; simpl.
- rewrite dyn_reservation_map_valid_eq /=. split; [apply ucmra_unit_valid|]. split.
+ rewrite difference_empty_L. apply top_infinite.
+ set_solver.
- split; simpl; [by rewrite left_id|by rewrite left_id_L].
- do 2 constructor; [apply (core_id_core _)|done].
Qed.
Canonical Structure dyn_reservation_mapUR :=
Ucmra (dyn_reservation_map A) dyn_reservation_map_ucmra_mixin.
Global Instance dyn_reservation_map_data_core_id k a :
CoreId a CoreId (dyn_reservation_map_data k a).
Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
Lemma dyn_reservation_map_data_valid k a :
(dyn_reservation_map_data k a) a.
Proof.
rewrite dyn_reservation_map_valid_eq /= singleton_valid.
split; first naive_solver. intros Ha.
split; first done. split; last set_solver.
rewrite difference_empty_L. apply top_infinite.
Qed.
Lemma dyn_reservation_map_token_valid E :
(dyn_reservation_map_token E) set_infinite ( E).
Proof.
rewrite dyn_reservation_map_valid_eq /=. split; first naive_solver.
intros Hinf. do 2 (split; first done). by left.
Qed.
Lemma dyn_reservation_map_data_op k a b :
dyn_reservation_map_data k (a b) = dyn_reservation_map_data k a dyn_reservation_map_data k b.
Proof.
by rewrite {2}/op /dyn_reservation_map_op_instance
/dyn_reservation_map_data /= singleton_op left_id_L.
Qed.
Lemma dyn_reservation_map_data_mono k a b :
a b dyn_reservation_map_data k a dyn_reservation_map_data k b.
Proof. intros [c ->]. by rewrite dyn_reservation_map_data_op. Qed.
Global Instance dyn_reservation_map_data_is_op k a b1 b2 :
IsOp a b1 b2
IsOp' (dyn_reservation_map_data k a) (dyn_reservation_map_data k b1) (dyn_reservation_map_data k b2).
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite dyn_reservation_map_data_op. Qed.
Lemma dyn_reservation_map_token_union E1 E2 :
E1 ## E2
dyn_reservation_map_token (E1 E2) = dyn_reservation_map_token E1 dyn_reservation_map_token E2.
Proof.
intros. by rewrite /op /dyn_reservation_map_op_instance
/dyn_reservation_map_token /= coPset_disj_union // left_id_L.
Qed.
Lemma dyn_reservation_map_token_difference E1 E2 :
E1 E2
dyn_reservation_map_token E2 = dyn_reservation_map_token E1 dyn_reservation_map_token (E2 E1).
Proof.
intros. rewrite -dyn_reservation_map_token_union; last set_solver.
by rewrite -union_difference_L.
Qed.
Lemma dyn_reservation_map_token_valid_op E1 E2 :
(dyn_reservation_map_token E1 dyn_reservation_map_token E2)
E1 ## E2 set_infinite ( (E1 E2)).
Proof.
split.
- rewrite dyn_reservation_map_valid_eq /= {1}/op /cmra_op /=. case_decide; last done.
naive_solver.
- intros [Hdisj Hinf]. rewrite -dyn_reservation_map_token_union //.
apply dyn_reservation_map_token_valid. done.
Qed.
Lemma dyn_reservation_map_reserve (Q : dyn_reservation_map A Prop) :
( E, set_infinite E Q (dyn_reservation_map_token E))
ε ~~>: Q.
Proof.
intros HQ. apply cmra_total_updateP=> n [mf [Ef|]];
rewrite left_id {1}dyn_reservation_map_validN_eq /=; last done.
intros [Hmap [Hinf Hdisj]].
(* Pick a fresh set disjoint from the existing tokens [Ef] and map [mf],
such that both that set [E1] and the remainder [E2] are infinite. *)
edestruct (coPset_split_infinite ( (Ef (gset_to_coPset $ dom mf)))) as
(E1 & E2 & HEunion & HEdisj & HE1inf & HE2inf).
{ rewrite -difference_difference_l_L.
by apply difference_infinite, gset_to_coPset_finite. }
exists (dyn_reservation_map_token E1).
split; first by apply HQ. clear HQ.
rewrite dyn_reservation_map_validN_eq /=.
rewrite coPset_disj_union; last set_solver.
split; first by rewrite left_id_L. split.
- eapply set_infinite_subseteq, HE2inf. set_solver.
- intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left.
destruct (mf !! i) as [p|] eqn:Hp; last by left.
apply elem_of_dom_2, elem_of_gset_to_coPset in Hp. right. set_solver.
Qed.
Lemma dyn_reservation_map_reserve' :
ε ~~>: λ x, E, set_infinite E x = dyn_reservation_map_token E.
Proof. eauto using dyn_reservation_map_reserve. Qed.
Lemma dyn_reservation_map_alloc E k a :
k E a dyn_reservation_map_token E ~~> dyn_reservation_map_data k a.
Proof.
intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
rewrite dyn_reservation_map_validN_eq /= {1}/op {1}/cmra_op /=.
case_decide; last done.
rewrite !left_id_L. intros [Hmf [Hinf Hdisj]]; split; last split.
- destruct (Hdisj k) as [Hmfi|]; last set_solver.
intros j. rewrite lookup_op.
destruct (decide (k = j)) as [<-|].
+ rewrite Hmfi lookup_singleton right_id_L. by apply cmra_valid_validN.
+ by rewrite lookup_singleton_ne // left_id_L.
- eapply set_infinite_subseteq, Hinf. set_solver.
- intros j. destruct (decide (k = j)); first set_solver.
rewrite lookup_op lookup_singleton_ne //.
destruct (Hdisj j) as [Hmfi|?]; last set_solver. rewrite Hmfi; auto.
Qed.
Lemma dyn_reservation_map_updateP P (Q : dyn_reservation_map A Prop) k a :
a ~~>: P
( a', P a' Q (dyn_reservation_map_data k a'))
dyn_reservation_map_data k a ~~>: Q.
Proof.
intros Hup HP. apply cmra_total_updateP=> n [mf [Ef|]] //.
rewrite dyn_reservation_map_validN_eq /= left_id_L. intros [Hmf [Hinf Hdisj]].
destruct (Hup n (mf !! k)) as (a'&?&?).
{ move: (Hmf (k)).
by rewrite lookup_op lookup_singleton Some_op_opM. }
exists (dyn_reservation_map_data k a'); split; first by eauto.
rewrite /= left_id_L. split; last split.
- intros j. destruct (decide (k = j)) as [<-|].
+ by rewrite lookup_op lookup_singleton Some_op_opM.
+ rewrite lookup_op lookup_singleton_ne // left_id_L.
move: (Hmf j). rewrite lookup_op. eauto using cmra_validN_op_r.
- done.
- intros j. move: (Hdisj j).
rewrite !lookup_op !op_None !lookup_singleton_None. naive_solver.
Qed.
Lemma dyn_reservation_map_update k a b :
a ~~> b
dyn_reservation_map_data k a ~~> dyn_reservation_map_data k b.
Proof.
rewrite !cmra_update_updateP. eauto using dyn_reservation_map_updateP with subst.
Qed.
End cmra.
Global Arguments dyn_reservation_mapR {_} _.
Global Arguments dyn_reservation_mapUR {_} _.
From iris.algebra Require Export cmra. From iris.algebra Require Export cmra.
From iris.algebra Require Import upred. From iris.prelude Require Import options.
Local Arguments validN _ _ _ !_ /.
Local Arguments validN _ _ _ _ !_ /.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
Inductive excl (A : Type) := Inductive excl (A : Type) :=
| Excl : A excl A | Excl : A excl A
| ExclBot : excl A. | ExclInvalid : excl A.
Arguments Excl {_} _. Global Arguments Excl {_} _.
Arguments ExclBot {_}. Global Arguments ExclInvalid {_}.
Global Instance: Params (@Excl) 1 := {}.
Global Instance: Params (@ExclInvalid) 1 := {}.
Notation excl' A := (option (excl A)).
Notation Excl' x := (Some (Excl x)). Notation Excl' x := (Some (Excl x)).
Notation ExclBot' := (Some ExclBot). Notation ExclInvalid' := (Some ExclInvalid).
Instance maybe_Excl {A} : Maybe (@Excl A) := λ x, Global Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
match x with Excl a => Some a | _ => None end. match x with Excl a => Some a | _ => None end.
Section excl. Section excl.
Context {A : cofeT}. Context {SI : sidx} {A : ofe}.
Implicit Types a b : A. Implicit Types a b : A.
Implicit Types x y : excl A. Implicit Types x y : excl A.
(* Cofe *) (* Cofe *)
Inductive excl_equiv : Equiv (excl A) := Inductive excl_equiv : Equiv (excl A) :=
| Excl_equiv a b : a b Excl a Excl b | Excl_equiv a b : a b Excl a Excl b
| ExclBot_equiv : ExclBot ExclBot. | ExclInvalid_equiv : ExclInvalid ExclInvalid.
Existing Instance excl_equiv. Local Existing Instance excl_equiv.
Inductive excl_dist : Dist (excl A) := Inductive excl_dist : Dist (excl A) :=
| Excl_dist a b n : a {n} b Excl a {n} Excl b | Excl_dist a b n : a {n} b Excl a {n} Excl b
| ExclBot_dist n : ExclBot {n} ExclBot. | ExclInvalid_dist n : ExclInvalid {n} ExclInvalid.
Existing Instance excl_dist. Local Existing Instance excl_dist.
Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A). Global Instance Excl_ne : NonExpansive (@Excl A).
Proof. by constructor. Qed. Proof. by constructor. Qed.
Global Instance Excl_proper : Proper (() ==> ()) (@Excl A). Global Instance Excl_proper : Proper (() ==> ()) (@Excl A).
Proof. by constructor. Qed. Proof. by constructor. Qed.
...@@ -39,80 +44,68 @@ Proof. by inversion_clear 1. Qed. ...@@ -39,80 +44,68 @@ Proof. by inversion_clear 1. Qed.
Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A). Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
Proof. by inversion_clear 1. Qed. Proof. by inversion_clear 1. Qed.
Program Definition excl_chain (c : chain (excl A)) (a : A) : chain A := Definition excl_ofe_mixin : OfeMixin (excl A).
{| chain_car n := match c n return _ with Excl y => y | _ => a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Instance excl_compl : Compl (excl A) := λ c,
match c 0 with Excl a => Excl (compl (excl_chain c a)) | x => x end.
Definition excl_cofe_mixin : CofeMixin (excl A).
Proof. Proof.
split. apply (iso_ofe_mixin (maybe Excl)).
- intros x y; split; [by destruct 1; constructor; apply equiv_dist|]. - by intros [a|] [b|]; split; inversion_clear 1; constructor.
intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist. - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
by intros n; feed inversion (Hxy n). Qed.
- intros n; split. Canonical Structure exclO : ofe := Ofe (excl A) excl_ofe_mixin.
+ by intros []; constructor.
+ by destruct 1; constructor. Global Instance excl_cofe `{!Cofe A} : Cofe exclO.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto. Proof.
- by inversion_clear 1; constructor; apply dist_S. apply (iso_cofe (from_option Excl ExclInvalid) (maybe Excl)).
- intros n c; rewrite /compl /excl_compl. - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. - by intros []; constructor.
rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
Qed. Qed.
Canonical Structure exclC : cofeT := CofeT (excl A) excl_cofe_mixin.
Global Instance excl_discrete : Discrete A Discrete exclC. Global Instance excl_ofe_discrete : OfeDiscrete A OfeDiscrete exclO.
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A LeibnizEquiv (excl A). Global Instance excl_leibniz : LeibnizEquiv A LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed. Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
Global Instance Excl_timeless a : Timeless a Timeless (Excl a). Global Instance Excl_discrete a : Discrete a Discrete (Excl a).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
Global Instance ExclBot_timeless : Timeless (@ExclBot A). Global Instance ExclInvalid_discrete : Discrete (@ExclInvalid A).
Proof. by inversion_clear 1; constructor. Qed. Proof. by inversion_clear 1; constructor. Qed.
(* CMRA *) (* CMRA *)
Instance excl_valid : Valid (excl A) := λ x, Local Instance excl_valid_instance : Valid (excl A) := λ x,
match x with Excl _ => True | ExclBot => False end. match x with Excl _ => True | ExclInvalid => False end.
Instance excl_validN : ValidN (excl A) := λ n x, Local Instance excl_validN_instance : ValidN (excl A) := λ n x,
match x with Excl _ => True | ExclBot => False end. match x with Excl _ => True | ExclInvalid => False end.
Instance excl_pcore : PCore (excl A) := λ _, None. Local Instance excl_pcore_instance : PCore (excl A) := λ _, None.
Instance excl_op : Op (excl A) := λ x y, ExclBot. Local Instance excl_op_instance : Op (excl A) := λ x y, ExclInvalid.
Lemma excl_cmra_mixin : CMRAMixin (excl A). Lemma excl_cmra_mixin : CmraMixin (excl A).
Proof. Proof.
split; try discriminate. split; try discriminate.
- by intros n []; destruct 1; constructor. - by intros [] n; destruct 1; constructor.
- by destruct 1; intros ?. - by destruct 1; intros ?.
- intros x; split. done. by move=> /(_ 0). - intros x; split; [done|]. by move=> /(_ 0).
- intros n [?|]; simpl; auto with lia. - intros n m [?|]; simpl; auto.
- by intros [?|] [?|] [?|]; constructor. - by intros [?|] [?|] [?|]; constructor.
- by intros [?|] [?|]; constructor. - by intros [?|] [?|]; constructor.
- by intros n [?|] [?|]. - by intros n [?|] [?|].
- intros n x y1 y2 ? Hx. - intros n x [?|] [?|] ? Hx; eexists _, _; inversion_clear Hx; eauto.
by exists match y1, y2 with
| Excl a1, Excl a2 => (Excl a1, Excl a2)
| ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
Qed. Qed.
Canonical Structure exclR := Canonical Structure exclR := Cmra (excl A) excl_cmra_mixin.
CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
Global Instance excl_cmra_discrete : OfeDiscrete A CmraDiscrete exclR.
Global Instance excl_cmra_discrete : Discrete A CMRADiscrete exclR. Proof. split; first apply _. by intros []. Qed.
Proof. split. apply _. by intros []. Qed.
Lemma excl_included x y : x y y = ExclInvalid.
(** Internalized properties *)
Lemma excl_equivI {M} (x y : excl A) :
x y ⊣⊢ (match x, y with
| Excl a, Excl b => a b
| ExclBot, ExclBot => True
| _, _ => False
end : uPred M).
Proof. Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor. split.
- destruct x, y; intros [[] Hxy]; by inv Hxy.
- intros ->. by exists ExclInvalid.
Qed.
Lemma excl_includedN n x y : x {n} y y = ExclInvalid.
Proof.
split.
- destruct x, y; intros [[] Hxy]; by inv Hxy.
- intros ->. by exists ExclInvalid.
Qed. Qed.
Lemma excl_validI {M} (x : excl A) :
x ⊣⊢ (if x is ExclBot then False else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** Exclusive *) (** Exclusive *)
Global Instance excl_exclusive x : Exclusive x. Global Instance excl_exclusive x : Exclusive x.
...@@ -123,61 +116,70 @@ Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None. ...@@ -123,61 +116,70 @@ Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None.
Proof. by destruct mx. Qed. Proof. by destruct mx. Qed.
Lemma excl_validN_inv_r n mx a : {n} (mx Excl' a) mx = None. Lemma excl_validN_inv_r n mx a : {n} (mx Excl' a) mx = None.
Proof. by destruct mx. Qed. Proof. by destruct mx. Qed.
Lemma Excl_includedN n a mx : {n} mx Excl' a {n} mx mx {n} Excl' a.
Lemma Excl_includedN n a b : Excl' a {n} Excl' b a {n} b.
Proof. Proof.
intros Hvalid; split; [|by intros ->]. split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a).
Qed. Qed.
Lemma Excl_included a b : Excl' a Excl' b a b.
Proof.
split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
Qed.
Lemma ExclInvalid_included ea : ea ExclInvalid.
Proof. by exists ExclInvalid. Qed.
End excl. End excl.
Arguments exclC : clear implicits. (* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
Arguments exclR : clear implicits. the new unification algorithm. The old unification algorithm sometimes gets
confused by going from [ucmra]'s to [cmra]'s and back. *)
Global Hint Extern 0 (_ ExclInvalid) => apply: ExclInvalid_included : core.
Global Arguments exclO {_} _.
Global Arguments exclR {_} _.
(* Functor *) (* Functor *)
Definition excl_map {A B} (f : A B) (x : excl A) : excl B := Definition excl_map {A B} (f : A B) (x : excl A) : excl B :=
match x with Excl a => Excl (f a) | ExclBot => ExclBot end. match x with Excl a => Excl (f a) | ExclInvalid => ExclInvalid end.
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x. Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
Proof. by destruct x. Qed. Proof. by destruct x. Qed.
Lemma excl_map_compose {A B C} (f : A B) (g : B C) (x : excl A) : Lemma excl_map_compose {A B C} (f : A B) (g : B C) (x : excl A) :
excl_map (g f) x = excl_map g (excl_map f x). excl_map (g f) x = excl_map g (excl_map f x).
Proof. by destruct x. Qed. Proof. by destruct x. Qed.
Lemma excl_map_ext {A B : cofeT} (f g : A B) x : Lemma excl_map_ext {SI : sidx} {A B : ofe} (f g : A B) x :
( x, f x g x) excl_map f x excl_map g x. ( x, f x g x) excl_map f x excl_map g x.
Proof. by destruct x; constructor. Qed. Proof. by destruct x; constructor. Qed.
Instance excl_map_ne {A B : cofeT} n : Global Instance excl_map_ne {SI : sidx} {A B : ofe} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B). Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed. Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
Instance excl_map_cmra_monotone {A B : cofeT} (f : A B) : Global Instance excl_map_cmra_morphism {SI : sidx} {A B : ofe} (f : A B) :
( n, Proper (dist n ==> dist n) f) CMRAMonotone (excl_map f). NonExpansive f CmraMorphism (excl_map f).
Proof. Proof. split; try done; try apply _. by intros n [a|]. Qed.
split; try apply _. Definition exclO_map {SI : sidx} {A B} (f : A -n> B) : exclO A -n> exclO B :=
- by intros n [a|]. OfeMor (excl_map f).
- intros x y [z Hy]; exists (excl_map f z); apply equiv_dist=> n. Global Instance exclO_map_ne {SI : sidx} A B : NonExpansive (@exclO_map SI A B).
move: Hy=> /equiv_dist /(_ n) ->; by destruct x, z. Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
Qed.
Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B := Program Definition exclRF {SI : sidx} (F : oFunctor) : rFunctor := {|
CofeMor (excl_map f). rFunctor_car A _ B _ := (exclR (oFunctor_car F A B));
Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B). rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclO_map (oFunctor_map F fg)
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
Program Definition exclRF (F : cFunctor) : rFunctor := {|
rFunctor_car A B := (exclR (cFunctor_car F A B));
rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
|}. |}.
Next Obligation. Next Obligation.
intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne. intros ? F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??.
by apply exclO_map_ne, oFunctor_map_ne.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A B x; simpl. rewrite -{2}(excl_map_id x). intros ? F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
apply excl_map_ext=>y. by rewrite cFunctor_id. apply excl_map_ext=>y. by rewrite oFunctor_map_id.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -excl_map_compose. intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl.
apply excl_map_ext=>y; apply cFunctor_compose. rewrite -excl_map_compose.
apply excl_map_ext=>y; apply oFunctor_map_compose.
Qed. Qed.
Instance exclRF_contractive F : Global Instance exclRF_contractive {SI : sidx} F :
cFunctorContractive F rFunctorContractive (exclRF F). oFunctorContractive F rFunctorContractive (exclRF F).
Proof. Proof.
intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive. intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??.
by apply exclO_map_ne, oFunctor_map_contractive.
Qed. Qed.
(** This file provides a version of the fractional camera whose elements are
in the internal (0,1] of the rational numbers.
Notice that this camera could in principle be obtained by restricting the
validity of the unbounded fractional camera [ufrac]. *)
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes.
From iris.prelude Require Import options.
(** Since the standard (0,1] fractional camera is used more often, we define
[frac] through a [Notation] instead of a [Definition]. That way, Coq infers the
[frac] camera by default when using the [Qp] type. *)
Notation frac := Qp (only parsing).
Section frac.
Context {SI : sidx}.
Canonical Structure fracO := leibnizO frac.
Local Instance frac_valid_instance : Valid frac := λ x, (x 1)%Qp.
Local Instance frac_pcore_instance : PCore frac := λ _, None.
Local Instance frac_op_instance : Op frac := λ x y, (x + y)%Qp.
Lemma frac_valid p : p (p 1)%Qp.
Proof. done. Qed.
Lemma frac_valid_1 : 1%Qp.
Proof. done. Qed.
Lemma frac_op p q : p q = (p + q)%Qp.
Proof. done. Qed.
Lemma frac_included p q : p q (p < q)%Qp.
Proof. by rewrite Qp.lt_sum. Qed.
Corollary frac_included_weak p q : p q (p q)%Qp.
Proof. rewrite frac_included. apply Qp.lt_le_incl. Qed.
Definition frac_ra_mixin : RAMixin frac.
Proof.
split; try apply _; try done.
intros p q. rewrite !frac_valid frac_op=> ?.
trans (p + q)%Qp; last done. apply Qp.le_add_l.
Qed.
Canonical Structure fracR := discreteR frac frac_ra_mixin.
Global Instance frac_cmra_discrete : CmraDiscrete fracR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance frac_full_exclusive : Exclusive 1%Qp.
Proof. intros p. apply Qp.not_add_le_l. Qed.
Global Instance frac_cancelable (q : frac) : Cancelable q.
Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.
Global Instance frac_id_free (q : frac) : IdFree q.
Proof. intros p _. apply Qp.add_id_free. Qed.
(* This one has a higher precendence than [is_op_op] so we get a [+] instead
of an [⋅]. *)
Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
Proof. done. Qed.
Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp frac_op Qp.div_2. Qed.
End frac.
From stdpp Require Import finite.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
From iris.prelude Require Import options.
Definition discrete_fun_insert {SI : sidx} `{!EqDecision A} {B : A ofe}
(x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x',
match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
Global Instance: Params (@discrete_fun_insert) 6 := {}.
Definition discrete_fun_singleton {SI : sidx} `{!EqDecision A} {B : A ucmra}
(x : A) (y : B x) : discrete_fun B := discrete_fun_insert x y ε.
Global Instance: Params (@discrete_fun_singleton) 6 := {}.
Section ofe.
Context {SI : sidx} `{!EqDecision A} {B : A ofe}.
Implicit Types x : A.
Implicit Types f g : discrete_fun B.
Global Instance discrete_funO_ofe_discrete :
( i, OfeDiscrete (B i)) OfeDiscrete (discrete_funO B).
Proof. intros HB f f' Heq i. apply HB, Heq. Qed.
(** Properties of discrete_fun_insert. *)
Global Instance discrete_fun_insert_ne x :
NonExpansive2 (discrete_fun_insert (B:=B) x).
Proof.
intros n y1 y2 ? f1 f2 ? x'; rewrite /discrete_fun_insert.
by destruct (decide _) as [[]|].
Qed.
Global Instance discrete_fun_insert_proper x :
Proper (() ==> () ==> ()) (discrete_fun_insert (B:=B) x) := ne_proper_2 _.
Lemma discrete_fun_lookup_insert f x y : (discrete_fun_insert x y f) x = y.
Proof.
rewrite /discrete_fun_insert; destruct (decide _) as [Hx|]; last done.
by rewrite (proof_irrel Hx eq_refl).
Qed.
Lemma discrete_fun_lookup_insert_ne f x x' y :
x x' (discrete_fun_insert x y f) x' = f x'.
Proof. by rewrite /discrete_fun_insert; destruct (decide _). Qed.
Global Instance discrete_fun_insert_discrete f x y :
Discrete f Discrete y Discrete (discrete_fun_insert x y f).
Proof.
intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
- rewrite discrete_fun_lookup_insert.
apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert.
- rewrite discrete_fun_lookup_insert_ne //.
apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert_ne.
Qed.
End ofe.
Section cmra.
Context {SI : sidx} `{!EqDecision A} {B : A ucmra}.
Implicit Types x : A.
Implicit Types f g : discrete_fun B.
Global Instance discrete_funR_cmra_discrete:
( i, CmraDiscrete (B i)) CmraDiscrete (discrete_funR B).
Proof. intros HB. split; [apply _|]. intros x Hv i. apply HB, Hv. Qed.
Global Instance discrete_fun_singleton_ne x :
NonExpansive (discrete_fun_singleton x : B x _).
Proof.
intros n y1 y2 ?; apply discrete_fun_insert_ne; [done|].
by apply equiv_dist.
Qed.
Global Instance discrete_fun_singleton_proper x :
Proper (() ==> ()) (discrete_fun_singleton x) := ne_proper _.
Lemma discrete_fun_lookup_singleton x (y : B x) : (discrete_fun_singleton x y) x = y.
Proof. by rewrite /discrete_fun_singleton discrete_fun_lookup_insert. Qed.
Lemma discrete_fun_lookup_singleton_ne x x' (y : B x) :
x x' (discrete_fun_singleton x y) x' = ε.
Proof. intros; by rewrite /discrete_fun_singleton discrete_fun_lookup_insert_ne. Qed.
Global Instance discrete_fun_singleton_discrete x (y : B x) :
( i, Discrete (ε : B i)) Discrete y Discrete (discrete_fun_singleton x y).
Proof. apply _. Qed.
Lemma discrete_fun_singleton_validN n x (y : B x) : {n} discrete_fun_singleton x y {n} y.
Proof.
split; [by move=>/(_ x); rewrite discrete_fun_lookup_singleton|].
move=>Hx x'; destruct (decide (x = x')) as [->|];
rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne //.
by apply ucmra_unit_validN.
Qed.
Lemma discrete_fun_singleton_valid x (y : B x) : discrete_fun_singleton x y y.
Proof.
by rewrite !cmra_valid_validN; setoid_rewrite discrete_fun_singleton_validN.
Qed.
Lemma discrete_fun_singleton_unit x : discrete_fun_singleton x (ε : B x) ε.
Proof.
move=>x'; destruct (decide (x = x')) as [->|];
by rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne.
Qed.
Lemma discrete_fun_singleton_core x (y : B x) :
core (discrete_fun_singleton x y) discrete_fun_singleton x (core y).
Proof.
move=>x'; destruct (decide (x = x')) as [->|];
by rewrite discrete_fun_lookup_core ?discrete_fun_lookup_singleton
?discrete_fun_lookup_singleton_ne // (core_id_core _).
Qed.
Global Instance discrete_fun_singleton_core_id x (y : B x) :
CoreId y CoreId (discrete_fun_singleton x y).
Proof. by rewrite !core_id_total discrete_fun_singleton_core=> ->. Qed.
Lemma discrete_fun_singleton_op (x : A) (y1 y2 : B x) :
discrete_fun_singleton x y1 discrete_fun_singleton x y2 discrete_fun_singleton x (y1 y2).
Proof.
intros x'; destruct (decide (x' = x)) as [->|].
- by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton.
- by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton_ne // left_id.
Qed.
Lemma discrete_fun_insert_updateP x (P : B x Prop) (Q : discrete_fun B Prop) g y1 :
y1 ~~>: P ( y2, P y2 Q (discrete_fun_insert x y2 g))
discrete_fun_insert x y1 g ~~>: Q.
Proof.
intros Hy1 HP; apply cmra_total_updateP.
intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
{ move: (Hg x). by rewrite discrete_fun_lookup_op discrete_fun_lookup_insert. }
exists (discrete_fun_insert x y2 g); split; [auto|].
intros x'; destruct (decide (x' = x)) as [->|];
rewrite discrete_fun_lookup_op ?discrete_fun_lookup_insert //; [].
move: (Hg x'). by rewrite discrete_fun_lookup_op !discrete_fun_lookup_insert_ne.
Qed.
Lemma discrete_fun_insert_updateP' x (P : B x Prop) g y1 :
y1 ~~>: P
discrete_fun_insert x y1 g ~~>: λ g', y2, g' = discrete_fun_insert x y2 g P y2.
Proof. eauto using discrete_fun_insert_updateP. Qed.
Lemma discrete_fun_insert_update g x y1 y2 :
y1 ~~> y2 discrete_fun_insert x y1 g ~~> discrete_fun_insert x y2 g.
Proof.
rewrite !cmra_update_updateP; eauto using discrete_fun_insert_updateP with subst.
Qed.
Lemma discrete_fun_singleton_updateP x (P : B x Prop) (Q : discrete_fun B Prop) y1 :
y1 ~~>: P ( y2, P y2 Q (discrete_fun_singleton x y2))
discrete_fun_singleton x y1 ~~>: Q.
Proof. rewrite /discrete_fun_singleton; eauto using discrete_fun_insert_updateP. Qed.
Lemma discrete_fun_singleton_updateP' x (P : B x Prop) y1 :
y1 ~~>: P
discrete_fun_singleton x y1 ~~>: λ g, y2, g = discrete_fun_singleton x y2 P y2.
Proof. eauto using discrete_fun_singleton_updateP. Qed.
Lemma discrete_fun_singleton_update x (y1 y2 : B x) :
y1 ~~> y2 discrete_fun_singleton x y1 ~~> discrete_fun_singleton x y2.
Proof. eauto using discrete_fun_insert_update. Qed.
Lemma discrete_fun_singleton_updateP_empty x (P : B x Prop) (Q : discrete_fun B Prop) :
ε ~~>: P ( y2, P y2 Q (discrete_fun_singleton x y2)) ε ~~>: Q.
Proof.
intros Hx HQ; apply cmra_total_updateP.
intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
exists (discrete_fun_singleton x y2); split; [by apply HQ|].
intros x'; destruct (decide (x' = x)) as [->|].
- by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton.
- rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //; by apply Hg.
Qed.
Lemma discrete_fun_singleton_updateP_empty' x (P : B x Prop) :
ε ~~>: P ε ~~>: λ g, y2, g = discrete_fun_singleton x y2 P y2.
Proof. eauto using discrete_fun_singleton_updateP_empty. Qed.
Lemma discrete_fun_singleton_update_empty x (y : B x) :
ε ~~> y ε ~~> discrete_fun_singleton x y.
Proof.
rewrite !cmra_update_updateP;
eauto using discrete_fun_singleton_updateP_empty with subst.
Qed.
Lemma discrete_fun_updateP `{!Finite A} f P Q :
( a, f a ~~>: P a) ( f', ( a, P a (f' a)) Q f') f ~~>: Q.
Proof.
repeat setoid_rewrite cmra_total_updateP. intros Hf HP n h Hh.
destruct (finite_choice
(λ a y, P a y {n} (y (h a)))) as [f' Hf']; first naive_solver.
naive_solver.
Qed.
Lemma discrete_fun_updateP' `{!Finite A} f P :
( a, f a ~~>: P a) f ~~>: λ f', a, P a (f' a).
Proof. eauto using discrete_fun_updateP. Qed.
Lemma discrete_fun_update f g :
( a, f a ~~> g a) f ~~> g.
Proof.
repeat setoid_rewrite cmra_total_update.
intros Hfg n h Hh a. apply (Hfg a), Hh.
Qed.
End cmra.
From stdpp Require Export list gmap.
From iris.algebra Require Export list cmra.
From iris.algebra Require Import gset.
From iris.algebra Require Import updates local_updates proofmode_classes big_op.
From iris.prelude Require Import options.
Section ofe.
Context {SI : sidx} `{Countable K} {A : ofe}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Local Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
i, m1 !! i {n} m2 !! i.
Definition gmap_ofe_mixin : OfeMixin (gmap K A).
Proof.
split.
- intros m1 m2; split.
+ by intros Hm n k; apply equiv_dist.
+ intros Hm k; apply equiv_dist; intros n; apply Hm.
- intros n; split.
+ by intros m k.
+ by intros m1 m2 ? k.
+ by intros m1 m2 m3 ?? k; trans (m2 !! k).
- intros n n' m1 m2 ? k ?. by eapply dist_le.
Qed.
Canonical Structure gmapO : ofe := Ofe (gmap K A) gmap_ofe_mixin.
Program Definition gmap_chain (c : chain gmapO) (k : K) : chain (optionO A) :=
{| chain_car n := c n !! k |}.
Next Obligation. intros c k n p Hp. by apply c. Qed.
Program Definition gmap_bchain {n} (c : bchain gmapO n)
(k : K) : bchain (optionO A) n :=
{| bchain_car p Hp := c p Hp !! k |}.
Next Obligation. intros n c k p γ Hpγ Hp ; by apply c. Qed.
Definition gmap_compl `{!Cofe A} : Compl gmapO := λ c,
map_imap (λ i _, compl (gmap_chain c i)) (c 0).
Definition gmap_lbcompl `{!Cofe A} : LBCompl gmapO := λ n Hn c,
map_imap (λ i _, lbcompl Hn (gmap_bchain c i)) (c _ (SIdx.limit_lt_0 _ Hn)).
Global Program Instance gmap_cofe `{!Cofe A} : Cofe gmapO :=
{| compl := gmap_compl; lbcompl := gmap_lbcompl |}.
Next Obligation.
intros ? n c k. rewrite /gmap_compl map_lookup_imap.
oinversion (λ H, chain_cauchy c 0 n H k); simplify_option_eq;
[apply SIdx.le_0_l| |done].
rewrite conv_compl /=. by apply reflexive_eq.
Qed.
Next Obligation.
intros ? n Hn c p Hp k. rewrite /lbcompl /gmap_lbcompl.
rewrite map_lookup_imap.
oinversion (bchain_cauchy _ c _ p (SIdx.limit_lt_0 _ Hn) Hp _ k);
simplify_option_eq; [apply SIdx.le_0_l| |done].
rewrite (conv_lbcompl _ _ Hp) /=. by apply reflexive_eq.
Qed.
Next Obligation.
intros ? n Hn c1 c2 p Hc k. rewrite /gmap_lbcompl !map_lookup_imap.
oinversion (Hc _ (SIdx.limit_lt_0 _ Hn) k); simpl; eauto.
apply lbcompl_ne=> ??. apply Hc.
Qed.
Global Instance gmap_ofe_discrete : OfeDiscrete A OfeDiscrete gmapO.
Proof. intros ? m m' ? i. by apply (discrete_0 _). Qed.
(* why doesn't this go automatic? *)
Global Instance gmapO_leibniz: LeibnizEquiv A LeibnizEquiv gmapO.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
Global Instance lookup_ne k : NonExpansive (lookup k : gmap K A option A).
Proof. by intros n m1 m2. Qed.
Global Instance lookup_total_ne `{!Inhabited A} k :
NonExpansive (lookup_total k : gmap K A A).
Proof. intros n m1 m2. rewrite !lookup_total_alt. by intros ->. Qed.
Global Instance partial_alter_ne n :
Proper ((dist n ==> dist n) ==> (=) ==> dist n ==> dist n)
(partial_alter (M:=gmap K A)).
Proof.
by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
rewrite ?lookup_partial_alter ?lookup_partial_alter_ne //;
try apply Hf; apply lookup_ne.
Qed.
Global Instance insert_ne i : NonExpansive2 (insert (M:=gmap K A) i).
Proof. intros n x y ? m m' ? j; apply partial_alter_ne; by try constructor. Qed.
Global Instance singleton_ne i : NonExpansive (singletonM i : A gmap K A).
Proof. by intros ????; apply insert_ne. Qed.
Global Instance delete_ne i : NonExpansive (delete (M:=gmap K A) i).
Proof.
intros n m m' ? j; destruct (decide (i = j)); simplify_map_eq;
[by constructor|by apply lookup_ne].
Qed.
Global Instance alter_ne (f : A A) (k : K) n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (alter (M := gmap K A) f k).
Proof. intros ? m m' Hm k'. by apply partial_alter_ne; [solve_proper|..]. Qed.
Global Instance gmap_empty_discrete : Discrete ( : gmap K A).
Proof.
intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
inversion_clear Hm; constructor.
Qed.
Global Instance gmap_lookup_discrete m i : Discrete m Discrete (m !! i).
Proof.
intros ? [x|] Hx; [|by symmetry; apply: discrete].
assert (m {0} <[i:=x]> m)
by (by symmetry in Hx; inversion Hx; ofe_subst; rewrite insert_id).
by rewrite (discrete_0 m (<[i:=x]>m)) // lookup_insert.
Qed.
Global Instance gmap_insert_discrete m i x :
Discrete x Discrete m Discrete (<[i:=x]>m).
Proof.
intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
{ by apply: discrete; rewrite -Hm lookup_insert. }
by apply: discrete; rewrite -Hm lookup_insert_ne.
Qed.
Global Instance gmap_singleton_discrete i x :
Discrete x Discrete ({[ i := x ]} : gmap K A).
Proof. rewrite /singletonM /map_singleton. apply _. Qed.
Lemma insert_idN n m i x :
m !! i {n} Some x <[i:=x]>m {n} m.
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
Global Instance gmap_dom_ne n :
Proper (({n}@{gmap K A}) ==> (=)) dom.
Proof. intros m1 m2 Hm. apply set_eq=> k. by rewrite !elem_of_dom Hm. Qed.
End ofe.
Global Instance map_seq_ne {SI : sidx} {A : ofe} start :
NonExpansive (map_seq (M:=gmap nat A) start).
Proof.
intros n l1 l2 Hl. revert start.
induction Hl; intros; simpl; repeat (done || f_equiv).
Qed.
Global Arguments gmapO {_} _ {_ _} _.
Global Instance merge_ne {SI : sidx} `{Countable K} {A B C : ofe} n :
Proper ((dist (A:=option A) n ==> dist (A:=option B) n ==> dist (A:=option C) n) ==>
dist n ==> dist n ==> ({n}@{gmap K C})) merge.
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
Qed.
Global Instance union_with_ne {SI : sidx} `{Countable K} {A : ofe} n :
Proper ((dist n ==> dist n ==> dist n) ==>
dist n ==> dist n ==> dist n) (union_with (M:=gmap K A)).
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
by do 2 destruct 1; first [apply Hf | constructor].
Qed.
Global Instance map_fmap_ne {SI : sidx} `{Countable K} {A B : ofe} (f : A B) n :
Proper (dist n ==> dist n) f
Proper (dist n ==> ({n}@{gmap K B})) (fmap f).
Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
Global Instance map_zip_with_ne {SI : sidx}
`{Countable K} {A B C : ofe} (f : A B C) n :
Proper (dist n ==> dist n ==> dist n) f
Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
Proof.
intros Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ne; try done.
destruct 1; destruct 1; repeat f_equiv; constructor || done.
Qed.
Global Instance gmap_union_ne {SI : sidx} `{Countable K} {A : ofe} :
NonExpansive2 (union (A:=gmap K A)).
Proof. intros n. apply union_with_ne. by constructor. Qed.
Global Instance gmap_disjoint_ne {SI : sidx} `{Countable K} {A : ofe} n :
Proper (dist n ==> dist n ==> iff) (map_disjoint (M:=gmap K) (A:=A)).
Proof.
intros m1 m1' Hm1 m2 m2' Hm2; split;
intros Hm i; specialize (Hm i); by destruct (Hm1 i), (Hm2 i).
Qed.
Lemma gmap_union_dist_eq {SI : sidx} `{Countable K} {A : ofe}
(m m1 m2 : gmap K A) n :
m {n} m1 m2 m1' m2', m = m1' m2' m1' {n} m1 m2' {n} m2.
Proof.
split; last first.
{ by intros (m1'&m2'&->&<-&<-). }
intros Hm.
exists (filter (λ '(l,_), is_Some (m1 !! l)) m),
(m2 m1 filter (λ '(l,_), is_Some (m2 !! l)) m).
split_and!; [apply map_eq|..]; intros k; move: (Hm k);
rewrite ?lookup_union ?lookup_intersection !map_lookup_filter;
case _ : (m !! k)=> [x|] /=; case _ : (m1 !! k)=> [x1|] /=;
case _ : (m2 !! k)=> [x2|] /=; by inversion 1.
Qed.
Lemma big_opM_ne_2 {SI : sidx} {M: ofe} {o: M M M}
`{!Monoid o} `{Countable K} {A : ofe} (f g : K A M) m1 m2 n :
m1 {n} m2
( k y1 y2,
m1 !! k = Some y1 m2 !! k = Some y2 y1 {n} y2 f k y1 {n} g k y2)
([^o map] k y m1, f k y) {n} ([^o map] k y m2, g k y).
Proof.
intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
{ by intros ?? ->. }
{ apply monoid_ne. }
intros k. assert (m1 !! k {n} m2 !! k) as Hlk by (by f_equiv).
destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
(* CMRA *)
Section cmra.
Context {SI : sidx} `{Countable K} {A : cmra}.
Implicit Types m : gmap K A.
Local Instance gmap_unit_instance : Unit (gmap K A) := ( : gmap K A).
Local Instance gmap_op_instance : Op (gmap K A) := merge op.
Local Instance gmap_pcore_instance : PCore (gmap K A) := λ m, Some (omap pcore m).
Local Instance gmap_valid_instance : Valid (gmap K A) := λ m, i, (m !! i).
Local Instance gmap_validN_instance : ValidN (gmap K A) := λ n m, i, {n} (m !! i).
Lemma gmap_op m1 m2 : m1 m2 = merge op m1 m2.
Proof. done. Qed.
Lemma lookup_op m1 m2 i : (m1 m2) !! i = m1 !! i m2 !! i.
Proof. rewrite lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
Lemma lookup_core m i : core m !! i = core (m !! i).
Proof. by apply lookup_omap. Qed.
Lemma lookup_includedN n (m1 m2 : gmap K A) : m1 {n} m2 i, m1 !! i {n} m2 !! i.
Proof.
split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
{ exists m2. by rewrite left_id. }
destruct (IH (delete i m2)) as [m2' Hm2'].
{ intros j. move: (Hm j); destruct (decide (i = j)) as [->|].
- intros _. rewrite Hi. apply: ucmra_unit_leastN.
- rewrite lookup_insert_ne // lookup_delete_ne //. }
destruct (Hm i) as [my Hi']; simplify_map_eq.
exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|].
- by rewrite Hi' lookup_op lookup_insert lookup_partial_alter.
- move: (Hm2' j). by rewrite !lookup_op lookup_delete_ne //
lookup_insert_ne // lookup_partial_alter_ne.
Qed.
(* [m1 ≼ m2] is not equivalent to [∀ n, m1 ≼{n} m2],
so there is no good way to reuse the above proof. *)
Lemma lookup_included (m1 m2 : gmap K A) : m1 m2 i, m1 !! i m2 !! i.
Proof.
split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
{ exists m2. by rewrite left_id. }
destruct (IH (delete i m2)) as [m2' Hm2'].
{ intros j. move: (Hm j); destruct (decide (i = j)) as [->|].
- intros _. rewrite Hi. apply: ucmra_unit_least.
- rewrite lookup_insert_ne // lookup_delete_ne //. }
destruct (Hm i) as [my Hi']; simplify_map_eq.
exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|].
- by rewrite Hi' lookup_op lookup_insert lookup_partial_alter.
- move: (Hm2' j). by rewrite !lookup_op lookup_delete_ne //
lookup_insert_ne // lookup_partial_alter_ne.
Qed.
Lemma gmap_cmra_mixin : CmraMixin (gmap K A).
Proof.
apply cmra_total_mixin.
- eauto.
- intros n m1 m2 m3 Hm i; by rewrite !lookup_op (Hm i).
- intros n m1 m2 Hm i; by rewrite !lookup_core (Hm i).
- intros n m1 m2 Hm ? i; by rewrite -(Hm i).
- intros m; split.
+ by intros ? n i; apply cmra_valid_validN.
+ intros Hm i; apply cmra_valid_validN=> n; apply Hm.
- intros n m Hm i ? ?; eauto using cmra_validN_le.
- by intros m1 m2 m3 i; rewrite !lookup_op assoc.
- by intros m1 m2 i; rewrite !lookup_op comm.
- intros m i. by rewrite lookup_op lookup_core cmra_core_l.
- intros m i. by rewrite !lookup_core cmra_core_idemp.
- intros m1 m2; rewrite !lookup_included=> Hm i.
rewrite !lookup_core. by apply cmra_core_mono.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- intros n m y1 y2 Hm Heq.
refine ((λ FUN, _) (λ i, cmra_extend n (m !! i) (y1 !! i) (y2 !! i) (Hm i) _));
last by rewrite -lookup_op.
exists (map_imap (λ i _, projT1 (FUN i)) y1).
exists (map_imap (λ i _, proj1_sig (projT2 (FUN i))) y2).
split; [|split]=>i; rewrite ?lookup_op !map_lookup_imap;
destruct (FUN i) as (z1i&z2i&Hmi&Hz1i&Hz2i)=>/=.
+ destruct (y1 !! i), (y2 !! i); inversion Hz1i; inversion Hz2i; subst=>//.
+ revert Hz1i. case: (y1!!i)=>[?|] //.
+ revert Hz2i. case: (y2!!i)=>[?|] //.
Qed.
Canonical Structure gmapR := Cmra (gmap K A) gmap_cmra_mixin.
Global Instance gmap_cmra_discrete : CmraDiscrete A CmraDiscrete gmapR.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
Lemma gmap_ucmra_mixin : UcmraMixin (gmap K A).
Proof.
split.
- by intros i; rewrite lookup_empty.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- constructor=> i. by rewrite lookup_omap lookup_empty.
Qed.
Canonical Structure gmapUR := Ucmra (gmap K A) gmap_ucmra_mixin.
Global Instance gmap_op_empty_l_L : LeftId (=@{gmap K A}) op.
Proof. apply _. Qed.
Global Instance gmap_op_empty_r : RightId (=@{gmap K A}) op.
Proof. apply _. Qed.
End cmra.
Global Arguments gmapR {_} _ {_ _} _.
Global Arguments gmapUR {_} _ {_ _} _.
Section properties.
Context {SI : sidx} `{Countable K} {A : cmra}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
Global Instance lookup_op_homomorphism i :
MonoidHomomorphism op op () (lookup i : gmap K A option A).
Proof.
split; [split|]; try apply _.
- intros m1 m2; by rewrite lookup_op.
- done.
Qed.
Lemma lookup_opM m1 mm2 i : (m1 ? mm2) !! i = m1 !! i (mm2 ≫= (.!! i)).
Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
Lemma lookup_validN_Some n m i x : {n} m m !! i {n} Some x {n} x.
Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
Lemma lookup_valid_Some m i x : m m !! i Some x x.
Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed.
Lemma insert_validN n m i x : {n} x {n} m {n} <[i:=x]>m.
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
Lemma insert_valid m i x : x m <[i:=x]>m.
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
Lemma singleton_validN n i x : {n} ({[ i := x ]} : gmap K A) {n} x.
Proof.
split.
- move=>/(_ i); by simplify_map_eq.
- intros. apply insert_validN; first done. apply: ucmra_unit_validN.
Qed.
Lemma singleton_valid i x : ({[ i := x ]} : gmap K A) x.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
Lemma delete_validN n m i : {n} m {n} (delete i m).
Proof. intros Hm j; destruct (decide (i = j)); by simplify_map_eq. Qed.
Lemma delete_valid m i : m (delete i m).
Proof. intros Hm j; destruct (decide (i = j)); by simplify_map_eq. Qed.
Lemma insert_singleton_op m i x : m !! i = None <[i:=x]> m = {[ i := x ]} m.
Proof.
intros Hi; apply map_eq=> j; destruct (decide (i = j)) as [->|].
- by rewrite lookup_op lookup_insert lookup_singleton Hi right_id_L.
- by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id_L.
Qed.
Lemma singleton_core (i : K) (x : A) cx :
pcore x = Some cx core {[ i := x ]} =@{gmap K A} {[ i := cx ]}.
Proof. apply omap_singleton_Some. Qed.
Lemma singleton_core' (i : K) (x : A) cx :
pcore x Some cx core {[ i := x ]} ≡@{gmap K A} {[ i := cx ]}.
Proof.
intros (cx'&?&<-)%Some_equiv_eq. by rewrite (singleton_core _ _ cx').
Qed.
Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) :
core {[ i := x ]} =@{gmap K A} {[ i := core x ]}.
Proof. apply singleton_core. rewrite cmra_pcore_core //. Qed.
Lemma singleton_op (i : K) (x y : A) :
{[ i := x ]} {[ i := y ]} =@{gmap K A} {[ i := x y ]}.
Proof. by apply (merge_singleton _ _ _ x y). Qed.
Global Instance singleton_is_op i a a1 a2 :
IsOp a a1 a2 IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -singleton_op. Qed.
Lemma gmap_core_id m : ( i x, m !! i = Some x CoreId x) CoreId m.
Proof.
intros Hcore; apply core_id_total=> i.
rewrite lookup_core. destruct (m !! i) as [x|] eqn:Hix; rewrite Hix; [|done].
by eapply Hcore.
Qed.
Global Instance gmap_core_id' m : ( x : A, CoreId x) CoreId m.
Proof. auto using gmap_core_id. Qed.
Global Instance gmap_singleton_core_id i (x : A) :
CoreId x CoreId {[ i := x ]}.
Proof. intros. by apply core_id_total, singleton_core'. Qed.
Lemma singleton_includedN_l n m i x :
{[ i := x ]} {n} m y, m !! i {n} Some y Some x {n} Some y.
Proof.
split.
- move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hi.
exists (x ? m' !! i). rewrite -Some_op_opM.
split; first done. apply cmra_includedN_l.
- intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
intros j; destruct (decide (i = j)) as [->|].
+ by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
+ by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
Qed.
(* We do not have [x ≼ y ↔ ∀ n, x ≼{n} y], so we cannot use the previous lemma *)
Lemma singleton_included_l m i x :
{[ i := x ]} m y, m !! i Some y Some x Some y.
Proof.
split.
- move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
exists (x ? m' !! i). by rewrite -Some_op_opM.
- intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
intros j; destruct (decide (i = j)) as [->|].
+ by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
+ by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
Qed.
Lemma singleton_included_exclusive_l m i x :
Exclusive x m
{[ i := x ]} m m !! i Some x.
Proof.
intros ? Hm. rewrite singleton_included_l. split; last by eauto.
intros (y&?&->%(Some_included_exclusive _)); eauto using lookup_valid_Some.
Qed.
Lemma singleton_included i x y :
{[ i := x ]} ({[ i := y ]} : gmap K A) Some x Some y.
Proof.
rewrite singleton_included_l. split.
- intros (y'&Hi&?). rewrite lookup_insert in Hi. by rewrite Hi.
- intros ?. exists y. by rewrite lookup_insert.
Qed.
Lemma singleton_included_total `{!CmraTotal A} i x y :
{[ i := x ]} ({[ i := y ]} : gmap K A) x y.
Proof. rewrite singleton_included Some_included_total. done. Qed.
Lemma singleton_included_mono i x y :
x y {[ i := x ]} ({[ i := y ]} : gmap K A).
Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed.
Global Instance singleton_cancelable i x :
Cancelable (Some x) Cancelable {[ i := x ]}.
Proof.
intros ? n m1 m2 Hv EQ j. move: (Hv j) (EQ j). rewrite !lookup_op.
destruct (decide (i = j)) as [->|].
- rewrite lookup_singleton. by apply cancelableN.
- by rewrite lookup_singleton_ne // !(left_id None _).
Qed.
Global Instance gmap_cancelable (m : gmap K A) :
( x : A, IdFree x) ( x : A, Cancelable x) Cancelable m.
Proof.
intros ?? n m1 m2 ?? i. apply (cancelableN (m !! i)); by rewrite -!lookup_op.
Qed.
Lemma insert_op m1 m2 i x y :
<[i:=x y]>(m1 m2) = <[i:=x]>m1 <[i:=y]>m2.
Proof. by rewrite (insert_merge () m1 m2 i (x y) x y). Qed.
Lemma insert_updateP (P : A Prop) (Q : gmap K A Prop) m i x :
x ~~>: P
( y, P y Q (<[i:=y]>m))
<[i:=x]>m ~~>: Q.
Proof.
intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm.
destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done.
{ by generalize (Hm i); rewrite lookup_op; simplify_map_eq. }
exists (<[i:=y]> m); split; first by auto.
intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
destruct (decide (i = j)); simplify_map_eq/=; auto.
Qed.
Lemma insert_updateP' (P : A Prop) m i x :
x ~~>: P <[i:=x]>m ~~>: λ m', y, m' = <[i:=y]>m P y.
Proof. eauto using insert_updateP. Qed.
Lemma insert_update m i x y : x ~~> y <[i:=x]>m ~~> <[i:=y]>m.
Proof. rewrite !cmra_update_updateP; eauto using insert_updateP with subst. Qed.
Lemma singleton_updateP (P : A Prop) (Q : gmap K A Prop) i x :
x ~~>: P ( y, P y Q {[ i := y ]}) {[ i := x ]} ~~>: Q.
Proof. apply insert_updateP. Qed.
Lemma singleton_updateP' (P : A Prop) i x :
x ~~>: P {[ i := x ]} ~~>: λ m, y, m = {[ i := y ]} P y.
Proof. apply insert_updateP'. Qed.
Lemma singleton_update i (x y : A) : x ~~> y {[ i := x ]} ~~> {[ i := y ]}.
Proof. apply insert_update. Qed.
Lemma delete_update m i : m ~~> delete i m.
Proof.
apply cmra_total_update=> n mf Hm j; destruct (decide (i = j)); subst.
- move: (Hm j). rewrite !lookup_op lookup_delete left_id.
apply cmra_validN_op_r.
- move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
Qed.
Lemma gmap_op_union m1 m2 : m1 ## m2 m1 m2 = m1 m2.
Proof.
intros Hm. apply map_eq=> k. specialize (Hm k).
rewrite lookup_op lookup_union. by destruct (m1 !! k), (m2 !! k).
Qed.
Lemma gmap_op_valid0_disjoint m1 m2 :
{0} (m1 m2) ( k x, m1 !! k = Some x Exclusive x) m1 ## m2.
Proof.
unfold Exclusive. intros Hvalid Hexcl k.
specialize (Hvalid k). rewrite lookup_op in Hvalid. specialize (Hexcl k).
destruct (m1 !! k), (m2 !! k); [|done..].
rewrite -Some_op Some_validN in Hvalid. naive_solver.
Qed.
Lemma gmap_op_valid_disjoint m1 m2 :
(m1 m2) ( k x, m1 !! k = Some x Exclusive x) m1 ## m2.
Proof. move=> /cmra_valid_validN /(_ 0). apply gmap_op_valid0_disjoint. Qed.
Lemma dom_op m1 m2 : dom (m1 m2) = dom m1 dom m2.
Proof.
apply set_eq=> i; rewrite elem_of_union !elem_of_dom.
unfold is_Some; setoid_rewrite lookup_op.
destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Lemma dom_included m1 m2 : m1 m2 dom m1 dom m2.
Proof.
rewrite lookup_included=>? i; rewrite !elem_of_dom. by apply is_Some_included.
Qed.
Section freshness.
Local Set Default Proof Using "Type*".
Context `{!Infinite K}.
Lemma alloc_updateP_strong_dep (Q : gmap K A Prop) (I : K Prop) m (f : K A) :
pred_infinite I
( i, m !! i = None I i (f i))
( i, m !! i = None I i Q (<[i:=f i]>m)) m ~~>: Q.
Proof.
move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ.
apply cmra_total_updateP. intros n mf Hm.
destruct (HP (dom (m mf))) as [i [Hi1 Hi2]].
assert (m !! i = None).
{ eapply not_elem_of_dom. revert Hi2.
rewrite dom_op not_elem_of_union. naive_solver. }
exists (<[i:=f i]>m); split.
- by apply HQ.
- rewrite insert_singleton_op //.
rewrite -assoc -insert_singleton_op; last by eapply not_elem_of_dom.
apply insert_validN; [apply cmra_valid_validN|]; auto.
Qed.
Lemma alloc_updateP_strong (Q : gmap K A Prop) (I : K Prop) m x :
pred_infinite I
x ( i, m !! i = None I i Q (<[i:=x]>m)) m ~~>: Q.
Proof.
move=> HP ? HQ. eapply (alloc_updateP_strong_dep _ _ _ (λ _, x)); eauto.
Qed.
Lemma alloc_updateP (Q : gmap K A Prop) m x :
x ( i, m !! i = None Q (<[i:=x]>m)) m ~~>: Q.
Proof.
move=>??.
eapply (alloc_updateP_strong _ (λ _, True));
eauto using pred_infinite_True.
Qed.
Lemma alloc_updateP_cofinite (Q : gmap K A Prop) (J : gset K) m x :
x ( i, m !! i = None i J Q (<[i:=x]>m)) m ~~>: Q.
Proof.
eapply alloc_updateP_strong.
apply (pred_infinite_set (C:=gset K)).
intros E. exists (fresh (J E)).
apply not_elem_of_union, is_fresh.
Qed.
(* Variants without the universally quantified Q, for use in case that is an evar. *)
Lemma alloc_updateP_strong_dep' m (f : K A) (I : K Prop) :
pred_infinite I
( i, m !! i = None I i (f i))
m ~~>: λ m', i, I i m' = <[i:=f i]>m m !! i = None.
Proof. eauto using alloc_updateP_strong_dep. Qed.
Lemma alloc_updateP_strong' m x (I : K Prop) :
pred_infinite I
x m ~~>: λ m', i, I i m' = <[i:=x]>m m !! i = None.
Proof. eauto using alloc_updateP_strong. Qed.
Lemma alloc_updateP' m x :
x m ~~>: λ m', i, m' = <[i:=x]>m m !! i = None.
Proof. eauto using alloc_updateP. Qed.
Lemma alloc_updateP_cofinite' m x (J : gset K) :
x m ~~>: λ m', i, i J m' = <[i:=x]>m m !! i = None.
Proof. eauto using alloc_updateP_cofinite. Qed.
End freshness.
Lemma alloc_unit_singleton_updateP (P : A Prop) (Q : gmap K A Prop) u i :
u LeftId () u ()
u ~~>: P ( y, P y Q {[ i := y ]}) ~~>: Q.
Proof.
intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
destruct (Hx n (gf !! i)) as (y&?&Hy).
{ move:(Hg i). rewrite !left_id.
case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
intros; by apply cmra_valid_validN. }
exists {[ i := y ]}; split; first by auto.
intros i'; destruct (decide (i' = i)) as [->|].
- rewrite lookup_op lookup_singleton.
move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
- move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
Qed.
Lemma alloc_unit_singleton_updateP' (P: A Prop) u i :
u LeftId () u ()
u ~~>: P ~~>: λ m, y, m = {[ i := y ]} P y.
Proof. eauto using alloc_unit_singleton_updateP. Qed.
Lemma alloc_unit_singleton_update (u : A) i (y : A) :
u LeftId () u () u ~~> y (∅:gmap K A) ~~> {[ i := y ]}.
Proof.
rewrite !cmra_update_updateP;
eauto using alloc_unit_singleton_updateP with subst.
Qed.
Lemma gmap_local_update m1 m2 m1' m2' :
( i, (m1 !! i, m2 !! i) ~l~> (m1' !! i, m2' !! i))
(m1, m2) ~l~> (m1', m2').
Proof.
intros Hupd. apply local_update_unital=> n mf Hmv Hm.
apply forall_and_distr=> i. rewrite lookup_op -cmra_opM_fmap_Some.
apply Hupd; simpl; first done. by rewrite Hm lookup_op cmra_opM_fmap_Some.
Qed.
Lemma alloc_local_update m1 m2 i x :
m1 !! i = None x (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
Proof.
intros Hi ?. apply gmap_local_update=> j.
destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
rewrite !lookup_insert Hi. by apply alloc_option_local_update.
Qed.
Lemma alloc_singleton_local_update m i x :
m !! i = None x (m,) ~l~> (<[i:=x]>m, {[ i:=x ]}).
Proof. apply alloc_local_update. Qed.
Lemma insert_local_update m1 m2 i x y x' y' :
m1 !! i = Some x m2 !! i = Some y
(x, y) ~l~> (x', y')
(m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
Proof.
intros Hi1 Hi2 Hup. apply gmap_local_update=> j.
destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
rewrite !lookup_insert Hi1 Hi2. by apply option_local_update.
Qed.
Lemma singleton_local_update_any m i y x' y' :
( x, m !! i = Some x (x, y) ~l~> (x', y'))
(m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
Proof.
intros. apply gmap_local_update=> j.
destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
rewrite !lookup_singleton lookup_insert.
destruct (m !! j); first by eauto using option_local_update.
apply local_update_total_valid0=> _ _ /option_includedN; naive_solver.
Qed.
Lemma singleton_local_update m i x y x' y' :
m !! i = Some x
(x, y) ~l~> (x', y')
(m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
Proof.
intros Hmi ?. apply singleton_local_update_any.
intros x2. rewrite Hmi=>[=<-]. done.
Qed.
Lemma delete_local_update m1 m2 i x `{!Exclusive x} :
m2 !! i = Some x (m1, m2) ~l~> (delete i m1, delete i m2).
Proof.
intros Hi. apply gmap_local_update=> j.
destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
rewrite !lookup_delete Hi. by apply delete_option_local_update.
Qed.
Lemma delete_singleton_local_update m i x `{!Exclusive x} :
(m, {[ i := x ]}) ~l~> (delete i m, ).
Proof.
rewrite -(delete_singleton i x).
by eapply delete_local_update, lookup_singleton.
Qed.
Lemma delete_local_update_cancelable m1 m2 i mx `{!Cancelable mx} :
m1 !! i mx m2 !! i mx
(m1, m2) ~l~> (delete i m1, delete i m2).
Proof.
intros Hi1 Hi2. apply gmap_local_update=> j.
destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
rewrite !lookup_delete Hi1 Hi2. by apply delete_option_local_update_cancelable.
Qed.
Lemma delete_singleton_local_update_cancelable m i x `{!Cancelable (Some x)} :
m !! i Some x (m, {[ i := x ]}) ~l~> (delete i m, ).
Proof.
intros. rewrite -(delete_singleton i x).
apply (delete_local_update_cancelable m _ i (Some x));
[done|by rewrite lookup_singleton].
Qed.
Lemma gmap_fmap_mono {B : cmra} (f : A B) m1 m2 :
Proper (() ==> ()) f
( x y, x y f x f y) m1 m2 fmap f m1 fmap f m2.
Proof.
intros ??. rewrite !lookup_included=> Hm i.
rewrite !lookup_fmap. by apply option_fmap_mono.
Qed.
Lemma big_opM_singletons m :
([^op map] k x m, {[ k := x ]}) = m.
Proof.
(* We are breaking the big_opM abstraction here. The reason is that [map_ind]
is too weak: we need an induction principle that visits all the keys in the
right order, namely the order in which they appear in map_to_list. Here,
we achieve this by unfolding [big_opM] and doing induction over that list
instead. *)
rewrite big_op.big_opM_unseal /big_op.big_opM_def -{2}(list_to_map_to_list m).
assert (NoDup (map_to_list m).*1) as Hnodup by apply NoDup_fst_map_to_list.
revert Hnodup. induction (map_to_list m) as [|[k x] l IH]; csimpl; first done.
intros [??]%NoDup_cons. rewrite IH //.
rewrite insert_singleton_op ?not_elem_of_list_to_map_1 //.
Qed.
Lemma big_opS_gset_to_gmap (X : gset K) (a : A) :
([^op set] x X, {[ x := a ]}) gset_to_gmap a X.
Proof.
induction X as [|x X ? IH] using set_ind_L.
{ rewrite big_opS_empty gset_to_gmap_empty //. }
rewrite big_opS_insert //.
rewrite gset_to_gmap_union_singleton.
rewrite insert_singleton_op; [|by rewrite lookup_gset_to_gmap_None].
by rewrite IH.
Qed.
Lemma big_opS_gset_to_gmap_L `{!LeibnizEquiv A} (X : gset K) (a : A) :
([^op set] x X, {[ x := a ]}) = gset_to_gmap a X.
Proof. apply leibniz_equiv, big_opS_gset_to_gmap. Qed.
End properties.
Section unital_properties.
Context {SI : sidx} `{Countable K} {A : ucmra}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
Lemma insert_alloc_local_update m1 m2 i x x' y' :
m1 !! i = Some x m2 !! i = None
(x, ε) ~l~> (x', y')
(m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
Proof.
intros Hi1 Hi2 Hup. apply local_update_unital=> n mf Hm1v Hm.
assert (mf !! i {n} Some x) as Hif.
{ move: (Hm i). by rewrite lookup_op Hi1 Hi2 left_id. }
destruct (Hup n (mf !! i)) as [Hx'v Hx'eq].
{ move: (Hm1v i). by rewrite Hi1. }
{ by rewrite Hif -(inj_iff Some) -Some_op_opM -Some_op left_id. }
split.
- by apply insert_validN.
- simpl in Hx'eq. by rewrite -(insert_idN n mf i x) // -insert_op -Hm Hx'eq Hif.
Qed.
End unital_properties.
(** Functor *)
Global Instance gmap_fmap_ne {SI : sidx} `{Countable K} {A B : ofe} (f : A B) n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist (A:=gmap K _) n) (fmap f).
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
Lemma gmap_fmap_ne_ext {SI : sidx} `{Countable K}
{A : Type} {B : ofe} (f1 f2 : A B) (m : gmap K A) n :
( i x, m !! i = Some x f1 x {n} f2 x)
f1 <$> m {n} f2 <$> m.
Proof.
move => Hf i. rewrite !lookup_fmap.
destruct (m !! i) eqn:?; constructor; by eauto.
Qed.
Global Instance gmap_fmap_cmra_morphism {SI : sidx} `{Countable K} {A B : cmra}
(f : A B) `{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A gmap K B).
Proof.
split; try apply _.
- by intros n m ? i; rewrite lookup_fmap; apply (cmra_morphism_validN _).
- intros m. apply Some_proper=>i. rewrite lookup_fmap !lookup_omap lookup_fmap.
case: (m!!i)=> //= ?. apply cmra_morphism_pcore, _.
- intros m1 m2 i. by rewrite lookup_op !lookup_fmap lookup_op cmra_morphism_op.
Qed.
Definition gmapO_map {SI : sidx} `{Countable K} {A B: ofe} (f: A -n> B) :
gmapO K A -n> gmapO K B := OfeMor (fmap f : gmapO K A gmapO K B).
Global Instance gmapO_map_ne {SI : sidx} `{Countable K} {A B: ofe} :
NonExpansive (@gmapO_map _ K _ _ A B).
Proof.
intros n f g Hf m k; rewrite /= !lookup_fmap.
destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
Program Definition gmapOF {SI : sidx} K `{Countable K}
(F : oFunctor) : oFunctor := {|
oFunctor_car A _ B _ := gmapO K (oFunctor_car F A B);
oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (oFunctor_map F fg)
|}.
Next Obligation.
intros ? K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
by apply gmapO_map_ne, oFunctor_map_ne.
Qed.
Next Obligation.
intros ? K ?? F A ? B ? m; simpl in *. rewrite /= -{2}(map_fmap_id m).
apply: map_fmap_equiv_ext=>y ??; apply oFunctor_map_id.
Qed.
Next Obligation.
intros ? K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' m.
rewrite /= -map_fmap_compose.
apply: map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
Qed.
Global Instance gmapOF_contractive {SI : sidx} `{Countable K} F :
oFunctorContractive F oFunctorContractive (gmapOF K F).
Proof.
by intros ? ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
apply gmapO_map_ne, oFunctor_map_contractive.
Qed.
Program Definition gmapURF {SI : sidx} K `{Countable K}
(F : rFunctor) : urFunctor := {|
urFunctor_car A _ B _ := gmapUR K (rFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros ? K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg;
apply gmapO_map_ne, rFunctor_map_ne.
Qed.
Next Obligation.
intros ? K ?? F A ? B ? m. rewrite /= -{2}(map_fmap_id m).
apply: map_fmap_equiv_ext=> y ??. apply rFunctor_map_id.
Qed.
Next Obligation.
intros ? K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' m.
rewrite /= -map_fmap_compose.
apply: map_fmap_equiv_ext=> y ??. apply rFunctor_map_compose.
Qed.
Global Instance gmapURF_contractive {SI : sidx} `{Countable K} F :
rFunctorContractive F urFunctorContractive (gmapURF K F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
by apply gmapO_map_ne, rFunctor_map_contractive.
Qed.
Program Definition gmapRF {SI : sidx} K `{Countable K}
(F : rFunctor) : rFunctor := {|
rFunctor_car A _ B _ := gmapR K (rFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
|}.
Solve Obligations with apply @gmapURF.
Global Instance gmapRF_contractive {SI : sidx} `{Countable K} F :
rFunctorContractive F rFunctorContractive (gmapRF K F).
Proof. apply gmapURF_contractive. Qed.
From stdpp Require Export sets gmultiset countable.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates big_op.
From iris.prelude Require Import options.
(* The multiset union CMRA *)
Section gmultiset.
Context `{Countable K} {SI : sidx}.
Implicit Types X Y : gmultiset K.
Canonical Structure gmultisetO := discreteO (gmultiset K).
Local Instance gmultiset_valid_instance : Valid (gmultiset K) := λ _, True.
Local Instance gmultiset_validN_instance : ValidN (gmultiset K) := λ _ _, True.
Local Instance gmultiset_unit_instance : Unit (gmultiset K) := ( : gmultiset K).
Local Instance gmultiset_op_instance : Op (gmultiset K) := disj_union.
Local Instance gmultiset_pcore_instance : PCore (gmultiset K) := λ X, Some ∅.
Lemma gmultiset_op X Y : X Y = X Y.
Proof. done. Qed.
Lemma gmultiset_core X : core X = ∅.
Proof. done. Qed.
Lemma gmultiset_included X Y : X Y X Y.
Proof.
split.
- intros [Z ->%leibniz_equiv].
rewrite gmultiset_op. apply gmultiset_disj_union_subseteq_l.
- intros ->%gmultiset_disj_union_difference. by exists (Y X).
Qed.
Lemma gmultiset_ra_mixin : RAMixin (gmultiset K).
Proof.
apply ra_total_mixin; eauto.
- by intros X Y Z ->%leibniz_equiv.
- by intros X Y ->%leibniz_equiv.
- solve_proper.
- intros X1 X2 X3. by rewrite !gmultiset_op assoc_L.
- intros X1 X2. by rewrite !gmultiset_op comm_L.
- intros X. by rewrite gmultiset_core left_id.
- intros X1 X2 HX. rewrite !gmultiset_core. exists ∅.
by rewrite left_id.
Qed.
Canonical Structure gmultisetR := discreteR (gmultiset K) gmultiset_ra_mixin.
Global Instance gmultiset_cmra_discrete : CmraDiscrete gmultisetR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
Proof.
split; [done | | done]. intros X.
by rewrite gmultiset_op left_id_L.
Qed.
Canonical Structure gmultisetUR := Ucmra (gmultiset K) gmultiset_ucmra_mixin.
Global Instance gmultiset_cancelable X : Cancelable X.
Proof.
apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X ⊎.)).
Qed.
Lemma gmultiset_opM X mY : X ? mY = X default mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
Lemma gmultiset_update X Y : X ~~> Y.
Proof. done. Qed.
Lemma gmultiset_local_update X Y X' Y' : X Y' = X' Y (X,Y) ~l~> (X', Y').
Proof.
intros HXY. rewrite local_update_unital_discrete=> Z' _. intros ->%leibniz_equiv.
split; first done. apply leibniz_equiv_iff, (inj (. Y)).
rewrite -HXY !gmultiset_op.
by rewrite -(comm_L _ Y) (comm_L _ Y') assoc_L.
Qed.
Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X X', Y X').
Proof. apply gmultiset_local_update. by rewrite (comm_L _ Y) assoc_L. Qed.
Lemma gmultiset_local_update_dealloc X Y X' :
X' Y (X,Y) ~l~> (X X', Y X').
Proof.
intros ->%gmultiset_disj_union_difference. apply local_update_total_valid.
intros _ _ ->%gmultiset_included%gmultiset_disj_union_difference.
apply gmultiset_local_update. apply gmultiset_eq=> x.
repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
lia.
Qed.
Lemma big_opMS_singletons X :
([^op mset] x X, {[+ x +]}) = X.
Proof.
induction X as [|x X IH] using gmultiset_ind.
- rewrite big_opMS_empty. done.
- unfold_leibniz. rewrite big_opMS_disj_union // big_opMS_singleton IH //.
Qed.
End gmultiset.
Global Arguments gmultisetO _ {_ _ _}.
Global Arguments gmultisetR _ {_ _ _}.
Global Arguments gmultisetUR _ {_ _ _}.
From stdpp Require Export sets gmap mapset.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates big_op.
From iris.prelude Require Import options.
(* The union CMRA *)
Section gset.
Context {SI : sidx} `{Countable K}.
Implicit Types X Y : gset K.
Canonical Structure gsetO := discreteO (gset K).
Local Instance gset_valid_instance : Valid (gset K) := λ _, True.
Local Instance gset_unit_instance : Unit (gset K) := ( : gset K).
Local Instance gset_op_instance : Op (gset K) := union.
Local Instance gset_pcore_instance : PCore (gset K) := λ X, Some X.
Lemma gset_op X Y : X Y = X Y.
Proof. done. Qed.
Lemma gset_core X : core X = X.
Proof. done. Qed.
Lemma gset_included X Y : X Y X Y.
Proof.
split.
- intros [Z ->]. rewrite gset_op. set_solver.
- intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
Qed.
Lemma gset_ra_mixin : RAMixin (gset K).
Proof.
apply ra_total_mixin; apply _ || eauto; [].
intros X. by rewrite gset_core idemp_L.
Qed.
Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
Global Instance gset_cmra_discrete : CmraDiscrete gsetR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma gset_ucmra_mixin : UcmraMixin (gset K).
Proof. split; [ done | | done ]. intros X. by rewrite gset_op left_id_L. Qed.
Canonical Structure gsetUR := Ucmra (gset K) gset_ucmra_mixin.
Lemma gset_opM X mY : X ? mY = X default mY.
Proof using SI. destruct mY; by rewrite /= ?right_id_L. Qed.
Lemma gset_update X Y : X ~~> Y.
Proof. done. Qed.
Lemma gset_local_update X Y X' : X X' (X,Y) ~l~> (X',X').
Proof.
intros (Z&->&?)%subseteq_disjoint_union_L.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
split; [done|]. rewrite gset_op. set_solver.
Qed.
Global Instance gset_core_id X : CoreId X.
Proof. by apply core_id_total; rewrite gset_core. Qed.
Lemma big_opS_singletons X :
([^op set] x X, {[ x ]}) = X.
Proof.
induction X as [|x X Hx IH] using set_ind_L.
- rewrite big_opS_empty. done.
- unfold_leibniz. rewrite big_opS_insert // IH //.
Qed.
(** Add support [X ≼ Y] to [set_solver]. (We get support for [⋅] for free
because it is definitionally equal to [∪]). *)
Global Instance set_unfold_gset_included X Y Q :
SetUnfold (X Y) Q SetUnfold (X Y) Q.
Proof. intros [?]; constructor. by rewrite gset_included. Qed.
End gset.
Global Arguments gsetO {_} _ {_ _}.
Global Arguments gsetR {_} _ {_ _}.
Global Arguments gsetUR {_} _ {_ _}.
(* The disjoint union CMRA *)
Inductive gset_disj K `{Countable K} :=
| GSet : gset K gset_disj K
| GSetInvalid : gset_disj K.
Global Arguments GSet {_ _ _} _.
Global Arguments GSetInvalid {_ _ _}.
Section gset_disj.
Context {SI : sidx} `{Countable K}.
Local Arguments op _ _ !_ !_ /.
Local Arguments cmra_op _ !_ !_ /.
Local Arguments ucmra_op _ !_ !_ /.
Global Instance GSet_inj : Inj (=@{gset K}) (=) GSet.
Proof. intros ???. naive_solver. Qed.
Canonical Structure gset_disjO := leibnizO (gset_disj K).
Local Instance gset_disj_valid_instance : Valid (gset_disj K) := λ X,
match X with GSet _ => True | GSetInvalid => False end.
Local Instance gset_disj_unit_instance : Unit (gset_disj K) := GSet ∅.
Local Instance gset_disj_op_instance : Op (gset_disj K) := λ X Y,
match X, Y with
| GSet X, GSet Y => if decide (X ## Y) then GSet (X Y) else GSetInvalid
| _, _ => GSetInvalid
end.
Local Instance gset_disj_pcore_instance : PCore (gset_disj K) := λ _, Some ε.
Ltac gset_disj_solve :=
repeat (simpl || case_decide);
first [apply (f_equal GSet)|done|exfalso]; set_solver by eauto.
Lemma gset_disj_included X Y : GSet X GSet Y X Y.
Proof.
split.
- move=> [[Z|]]; simpl; try case_decide; set_solver.
- intros (Z&->&?)%subseteq_disjoint_union_L.
exists (GSet Z). gset_disj_solve.
Qed.
Lemma gset_disj_valid_inv_l X Y : (GSet X Y) Y', Y = GSet Y' X ## Y'.
Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
Lemma gset_disj_union X Y : X ## Y GSet X GSet Y = GSet (X Y).
Proof. intros. by rewrite /= decide_True. Qed.
Lemma gset_disj_valid_op X Y : (GSet X GSet Y) X ## Y.
Proof. simpl. case_decide; by split. Qed.
Lemma gset_disj_ra_mixin : RAMixin (gset_disj K).
Proof.
apply ra_total_mixin; eauto.
- intros [?|]; destruct 1; gset_disj_solve.
- by constructor.
- by destruct 1.
- intros [X1|] [X2|] [X3|]; gset_disj_solve.
- intros [X1|] [X2|]; gset_disj_solve.
- intros [X|]; gset_disj_solve.
- exists (GSet ); gset_disj_solve.
- intros [X1|] [X2|]; gset_disj_solve.
Qed.
Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.
Global Instance gset_disj_cmra_discrete : CmraDiscrete gset_disjR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma gset_disj_ucmra_mixin : UcmraMixin (gset_disj K).
Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
Canonical Structure gset_disjUR := Ucmra (gset_disj K) gset_disj_ucmra_mixin.
Local Arguments op _ _ _ _ : simpl never.
Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K Prop) X :
( Y, X Y j, j Y P j)
( i, i X P i Q (GSet ({[i]} X)))
GSet X ~~>: Q.
Proof.
intros Hfresh HQ.
apply cmra_discrete_total_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
destruct (Hfresh (X Y)) as (i&?&?); first set_solver.
exists (GSet ({[ i ]} X)); split.
- apply HQ; set_solver by eauto.
- apply gset_disj_valid_op. set_solver by eauto.
Qed.
Lemma gset_disj_alloc_updateP_strong' P X :
( Y, X Y j, j Y P j)
GSet X ~~>: λ Y, i, Y = GSet ({[ i ]} X) i X P i.
Proof. eauto using gset_disj_alloc_updateP_strong. Qed.
Lemma gset_disj_alloc_empty_updateP_strong P (Q : gset_disj K Prop) :
( Y : gset K, j, j Y P j)
( i, P i Q (GSet {[i]})) GSet ~~>: Q.
Proof.
intros. apply (gset_disj_alloc_updateP_strong P); eauto.
intros i; rewrite right_id_L; auto.
Qed.
Lemma gset_disj_alloc_empty_updateP_strong' P :
( Y : gset K, j, j Y P j)
GSet ~~>: λ Y, i, Y = GSet {[ i ]} P i.
Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.
Section fresh_updates.
Local Set Default Proof Using "Type*".
Context `{!Infinite K}.
Lemma gset_disj_alloc_updateP (Q : gset_disj K Prop) X :
( i, i X Q (GSet ({[i]} X))) GSet X ~~>: Q.
Proof.
intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto.
intros Y ?; exists (fresh Y). split; [|done]. apply is_fresh.
Qed.
Lemma gset_disj_alloc_updateP' X :
GSet X ~~>: λ Y, i, Y = GSet ({[ i ]} X) i X.
Proof. eauto using gset_disj_alloc_updateP. Qed.
Lemma gset_disj_alloc_empty_updateP (Q : gset_disj K Prop) :
( i, Q (GSet {[i]})) GSet ~~>: Q.
Proof.
intro. apply gset_disj_alloc_updateP. intros i; rewrite right_id_L; auto.
Qed.
Lemma gset_disj_alloc_empty_updateP' : GSet ~~>: λ Y, i, Y = GSet {[ i ]}.
Proof. eauto using gset_disj_alloc_empty_updateP. Qed.
End fresh_updates.
Lemma gset_disj_dealloc_local_update X Y :
(GSet X, GSet Y) ~l~> (GSet (X Y), GSet ).
Proof.
apply local_update_total_valid=> _ _ /gset_disj_included HYX.
rewrite local_update_unital_discrete=> -[Xf|] _ /leibniz_equiv_iff //=.
rewrite {1}/op /=. destruct (decide _) as [HXf|]; [intros[= ->]|done].
by rewrite difference_union_distr_l_L
difference_diag_L !left_id_L difference_disjoint_L.
Qed.
Lemma gset_disj_dealloc_empty_local_update X Z :
(GSet Z GSet X, GSet Z) ~l~> (GSet X, GSet ).
Proof.
apply local_update_total_valid=> /gset_disj_valid_op HZX _ _.
assert (X = (Z X) Z) as HX by set_solver.
rewrite gset_disj_union // {2}HX. apply gset_disj_dealloc_local_update.
Qed.
Lemma gset_disj_dealloc_op_local_update X Y Z :
(GSet Z GSet X, GSet Z GSet Y) ~l~> (GSet X,GSet Y).
Proof.
rewrite -{2}(left_id ε _ (GSet Y)).
apply op_local_update_frame, gset_disj_dealloc_empty_local_update.
Qed.
Lemma gset_disj_alloc_op_local_update X Y Z :
Z ## X (GSet X,GSet Y) ~l~> (GSet Z GSet X, GSet Z GSet Y).
Proof.
intros. apply op_local_update_discrete. by rewrite gset_disj_valid_op.
Qed.
Lemma gset_disj_alloc_local_update X Y Z :
Z ## X (GSet X,GSet Y) ~l~> (GSet (Z X), GSet (Z Y)).
Proof.
intros. apply local_update_total_valid=> _ _ /gset_disj_included ?.
rewrite -!gset_disj_union //; last set_solver.
auto using gset_disj_alloc_op_local_update.
Qed.
Lemma gset_disj_alloc_empty_local_update X Z :
Z ## X (GSet X, GSet ) ~l~> (GSet (Z X), GSet Z).
Proof.
intros. rewrite -{2}(right_id_L _ union Z).
apply gset_disj_alloc_local_update; set_solver.
Qed.
(** Add some basic support for [GSet X = GSet Y], [GSet X ≼ GSet Y], and
[✓ (GSet X ⋅ GSet Y)] to [set_solver]. There are probably more cases we could
cover (e.g., involving [GSetInvalid], or nesting of [⋅]), but it is not clear
these are useful in practice, nor how to handle them effectively. *)
Global Instance set_unfold_gset_eq (X Y : gset K) Q :
SetUnfold (X = Y) Q SetUnfold (GSet X = GSet Y) Q.
Proof. intros [?]; constructor. by rewrite (inj_iff _). Qed.
Global Instance set_unfold_gset_disj_included (X Y : gset K) Q :
SetUnfold (X Y) Q SetUnfold (GSet X GSet Y) Q.
Proof. intros [?]; constructor. by rewrite gset_disj_included. Qed.
Global Instance set_unfold_gset_disj_valid_op (X Y : gset K) Q :
SetUnfold (X ## Y) Q SetUnfold ( (GSet X GSet Y)) Q.
Proof. intros [?]; constructor. by rewrite gset_disj_valid_op. Qed.
End gset_disj.
Global Arguments gset_disjO {_} _ {_ _}.
Global Arguments gset_disjR {_} _ {_ _}.
Global Arguments gset_disjUR {_} _ {_ _}.
From iris.algebra Require Export dfrac agree updates local_updates.
From iris.algebra Require Import proofmode_classes.
From iris.prelude Require Import options.
Definition dfrac_agreeR {SI : sidx} (A : ofe) : cmra := prodR dfracR (agreeR A).
Definition to_dfrac_agree {SI : sidx} {A : ofe} (d : dfrac) (a : A) : dfrac_agreeR A :=
(d, to_agree a).
Global Instance: Params (@to_dfrac_agree) 3 := {}.
(** To make it easier to work with the [Qp] version of this, we also provide
[to_frac_agree] and appropriate lemmas. *)
Definition to_frac_agree {SI : sidx} {A : ofe} (q : Qp) (a : A) : dfrac_agreeR A :=
to_dfrac_agree (DfracOwn q) a.
Global Instance: Params (@to_frac_agree) 3 := {}.
Section lemmas.
Context {SI : sidx} {A : ofe}.
Implicit Types (q : Qp) (d : dfrac) (a : A).
Global Instance to_dfrac_agree_ne d : NonExpansive (@to_dfrac_agree SI A d).
Proof. solve_proper. Qed.
Global Instance to_dfrac_agree_proper d :
Proper (() ==> ()) (@to_dfrac_agree SI A d).
Proof. solve_proper. Qed.
Global Instance to_dfrac_agree_exclusive a :
Exclusive (to_dfrac_agree (DfracOwn 1) a).
Proof. apply _. Qed.
Global Instance to_dfrac_agree_discrete d a : Discrete a Discrete (to_dfrac_agree d a).
Proof. apply _. Qed.
Global Instance to_dfrac_agree_injN n :
Inj2 (dist n) (dist n) (dist n) (@to_dfrac_agree SI A).
Proof. by intros d1 a1 d2 a2 [??%(inj to_agree)]. Qed.
Global Instance to_dfrac_agree_inj : Inj2 () () () (@to_dfrac_agree SI A).
Proof. by intros d1 a1 d2 a2 [??%(inj to_agree)]. Qed.
Lemma dfrac_agree_op d1 d2 a :
to_dfrac_agree (d1 d2) a to_dfrac_agree d1 a to_dfrac_agree d2 a.
Proof. rewrite /to_dfrac_agree -pair_op agree_idemp //. Qed.
Lemma frac_agree_op q1 q2 a :
to_frac_agree (q1 + q2) a to_frac_agree q1 a to_frac_agree q2 a.
Proof. rewrite -dfrac_agree_op. done. Qed.
Lemma dfrac_agree_op_valid d1 a1 d2 a2 :
(to_dfrac_agree d1 a1 to_dfrac_agree d2 a2)
(d1 d2) a1 a2.
Proof.
rewrite /to_dfrac_agree -pair_op pair_valid to_agree_op_valid. done.
Qed.
Lemma dfrac_agree_op_valid_L `{!LeibnizEquiv A} d1 a1 d2 a2 :
(to_dfrac_agree d1 a1 to_dfrac_agree d2 a2)
(d1 d2) a1 = a2.
Proof. unfold_leibniz. apply dfrac_agree_op_valid. Qed.
Lemma dfrac_agree_op_validN d1 a1 d2 a2 n :
{n} (to_dfrac_agree d1 a1 to_dfrac_agree d2 a2)
(d1 d2) a1 {n} a2.
Proof.
rewrite /to_dfrac_agree -pair_op pair_validN to_agree_op_validN. done.
Qed.
Lemma frac_agree_op_valid q1 a1 q2 a2 :
(to_frac_agree q1 a1 to_frac_agree q2 a2)
(q1 + q2 1)%Qp a1 a2.
Proof. apply dfrac_agree_op_valid. Qed.
Lemma frac_agree_op_valid_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
(to_frac_agree q1 a1 to_frac_agree q2 a2)
(q1 + q2 1)%Qp a1 = a2.
Proof. apply dfrac_agree_op_valid_L. Qed.
Lemma frac_agree_op_validN q1 a1 q2 a2 n :
{n} (to_frac_agree q1 a1 to_frac_agree q2 a2)
(q1 + q2 1)%Qp a1 {n} a2.
Proof. apply dfrac_agree_op_validN. Qed.
Lemma dfrac_agree_included d1 a1 d2 a2 :
to_dfrac_agree d1 a1 to_dfrac_agree d2 a2
(d1 d2) a1 a2.
Proof. by rewrite pair_included to_agree_included. Qed.
Lemma dfrac_agree_included_L `{!LeibnizEquiv A} d1 a1 d2 a2 :
to_dfrac_agree d1 a1 to_dfrac_agree d2 a2
(d1 d2) a1 = a2.
Proof. unfold_leibniz. apply dfrac_agree_included. Qed.
Lemma dfrac_agree_includedN d1 a1 d2 a2 n :
to_dfrac_agree d1 a1 {n} to_dfrac_agree d2 a2
(d1 d2) a1 {n} a2.
Proof.
by rewrite pair_includedN -cmra_discrete_included_iff
to_agree_includedN.
Qed.
Lemma frac_agree_included q1 a1 q2 a2 :
to_frac_agree q1 a1 to_frac_agree q2 a2
(q1 < q2)%Qp a1 a2.
Proof. by rewrite dfrac_agree_included dfrac_own_included. Qed.
Lemma frac_agree_included_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
to_frac_agree q1 a1 to_frac_agree q2 a2
(q1 < q2)%Qp a1 = a2.
Proof. by rewrite dfrac_agree_included_L dfrac_own_included. Qed.
Lemma frac_agree_includedN q1 a1 q2 a2 n :
to_frac_agree q1 a1 {n} to_frac_agree q2 a2
(q1 < q2)%Qp a1 {n} a2.
Proof. by rewrite dfrac_agree_includedN dfrac_own_included. Qed.
(** While [cmra_update_exclusive] takes care of most updates, it is not sufficient
for this one since there is no abstraction-preserving way to rewrite
[to_dfrac_agree d1 v1 ⋅ to_dfrac_agree d2 v2] into something simpler. *)
Lemma dfrac_agree_update_2 d1 d2 a1 a2 a' :
d1 d2 = DfracOwn 1
to_dfrac_agree d1 a1 to_dfrac_agree d2 a2 ~~>
to_dfrac_agree d1 a' to_dfrac_agree d2 a'.
Proof.
intros Hq. rewrite -pair_op Hq.
apply cmra_update_exclusive.
rewrite dfrac_agree_op_valid Hq //.
Qed.
Lemma frac_agree_update_2 q1 q2 a1 a2 a' :
(q1 + q2 = 1)%Qp
to_frac_agree q1 a1 to_frac_agree q2 a2 ~~>
to_frac_agree q1 a' to_frac_agree q2 a'.
Proof. intros Hq. apply dfrac_agree_update_2. rewrite dfrac_op_own Hq //. Qed.
Lemma dfrac_agree_persist d a :
to_dfrac_agree d a ~~> to_dfrac_agree DfracDiscarded a.
Proof.
rewrite /to_dfrac_agree. apply prod_update; last done.
simpl. apply dfrac_discard_update.
Qed.
Lemma dfrac_agree_unpersist a :
to_dfrac_agree DfracDiscarded a ~~>: λ k, q, k = to_dfrac_agree (DfracOwn q) a.
Proof.
rewrite /to_dfrac_agree. eapply prod_updateP; first apply dfrac_undiscard_update.
{ by eapply cmra_update_updateP. }
naive_solver.
Qed.
End lemmas.
Definition dfrac_agreeRF {SI : sidx} (F : oFunctor) : rFunctor :=
prodRF (constRF dfracR) (agreeRF F).
Global Instance dfrac_agreeRF_contractive {SI : sidx} F :
oFunctorContractive F rFunctorContractive (dfrac_agreeRF F).
Proof. apply _. Qed.
Global Typeclasses Opaque to_dfrac_agree.
(* [to_frac_agree] is deliberately transparent to reuse the [to_dfrac_agree] instances *)
From iris.algebra Require Export auth excl updates.
From iris.algebra Require Import local_updates.
From iris.prelude Require Import options.
(** Authoritative CMRA where the fragment is exclusively owned.
This is effectively a single "ghost variable" with two views, the frament [◯E a]
and the authority [●E a]. *)
Definition excl_authR {SI : sidx} (A : ofe) : cmra :=
authR (optionUR (exclR A)).
Definition excl_authUR {SI : sidx} (A : ofe) : ucmra :=
authUR (optionUR (exclR A)).
Definition excl_auth_auth {SI : sidx} {A : ofe} (a : A) : excl_authR A :=
(Some (Excl a)).
Definition excl_auth_frag {SI : sidx} {A : ofe} (a : A) : excl_authR A :=
(Some (Excl a)).
Global Typeclasses Opaque excl_auth_auth excl_auth_frag.
Global Instance: Params (@excl_auth_auth) 2 := {}.
Global Instance: Params (@excl_auth_frag) 3 := {}.
Notation "●E a" := (excl_auth_auth a) (at level 10).
Notation "◯E a" := (excl_auth_frag a) (at level 10).
Section excl_auth.
Context {SI : sidx} {A : ofe}.
Implicit Types a b : A.
Global Instance excl_auth_auth_ne : NonExpansive (@excl_auth_auth SI A).
Proof. solve_proper. Qed.
Global Instance excl_auth_auth_proper :
Proper (() ==> ()) (@excl_auth_auth SI A).
Proof. solve_proper. Qed.
Global Instance excl_auth_frag_ne : NonExpansive (@excl_auth_frag SI A).
Proof. solve_proper. Qed.
Global Instance excl_auth_frag_proper :
Proper (() ==> ()) (@excl_auth_frag SI A).
Proof. solve_proper. Qed.
Global Instance excl_auth_auth_discrete a : Discrete a Discrete (E a).
Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
Global Instance excl_auth_frag_discrete a : Discrete a Discrete (E a).
Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
Lemma excl_auth_validN n a : {n} (E a E a).
Proof. by rewrite auth_both_validN. Qed.
Lemma excl_auth_valid a : (E a E a).
Proof. intros. by apply auth_both_valid_2. Qed.
Lemma excl_auth_agreeN n a b : {n} (E a E b) a {n} b.
Proof.
rewrite auth_both_validN /= => -[Hincl Hvalid].
move: Hincl=> /Some_includedN_exclusive /(_ I) ?. by apply (inj Excl).
Qed.
Lemma excl_auth_agree a b : (E a E b) a b.
Proof.
intros. apply equiv_dist=> n. by apply excl_auth_agreeN, cmra_valid_validN.
Qed.
Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : (E a E b) a = b.
Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
Lemma excl_auth_auth_op_validN n a b : {n} (E a E b) False.
Proof. apply auth_auth_op_validN. Qed.
Lemma excl_auth_auth_op_valid a b : (E a E b) False.
Proof. apply auth_auth_op_valid. Qed.
Lemma excl_auth_frag_op_validN n a b : {n} (E a E b) False.
Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
Lemma excl_auth_frag_op_valid a b : (E a E b) False.
Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.
Lemma excl_auth_update a b a' : E a E b ~~> E a' E a'.
Proof.
intros. by apply auth_update, option_local_update, exclusive_local_update.
Qed.
End excl_auth.
Definition excl_authURF {SI : sidx} (F : oFunctor) : urFunctor :=
authURF (optionURF (exclRF F)).
Global Instance excl_authURF_contractive {SI : sidx} F :
oFunctorContractive F urFunctorContractive (excl_authURF F).
Proof. apply _. Qed.
Definition excl_authRF {SI : sidx} (F : oFunctor) : rFunctor :=
authRF (optionURF (exclRF F)).
Global Instance excl_authRF_contractive {SI : sidx} F :
oFunctorContractive F rFunctorContractive (excl_authRF F).
Proof. apply _. Qed.
From iris.algebra Require Export frac auth updates local_updates.
From iris.algebra Require Import proofmode_classes.
From iris.prelude Require Import options.
(** Authoritative CMRA where the NON-authoritative parts can be fractional.
This CMRA allows the original non-authoritative element [◯ a] to be split into
fractional parts [◯F{q} a]. Using [◯F a ≡ ◯F{1} a] is in effect the same as
using the original [◯ a]. Currently, however, this CMRA hides the ability to
split the authoritative part into fractions.
*)
Definition frac_authR {SI : sidx} (A : cmra) : cmra :=
authR (optionUR (prodR fracR A)).
Definition frac_authUR {SI : sidx} (A : cmra) : ucmra :=
authUR (optionUR (prodR fracR A)).
Definition frac_auth_auth {SI : sidx} {A : cmra} (x : A) : frac_authR A :=
(Some (1%Qp,x)).
Definition frac_auth_frag {SI : sidx}
{A : cmra} (q : frac) (x : A) : frac_authR A :=
(Some (q,x)).
Global Typeclasses Opaque frac_auth_auth frac_auth_frag.
Global Instance: Params (@frac_auth_auth) 2 := {}.
Global Instance: Params (@frac_auth_frag) 3 := {}.
Notation "●F a" := (frac_auth_auth a) (at level 10).
Notation "◯F{ q } a" := (frac_auth_frag q a) (at level 10, format "◯F{ q } a").
Notation "◯F a" := (frac_auth_frag 1 a) (at level 10).
Section frac_auth.
Context {SI : sidx} {A : cmra}.
Implicit Types a b : A.
Global Instance frac_auth_auth_ne : NonExpansive (@frac_auth_auth SI A).
Proof. solve_proper. Qed.
Global Instance frac_auth_auth_proper :
Proper (() ==> ()) (@frac_auth_auth SI A).
Proof. solve_proper. Qed.
Global Instance frac_auth_frag_ne q : NonExpansive (@frac_auth_frag SI A q).
Proof. solve_proper. Qed.
Global Instance frac_auth_frag_proper q :
Proper (() ==> ()) (@frac_auth_frag SI A q).
Proof. solve_proper. Qed.
Global Instance frac_auth_auth_discrete a : Discrete a Discrete (F a).
Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
Global Instance frac_auth_frag_discrete q a : Discrete a Discrete (F{q} a).
Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
Lemma frac_auth_validN n a : {n} a {n} (F a F a).
Proof. by rewrite auth_both_validN. Qed.
Lemma frac_auth_valid a : a (F a F a).
Proof. intros. by apply auth_both_valid_2. Qed.
Lemma frac_auth_agreeN n a b : {n} (F a F b) a {n} b.
Proof.
rewrite auth_both_validN /= => -[Hincl Hvalid].
by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??].
Qed.
Lemma frac_auth_agree a b : (F a F b) a b.
Proof.
intros. apply equiv_dist=> n. by apply frac_auth_agreeN, cmra_valid_validN.
Qed.
Lemma frac_auth_agree_L `{!LeibnizEquiv A} a b : (F a F b) a = b.
Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.
Lemma frac_auth_includedN n q a b : {n} (F a F{q} b) Some b {n} Some a.
Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
Lemma frac_auth_included `{!CmraDiscrete A} q a b :
(F a F{q} b) Some b Some a.
Proof. by rewrite auth_both_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
Lemma frac_auth_includedN_total `{!CmraTotal A} n q a b :
{n} (F a F{q} b) b {n} a.
Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
Lemma frac_auth_included_total `{!CmraDiscrete A, !CmraTotal A} q a b :
(F a F{q} b) b a.
Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.
Lemma frac_auth_auth_validN n a : {n} (F a) {n} a.
Proof.
rewrite auth_auth_dfrac_validN Some_validN. split.
- by intros [?[]].
- intros. by split.
Qed.
Lemma frac_auth_auth_valid a : (F a) a.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.
Lemma frac_auth_frag_validN n q a : {n} (F{q} a) (q 1)%Qp {n} a.
Proof. by rewrite /frac_auth_frag auth_frag_validN. Qed.
Lemma frac_auth_frag_valid q a : (F{q} a) (q 1)%Qp a.
Proof. by rewrite /frac_auth_frag auth_frag_valid. Qed.
Lemma frac_auth_frag_op q1 q2 a1 a2 : F{q1+q2} (a1 a2) F{q1} a1 F{q2} a2.
Proof. done. Qed.
Lemma frac_auth_frag_op_validN n q1 q2 a b :
{n} (F{q1} a F{q2} b) (q1 + q2 1)%Qp {n} (a b).
Proof. by rewrite -frac_auth_frag_op frac_auth_frag_validN. Qed.
Lemma frac_auth_frag_op_valid q1 q2 a b :
(F{q1} a F{q2} b) (q1 + q2 1)%Qp (a b).
Proof. by rewrite -frac_auth_frag_op frac_auth_frag_valid. Qed.
Global Instance frac_auth_is_op (q q1 q2 : frac) (a a1 a2 : A) :
IsOp q q1 q2 IsOp a a1 a2 IsOp' (F{q} a) (F{q1} a1) (F{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
Global Instance frac_auth_is_op_core_id (q q1 q2 : frac) (a : A) :
CoreId a IsOp q q1 q2 IsOp' (F{q} a) (F{q1} a) (F{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
by rewrite -frac_auth_frag_op -core_id_dup.
Qed.
Lemma frac_auth_update q a b a' b' :
(a,b) ~l~> (a',b') F a F{q} b ~~> F a' F{q} b'.
Proof.
intros. by apply auth_update, option_local_update, prod_local_update_2.
Qed.
Lemma frac_auth_update_1 a b a' : a' F a F b ~~> F a' F a'.
Proof.
intros. by apply auth_update, option_local_update, exclusive_local_update.
Qed.
End frac_auth.
Definition frac_authURF {SI : sidx} (F : rFunctor) : urFunctor :=
authURF (optionURF (prodRF (constRF fracR) F)).
Global Instance frac_authURF_contractive {SI : sidx} F :
rFunctorContractive F urFunctorContractive (frac_authURF F).
Proof. apply _. Qed.
Definition frac_authRF {SI : sidx} (F : rFunctor) : rFunctor :=
authRF (optionURF (prodRF (constRF fracR) F)).
Global Instance frac_authRF_contractive {SI : sidx} F :
rFunctorContractive F rFunctorContractive (frac_authRF F).
Proof. apply _. Qed.
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export view gmap frac dfrac.
From iris.algebra Require Import local_updates proofmode_classes big_op.
From iris.prelude Require Import options.
(** * CMRA for a "view of a gmap".
The authoritative element [gmap_view_auth] is any [gmap K V]. The fragments
[gmap_view_frag] represent ownership of a single key in that map. Ownership is
governed by a discardable fraction, which provides the possibiltiy to obtain
persistent read-only ownership of a key.
The key frame-preserving updates are [gmap_view_alloc] to allocate a new key,
[gmap_view_update] to update a key given full ownership of the corresponding
fragment, and [gmap_view_persist] to make a key read-only by discarding any
fraction of the corresponding fragment. Crucially, the latter does not require
owning the authoritative element.
NOTE: The API surface for [gmap_view] is experimental and subject to change. We
plan to add notations for authoritative elements and fragments, and hope to
support arbitrary maps as fragments. *)
Local Definition gmap_view_fragUR {SI : sidx}
(K : Type) `{Countable K} (V : cmra) : ucmra :=
gmapUR K (prodR dfracR V).
(** View relation. *)
Section rel.
Context {SI : sidx} (K : Type) `{Countable K} (V : cmra).
Implicit Types (m : gmap K V) (k : K) (v : V) (n : SI).
Implicit Types (f : gmap K (dfrac * V)).
(* If we exactly followed [auth], we'd write something like [f ≼{n} m ∧ ✓{n} m],
which is equivalent to:
[map_Forall (λ k fv, ∃ v, m !! k = Some v ∧ Some fv ≼{n} Some v ∧ ✓{n} v) f].
(Note the use of [Some] in the inclusion; the elementwise RA might not have a
unit and we want a reflexive relation!) However, [f] and [m] do not have the
same type, so this definition does not type-check: the fractions have been
erased from the authoritative [m]. So we additionally quantify over the erased
fraction [dq] and [(dq, v)] becomes the authoritative value.
An alternative definition one might consider is to replace the erased fraction
by a hard-coded [DfracOwn 1], the biggest possible fraction. That would not
work: we would end up with [Some dv ≼{n} Some (DfracOwn 1, v)] but that cannot
be satisfied if [dv.1 = DfracDiscarded], a case that we definitely want to
allow!
It is possible that [∀ k, ∃ dq, let auth := (pair dq) <$> m !! k in ✓{n} auth
∧ f !! k ≼{n} auth] would also work, but now the proofs are all done already. ;)
The two are probably equivalent, with a proof similar to [lookup_includedN]? *)
Local Definition gmap_view_rel_raw n m f :=
map_Forall (λ k fv,
v dq, m !! k = Some v {n} (dq, v) (Some fv {n} Some (dq, v))) f.
Local Lemma gmap_view_rel_raw_mono n1 n2 m1 m2 f1 f2 :
gmap_view_rel_raw n1 m1 f1
m1 {n2} m2
f2 {n2} f1
(n2 n1)%sidx
gmap_view_rel_raw n2 m2 f2.
Proof.
intros Hrel Hm Hf Hn k [dqa va] Hk.
(* For some reason applying the lemma in [Hf] does not work... *)
destruct (lookup_includedN n2 f2 f1) as [Hf' _].
specialize (Hf' Hf k). clear Hf. rewrite Hk in Hf'.
destruct (Some_includedN_is_Some _ _ _ Hf') as [[q' va'] Heq]. rewrite Heq in Hf'.
specialize (Hrel _ _ Heq) as (v & dq & Hm1 & [Hvval Hdqval] & Hvincl). simpl in *.
specialize (Hm k).
edestruct (dist_Some_inv_l _ _ _ _ Hm Hm1) as (v' & Hm2 & Hv).
eexists. exists dq. split; first done. split.
{ split; first done. simpl. rewrite -Hv. eapply cmra_validN_le; done. }
rewrite -Hv. etrans; first exact Hf'.
apply: cmra_includedN_le; done.
Qed.
Local Lemma gmap_view_rel_raw_valid n m f :
gmap_view_rel_raw n m f {n} f.
Proof.
intros Hrel k. destruct (f !! k) as [[dqa va]|] eqn:Hf; rewrite Hf; last done.
specialize (Hrel _ _ Hf) as (v & dq & Hmval & Hvval & Hvincl). simpl in *.
eapply cmra_validN_includedN. 2:done. done.
Qed.
Local Lemma gmap_view_rel_raw_unit n :
m, gmap_view_rel_raw n m ε.
Proof. exists ∅. apply: map_Forall_empty. Qed.
Local Canonical Structure gmap_view_rel :
view_rel (gmapO K V) (gmap_view_fragUR K V) :=
ViewRel gmap_view_rel_raw gmap_view_rel_raw_mono
gmap_view_rel_raw_valid gmap_view_rel_raw_unit.
Local Lemma gmap_view_rel_exists n f :
( m, gmap_view_rel n m f) {n} f.
Proof.
split.
{ intros [m Hrel]. eapply gmap_view_rel_raw_valid, Hrel. }
intros Hf.
cut ( m, gmap_view_rel n m f k, f !! k = None m !! k = None).
{ naive_solver. }
induction f as [|k [dq v] f Hk' IH] using map_ind.
{ exists ∅. split; [|done]. apply: map_Forall_empty. }
move: (Hf k). rewrite lookup_insert=> -[/= ??].
destruct IH as (m & Hm & Hdom).
{ intros k'. destruct (decide (k = k')) as [->|?]; [by rewrite Hk'|].
move: (Hf k'). by rewrite lookup_insert_ne. }
exists (<[k:=v]> m).
rewrite /gmap_view_rel /= /gmap_view_rel_raw map_Forall_insert //=. split_and!.
- exists v, dq. split; first by rewrite lookup_insert.
split; first by split. done.
- eapply map_Forall_impl; [apply Hm|]; simpl.
intros k' [dq' ag'] (v'&?&?&?). exists v'.
rewrite lookup_insert_ne; naive_solver.
- intros k'. rewrite !lookup_insert_None. naive_solver.
Qed.
Local Lemma gmap_view_rel_unit n m : gmap_view_rel n m ε.
Proof. apply: map_Forall_empty. Qed.
Local Lemma gmap_view_rel_discrete :
CmraDiscrete V ViewRelDiscrete gmap_view_rel.
Proof.
intros ? n m f Hrel k [df va] Hk.
destruct (Hrel _ _ Hk) as (v & dq & Hm & Hvval & Hvincl).
exists v, dq. split; first done.
split; first by apply cmra_discrete_valid_iff_0.
rewrite -cmra_discrete_included_iff_0. done.
Qed.
End rel.
Local Existing Instance gmap_view_rel_discrete.
(** [gmap_view] is a notation to give canonical structure search the chance
to infer the right instances (see [auth]). *)
Notation gmap_view K V := (view (gmap_view_rel_raw K V)).
Definition gmap_viewO {SI : sidx} (K : Type) `{Countable K} (V : cmra) : ofe :=
viewO (gmap_view_rel K V).
Definition gmap_viewR {SI : sidx} (K : Type) `{Countable K} (V : cmra) : cmra :=
viewR (gmap_view_rel K V).
Definition gmap_viewUR {SI : sidx} (K : Type) `{Countable K} (V : cmra) : ucmra :=
viewUR (gmap_view_rel K V).
Section definitions.
Context {SI : sidx} `{Countable K} {V : cmra}.
Definition gmap_view_auth (dq : dfrac) (m : gmap K V) : gmap_viewR K V :=
V{dq} m.
Definition gmap_view_frag (k : K) (dq : dfrac) (v : V) : gmap_viewR K V :=
V {[k := (dq, v)]}.
End definitions.
Section lemmas.
Context {SI : sidx} `{Countable K} {V : cmra}.
Implicit Types (m : gmap K V) (k : K) (q : Qp) (dq : dfrac) (v : V).
Global Instance : Params (@gmap_view_auth) 6 := {}.
Global Instance gmap_view_auth_ne dq :
NonExpansive (gmap_view_auth (K:=K) (V:=V) dq).
Proof. solve_proper. Qed.
Global Instance gmap_view_auth_proper dq :
Proper (() ==> ()) (gmap_view_auth (K:=K) (V:=V) dq).
Proof. apply ne_proper, _. Qed.
Global Instance : Params (@gmap_view_frag) 7 := {}.
Global Instance gmap_view_frag_ne k oq : NonExpansive (gmap_view_frag (V:=V) k oq).
Proof. solve_proper. Qed.
Global Instance gmap_view_frag_proper k oq :
Proper (() ==> ()) (gmap_view_frag (V:=V) k oq).
Proof. apply ne_proper, _. Qed.
(* Helper lemmas *)
Local Lemma gmap_view_rel_lookup n m k dq v :
gmap_view_rel K V n m {[k := (dq, v)]}
v' dq', m !! k = Some v' {n} (dq', v') Some (dq, v) {n} Some (dq', v').
Proof.
split.
- intros Hrel.
edestruct (Hrel k) as (v' & dq' & Hlookup & Hval & Hinc).
{ rewrite lookup_singleton. done. }
simpl in *. eexists _, _. split_and!; done.
- intros (v' & dq' & Hlookup & Hval & ?) j [df va].
destruct (decide (k = j)) as [<-|Hne]; last by rewrite lookup_singleton_ne.
rewrite lookup_singleton. intros [= <- <-]. simpl.
exists v', dq'. split_and!; by rewrite ?Hv'.
Qed.
(** Composition and validity *)
Lemma gmap_view_auth_dfrac_op dp dq m :
gmap_view_auth (dp dq) m
gmap_view_auth dp m gmap_view_auth dq m.
Proof. by rewrite /gmap_view_auth view_auth_dfrac_op. Qed.
Global Instance gmap_view_auth_dfrac_is_op dq dq1 dq2 m :
IsOp dq dq1 dq2
IsOp' (gmap_view_auth dq m) (gmap_view_auth dq1 m) (gmap_view_auth dq2 m).
Proof. rewrite /gmap_view_auth. apply _. Qed.
Lemma gmap_view_auth_dfrac_op_invN n dp m1 dq m2 :
{n} (gmap_view_auth dp m1 gmap_view_auth dq m2) m1 {n} m2.
Proof. apply view_auth_dfrac_op_invN. Qed.
Lemma gmap_view_auth_dfrac_op_inv dp m1 dq m2 :
(gmap_view_auth dp m1 gmap_view_auth dq m2) m1 m2.
Proof. apply view_auth_dfrac_op_inv. Qed.
Lemma gmap_view_auth_dfrac_validN m n dq : {n} gmap_view_auth dq m dq.
Proof.
rewrite view_auth_dfrac_validN. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_dfrac_valid m dq : gmap_view_auth dq m dq.
Proof.
rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_valid m : gmap_view_auth (DfracOwn 1) m.
Proof. rewrite gmap_view_auth_dfrac_valid. done. Qed.
Lemma gmap_view_auth_dfrac_op_validN n dq1 dq2 m1 m2 :
{n} (gmap_view_auth dq1 m1 gmap_view_auth dq2 m2) (dq1 dq2) m1 {n} m2.
Proof.
rewrite view_auth_dfrac_op_validN. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_dfrac_op_valid dq1 dq2 m1 m2 :
(gmap_view_auth dq1 m1 gmap_view_auth dq2 m2) (dq1 dq2) m1 m2.
Proof.
rewrite view_auth_dfrac_op_valid. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_op_validN n m1 m2 :
{n} (gmap_view_auth (DfracOwn 1) m1 gmap_view_auth (DfracOwn 1) m2) False.
Proof. apply view_auth_op_validN. Qed.
Lemma gmap_view_auth_op_valid m1 m2 :
(gmap_view_auth (DfracOwn 1) m1 gmap_view_auth (DfracOwn 1) m2) False.
Proof. apply view_auth_op_valid. Qed.
Lemma gmap_view_frag_validN n k dq v : {n} gmap_view_frag k dq v dq {n} v.
Proof.
rewrite view_frag_validN gmap_view_rel_exists singleton_validN pair_validN.
naive_solver.
Qed.
Lemma gmap_view_frag_valid k dq v : gmap_view_frag k dq v dq v.
Proof.
rewrite cmra_valid_validN. setoid_rewrite gmap_view_frag_validN.
rewrite cmra_valid_validN. pose 0. naive_solver.
Qed.
Lemma gmap_view_frag_op k dq1 dq2 v1 v2 :
gmap_view_frag k (dq1 dq2) (v1 v2)
gmap_view_frag k dq1 v1 gmap_view_frag k dq2 v2.
Proof. rewrite -view_frag_op singleton_op -pair_op //. Qed.
Lemma gmap_view_frag_add k q1 q2 v1 v2 :
gmap_view_frag k (DfracOwn (q1 + q2)) (v1 v2)
gmap_view_frag k (DfracOwn q1) v1 gmap_view_frag k (DfracOwn q2) v2.
Proof. rewrite -gmap_view_frag_op. done. Qed.
Lemma gmap_view_frag_op_validN n k dq1 dq2 v1 v2 :
{n} (gmap_view_frag k dq1 v1 gmap_view_frag k dq2 v2)
(dq1 dq2) {n} (v1 v2).
Proof.
rewrite view_frag_validN gmap_view_rel_exists singleton_op singleton_validN.
by rewrite -pair_op pair_validN.
Qed.
Lemma gmap_view_frag_op_valid k dq1 dq2 v1 v2 :
(gmap_view_frag k dq1 v1 gmap_view_frag k dq2 v2)
(dq1 dq2) (v1 v2).
Proof.
rewrite view_frag_valid. setoid_rewrite gmap_view_rel_exists.
rewrite -cmra_valid_validN singleton_op singleton_valid.
by rewrite -pair_op pair_valid.
Qed.
Lemma gmap_view_both_dfrac_validN n dp m k dq v :
{n} (gmap_view_auth dp m gmap_view_frag k dq v)
v' dq', dp m !! k = Some v' {n} (dq', v')
Some (dq, v) {n} Some (dq', v').
Proof.
rewrite /gmap_view_auth /gmap_view_frag.
rewrite view_both_dfrac_validN gmap_view_rel_lookup. naive_solver.
Qed.
Lemma gmap_view_both_validN n dp m k v :
{n} (gmap_view_auth dp m gmap_view_frag k (DfracOwn 1) v)
dp {n} v m !! k {n} Some v.
Proof.
rewrite gmap_view_both_dfrac_validN. split.
- intros [Hdp (v' & dq' & Hlookup & Hvalid & Hincl)].
split; first done. rewrite Hlookup.
destruct (Some_includedN_exclusive _ _ _ Hincl Hvalid) as [_ Heq].
simpl in Heq. split.
+ rewrite pair_validN in Hvalid. rewrite Heq. naive_solver.
+ by rewrite Heq.
- intros (Hdp & Hval & Hlookup).
apply dist_Some_inv_r' in Hlookup as [v' [Hlookup Heq]].
exists v', (DfracOwn 1). do 2 (split; [done|]). split.
+ rewrite pair_validN. by rewrite -Heq.
+ by apply: Some_includedN_refl.
Qed.
(** The backwards direction here does not hold: if [dq = DfracOwn 1] but
[v ≠ v'], we have to find a suitable erased fraction [dq'] to satisfy the view
relation, but there is no way to satisfy [Some (DfracOwn 1, v) ≼{n} Some (dq', v')]
for any [dq']. The "if and only if" version of this lemma would have to
involve some extra condition like [dq = DfracOwn 1 → v = v'], or phrased
more like the view relation itself: [∃ dq', ✓ dq' ∧ Some (v, dq) ≼{n} Some (v', dq')]. *)
Lemma gmap_view_both_dfrac_validN_total `{!CmraTotal V} n dp m k dq v :
{n} (gmap_view_auth dp m gmap_view_frag k dq v)
v', dp dq m !! k = Some v' {n} v' v {n} v'.
Proof.
rewrite gmap_view_both_dfrac_validN.
intros (v' & dq' & Hdp & Hlookup & Hvalid & Hincl).
exists v'. split; first done. split.
- eapply (cmra_valid_Some_included dq'); first by apply Hvalid.
eapply cmra_discrete_included_iff.
eapply Some_pair_includedN_l. done.
- split; first done. split; first apply Hvalid.
move:Hincl=> /Some_pair_includedN_r /Some_includedN_total. done.
Qed.
(** Without [CmraDiscrete], we cannot do much better than [∀ n, <same as above>].
This is because both the [dq'] and the witness for the [≼{n}] can be different for
each step-index. It is totally possible that at low step-indices, [v] has a frame
(and [dq' > dq]) while at higher step-indices, [v] has no frame (and [dq' = dq]). *)
Lemma gmap_view_both_dfrac_valid_discrete `{!CmraDiscrete V} 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.
rewrite cmra_valid_validN. setoid_rewrite gmap_view_both_dfrac_validN. split.
- intros Hvalid. specialize (Hvalid 0).
destruct Hvalid as (v' & dq' & Hdp & Hlookup & Hvalid & Hincl).
exists v', dq'. do 2 (split; first done).
split; first by apply cmra_discrete_valid.
by apply: cmra_discrete_included_r.
- intros (v' & dq' & Hdp & Hlookup & Hvalid & Hincl) n.
exists v', dq'. do 2 (split; first done).
split; first by apply cmra_valid_validN.
by apply: cmra_included_includedN.
Qed.
(** The backwards direction here does not hold: if [dq = DfracOwn 1] but
[v ≠ v'], we have to find a suitable erased fraction [dq'] to satisfy the view
relation, but there is no way to satisfy [Some (DfracOwn 1, v) ≼ Some (dq', v')]
for any [dq']. The "if and only if" version of this lemma would have to
involve some extra condition like [dq = DfracOwn 1 → v = v'], or phrased
more like the view relation itself: [∃ dq', ✓ dq' ∧ Some (v, dq) ≼ Some (v', dq')]. *)
Lemma gmap_view_both_dfrac_valid_discrete_total
`{!CmraDiscrete V, !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.
rewrite gmap_view_both_dfrac_valid_discrete.
intros (v' & dq' & Hdp & Hlookup & Hvalid & Hincl).
exists v'. split; first done. split.
- eapply (cmra_valid_Some_included dq'); first by apply Hvalid.
eapply Some_pair_included_l. done.
- split; first done. split; first apply Hvalid.
move:Hincl=> /Some_pair_included_r /Some_included_total. done.
Qed.
(** On the other hand, this one holds for all CMRAs, not just discrete ones. *)
Lemma gmap_view_both_valid m dp k v :
(gmap_view_auth dp m gmap_view_frag k (DfracOwn 1) v)
dp v m !! k Some v.
Proof.
rewrite cmra_valid_validN. setoid_rewrite gmap_view_both_validN. split.
- intros Hvalid. split; last split.
+ eapply (Hvalid 0).
+ apply cmra_valid_validN. intros n. eapply Hvalid.
+ apply equiv_dist. intros n. eapply Hvalid.
- intros (Hdp & Hval & Hlookup). intros n.
split; first done. split.
+ apply cmra_valid_validN. done.
+ rewrite Hlookup. done.
Qed.
(** Frame-preserving updates *)
Lemma gmap_view_alloc m k dq v :
m !! k = None
dq
v
gmap_view_auth (DfracOwn 1) m ~~>
gmap_view_auth (DfracOwn 1) (<[k := v]> m) gmap_view_frag k dq v.
Proof.
intros Hfresh Hdq Hval. apply view_update_alloc=>n bf Hrel j [df va] /=.
rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
- assert (bf !! k = None) as Hbf.
{ destruct (bf !! k) as [[df' va']|] eqn:Hbf; last done.
specialize (Hrel _ _ Hbf). destruct Hrel as (v' & dq' & Hm & _).
exfalso. rewrite Hm in Hfresh. done. }
rewrite lookup_singleton Hbf right_id.
intros [= <- <-]. eexists _, _.
rewrite lookup_insert. split; first done.
split; last by apply: Some_includedN_refl.
split; first done. by eapply cmra_valid_validN.
- rewrite lookup_singleton_ne; last done.
rewrite left_id=>Hbf.
specialize (Hrel _ _ Hbf). destruct Hrel as (v' & ? & Hm & ?).
eexists _, _. split; last done.
rewrite lookup_insert_ne //.
Qed.
Lemma gmap_view_alloc_big m m' dq :
m' ## m
dq
map_Forall (λ k v, v) m'
gmap_view_auth (DfracOwn 1) m ~~>
gmap_view_auth (DfracOwn 1) (m' m)
([^op map] kv m', gmap_view_frag k dq v).
Proof.
intros ?? Hm'.
induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
{ rewrite big_opM_empty left_id_L right_id. done. }
apply map_Forall_insert in Hm' as [??]; last done.
rewrite IH //. rewrite big_opM_insert // assoc.
apply cmra_update_op; last done.
rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); [|done..].
by apply lookup_union_None.
Qed.
Lemma gmap_view_delete m k v :
gmap_view_auth (DfracOwn 1) m gmap_view_frag k (DfracOwn 1) v ~~>
gmap_view_auth (DfracOwn 1) (delete k m).
Proof.
apply view_update_dealloc=>n bf Hrel j [df va] Hbf /=.
destruct (decide (j = k)) as [->|Hne].
- edestruct (Hrel k) as (v' & dq' & ? & Hval & Hincl).
{ rewrite lookup_op Hbf lookup_singleton -Some_op. done. }
eapply (cmra_validN_Some_includedN _ _ _ Hval) in Hincl as Hval'.
exfalso. clear Hval Hincl.
rewrite pair_validN /= in Hval'.
apply: dfrac_full_exclusive. apply Hval'.
- edestruct (Hrel j) as (v' & ? & ? & ?).
{ rewrite lookup_op lookup_singleton_ne // Hbf. done. }
eexists v', _. split; last done.
rewrite lookup_delete_ne //.
Qed.
Lemma gmap_view_delete_big m m' :
gmap_view_auth (DfracOwn 1) m
([^op map] kv m', gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth (DfracOwn 1) (m m').
Proof.
induction m' as [|k v m' ? IH] using map_ind.
{ rewrite right_id_L big_opM_empty right_id //. }
rewrite big_opM_insert //.
rewrite [gmap_view_frag _ _ _ _]comm assoc IH gmap_view_delete.
rewrite -delete_difference. done.
Qed.
(** We do not use [local_update] ([~l~>]) in the premise because we also want
to expose the role of the fractions. *)
Lemma gmap_view_update m k dq v mv' v' dq' :
( n mv f,
m !! k = Some mv
{n} ((dq, v) ? f)
mv {n} v ? (snd <$> f)
{n} ((dq', v') ? f) mv' {n} v' ? (snd <$> f))
gmap_view_auth (DfracOwn 1) m gmap_view_frag k dq v ~~>
gmap_view_auth (DfracOwn 1) (<[k := mv']> m) gmap_view_frag k dq' v'.
Proof.
intros Hup. apply view_update=> n bf Hrel j [df va].
rewrite lookup_op.
destruct (decide (j = k)) as [->|Hne]; last first.
{ (* prove that other keys are unaffected *)
simplify_map_eq. rewrite lookup_singleton_ne //.
(* FIXME simplify_map_eq should have done this *)
rewrite left_id. intros Hbf.
edestruct (Hrel j) as (mva & mdf & Hlookup & Hval & Hincl).
{ rewrite lookup_op lookup_singleton_ne // left_id //. }
naive_solver. }
simplify_map_eq. rewrite lookup_singleton.
(* FIXME simplify_map_eq should have done this *)
intros Hbf.
edestruct (Hrel k) as (mv & mdf & Hlookup & Hval & Hincl).
{ rewrite lookup_op lookup_singleton // Some_op_opM //. }
rewrite Some_includedN_opM in Hincl.
destruct Hincl as [f' Hincl]. rewrite cmra_opM_opM_assoc in Hincl.
set f := bf !! k f'. (* the complete frame *)
change (bf !! k f') with f in Hincl.
specialize (Hup n mv f). destruct Hup as (Hval' & Hincl').
{ done. }
{ rewrite -Hincl. done. }
{ destruct Hincl as [_ Hincl]. simpl in Hincl. rewrite Hincl.
by destruct f. }
eexists mv', (dq' ? (fst <$> f)). split; first done.
rewrite -Hbf. clear Hbf. split.
- rewrite Hincl'. destruct Hval'. by destruct f.
- rewrite Some_op_opM. rewrite Some_includedN_opM.
exists f'. rewrite Hincl'.
rewrite cmra_opM_opM_assoc. change (bf !! k f') with f.
by destruct f.
Qed.
(** This derived version cannot exploit [dq = DfracOwn 1]. *)
Lemma gmap_view_update_local m k dq mv v mv' v' :
m !! k = Some mv
(mv, v) ~l~> (mv', v')
gmap_view_auth (DfracOwn 1) m gmap_view_frag k dq v ~~>
gmap_view_auth (DfracOwn 1) (<[k := mv']> m) gmap_view_frag k dq v'.
Proof.
intros Hlookup Hup. apply gmap_view_update.
intros n mv0 f Hmv0 Hval Hincl.
rewrite Hlookup in Hmv0. injection Hmv0 as [= <-].
specialize (Hup n (snd <$> f)). destruct Hup as (Hval' & Hincl').
{ rewrite Hincl. destruct Hval. by destruct f. }
{ simpl. done. }
split; last done. split.
- destruct Hval. by destruct f.
- simpl in *. replace (((dq, v') ? f).2) with (v' ? (snd <$> f)).
2:{ by destruct f. }
rewrite -Hincl'. done.
Qed.
Lemma gmap_view_replace m k v v' :
v'
gmap_view_auth (DfracOwn 1) m gmap_view_frag k (DfracOwn 1) v ~~>
gmap_view_auth (DfracOwn 1) (<[k := v']> m) gmap_view_frag k (DfracOwn 1) v'.
Proof.
(* There would be a simple proof via delete-then-insert... but we use this as a
sanity check to make sure the update lemma is strong enough. *)
intros Hval'. apply gmap_view_update.
intros n mv f Hlookup Hval Hincl.
destruct f; simpl.
{ apply exclusiveN_l in Hval; first done. apply _. }
split; last done.
split; first done. simpl. apply cmra_valid_validN. done.
Qed.
Lemma gmap_view_replace_big m m0 m1 :
dom m0 = dom m1
map_Forall (λ k v, v) m1
gmap_view_auth (DfracOwn 1) m
([^op map] kv m0, gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth (DfracOwn 1) (m1 m)
([^op map] kv m1, gmap_view_frag k (DfracOwn 1) v).
Proof.
intros Hdom%eq_sym. revert m1 Hdom.
induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom Hval.
{ rewrite dom_empty_L in Hdom.
apply dom_empty_iff_L in Hdom as ->.
rewrite left_id_L big_opM_empty. done. }
rewrite dom_insert_L in Hdom.
assert (k dom m1) as Hindom by set_solver.
apply elem_of_dom in Hindom as [v' Hlookup].
rewrite big_opM_insert //.
rewrite [gmap_view_frag _ _ _ _]comm assoc.
rewrite (IH (delete k m1)); last first.
{ by apply map_Forall_delete. }
{ rewrite dom_delete_L Hdom.
apply not_elem_of_dom in Hnotdom. set_solver -Hdom. }
rewrite -assoc [_ gmap_view_frag _ _ _]comm assoc.
rewrite (gmap_view_replace _ _ _ v').
2:{ eapply Hval. done. }
rewrite (big_opM_delete _ m1 k v') // -assoc.
rewrite insert_union_r; last by rewrite lookup_delete.
rewrite union_delete_insert //.
Qed.
Lemma gmap_view_auth_persist dq m :
gmap_view_auth dq m ~~> gmap_view_auth DfracDiscarded m.
Proof. apply view_update_auth_persist. Qed.
Lemma gmap_view_auth_unpersist m :
gmap_view_auth DfracDiscarded m ~~>: λ a, q, a = gmap_view_auth (DfracOwn q) m.
Proof. apply view_updateP_auth_unpersist. Qed.
Local Lemma gmap_view_frag_dfrac k dq P v :
dq ~~>: P
gmap_view_frag k dq v ~~>: λ a, dq', a = gmap_view_frag k dq' v P dq'.
Proof.
intros Hdq.
eapply cmra_updateP_weaken;
[apply view_updateP_frag
with (P := λ b', dq', V b' = gmap_view_frag k dq' v P dq')
|naive_solver].
intros m n bf Hrel.
destruct (Hrel k ((dq, v) ? bf !! k)) as (v' & dq' & Hlookup & Hval & Hincl).
{ by rewrite lookup_op lookup_singleton Some_op_opM. }
rewrite Some_includedN_opM in Hincl.
destruct Hincl as [f' Hincl]. rewrite cmra_opM_opM_assoc in Hincl.
set f := bf !! k f'. (* the complete frame *)
change (bf !! k f') with f in Hincl.
destruct (Hdq n (option_map fst f)) as (dq'' & HPdq'' & Hvdq'').
{ destruct Hincl as [Heq _]. simpl in Heq. rewrite Heq in Hval.
destruct Hval as [Hval _]. by destruct f. }
eexists. split; first by exists dq''.
intros j [df va] Heq.
destruct (decide (k = j)) as [->|Hne].
- rewrite lookup_op lookup_singleton in Heq.
eexists v', (dq'' ? (fst <$> f)).
split; first done. split.
+ split; last by apply Hval. simpl. done.
+ rewrite -Heq. exists f'.
rewrite -assoc. change (bf !! j f') with f.
destruct Hincl as [_ Hincl]. simpl in Hincl. rewrite Hincl.
by destruct f.
- rewrite lookup_op lookup_singleton_ne // left_id in Heq.
eapply Hrel. rewrite lookup_op lookup_singleton_ne // left_id Heq //.
Qed.
Lemma gmap_view_frag_persist k dq v :
gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
Proof.
eapply (cmra_update_lift_updateP (λ dq, gmap_view_frag k dq v)).
- intros. by apply gmap_view_frag_dfrac.
- apply dfrac_discard_update.
Qed.
Lemma gmap_view_frag_unpersist k v :
gmap_view_frag k DfracDiscarded v ~~>:
λ a, q, a = gmap_view_frag k (DfracOwn q) v.
Proof.
eapply cmra_updateP_weaken.
{ apply gmap_view_frag_dfrac, dfrac_undiscard_update. }
naive_solver.
Qed.
(** Typeclass instances *)
Global Instance gmap_view_frag_core_id k dq v :
CoreId dq CoreId v CoreId (gmap_view_frag k dq v).
Proof. apply _. Qed.
Global Instance gmap_view_cmra_discrete :
CmraDiscrete V CmraDiscrete (gmap_viewR K V).
Proof. apply _. Qed.
Global Instance gmap_view_frag_mut_is_op dq dq1 dq2 k v v1 v2 :
IsOp dq dq1 dq2
IsOp v v1 v2
IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v1) (gmap_view_frag k dq2 v2).
Proof. rewrite /IsOp' /IsOp => -> ->. apply gmap_view_frag_op. Qed.
End lemmas.
(** Functor *)
Program Definition gmap_viewURF {SI : sidx} (K : Type) `{Countable K}
(F : rFunctor) : urFunctor := {|
urFunctor_car A _ B _ := gmap_viewUR K (rFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
viewO_map (rel:=gmap_view_rel K (rFunctor_car F A1 B1))
(rel':=gmap_view_rel K (rFunctor_car F A2 B2))
(gmapO_map (K:=K) (rFunctor_map F fg))
(gmapO_map (K:=K) (prodO_map cid (rFunctor_map F fg)))
|}.
Next Obligation.
intros ? K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
apply viewO_map_ne.
- apply gmapO_map_ne, rFunctor_map_ne. done.
- apply gmapO_map_ne. apply prodO_map_ne; first done.
apply rFunctor_map_ne. done.
Qed.
Next Obligation.
intros ? K ? ? F A ? B ? m; simpl in *. rewrite -{2}(view_map_id m).
apply (view_map_ext _ _ _ _)=> y.
- rewrite /= -{2}(map_fmap_id y).
apply: map_fmap_equiv_ext=>k ??.
apply rFunctor_map_id.
- rewrite /= -{2}(map_fmap_id y).
apply: map_fmap_equiv_ext=>k [df va] ?.
split; first done. simpl.
apply rFunctor_map_id.
Qed.
Next Obligation.
intros ? K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' m; simpl in *.
rewrite -view_map_compose.
apply (view_map_ext _ _ _ _)=> y.
- rewrite /= -map_fmap_compose.
apply: map_fmap_equiv_ext=>k ??.
apply rFunctor_map_compose.
- rewrite /= -map_fmap_compose.
apply: map_fmap_equiv_ext=>k [df va] ?.
split; first done. simpl.
apply rFunctor_map_compose.
Qed.
Next Obligation.
intros ? K ?? F A1 ? A2 ? B1 ? B2 ? fg; simpl.
(* [apply] does not work, probably the usual unification probem (Coq #6294) *)
eapply @view_map_cmra_morphism; [apply _..|]=> n m f.
intros Hrel k [df va] Hf. move: Hf.
rewrite !lookup_fmap.
destruct (f !! k) as [[df' va']|] eqn:Hfk; rewrite Hfk; last done.
simpl=>[= <- <-].
specialize (Hrel _ _ Hfk). simpl in Hrel.
destruct Hrel as (v & dq & Hlookup & Hval & Hincl).
eexists (rFunctor_map F fg v), dq.
rewrite Hlookup. split; first done. split.
- split; first by apply Hval. simpl. apply: cmra_morphism_validN. apply Hval.
- destruct Hincl as [[[fdq fv]|] Hincl].
+ apply: Some_includedN_mono. rewrite -Some_op in Hincl.
apply (inj _) in Hincl. rewrite -pair_op in Hincl.
exists (fdq, rFunctor_map F fg fv). rewrite -pair_op.
split; first apply Hincl. rewrite -cmra_morphism_op.
simpl. f_equiv. apply Hincl.
+ exists None. rewrite right_id in Hincl. apply (inj _) in Hincl.
rewrite right_id. f_equiv. split; first apply Hincl.
simpl. f_equiv. apply Hincl.
Qed.
Global Instance gmap_viewURF_contractive {SI : sidx} `{Countable K} F :
rFunctorContractive F urFunctorContractive (gmap_viewURF K F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
apply viewO_map_ne.
- apply gmapO_map_ne. apply rFunctor_map_contractive. done.
- apply gmapO_map_ne. apply prodO_map_ne; first done.
apply rFunctor_map_contractive. done.
Qed.
Program Definition gmap_viewRF {SI : sidx} (K : Type) `{Countable K}
(F : rFunctor) : rFunctor := {|
rFunctor_car A _ B _ := gmap_viewR K (rFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
viewO_map (rel:=gmap_view_rel K (rFunctor_car F A1 B1))
(rel':=gmap_view_rel K (rFunctor_car F A2 B2))
(gmapO_map (K:=K) (rFunctor_map F fg))
(gmapO_map (K:=K) (prodO_map cid (rFunctor_map F fg)))
|}.
Solve Obligations with apply @gmap_viewURF.
Global Instance gmap_viewRF_contractive {SI : sidx} `{Countable K} F :
rFunctorContractive F rFunctorContractive (gmap_viewRF K F).
Proof. apply gmap_viewURF_contractive. Qed.
Global Typeclasses Opaque gmap_view_auth gmap_view_frag.
(** RA for monotone partial bijections.
This RA is a view where the authoritative element is a partial bijection between
types [A] and [B] and the fragments are subrels of the bijection. The data for
the bijection is represented as a set of pairs [A * B], and the view relation
enforces when an authoritative element is valid it is a bijection (that is, it
is deterministic as a function from [A → option B] and [B → option A]).
The fragments compose by set union, which means that fragments are their own
core, ownership of a fragment is persistent, and the authoritative element can
only grow (in that it can only map more pairs [(a,b)]). *)
(* [algebra.view] needs to be exported for the canonical instances *)
From iris.algebra Require Export view gset.
From iris.algebra Require Import updates.
From iris.prelude Require Import options.
Section gset_bijective.
Context {SI : sidx} `{Countable A, Countable B}.
Implicit Types (a : A) (b : B).
(** [gset_bijective] states that for a graph [L] of [(a, b)] pairs, [L] maps
from [A] to [B] and back deterministically. The key property characterizing
[gset_bijective] is [gset_bijective_eq_iff]. *)
Definition gset_bijective (L : gset (A * B)) :=
a b, (a, b) L
( b', (a, b') L b' = b) ( a', (a', b) L a' = a).
(* Properties of [gset_bijective]. *)
Lemma gset_bijective_empty : gset_bijective ( : gset (A * B)).
Proof. by intros ?? []%not_elem_of_empty. Qed.
(* a bijective graph [L] can be extended with a new mapping [(a,b)] as long as
neither [a] nor [b] is currently mapped to anything. *)
Lemma gset_bijective_extend L a b :
gset_bijective L
( b', (a, b') L)
( a', (a', b) L)
gset_bijective ({[(a, b)]} L).
Proof. rewrite /gset_bijective. set_solver. Qed.
Lemma gset_bijective_eq_iff L (a1 a2 : A) (b1 b2 : B) :
gset_bijective L
(a1, b1) L
(a2, b2) L
a1 = a2 b1 = b2.
Proof. rewrite /gset_bijective. set_solver. Qed.
Lemma gset_bijective_pair a1 b1 a2 b2 :
gset_bijective {[(a1, b1); (a2, b2)]}
(a1 = a2 b1 = b2).
Proof. rewrite /gset_bijective. set_solver. Qed.
Lemma subseteq_gset_bijective L L' :
gset_bijective L
L' L
gset_bijective L'.
Proof. rewrite /gset_bijective. set_solver. Qed.
End gset_bijective.
Section gset_bij_view_rel.
Context {SI : sidx} `{Countable A, Countable B}.
Implicit Types (bijL : gset (A * B)) (L : gsetUR (A * B)).
Local Definition gset_bij_view_rel_raw (n : SI) bijL L: Prop :=
L bijL gset_bijective bijL.
Local Lemma gset_bij_view_rel_raw_mono n1 n2 bijL1 bijL2 L1 L2 :
gset_bij_view_rel_raw n1 bijL1 L1
bijL1 {n2} bijL2
L2 {n2} L1
(n2 n1)%sidx
gset_bij_view_rel_raw n2 bijL2 L2.
Proof.
intros [??] <-%(discrete_iff _ _)%leibniz_equiv ?%gset_included _.
split; [|done]. by trans L1.
Qed.
Local Lemma gset_bij_view_rel_raw_valid n bijL L :
gset_bij_view_rel_raw n bijL L {n}L.
Proof. by intros _. Qed.
Local Lemma gset_bij_view_rel_raw_unit n :
bijL, gset_bij_view_rel_raw n bijL ε.
Proof. exists ∅. split; eauto using gset_bijective_empty. Qed.
Canonical Structure gset_bij_view_rel : view_rel (gsetO (A * B)) (gsetUR (A * B)) :=
ViewRel gset_bij_view_rel_raw gset_bij_view_rel_raw_mono
gset_bij_view_rel_raw_valid gset_bij_view_rel_raw_unit.
Global Instance gset_bij_view_rel_discrete : ViewRelDiscrete gset_bij_view_rel.
Proof. intros n bijL L [??]. split; auto. Qed.
Local Lemma gset_bij_view_rel_iff n bijL L :
gset_bij_view_rel n bijL L L bijL gset_bijective bijL.
Proof. done. Qed.
End gset_bij_view_rel.
Definition gset_bij {SI : sidx} A B `{Countable A, Countable B} :=
view (gset_bij_view_rel_raw (A:=A) (B:=B)).
Definition gset_bijO {SI : sidx} A B `{Countable A, Countable B} : ofe :=
viewO (gset_bij_view_rel (A:=A) (B:=B)).
Definition gset_bijR {SI : sidx} A B `{Countable A, Countable B} : cmra :=
viewR (gset_bij_view_rel (A:=A) (B:=B)).
Definition gset_bijUR {SI : sidx} A B `{Countable A, Countable B} : ucmra :=
viewUR (gset_bij_view_rel (A:=A) (B:=B)).
Definition gset_bij_auth {SI : sidx} `{Countable A, Countable B}
(dq : dfrac) (L : gset (A * B)) : gset_bij A B := V{dq} L V L.
Definition gset_bij_elem {SI : sidx} `{Countable A, Countable B}
(a : A) (b : B) : gset_bij A B := V {[ (a, b) ]}.
Section gset_bij.
Context {SI : sidx} `{Countable A, Countable B}.
Implicit Types (a : A) (b : B).
Implicit Types (L : gset (A*B)).
Implicit Types dq : dfrac.
Global Instance gset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
Proof. apply _. Qed.
Lemma gset_bij_auth_dfrac_op dq1 dq2 L :
gset_bij_auth dq1 L gset_bij_auth dq2 L gset_bij_auth (dq1 dq2) L.
Proof.
rewrite /gset_bij_auth view_auth_dfrac_op.
rewrite (comm _ (V{dq2} _)) -!assoc (assoc _ (V _)).
by rewrite -core_id_dup (comm _ (V _)).
Qed.
Lemma gset_bij_auth_dfrac_valid dq L : gset_bij_auth dq L dq gset_bijective L.
Proof.
rewrite /gset_bij_auth view_both_dfrac_valid.
setoid_rewrite gset_bij_view_rel_iff. pose 0. naive_solver.
Qed.
Lemma gset_bij_auth_valid L : gset_bij_auth (DfracOwn 1) L gset_bijective L.
Proof. rewrite gset_bij_auth_dfrac_valid. naive_solver by done. Qed.
Lemma gset_bij_auth_empty_dfrac_valid dq : gset_bij_auth (A:=A) (B:=B) dq dq.
Proof.
rewrite gset_bij_auth_dfrac_valid. naive_solver eauto using gset_bijective_empty.
Qed.
Lemma gset_bij_auth_empty_valid : gset_bij_auth (A:=A) (B:=B) (DfracOwn 1) ∅.
Proof. by apply gset_bij_auth_empty_dfrac_valid. Qed.
Lemma gset_bij_auth_dfrac_op_valid dq1 dq2 L1 L2 :
(gset_bij_auth dq1 L1 gset_bij_auth dq2 L2)
(dq1 dq2) L1 = L2 gset_bijective L1.
Proof.
rewrite /gset_bij_auth (comm _ (V{dq2} _)) -!assoc (assoc _ (V _)).
rewrite -view_frag_op (comm _ (V _)) assoc. split.
- move=> /cmra_valid_op_l /view_auth_dfrac_op_valid.
setoid_rewrite gset_bij_view_rel_iff. pose 0. naive_solver.
- intros (?&->&?). rewrite -core_id_dup -view_auth_dfrac_op.
apply view_both_dfrac_valid. setoid_rewrite gset_bij_view_rel_iff. naive_solver.
Qed.
Lemma gset_bij_auth_op_valid L1 L2 :
(gset_bij_auth (DfracOwn 1) L1 gset_bij_auth (DfracOwn 1) L2) False.
Proof. rewrite gset_bij_auth_dfrac_op_valid. naive_solver. Qed.
Lemma bij_both_dfrac_valid dq L a b :
(gset_bij_auth dq L gset_bij_elem a b) dq gset_bijective L (a, b) L.
Proof.
rewrite /gset_bij_auth /gset_bij_elem -assoc -view_frag_op view_both_dfrac_valid.
setoid_rewrite gset_bij_view_rel_iff. pose 0. set_solver.
Qed.
Lemma bij_both_valid L a b :
(gset_bij_auth (DfracOwn 1) L gset_bij_elem a b) gset_bijective L (a, b) L.
Proof. rewrite bij_both_dfrac_valid. naive_solver by done. Qed.
Lemma gset_bij_elem_agree a1 b1 a2 b2 :
(gset_bij_elem a1 b1 gset_bij_elem a2 b2) (a1 = a2 b1 = b2).
Proof.
rewrite /gset_bij_elem -view_frag_op gset_op view_frag_valid.
setoid_rewrite gset_bij_view_rel_iff. intros. apply gset_bijective_pair.
pose 0. naive_solver eauto using subseteq_gset_bijective.
Qed.
Lemma bij_view_included dq L a b :
(a,b) L gset_bij_elem a b gset_bij_auth dq L.
Proof.
intros. etrans; [|apply cmra_included_r].
apply view_frag_mono, gset_included. set_solver.
Qed.
Lemma gset_bij_auth_extend {L} a b :
( b', (a, b') L) ( a', (a', b) L)
gset_bij_auth (DfracOwn 1) L ~~> gset_bij_auth (DfracOwn 1) ({[(a, b)]} L).
Proof.
intros. apply view_update=> n bijL.
rewrite !gset_bij_view_rel_iff gset_op.
set_solver by eauto using gset_bijective_extend.
Qed.
End gset_bij.
From iris.algebra Require Export auth.
From iris.algebra Require Import numbers updates.
From iris.prelude Require Import options.
(** Authoritative CMRA over [max_Z]. The authoritative element is a
monotonically increasing [Z], while a fragment is a lower bound. *)
Definition mono_Z {SI: sidx} := auth (option max_ZR).
Definition mono_ZR {SI: sidx} := authR (optionUR max_ZR).
Definition mono_ZUR {SI: sidx} := authUR (optionUR max_ZR).
(** [mono_Z_auth] is the authoritative element. The definition includes the
fragment at the same value so that lemma [mono_Z_included], which states that
[mono_Z_lb n ≼ mono_Z_auth dq n], holds. Without this trick, a frame-preserving
update lemma would be required instead. *)
Definition mono_Z_auth {SI : sidx} (dq : dfrac) (n : Z) : mono_Z :=
{dq} (Some (MaxZ n)) (Some (MaxZ n)).
Definition mono_Z_lb {SI : sidx} (n : Z) : mono_Z := (Some (MaxZ n)).
Notation "●MZ dq a" := (mono_Z_auth dq a)
(at level 20, dq custom dfrac at level 1, format "●MZ dq a").
Notation "◯MZ a" := (mono_Z_lb a) (at level 20).
Section mono_Z.
Context {SI : sidx}.
Implicit Types (n : Z).
Local Open Scope Z_scope.
Global Instance mono_Z_lb_core_id n : CoreId (MZ n).
Proof. apply _. Qed.
Global Instance mono_Z_auth_core_id l : CoreId (MZ l).
Proof. apply _. Qed.
Lemma mono_Z_auth_dfrac_op dq1 dq2 n :
MZ{dq1 dq2} n MZ{dq1} n MZ{dq2} n.
Proof.
rewrite /mono_Z_auth auth_auth_dfrac_op.
rewrite (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
by rewrite -core_id_dup (comm _ ( _)).
Qed.
Lemma mono_Z_lb_op n1 n2 :
MZ (n1 `max` n2) = MZ n1 MZ n2.
Proof. rewrite -auth_frag_op -Some_op max_Z_op //. Qed.
Lemma mono_Z_auth_lb_op dq n :
MZ{dq} n MZ{dq} n MZ n.
Proof.
rewrite /mono_Z_auth /mono_Z_lb.
rewrite -!assoc -auth_frag_op -Some_op max_Z_op.
rewrite Z.max_id //.
Qed.
Global Instance mono_Z_auth_dfrac_is_op dq dq1 dq2 n :
IsOp dq dq1 dq2 IsOp' (MZ{dq} n) (MZ{dq1} n) (MZ{dq2} n).
Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_Z_auth_dfrac_op //. Qed.
Global Instance mono_Z_lb_max_is_op n n1 n2 :
IsOp (MaxZ n) (MaxZ n1) (MaxZ n2) IsOp' (MZ n) (MZ n1) (MZ n2).
Proof. rewrite /IsOp' /IsOp /mono_Z_lb=> ->. done. Qed.
(** rephrasing of [mono_Z_lb_op] useful for weakening a fragment to a
smaller lower-bound *)
Lemma mono_Z_lb_op_le_l n n' :
n' n
MZ n = MZ n' MZ n.
Proof. intros. rewrite -mono_Z_lb_op Z.max_r //. Qed.
Lemma mono_Z_auth_dfrac_valid dq n : ( MZ{dq} n) dq.
Proof.
rewrite /mono_Z_auth auth_both_dfrac_valid_discrete /=. naive_solver.
Qed.
Lemma mono_Z_auth_valid n : MZ n.
Proof. by apply auth_both_valid. Qed.
Lemma mono_Z_auth_dfrac_op_valid dq1 dq2 n1 n2 :
(MZ{dq1} n1 MZ{dq2} n2) (dq1 dq2) n1 = n2.
Proof.
rewrite /mono_Z_auth (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
rewrite -auth_frag_op (comm _ ( _)) assoc. split.
- move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
- intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
by apply auth_both_dfrac_valid_discrete.
Qed.
Lemma mono_Z_auth_op_valid n1 n2 :
(MZ n1 MZ n2) False.
Proof. rewrite mono_Z_auth_dfrac_op_valid. naive_solver. Qed.
Lemma mono_Z_both_dfrac_valid dq n m :
(MZ{dq} n MZ m) dq m n.
Proof.
rewrite /mono_Z_auth /mono_Z_lb -assoc -auth_frag_op.
rewrite auth_both_dfrac_valid_discrete Some_included_total max_Z_included /=.
naive_solver lia.
Qed.
Lemma mono_Z_both_valid n m :
(MZ n MZ m) m n.
Proof. rewrite mono_Z_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
Lemma mono_Z_lb_mono n1 n2 : n1 n2 MZ n1 MZ n2.
Proof.
intros. by apply auth_frag_mono, Some_included_total, max_Z_included.
Qed.
Lemma mono_Z_included dq n : MZ n MZ{dq} n.
Proof. apply: cmra_included_r. Qed.
Lemma mono_Z_update {n} n' :
n n' MZ n ~~> MZ n'.
Proof.
intros. rewrite /mono_Z_auth /mono_Z_lb.
by apply auth_update, option_local_update, max_Z_local_update.
Qed.
Lemma mono_Z_auth_persist n dq :
MZ{dq} n ~~> MZ n.
Proof.
intros. rewrite /mono_Z_auth /mono_Z_lb.
eapply cmra_update_op_proper; last done.
eapply auth_update_auth_persist.
Qed.
Lemma mono_Z_auth_unpersist n :
MZ n ~~>: λ k, q, k = MZ{# q} n.
Proof. eapply auth_updateP_both_unpersist. Qed.
End mono_Z.
Global Typeclasses Opaque mono_Z_auth mono_Z_lb.
(** Authoritative CMRA of append-only lists, where the fragment represents a
snap-shot of the list, and the authoritative element can only grow by
appending. *)
From iris.algebra Require Export auth dfrac max_prefix_list.
From iris.algebra Require Import updates local_updates proofmode_classes.
From iris.prelude Require Import options.
Definition mono_listR {SI : sidx} (A : ofe) : cmra := authR (max_prefix_listUR A).
Definition mono_listUR {SI : sidx} (A : ofe) : ucmra := authUR (max_prefix_listUR A).
Definition mono_list_auth {SI : sidx}
{A : ofe} (q : dfrac) (l : list A) : mono_listR A :=
{q} (to_max_prefix_list l) (to_max_prefix_list l).
Definition mono_list_lb {SI : sidx} {A : ofe} (l : list A) : mono_listR A :=
(to_max_prefix_list l).
Global Instance: Params (@mono_list_auth) 3 := {}.
Global Instance: Params (@mono_list_lb) 2 := {}.
Global Typeclasses Opaque mono_list_auth mono_list_lb.
Notation "●ML dq l" := (mono_list_auth dq l)
(at level 20, dq custom dfrac at level 1, format "●ML dq l").
Notation "◯ML l" := (mono_list_lb l) (at level 20).
Section mono_list_props.
Context {SI : sidx} {A : ofe}.
Implicit Types l : list A.
Implicit Types q : frac.
Implicit Types dq : dfrac.
(** Setoid properties *)
Global Instance mono_list_auth_ne dq : NonExpansive (@mono_list_auth SI A dq).
Proof. solve_proper. Qed.
Global Instance mono_list_auth_proper dq :
Proper (() ==> ()) (@mono_list_auth SI A dq).
Proof. solve_proper. Qed.
Global Instance mono_list_lb_ne : NonExpansive (@mono_list_lb SI A).
Proof. solve_proper. Qed.
Global Instance mono_list_lb_proper : Proper (() ==> ()) (@mono_list_lb SI A).
Proof. solve_proper. Qed.
Global Instance mono_list_lb_dist_inj n :
Inj (dist n) (dist n) (@mono_list_lb SI A).
Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.
Global Instance mono_list_lb_inj : Inj () () (@mono_list_lb SI A).
Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.
(** * Operation *)
Global Instance mono_list_lb_core_id l : CoreId (ML l).
Proof. rewrite /mono_list_lb. apply _. Qed.
Global Instance mono_list_auth_core_id l : CoreId (ML l).
Proof. rewrite /mono_list_auth. apply _. Qed.
Lemma mono_list_auth_dfrac_op dq1 dq2 l :
ML{dq1 dq2} l ML{dq1} l ML{dq2} l.
Proof.
rewrite /mono_list_auth auth_auth_dfrac_op.
rewrite (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
by rewrite -core_id_dup (comm _ ( _)).
Qed.
Lemma mono_list_lb_op_l l1 l2 : l1 `prefix_of` l2 ML l1 ML l2 ML l2.
Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_l. Qed.
Lemma mono_list_lb_op_r l1 l2 : l1 `prefix_of` l2 ML l2 ML l1 ML l2.
Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_r. Qed.
Lemma mono_list_auth_lb_op dq l : ML{dq} l ML{dq} l ML l.
Proof.
by rewrite /mono_list_auth /mono_list_lb -!assoc -auth_frag_op -core_id_dup.
Qed.
Global Instance mono_list_auth_dfrac_is_op dq dq1 dq2 l :
IsOp dq dq1 dq2 IsOp' (ML{dq} l) (ML{dq1} l) (ML{dq2} l).
Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_list_auth_dfrac_op //. Qed.
(** * Validity *)
Lemma mono_list_auth_dfrac_validN n dq l : {n} (ML{dq} l) dq.
Proof.
rewrite /mono_list_auth auth_both_dfrac_validN.
naive_solver apply to_max_prefix_list_validN.
Qed.
Lemma mono_list_auth_validN n l : {n} (ML l).
Proof. by apply mono_list_auth_dfrac_validN. Qed.
Lemma mono_list_auth_dfrac_valid dq l : (ML{dq} l) dq.
Proof.
rewrite /mono_list_auth auth_both_dfrac_valid.
naive_solver apply to_max_prefix_list_valid.
Qed.
Lemma mono_list_auth_valid l : (ML l).
Proof. by apply mono_list_auth_dfrac_valid. Qed.
Lemma mono_list_auth_dfrac_op_validN n dq1 dq2 l1 l2 :
{n} (ML{dq1} l1 ML{dq2} l2) (dq1 dq2) l1 {n} l2.
Proof.
rewrite /mono_list_auth (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
rewrite -auth_frag_op (comm _ ( _)) assoc. split.
- move=> /cmra_validN_op_l /auth_auth_dfrac_op_validN.
rewrite (inj_iff to_max_prefix_list). naive_solver.
- intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op auth_both_dfrac_validN.
naive_solver apply to_max_prefix_list_validN.
Qed.
Lemma mono_list_auth_op_validN n l1 l2 : {n} (ML l1 ML l2) False.
Proof. rewrite mono_list_auth_dfrac_op_validN. naive_solver. Qed.
Lemma mono_list_auth_dfrac_op_valid dq1 dq2 l1 l2 :
(ML{dq1} l1 ML{dq2} l2) (dq1 dq2) l1 l2.
Proof.
rewrite cmra_valid_validN equiv_dist.
setoid_rewrite mono_list_auth_dfrac_op_validN. pose 0. naive_solver.
Qed.
Lemma mono_list_auth_op_valid l1 l2 : (ML l1 ML l2) False.
Proof. rewrite mono_list_auth_dfrac_op_valid. naive_solver. Qed.
Lemma mono_list_auth_dfrac_op_valid_L `{!LeibnizEquiv A} dq1 dq2 l1 l2 :
(ML{dq1} l1 ML{dq2} l2) (dq1 dq2) l1 = l2.
Proof. unfold_leibniz. apply mono_list_auth_dfrac_op_valid. Qed.
Lemma mono_list_both_dfrac_validN n dq l1 l2 :
{n} (ML{dq} l1 ML l2) dq l, l1 {n} l2 ++ l.
Proof.
rewrite /mono_list_auth /mono_list_lb -assoc
-auth_frag_op auth_both_dfrac_validN -to_max_prefix_list_includedN.
f_equiv; split.
- intros [Hincl _]. etrans; [apply: cmra_includedN_r|done].
- intros. split; [|by apply to_max_prefix_list_validN].
rewrite {2}(core_id_dup (to_max_prefix_list l1)). by f_equiv.
Qed.
Lemma mono_list_both_validN n l1 l2 :
{n} (ML l1 ML l2) l, l1 {n} l2 ++ l.
Proof. rewrite mono_list_both_dfrac_validN. split; [naive_solver|done]. Qed.
Lemma mono_list_both_dfrac_valid dq l1 l2 :
(ML{dq} l1 ML l2) dq l, l1 l2 ++ l.
Proof.
rewrite /mono_list_auth /mono_list_lb -assoc -auth_frag_op
auth_both_dfrac_valid -max_prefix_list_included_includedN
-to_max_prefix_list_included.
f_equiv; split.
- intros [Hincl _]. etrans; [apply: cmra_included_r|done].
- intros. split; [|by apply to_max_prefix_list_valid].
rewrite {2}(core_id_dup (to_max_prefix_list l1)). by f_equiv.
Qed.
Lemma mono_list_both_valid l1 l2 :
(ML l1 ML l2) l, l1 l2 ++ l.
Proof. rewrite mono_list_both_dfrac_valid. split; [naive_solver|done]. Qed.
Lemma mono_list_both_dfrac_valid_L `{!LeibnizEquiv A} dq l1 l2 :
(ML{dq} l1 ML l2) dq l2 `prefix_of` l1.
Proof. rewrite /prefix. rewrite mono_list_both_dfrac_valid. naive_solver. Qed.
Lemma mono_list_both_valid_L `{!LeibnizEquiv A} l1 l2 :
(ML l1 ML l2) l2 `prefix_of` l1.
Proof. rewrite /prefix. rewrite mono_list_both_valid. naive_solver. Qed.
Lemma mono_list_lb_op_validN n l1 l2 :
{n} (ML l1 ML l2) ( l, l2 {n} l1 ++ l) ( l, l1 {n} l2 ++ l).
Proof. by rewrite auth_frag_op_validN to_max_prefix_list_op_validN. Qed.
Lemma mono_list_lb_op_valid l1 l2 :
(ML l1 ML l2) ( l, l2 l1 ++ l) ( l, l1 l2 ++ l).
Proof. by rewrite auth_frag_op_valid to_max_prefix_list_op_valid. Qed.
Lemma mono_list_lb_op_valid_L `{!LeibnizEquiv A} l1 l2 :
(ML l1 ML l2) l1 `prefix_of` l2 l2 `prefix_of` l1.
Proof. rewrite mono_list_lb_op_valid / prefix. naive_solver. Qed.
Lemma mono_list_lb_op_valid_1_L `{!LeibnizEquiv A} l1 l2 :
(ML l1 ML l2) l1 `prefix_of` l2 l2 `prefix_of` l1.
Proof. by apply mono_list_lb_op_valid_L. Qed.
Lemma mono_list_lb_op_valid_2_L `{!LeibnizEquiv A} l1 l2 :
l1 `prefix_of` l2 l2 `prefix_of` l1 (ML l1 ML l2).
Proof. by apply mono_list_lb_op_valid_L. Qed.
Lemma mono_list_lb_mono l1 l2 : l1 `prefix_of` l2 ML l1 ML l2.
Proof. intros. exists (ML l2). by rewrite mono_list_lb_op_l. Qed.
Lemma mono_list_included dq l : ML l ML{dq} l.
Proof. apply cmra_included_r. Qed.
(** * Update *)
Lemma mono_list_update {l1} l2 : l1 `prefix_of` l2 ML l1 ~~> ML l2.
Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed.
Lemma mono_list_auth_persist dq l : ML{dq} l ~~> ML l.
Proof.
rewrite /mono_list_auth. apply cmra_update_op; [|done].
by apply auth_update_auth_persist.
Qed.
Lemma mono_list_auth_unpersist l :
ML l ~~>: λ k, q, k = ML{#q} l.
Proof. eapply auth_updateP_both_unpersist. Qed.
End mono_list_props.
Definition mono_listURF {SI : sidx} (F : oFunctor) : urFunctor :=
authURF (max_prefix_listURF F).
Global Instance mono_listURF_contractive {SI : sidx} F :
oFunctorContractive F urFunctorContractive (mono_listURF F).
Proof. apply _. Qed.
Definition mono_listRF {SI : sidx} (F : oFunctor) : rFunctor :=
authRF (max_prefix_listURF F).
Global Instance mono_listRF_contractive {SI : sidx} F :
oFunctorContractive F rFunctorContractive (mono_listRF F).
Proof. apply _. Qed.
From iris.algebra Require Export auth.
From iris.algebra Require Import numbers updates.
From iris.prelude Require Import options.
(** Authoritative CMRA over [max_nat]. The authoritative element is a
monotonically increasing [nat], while a fragment is a lower bound. *)
Definition mono_nat {SI : sidx} := auth max_natUR.
Definition mono_natR {SI : sidx} := authR max_natUR.
Definition mono_natUR {SI : sidx} := authUR max_natUR.
(** [mono_nat_auth] is the authoritative element. The definition includes the
fragment at the same value so that lemma [mono_nat_included], which states that
[mono_nat_lb n ≼ mono_nat_auth dq n], holds. Without this trick, a
frame-preserving update lemma would be required instead. *)
Definition mono_nat_auth {SI : sidx} (dq : dfrac) (n : nat) : mono_nat :=
{dq} MaxNat n MaxNat n.
Definition mono_nat_lb {SI : sidx} (n : nat) : mono_nat := MaxNat n.
Notation "●MN dq a" := (mono_nat_auth dq a)
(at level 20, dq custom dfrac at level 1, format "●MN dq a").
Notation "◯MN a" := (mono_nat_lb a) (at level 20).
Section mono_nat.
Context {SI : sidx}.
Implicit Types (n : nat).
Global Instance mono_nat_lb_core_id n : CoreId (MN n).
Proof. apply _. Qed.
Global Instance mono_nat_auth_core_id l : CoreId (MN l).
Proof. apply _. Qed.
Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
MN{dq1 dq2} n MN{dq1} n MN{dq2} n.
Proof.
rewrite /mono_nat_auth auth_auth_dfrac_op.
rewrite (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
by rewrite -core_id_dup (comm _ ( _)).
Qed.
Lemma mono_nat_lb_op n1 n2 :
MN (n1 `max` n2) = MN n1 MN n2.
Proof. rewrite -auth_frag_op max_nat_op //. Qed.
Lemma mono_nat_auth_lb_op dq n :
MN{dq} n MN{dq} n MN n.
Proof.
rewrite /mono_nat_auth /mono_nat_lb.
rewrite -!assoc -auth_frag_op max_nat_op.
rewrite Nat.max_id //.
Qed.
Global Instance mono_nat_auth_dfrac_is_op dq dq1 dq2 n :
IsOp dq dq1 dq2 IsOp' (MN{dq} n) (MN{dq1} n) (MN{dq2} n).
Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_nat_auth_dfrac_op //. Qed.
Global Instance mono_nat_lb_max_is_op n n1 n2 :
IsOp (MaxNat n) (MaxNat n1) (MaxNat n2) IsOp' (MN n) (MN n1) (MN n2).
Proof. rewrite /IsOp' /IsOp /mono_nat_lb=> ->. done. Qed.
(** rephrasing of [mono_nat_lb_op] useful for weakening a fragment to a
smaller lower-bound *)
Lemma mono_nat_lb_op_le_l n n' :
n' n
MN n = MN n' MN n.
Proof. intros. rewrite -mono_nat_lb_op Nat.max_r //. Qed.
Lemma mono_nat_auth_dfrac_valid dq n : ( MN{dq} n) dq.
Proof.
rewrite /mono_nat_auth auth_both_dfrac_valid_discrete /=. naive_solver.
Qed.
Lemma mono_nat_auth_valid n : MN n.
Proof. by apply auth_both_valid. Qed.
Lemma mono_nat_auth_dfrac_op_valid dq1 dq2 n1 n2 :
(MN{dq1} n1 MN{dq2} n2) (dq1 dq2) n1 = n2.
Proof.
rewrite /mono_nat_auth (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
rewrite -auth_frag_op (comm _ ( _)) assoc. split.
- move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
- intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
by apply auth_both_dfrac_valid_discrete.
Qed.
Lemma mono_nat_auth_op_valid n1 n2 :
(MN n1 MN n2) False.
Proof. rewrite mono_nat_auth_dfrac_op_valid. naive_solver. Qed.
Lemma mono_nat_both_dfrac_valid dq n m :
(MN{dq} n MN m) dq m n.
Proof.
rewrite /mono_nat_auth /mono_nat_lb -assoc -auth_frag_op.
rewrite auth_both_dfrac_valid_discrete max_nat_included /=.
naive_solver lia.
Qed.
Lemma mono_nat_both_valid n m :
(MN n MN m) m n.
Proof. rewrite mono_nat_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
Lemma mono_nat_lb_mono n1 n2 : n1 n2 MN n1 MN n2.
Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
Lemma mono_nat_included dq n : MN n MN{dq} n.
Proof. apply cmra_included_r. Qed.
Lemma mono_nat_update {n} n' :
n n' MN n ~~> MN n'.
Proof.
intros. rewrite /mono_nat_auth /mono_nat_lb.
by apply auth_update, max_nat_local_update.
Qed.
Lemma mono_nat_auth_persist n dq :
MN{dq} n ~~> MN n.
Proof.
intros. rewrite /mono_nat_auth /mono_nat_lb.
eapply cmra_update_op_proper; last done.
eapply auth_update_auth_persist.
Qed.
Lemma mono_nat_auth_unpersist n :
MN n ~~>: λ k, q, k = MN{# q} n.
Proof. eapply auth_updateP_both_unpersist. Qed.
End mono_nat.
Global Typeclasses Opaque mono_nat_auth mono_nat_lb.