Skip to content

GitLab

I
iris-coq
Commit 69d67c60 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Introduce a canonical structure for CMRAs with a unit element.

parent d6aadd43
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 594 additions and 443 deletions
algebra/auth.v
View file @ 69d67c60
......@@ -66,11 +66,10 @@ Arguments authC : clear implicits.
(* CMRA *)
Section cmra.
Context {A : cmraT}.
Context {A : ucmraT}.
Implicit Types a b : A.
Implicit Types x y : auth A.
Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
Instance auth_valid : Valid (auth A) := λ x,
match authoritative x with
| Excl a => (∀ n, own x ≼{n} a) ∧ ✓ a
......@@ -101,7 +100,7 @@ Proof. by destruct x as [[]]. Qed.
Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} own x.
Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
Definition auth_cmra_mixin : CMRAMixin (auth A).
Lemma auth_cmra_mixin : CMRAMixin (auth A).
Proof.
split.
- by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
......@@ -128,7 +127,7 @@ Proof.
as (b&?&?&?); auto using own_validN.
by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
Qed.
Canonical Structure authR : cmraT :=
Canonical Structure authR :=
CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
Proof.
......@@ -139,6 +138,17 @@ Proof.
- by rewrite -cmra_discrete_valid_iff.
Qed.
Instance auth_empty : Empty (auth A) := Auth ∅ ∅.
Lemma auth_ucmra_mixin : UCMRAMixin (auth A).
Proof.
split; simpl.
- apply (@ucmra_unit_valid A).
- by intros x; constructor; rewrite /= left_id.
- apply _.
Qed.
Canonical Structure authUR :=
UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
(x ≡ y) ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M).
......@@ -151,17 +161,6 @@ Lemma auth_validI {M} (x : auth A) :
end : uPred M).
Proof. uPred.unseal. by destruct x as [[]]. Qed.
(** The notations ◯ and ● only work for CMRAs with an empty element. So, in
what follows, we assume we have an empty element. *)
Context `{Empty A, !CMRAUnit A}.
Global Instance auth_cmra_unit : CMRAUnit authR.
Proof.
split; simpl.
- by apply (@cmra_unit_valid A _).
- by intros x; constructor; rewrite /= left_id.
- apply _.
Qed.
Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed.
Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
......@@ -206,6 +205,7 @@ Qed.
End cmra.
Arguments authR : clear implicits.
Arguments authUR : clear implicits.
(* Functor *)
Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
......@@ -223,7 +223,7 @@ Instance auth_map_cmra_ne {A B : cofeT} n :
Proof.
intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf].
Qed.
Instance auth_map_cmra_monotone {A B : cmraT} (f : A → B) :
Instance auth_map_cmra_monotone {A B : ucmraT} (f : A → B) :
CMRAMonotone f → CMRAMonotone (auth_map f).
Proof.
split; try apply _.
......@@ -237,24 +237,24 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.
Program Definition authRF (F : rFunctor) : rFunctor := {|
rFunctor_car A B := authR (rFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := authC_map (rFunctor_map F fg)
Program Definition authURF (F : urFunctor) : urFunctor := {|
urFunctor_car A B := authUR (urFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_ne.
by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(auth_map_id x).
apply auth_map_ext=>y; apply rFunctor_id.
apply auth_map_ext=>y; apply urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
apply auth_map_ext=>y; apply rFunctor_compose.
apply auth_map_ext=>y; apply urFunctor_compose.
Qed.
Instance authRF_contractive F :
rFunctorContractive F → rFunctorContractive (authRF F).
Instance authURF_contractive F :
urFunctorContractive F → urFunctorContractive (authURF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_contractive.
by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
Qed.
algebra/cmra.v
View file @ 69d67c60
This diff is collapsed.
algebra/cmra_big_op.v
View file @ 69d67c60
From iris.algebra Require Export cmra list.
From iris.prelude Require Import gmap.
Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
Fixpoint big_op {A : ucmraT} (xs : list A) : A :=
match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
Arguments big_op _ _ !_ /.
Instance: Params (@big_op) 2.
Definition big_opM `{Countable K} {A : cmraT} `{Empty A} (m : gmap K A) : A :=
Arguments big_op _ !_ /.
Instance: Params (@big_op) 1.
Definition big_opM `{Countable K} {A : ucmraT} (m : gmap K A) : A :=
big_op (snd <$> map_to_list m).
Instance: Params (@big_opM) 5.
Instance: Params (@big_opM) 4.
(** * Properties about big ops *)
Section big_op.
Context `{CMRAUnit A}.
Context {A : ucmraT}.
Implicit Types xs : list A.
(** * Big ops *)
Lemma big_op_nil : big_op (@nil A) = ∅.
Proof. done. Qed.
Lemma big_op_cons x xs : big_op (x :: xs) = x ⋅ big_op xs.
Proof. done. Qed.
Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) (@big_op A).
Proof.
induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ x).
- by trans (big_op xs2).
Qed.
Global Instance big_op_ne n : Proper (dist n ==> dist n) big_op.
Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op A).
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op := ne_proper _.
Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
......
algebra/cmra_tactics.v
View file @ 69d67c60
......@@ -3,7 +3,7 @@ From iris.algebra Require Import cmra_big_op.
(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
Context `{CMRAUnit A}.
Context {A : ucmraT}.
Inductive expr :=
| EVar : nat → expr
......@@ -24,8 +24,8 @@ Module ra_reflection. Section ra_reflection.
Lemma eval_flatten Σ e :
eval Σ e ≡ big_op ((λ n, from_option id ∅ (Σ !! n)) <$> flatten e).
Proof.
by induction e as [| |e1 IH1 e2 IH2];
rewrite /= ?right_id ?fmap_app ?big_op_app ?IH1 ?IH2.
induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
by rewrite fmap_app IH1 IH2 big_op_app.
Qed.
Lemma flatten_correct Σ e1 e2 :
flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
......
algebra/cofe.v
View file @ 69d67c60
......@@ -91,8 +91,8 @@ End cofe_mixin.
(** Discrete COFEs and Timeless elements *)
(* TODO: On paper, We called these "discrete elements". I think that makes
more sense. *)
Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
Arguments timeless {_} _ {_} _ _.
Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
Arguments timeless {_ _ _} _ {_} _ _.
Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x.
(** General properties *)
......
algebra/excl.v
View file @ 69d67c60
......@@ -77,8 +77,7 @@ Instance excl_valid : Valid (excl A) := λ x,
match x with Excl _ | ExclUnit => True | ExclBot => False end.
Instance excl_validN : ValidN (excl A) := λ n x,
match x with Excl _ | ExclUnit => True | ExclBot => False end.
Global Instance excl_empty : Empty (excl A) := ExclUnit.
Instance excl_core : Core (excl A) := λ _, ∅.
Instance excl_core : Core (excl A) := λ _, ExclUnit.
Instance excl_op : Op (excl A) := λ x y,
match x, y with
| Excl a, ExclUnit | ExclUnit, Excl a => Excl a
......@@ -86,7 +85,7 @@ Instance excl_op : Op (excl A) := λ x y,
| _, _=> ExclBot
end.
Definition excl_cmra_mixin : CMRAMixin (excl A).
Lemma excl_cmra_mixin : CMRAMixin (excl A).
Proof.
split.
- by intros n []; destruct 1; constructor.
......@@ -98,7 +97,7 @@ Proof.
- by intros [?| |] [?| |]; constructor.
- by intros [?| |]; constructor.
- constructor.
- by intros [?| |] [?| |]; exists ∅.
- by intros [?| |] [?| |]; exists ExclUnit.
- by intros n [?| |] [?| |].
- intros n x y1 y2 ? Hx.
by exists match y1, y2 with
......@@ -107,13 +106,18 @@ Proof.
| ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
Qed.
Canonical Structure exclR : cmraT :=
Canonical Structure exclR :=
CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
Global Instance excl_cmra_unit : CMRAUnit exclR.
Proof. split. done. by intros []. apply _. Qed.
Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR.
Proof. split. apply _. by intros []. Qed.
Instance excl_empty : Empty (excl A) := ExclUnit.
Lemma excl_ucmra_mixin : UCMRAMixin (excl A).
Proof. split. done. by intros []. apply _. Qed.
Canonical Structure exclUR :=
UCMRAT (excl A) excl_cofe_mixin excl_cmra_mixin excl_ucmra_mixin.
Lemma excl_validN_inv_l n x a : ✓{n} (Excl a ⋅ x) → x = ∅.
Proof. by destruct x. Qed.
Lemma excl_validN_inv_r n x a : ✓{n} (x ⋅ Excl a) → x = ∅.
......@@ -152,6 +156,7 @@ End excl.
Arguments exclC : clear implicits.
Arguments exclR : clear implicits.
Arguments exclUR : clear implicits.
(* Functor *)
Definition excl_map {A B} (f : A → B) (x : excl A) : excl B :=
......@@ -182,9 +187,9 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
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)
Program Definition exclURF (F : cFunctor) : urFunctor := {|
urFunctor_car A B := (exclUR (cFunctor_car F A B) : ucmraT);
urFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
|}.
Next Obligation.
intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
......@@ -198,8 +203,8 @@ Next Obligation.
apply excl_map_ext=>y; apply cFunctor_compose.
Qed.
Instance exclRF_contractive F :
cFunctorContractive F → rFunctorContractive (exclRF F).
Instance exclURF_contractive F :
cFunctorContractive F → urFunctorContractive (exclURF F).
Proof.
intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
Qed.
algebra/frac.v
View file @ 69d67c60
......@@ -119,8 +119,7 @@ Instance frac_valid : Valid (frac A) := λ x,
match x with Frac q a => (q ≤ 1)%Qc ∧ ✓ a | FracUnit => True end.
Instance frac_validN : ValidN (frac A) := λ n x,
match x with Frac q a => (q ≤ 1)%Qc ∧ ✓{n} a | FracUnit => True end.
Global Instance frac_empty : Empty (frac A) := FracUnit.
Instance frac_core : Core (frac A) := λ _, ∅.
Instance frac_core : Core (frac A) := λ _, FracUnit.
Instance frac_op : Op (frac A) := λ x y,
match x, y with
| Frac q1 a, Frac q2 b => Frac (q1 + q2) (a ⋅ b)
......@@ -148,25 +147,30 @@ Proof.
trans (q1 + q2)%Qp; simpl; last done.
rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak.
- intros n [q a|] y1 y2 Hx Hx'; last first.
{ by exists (∅, ∅); destruct y1, y2; inversion_clear Hx'. }
{ by exists (FracUnit, FracUnit); destruct y1, y2; inversion_clear Hx'. }
destruct Hx, y1 as [q1 b1|], y2 as [q2 b2|].
+ apply (inj2 Frac) in Hx'; destruct Hx' as [-> ?].
destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto.
exists (Frac q1 z1,Frac q2 z2); by repeat constructor.
+ exists (Frac q a, ∅); inversion_clear Hx'; by repeat constructor.
+ exists (∅, Frac q a); inversion_clear Hx'; by repeat constructor.
+ exists (Frac q a, FracUnit); inversion_clear Hx'; by repeat constructor.
+ exists (FracUnit, Frac q a); inversion_clear Hx'; by repeat constructor.
+ exfalso; inversion_clear Hx'.
Qed.
Canonical Structure fracR : cmraT :=
Canonical Structure fracR :=
CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin.
Global Instance frac_cmra_unit : CMRAUnit fracR.
Proof. split. done. by intros []. apply _. Qed.
Global Instance frac_cmra_discrete : CMRADiscrete A → CMRADiscrete fracR.
Proof.
split; first apply _.
intros [q a|]; destruct 1; split; auto using cmra_discrete_valid.
Qed.
Instance frac_empty : Empty (frac A) := FracUnit.
Definition frac_ucmra_mixin : UCMRAMixin (frac A).
Proof. split. done. by intros []. apply _. Qed.
Canonical Structure fracUR :=
UCMRAT (frac A) frac_cofe_mixin frac_cmra_mixin frac_ucmra_mixin.
Lemma frac_validN_inv_l n y a : ✓{n} (Frac 1 a ⋅ y) → y = ∅.
Proof.
destruct y as [q b|]; [|done]=> -[Hq ?]; destruct (Qcle_not_lt _ _ Hq).
......@@ -217,6 +221,7 @@ Qed.
End cmra.
Arguments fracR : clear implicits.
Arguments fracUR : clear implicits.
(* Functor *)
Instance frac_map_cmra_monotone {A B : cmraT} (f : A → B) :
......@@ -225,15 +230,15 @@ Proof.
split; try apply _.
- intros n [p a|]; destruct 1; split; auto using validN_preserving.
- intros [q1 a1|] [q2 a2|] [[q3 a3|] Hx];
inversion Hx; setoid_subst; try apply: cmra_unit_least; auto.
inversion Hx; setoid_subst; try apply: ucmra_unit_least; auto.
destruct (included_preserving f a1 (a1 ⋅ a3)) as [b ?].
{ by apply cmra_included_l. }
by exists (Frac q3 b); constructor.
Qed.
Program Definition fracRF (F : rFunctor) : rFunctor := {|
rFunctor_car A B := fracR (rFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg)
Program Definition fracURF (F : rFunctor) : urFunctor := {|
urFunctor_car A B := fracUR (rFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_ne.
......@@ -247,8 +252,8 @@ Next Obligation.
apply frac_map_ext=>y; apply rFunctor_compose.
Qed.
Instance fracRF_contractive F :
rFunctorContractive F → rFunctorContractive (fracRF F).
Instance fracURF_contractive F :
rFunctorContractive F → urFunctorContractive (fracURF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive.
Qed.
algebra/gmap.v
View file @ 69d67c60
......@@ -109,7 +109,7 @@ Proof.
{ 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: cmra_unit_least.
- 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 [->|].
......@@ -118,7 +118,7 @@ Proof.
lookup_insert_ne // lookup_partial_alter_ne.
Qed.
Definition gmap_cmra_mixin : CMRAMixin (gmap K A).
Lemma gmap_cmra_mixin : CMRAMixin (gmap K A).
Proof.
split.
- by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
......@@ -152,17 +152,21 @@ Proof.
pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
by symmetry; apply option_op_positive_dist_r with (m1 !! i).
Qed.
Canonical Structure gmapR : cmraT :=
Canonical Structure gmapR :=
CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
Global Instance gmap_cmra_unit : CMRAUnit gmapR.
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 _).
- apply gmap_empty_timeless.
Qed.
Global Instance gmap_cmra_discrete : CMRADiscrete A → CMRADiscrete gmapR.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
Canonical Structure gmapUR :=
UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
(** Internalized properties *)
Lemma gmap_equivI {M} m1 m2 : (m1 ≡ m2) ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
......@@ -172,6 +176,7 @@ Proof. by uPred.unseal. Qed.
End cmra.
Arguments gmapR _ {_ _} _.
Arguments gmapUR _ {_ _} _.
Section properties.
Context `{Countable K} {A : cmraT}.
......@@ -189,7 +194,7 @@ 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; [|by intros; apply insert_validN, cmra_unit_validN].
split; [|by intros; apply insert_validN, ucmra_unit_validN].
by move=>/(_ i); simplify_map_eq.
Qed.
Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
......@@ -265,25 +270,6 @@ Proof. apply insert_updateP'. Qed.
Lemma singleton_update i (x y : A) : x ~~> y → {[ i := x ]} ~~> {[ i := y ]}.
Proof. apply insert_update. Qed.
Lemma singleton_updateP_empty `{Empty A, !CMRAUnit A}
(P : A → Prop) (Q : gmap K A → Prop) i :
∅ ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
Proof.
intros Hx HQ n gf Hg.
destruct (Hx n (from_option id ∅ (gf !! i))) as (y&?&Hy).
{ move:(Hg i). rewrite !left_id.
case _: (gf !! i); simpl; auto using cmra_unit_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); first done.
by rewrite right_id.
- move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
Qed.
Lemma singleton_updateP_empty' `{Empty A, !CMRAUnit A} (P: A → Prop) i :
∅ ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
Proof. eauto using singleton_updateP_empty. Qed.
Section freshness.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma updateP_alloc_strong (Q : gmap K A → Prop) (I : gset K) m x :
......@@ -308,6 +294,31 @@ Proof. eauto using updateP_alloc_strong. Qed.
Lemma updateP_alloc' m x :
✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
Proof. eauto using updateP_alloc. Qed.
Lemma singleton_updateP_unit (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 n gf Hg.
destruct (Hx n (from_option id u (gf !! i))) as (y&?&Hy).
{ move:(Hg i). rewrite !left_id.
case _: (gf !! i); simpl; first done. 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); first done.
by rewrite /= (comm _ y) left_id right_id.
- move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
Qed.
Lemma singleton_updateP_unit' (P: A → Prop) u i :
✓ u → LeftId (≡) u (⋅) →
u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
Proof. eauto using singleton_updateP_unit. Qed.
Lemma singleton_update_unit u i (y : A) :
✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}.
Proof.
rewrite !cmra_update_updateP; eauto using singleton_updateP_unit with subst.
Qed.
End freshness.
(* Allocation is a local update: Just use composition with a singleton map. *)
......@@ -370,9 +381,9 @@ Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
Qed.
Program Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
rFunctor_car A B := gmapR K (rFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg)
Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
urFunctor_car A B := gmapUR K (rFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
......@@ -386,7 +397,7 @@ Next Obligation.
apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
Qed.
Instance gmapRF_contractive K `{Countable K} F :
rFunctorContractive F → rFunctorContractive (gmapRF K F).
rFunctorContractive F → urFunctorContractive (gmapURF K F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
Qed.
algebra/iprod.v
View file @ 69d67c60
This diff is collapsed.
algebra/list.v
View file @ 69d67c60
......@@ -113,7 +113,7 @@ Qed.
(* CMRA *)
Section cmra.
Context {A : cmraT}.
Context {A : ucmraT}.
Implicit Types l : list A.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
......@@ -196,17 +196,19 @@ Section cmra.
[inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
Qed.
Canonical Structure listR : cmraT :=
Canonical Structure listR :=
CMRAT (list A) list_cofe_mixin list_cmra_mixin.
Global Instance empty_list : Empty (list A) := [].
Global Instance list_cmra_unit : CMRAUnit listR.
Definition list_ucmra_mixin : UCMRAMixin (list A).
Proof.
split.
- constructor.
- by intros l.
- by inversion_clear 1.
Qed.
Canonical Structure listUR :=
UCMRAT (list A) list_cofe_mixin list_cmra_mixin list_ucmra_mixin.
Global Instance list_cmra_discrete : CMRADiscrete A → CMRADiscrete listR.
Proof.
......@@ -228,13 +230,15 @@ Section cmra.
End cmra.
Arguments listR : clear implicits.
Arguments listUR : clear implicits.
Global Instance list_singletonM `{Empty A} : SingletonM nat A (list A) := λ n x,
Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
replicate n ∅ ++ [x].
Section properties.
Context {A : cmraT}.
Context {A : ucmraT}.
Implicit Types l : list A.
Implicit Types x y z : A.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
......@@ -255,64 +259,58 @@ Section properties.
Lemma replicate_valid n (x : A) : ✓ x → ✓ replicate n x.
Proof. apply Forall_replicate. Qed.
Global Instance list_singletonM_ne n i :
Proper (dist n ==> dist n) (@list_singletonM A i).
Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
Global Instance list_singletonM_proper i :
Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
(* Singleton lists *)
Section singleton.
Context `{CMRAUnit A}.
Global Instance list_singletonM_ne n i :
Proper (dist n ==> dist n) (list_singletonM i).
Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
Global Instance list_singletonM_proper i :
Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
Lemma elem_of_list_singletonM i z x : z ∈ {[i := x]} → z = ∅ ∨ z = x.
Proof.
rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
Qed.
Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x.
Proof. induction i; by f_equal/=. Qed.
Lemma list_lookup_singletonM_ne i j x :
i ≠ j → {[ i := x ]} !! j = None ∨ {[ i := x ]} !! j = Some ∅.
Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
Lemma list_singletonM_validN n i x : ✓{n} {[ i := x ]} ↔ ✓{n} x.
Proof.
rewrite list_lookup_validN. split.
{ move=> /(_ i). by rewrite list_lookup_singletonM. }
intros Hx j; destruct (decide (i = j)); subst.
- by rewrite list_lookup_singletonM.
- destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
rewrite Hi; by try apply (cmra_unit_validN (A:=A)).
Qed.
Lemma list_singleton_valid i x : ✓ {[ i := x ]} ↔ ✓ x.
Proof.
rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
Qed.
Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
Proof.
rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
Qed.
Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
Proof.
rewrite /singletonM /list_singletonM /=.
induction i; constructor; auto using cmra_core_unit.
Qed.
Lemma list_op_singletonM i (x y : A) :
{[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
Proof.
rewrite /singletonM /list_singletonM /=.
induction i; constructor; rewrite ?left_id;