diff --git a/algebra/agree.v b/algebra/agree.v
index ecc0bd9758028e8fab806b46a3e96f514da1e2b5..320b7ae1e4847aeebf5cb7fac55ed63745a91672 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -60,7 +60,7 @@ Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x;
agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ≡{n}≡ y |}.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
-Instance agree_core : Core (agree A) := id.
+Instance agree_pcore : PCore (agree A) := Some.
Instance: Comm (≡) (@op (agree A) _).
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
@@ -106,11 +106,11 @@ Qed.
Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
- split; try (apply _ || done).
+ apply cmra_total_mixin; try apply _ || by eauto.
- intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
rewrite -(Hx n'); last auto.
symmetry; apply dist_le with n; try apply Hx; auto.
- - intros x; apply agree_idemp.
+ - intros x. apply agree_idemp.
- by intros n x y [(?&?&?) ?].
- intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
+ by rewrite agree_idemp.
@@ -119,8 +119,10 @@ Qed.
Canonical Structure agreeR : cmraT :=
CMRAT (agree A) agree_cofe_mixin agree_cmra_mixin.
+Global Instance agree_total : CMRATotal agreeR.
+Proof. rewrite /CMRATotal; eauto. Qed.
Global Instance agree_persistent (x : agree A) : Persistent x.
-Proof. done. Qed.
+Proof. by constructor. Qed.
Program Definition to_agree (x : A) : agree A :=
{| agree_car n := x; agree_is_valid n := True |}.
diff --git a/algebra/auth.v b/algebra/auth.v
index 21012546f19d09688633053919d7b962861d460b..4ae474849c058fc5b5975fa7b1bb07bb4b280f8a 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -3,18 +3,18 @@ From iris.algebra Require Import upred.
Local Arguments valid _ _ !_ /.
Local Arguments validN _ _ _ !_ /.
-Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
+Record auth (A : Type) := Auth { authoritative : option (excl A); own : A }.
Add Printing Constructor auth.
Arguments Auth {_} _ _.
Arguments authoritative {_} _.
Arguments own {_} _.
-Notation "â—¯ a" := (Auth ExclUnit a) (at level 20).
-Notation "◠a" := (Auth (Excl a) ∅) (at level 20).
+Notation "â—¯ a" := (Auth None a) (at level 20).
+Notation "◠a" := (Auth (Excl' a) ∅) (at level 20).
(* COFE *)
Section cofe.
Context {A : cofeT}.
-Implicit Types a : excl A.
+Implicit Types a : option (excl A).
Implicit Types b : A.
Implicit Types x y : auth A.
@@ -72,20 +72,20 @@ Implicit Types x y : auth A.
Instance auth_valid : Valid (auth A) := λ x,
match authoritative x with
- | Excl a => (∀ n, own x ≼{n} a) ∧ ✓ a
- | ExclUnit => ✓ own x
- | ExclBot => False
+ | Excl' a => (∀ n, own x ≼{n} a) ∧ ✓ a
+ | None => ✓ own x
+ | ExclBot' => False
end.
Global Arguments auth_valid !_ /.
Instance auth_validN : ValidN (auth A) := λ n x,
match authoritative x with
- | Excl a => own x ≼{n} a ∧ ✓{n} a
- | ExclUnit => ✓{n} own x
- | ExclBot => False
+ | Excl' a => own x ≼{n} a ∧ ✓{n} a
+ | None => ✓{n} own x
+ | ExclBot' => False
end.
Global Arguments auth_validN _ !_ /.
-Instance auth_core : Core (auth A) := λ x,
- Auth (core (authoritative x)) (core (own x)).
+Instance auth_pcore : PCore (auth A) := λ x,
+ Some (Auth (core (authoritative x)) (core (own x))).
Instance auth_op : Op (auth A) := λ x y,
Auth (authoritative x â‹… authoritative y) (own x â‹… own y).
@@ -96,20 +96,21 @@ Proof.
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} authoritative x.
-Proof. by destruct x as [[]]. Qed.
+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.
+Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
Lemma auth_cmra_mixin : CMRAMixin (auth A).
Proof.
- split.
+ apply cmra_total_mixin.
+ - eauto.
- by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- - intros n [x a] [y b] [Hx Ha]; simpl in *;
- destruct Hx; intros ?; cofe_subst; auto.
- - intros [[] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
+ - intros n [x a] [y b] [Hx Ha]; simpl in *.
+ destruct Hx as [?? Hx|]; first destruct Hx; intros ?; cofe_subst; auto.
+ - intros [[[?|]|] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
naive_solver eauto using O.
- - intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
+ - intros n [[[]|] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
- by split; simpl; rewrite assoc.
- by split; simpl; rewrite comm.
- by split; simpl; rewrite ?cmra_core_l.
@@ -118,7 +119,7 @@ Proof.
by split; simpl; apply cmra_core_preserving.
- assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
{ intros n a b1 b2 <-; apply cmra_includedN_l. }
- intros n [[a1| |] b1] [[a2| |] b2];
+ intros n [[[a1|]|] b1] [[[a2|]|] b2];
naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
- intros n x y1 y2 ? [??]; simpl in *.
destruct (cmra_extend n (authoritative x) (authoritative y1)
@@ -127,12 +128,12 @@ Proof.
as (b&?&?&?); auto using own_validN.
by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
Qed.
-Canonical Structure authR :=
- CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
+Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
+
Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
Proof.
split; first apply _.
- intros [[] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
+ intros [[[?|]|] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
- setoid_rewrite <-cmra_discrete_included_iff.
rewrite -cmra_discrete_valid_iff. tauto.
- by rewrite -cmra_discrete_valid_iff.
@@ -145,6 +146,7 @@ Proof.
- apply (@ucmra_unit_valid A).
- by intros x; constructor; rewrite /= left_id.
- apply _.
+ - do 2 constructor; simpl; apply (persistent_core _).
Qed.
Canonical Structure authUR :=
UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
@@ -155,22 +157,23 @@ Lemma auth_equivI {M} (x y : auth A) :
Proof. by uPred.unseal. Qed.
Lemma auth_validI {M} (x : auth A) :
(✓ x) ⊣⊢ (match authoritative x with
- | Excl a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
- | ExclUnit => ✓ own x
- | ExclBot => False
+ | Excl' a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
+ | None => ✓ own x
+ | ExclBot' => False
end : uPred M).
-Proof. uPred.unseal. by destruct x as [[]]. Qed.
+Proof. uPred.unseal. by destruct x as [[[]|]]. 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.
+Lemma auth_both_op a b : Auth (Excl' a) b ≡ ◠a ⋅ ◯ b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
Lemma auth_update a a' b b' :
(∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b) →
â— a â‹… â—¯ a' ~~> â— b â‹… â—¯ b'.
Proof.
- move=> Hab n [[?| |] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
+ intros Hab; apply cmra_total_update.
+ move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
destruct (Hab n (bf1 â‹… bf2)) as [Ha' ?]; auto.
{ by rewrite Ha left_id assoc. }
split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done].
@@ -209,25 +212,29 @@ Arguments authUR : clear implicits.
(* Functor *)
Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
- Auth (excl_map f (authoritative x)) (f (own x)).
+ Auth (excl_map f <$> authoritative x) (f (own x)).
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
-Proof. by destruct x; rewrite /auth_map excl_map_id. Qed.
+Proof. by destruct x as [[[]|]]. Qed.
Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
auth_map (g ∘ f) x = auth_map g (auth_map f x).
-Proof. by destruct x; rewrite /auth_map excl_map_compose. Qed.
+Proof. by destruct x as [[[]|]]. Qed.
Lemma auth_map_ext {A B : cofeT} (f g : A → B) x :
(∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
-Proof. constructor; simpl; auto using excl_map_ext. Qed.
-Instance auth_map_cmra_ne {A B : cofeT} n :
+Proof.
+ constructor; simpl; auto.
+ apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
+Qed.
+Instance auth_map_ne {A B : cofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
Proof.
- intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf].
+ intros f g Hf [??] [??] [??]; split; simpl in *; [|by apply Hf].
+ apply option_fmap_ne; [|done]=> x y ?; by apply excl_map_ne.
Qed.
Instance auth_map_cmra_monotone {A B : ucmraT} (f : A → B) :
CMRAMonotone f → CMRAMonotone (auth_map f).
Proof.
split; try apply _.
- - intros n [[a| |] b]; rewrite /= /cmra_validN /=; try
+ - intros n [[[a|]|] b]; rewrite /= /cmra_validN /=; try
naive_solver eauto using includedN_preserving, validN_preserving.
- by intros [x a] [y b]; rewrite !auth_included /=;
intros [??]; split; simpl; apply: included_preserving.
@@ -235,7 +242,7 @@ Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (auth_map f).
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.
+Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Program Definition authURF (F : urFunctor) : urFunctor := {|
urFunctor_car A B := authUR (urFunctor_car F A B);
diff --git a/algebra/cmra.v b/algebra/cmra.v
index e15086715cfcf1c1b2dc2be8d963aa205229b94c..fe76e9cbb9a91bf7f1750da556fb924eab21d579 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1,7 +1,7 @@
From iris.algebra Require Export cofe.
-Class Core (A : Type) := core : A → A.
-Instance: Params (@core) 2.
+Class PCore (A : Type) := pcore : A → option A.
+Instance: Params (@pcore) 2.
Class Op (A : Type) := op : A → A → A.
Instance: Params (@op) 2.
@@ -29,10 +29,11 @@ Notation "x ≼{ n } y" := (includedN n x y)
Instance: Params (@includedN) 4.
Hint Extern 0 (_ ≼{_} _) => reflexivity.
-Record CMRAMixin A `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A} := {
+Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
(* setoids *)
mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
- mixin_cmra_core_ne n : Proper (dist n ==> dist n) core;
+ mixin_cmra_pcore_ne n x y cx :
+ x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
(* valid *)
mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
@@ -40,9 +41,10 @@ Record CMRAMixin A `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A} := {
(* monoid *)
mixin_cmra_assoc : Assoc (≡) (⋅);
mixin_cmra_comm : Comm (≡) (⋅);
- mixin_cmra_core_l x : core x ⋅ x ≡ x;
- mixin_cmra_core_idemp x : core (core x) ≡ core x;
- mixin_cmra_core_preserving x y : x ≼ y → core x ≼ core y;
+ mixin_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
+ mixin_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
+ mixin_cmra_pcore_preserving x y cx :
+ x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
mixin_cmra_extend n x y1 y2 :
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
@@ -55,7 +57,7 @@ Structure cmraT := CMRAT {
cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car;
cmra_compl : Compl cmra_car;
- cmra_core : Core cmra_car;
+ cmra_pcore : PCore cmra_car;
cmra_op : Op cmra_car;
cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
@@ -67,14 +69,14 @@ Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Arguments cmra_compl : simpl never.
-Arguments cmra_core : simpl never.
+Arguments cmra_pcore : simpl never.
Arguments cmra_op : simpl never.
Arguments cmra_valid : simpl never.
Arguments cmra_validN : simpl never.
Arguments cmra_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Add Printing Constructor cmraT.
-Existing Instances cmra_core cmra_op cmra_valid cmra_validN.
+Existing Instances cmra_pcore cmra_op cmra_valid cmra_validN.
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
Canonical Structure cmra_cofeC.
@@ -84,8 +86,9 @@ Section cmra_mixin.
Implicit Types x y : A.
Global Instance cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x).
Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
- Global Instance cmra_core_ne n : Proper (dist n ==> dist n) (@core A _).
- Proof. apply (mixin_cmra_core_ne _ (cmra_mixin A)). Qed.
+ Lemma cmra_pcore_ne n x y cx :
+ x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy.
+ Proof. apply (mixin_cmra_pcore_ne _ (cmra_mixin A)). Qed.
Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
@@ -96,12 +99,13 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
Global Instance cmra_comm : Comm (≡) (@op A _).
Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed.
- Lemma cmra_core_l x : core x ⋅ x ≡ x.
- Proof. apply (mixin_cmra_core_l _ (cmra_mixin A)). Qed.
- Lemma cmra_core_idemp x : core (core x) ≡ core x.
- Proof. apply (mixin_cmra_core_idemp _ (cmra_mixin A)). Qed.
- Lemma cmra_core_preserving x y : x ≼ y → core x ≼ core y.
- Proof. apply (mixin_cmra_core_preserving _ (cmra_mixin A)). Qed.
+ Lemma cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x.
+ Proof. apply (mixin_cmra_pcore_l _ (cmra_mixin A)). Qed.
+ Lemma cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx.
+ Proof. apply (mixin_cmra_pcore_idemp _ (cmra_mixin A)). Qed.
+ Lemma cmra_pcore_preserving x y cx :
+ x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
+ Proof. apply (mixin_cmra_pcore_preserving _ (cmra_mixin A)). Qed.
Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
Lemma cmra_extend n x y1 y2 :
@@ -110,13 +114,33 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
End cmra_mixin.
+Definition opM {A : cmraT} (x : A) (my : option A) :=
+ match my with Some y => x â‹… y | None => x end.
+Infix "â‹…?" := opM (at level 50, left associativity) : C_scope.
+
+(** * Persistent elements *)
+Class Persistent {A : cmraT} (x : A) := persistent : pcore x ≡ Some x.
+Arguments persistent {_} _ {_}.
+
+(** * CMRAs whose core is total *)
+(** The function [core] may return a dummy when used on CMRAs without total
+core. *)
+Class CMRATotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
+
+Class Core (A : Type) := core : A → A.
+Instance: Params (@core) 2.
+
+Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x).
+Arguments core' _ _ _ /.
+
(** * CMRAs with a unit element *)
(** We use the notation ∅ because for most instances (maps, sets, etc) the
`empty' element is the unit. *)
-Record UCMRAMixin A `{Dist A, Equiv A, Op A, Valid A, Empty A} := {
+Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
mixin_ucmra_unit_valid : ✓ ∅;
mixin_ucmra_unit_left_id : LeftId (≡) ∅ (⋅);
- mixin_ucmra_unit_timeless : Timeless ∅
+ mixin_ucmra_unit_timeless : Timeless ∅;
+ mixin_ucmra_pcore_unit : pcore ∅ ≡ Some ∅
}.
Structure ucmraT := UCMRAT {
@@ -124,7 +148,7 @@ Structure ucmraT := UCMRAT {
ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car;
ucmra_compl : Compl ucmra_car;
- ucmra_core : Core ucmra_car;
+ ucmra_pcore : PCore ucmra_car;
ucmra_op : Op ucmra_car;
ucmra_valid : Valid ucmra_car;
ucmra_validN : ValidN ucmra_car;
@@ -138,7 +162,7 @@ Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
Arguments ucmra_compl : simpl never.
-Arguments ucmra_core : simpl never.
+Arguments ucmra_pcore : simpl never.
Arguments ucmra_op : simpl never.
Arguments ucmra_valid : simpl never.
Arguments ucmra_validN : simpl never.
@@ -163,12 +187,10 @@ Section ucmra_mixin.
Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
Global Instance ucmra_unit_timeless : Timeless (∅ : A).
Proof. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed.
+ Lemma ucmra_pcore_unit : pcore (∅:A) ≡ Some ∅.
+ Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
End ucmra_mixin.
-(** * Persistent elements *)
-Class Persistent {A : cmraT} (x : A) := persistent : core x ≡ x.
-Arguments persistent {_} _ {_}.
-
(** * Discrete CMRAs *)
Class CMRADiscrete (A : cmraT) := {
cmra_discrete :> Discrete A;
@@ -194,12 +216,13 @@ Class LocalUpdate {A : cmraT} (Lv : A → Prop) (L : A → A) := {
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
(** * Frame preserving updates *)
-Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n z,
- ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
+Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
+ ✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
Instance: Params (@cmra_updateP) 1.
Infix "~~>:" := cmra_updateP (at level 70).
-Definition cmra_update {A : cmraT} (x y : A) := ∀ n z,
- ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
+
+Definition cmra_update {A : cmraT} (x y : A) := ∀ n mz,
+ ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz).
Infix "~~>" := cmra_update (at level 70).
Instance: Params (@cmra_update) 1.
@@ -210,13 +233,24 @@ Implicit Types x y z : A.
Implicit Types xs ys zs : list A.
(** ** Setoids *)
-Global Instance cmra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
-Proof. apply (ne_proper _). Qed.
-Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
+Global Instance cmra_pcore_ne' n : Proper (dist n ==> dist n) (@pcore A _).
+Proof.
+ intros x y Hxy. destruct (pcore x) as [cx|] eqn:?.
+ { destruct (cmra_pcore_ne n x y cx) as (cy&->&->); auto. }
+ destruct (pcore y) as [cy|] eqn:?; auto.
+ destruct (cmra_pcore_ne n y x cy) as (cx&?&->); simplify_eq/=; auto.
+Qed.
+Lemma cmra_pcore_proper x y cx :
+ x ≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡ cy.
Proof.
- intros x1 x2 Hx y1 y2 Hy.
- by rewrite Hy (comm _ x1) Hx (comm _ y2).
+ intros. destruct (cmra_pcore_ne 0 x y cx) as (cy&?&?); auto.
+ exists cy; split; [done|apply equiv_dist=> n].
+ destruct (cmra_pcore_ne n x y cx) as (cy'&?&?); naive_solver.
Qed.
+Global Instance cmra_pcore_proper' : Proper ((≡) ==> (≡)) (@pcore A _).
+Proof. apply (ne_proper _). Qed.
+Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
+Proof. intros x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
Proof. apply (ne_proper_2 _). Qed.
Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
@@ -247,18 +281,26 @@ Proof.
intros x x' Hx y y' Hy.
by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
-Global Instance cmra_update_proper :
- Proper ((≡) ==> (≡) ==> iff) (@cmra_update A).
-Proof.
- intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
-Qed.
+Global Instance cmra_opM_ne n : Proper (dist n ==> dist n ==> dist n) (@opM A).
+Proof. destruct 2; by cofe_subst. Qed.
+Global Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A).
+Proof. destruct 2; by setoid_subst. Qed.
Global Instance cmra_updateP_proper :
Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
- intros x1 x2 Hx P1 P2 HP; split=>Hup n z;
- [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
+ rewrite /pointwise_relation /cmra_updateP=> x x' Hx P P' HP;
+ split=> ? n mz; setoid_subst; naive_solver.
+Qed.
+Global Instance cmra_update_proper :
+ Proper ((≡) ==> (≡) ==> iff) (@cmra_update A).
+Proof.
+ rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto.
Qed.
+(** ** Op *)
+Lemma cmra_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
+Proof. destruct mz; by rewrite /= -?assoc. Qed.
+
(** ** Validity *)
Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x.
Proof. induction 2; eauto using cmra_validN_S. Qed.
@@ -270,33 +312,37 @@ Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
(** ** Core *)
-Lemma cmra_core_r x : x ⋅ core x ≡ x.
-Proof. by rewrite (comm _ x) cmra_core_l. Qed.
-Lemma cmra_core_core x : core x ⋅ core x ≡ core x.
-Proof. by rewrite -{2}(cmra_core_idemp x) cmra_core_r. Qed.
-Lemma cmra_core_validN n x : ✓{n} x → ✓{n} core x.
-Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
-Lemma cmra_core_valid x : ✓ x → ✓ core x.
-Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
-Global Instance cmra_core_persistent x : Persistent (core x).
-Proof. apply cmra_core_idemp. Qed.
+Lemma cmra_pcore_l' x cx : pcore x ≡ Some cx → cx ⋅ x ≡ x.
+Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_l. Qed.
+Lemma cmra_pcore_r x cx : pcore x = Some cx → x ⋅ cx ≡ x.
+Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed.
+Lemma cmra_pcore_r' x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x.
+Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed.
+Lemma cmra_pcore_idemp' x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx.
+Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed.
+Lemma cmra_pcore_pcore x cx : pcore x = Some cx → cx ⋅ cx ≡ cx.
+Proof. eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
+Lemma cmra_pcore_pcore' x cx : pcore x ≡ Some cx → cx ⋅ cx ≡ cx.
+Proof. eauto using cmra_pcore_r', cmra_pcore_idemp'. Qed.
+Lemma cmra_pcore_validN n x cx : ✓{n} x → pcore x = Some cx → ✓{n} cx.
+Proof.
+ intros Hvx Hx%cmra_pcore_l. move: Hvx; rewrite -Hx. apply cmra_validN_op_l.
+Qed.
+Lemma cmra_pcore_valid x cx : ✓ x → pcore x = Some cx → ✓ cx.
+Proof.
+ intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
+Qed.
(** ** Order *)
Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
Proof. intros [z ->]. by exists z. Qed.
-Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
+Global Instance cmra_includedN_trans n : Transitive (@includedN A _ _ n).
Proof.
- split.
- - by intros x; exists (core x); rewrite cmra_core_r.
- - intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
- by rewrite assoc -Hy -Hz.
+ intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2). by rewrite assoc -Hy -Hz.
Qed.
-Global Instance cmra_included_preorder: PreOrder (@included A _ _).
+Global Instance cmra_included_trans: Transitive (@included A _ _).
Proof.
- split.
- - by intros x; exists (core x); rewrite cmra_core_r.
- - intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
- by rewrite assoc -Hy -Hz.
+ intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2). by rewrite assoc -Hy -Hz.
Qed.
Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x.
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
@@ -317,13 +363,26 @@ Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
Lemma cmra_included_r x y : y ≼ x ⋅ y.
Proof. rewrite (comm op); apply cmra_included_l. Qed.
-Lemma cmra_core_preservingN n x y : x ≼{n} y → core x ≼{n} core y.
+Lemma cmra_pcore_preserving' x y cx :
+ x ≼ y → pcore x ≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
+Proof.
+ intros ? (cx'&?&Hcx)%equiv_Some_inv_r'.
+ destruct (cmra_pcore_preserving x y cx') as (cy&->&?); auto.
+ exists cy; by rewrite Hcx.
+Qed.
+Lemma cmra_pcore_preservingN' n x y cx :
+ x ≼{n} y → pcore x ≡{n}≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼{n} cy.
Proof.
- intros [z ->].
- apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
+ intros [z Hy] (cx'&?&Hcx)%dist_Some_inv_r'.
+ destruct (cmra_pcore_preserving x (x â‹… z) cx')
+ as (cy&Hxy&?); auto using cmra_included_l.
+ assert (pcore y ≡{n}≡ Some cy) as (cy'&?&Hcy')%dist_Some_inv_r'.
+ { by rewrite Hy Hxy. }
+ exists cy'; split; first done.
+ rewrite Hcx -Hcy'; auto using cmra_included_includedN.
Qed.
-Lemma cmra_included_core x : core x ≼ x.
-Proof. by exists x; rewrite cmra_core_l. Qed.
+Lemma cmra_included_pcore x cx : pcore x = Some cx → cx ≼ x.
+Proof. exists x. by rewrite cmra_pcore_l. Qed.
Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
@@ -340,6 +399,74 @@ Proof.
by rewrite Hx1 Hx2.
Qed.
+(** ** Total core *)
+Section total_core.
+ Context `{CMRATotal A}.
+
+ Lemma cmra_core_l x : core x ⋅ x ≡ x.
+ Proof.
+ destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_l.
+ Qed.
+ Lemma cmra_core_idemp x : core (core x) ≡ core x.
+ Proof.
+ destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_idemp.
+ Qed.
+ Lemma cmra_core_preserving x y : x ≼ y → core x ≼ core y.
+ Proof.
+ intros; destruct (cmra_total x) as [cx Hcx].
+ destruct (cmra_pcore_preserving x y cx) as (cy&Hcy&?); auto.
+ by rewrite /core /= Hcx Hcy.
+ Qed.
+
+ Global Instance cmra_core_ne n : Proper (dist n ==> dist n) (@core A _).
+ Proof.
+ intros x y Hxy. destruct (cmra_total x) as [cx Hcx].
+ by rewrite /core /= -Hxy Hcx.
+ Qed.
+ Global Instance cmra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
+ Proof. apply (ne_proper _). Qed.
+
+ Lemma cmra_core_r x : x ⋅ core x ≡ x.
+ Proof. by rewrite (comm _ x) cmra_core_l. Qed.
+ Lemma cmra_core_core x : core x ⋅ core x ≡ core x.
+ Proof. by rewrite -{2}(cmra_core_idemp x) cmra_core_r. Qed.
+ Lemma cmra_core_validN n x : ✓{n} x → ✓{n} core x.
+ Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
+ Lemma cmra_core_valid x : ✓ x → ✓ core x.
+ Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
+
+ Lemma persistent_total x : Persistent x ↔ core x ≡ x.
+ Proof.
+ split; [intros; by rewrite /core /= (persistent x)|].
+ rewrite /Persistent /core /=.
+ destruct (cmra_total x) as [? ->]. by constructor.
+ Qed.
+ Lemma persistent_core x `{!Persistent x} : core x ≡ x.
+ Proof. by apply persistent_total. Qed.
+
+ Global Instance cmra_core_persistent x : Persistent (core x).
+ Proof.
+ destruct (cmra_total x) as [cx Hcx].
+ rewrite /Persistent /core /= Hcx /=. eauto using cmra_pcore_idemp.
+ Qed.
+
+ Lemma cmra_included_core x : core x ≼ x.
+ Proof. by exists x; rewrite cmra_core_l. Qed.
+ Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
+ Proof.
+ split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
+ Qed.
+ Global Instance cmra_included_preorder : PreOrder (@included A _ _).
+ Proof.
+ split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
+ Qed.
+ Lemma cmra_core_preservingN n x y : x ≼{n} y → core x ≼{n} core y.
+ Proof.
+ intros [z ->].
+ apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
+ Qed.
+End total_core.
+
(** ** Timeless *)
Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y.
Proof.
@@ -369,12 +496,6 @@ Proof.
split; first by apply cmra_included_includedN.
intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
Qed.
-Lemma cmra_discrete_updateP `{CMRADiscrete A} (x : A) (P : A → Prop) :
- (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P.
-Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
-Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
- (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y.
-Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
(** ** Local updates *)
Global Instance local_update_proper Lv (L : A → A) :
@@ -394,74 +515,143 @@ Global Instance local_update_id : LocalUpdate (λ _, True) (@id A).
Proof. split; auto with typeclass_instances. Qed.
(** ** Updates *)
-Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
-Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
-Proof.
- split.
- - by intros Hx z ?; exists y; split; [done|apply (Hx z)].
- - by intros Hx n z ?; destruct (Hx n z) as (?&<-&?).
-Qed.
+Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed.
Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P.
-Proof. by intros ? n z ?; exists x. Qed.
+Proof. intros ? n mz ?; eauto. Qed.
Lemma cmra_updateP_compose (P Q : A → Prop) x :
x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q.
-Proof.
- intros Hx Hy n z ?. destruct (Hx n z) as (y&?&?); auto. by apply (Hy y).
-Qed.
+Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed.
Lemma cmra_updateP_compose_l (Q : A → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q.
Proof.
rewrite cmra_update_updateP.
- intros; apply cmra_updateP_compose with (y =); intros; subst; auto.
+ intros; apply cmra_updateP_compose with (y =); naive_solver.
Qed.
-Lemma cmra_updateP_weaken (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
+Lemma cmra_updateP_weaken (P Q : A → Prop) x :
+ x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
+Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
+Proof.
+ split.
+ - intros x. by apply cmra_update_updateP, cmra_updateP_id.
+ - intros x y z. rewrite !cmra_update_updateP.
+ eauto using cmra_updateP_compose with subst.
+Qed.
Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
- x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q.
+ x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) →
+ x1 â‹… x2 ~~>: Q.
Proof.
- intros Hx1 Hx2 Hy n z ?.
- destruct (Hx1 n (x2 â‹… z)) as (y1&?&?); first by rewrite assoc.
- destruct (Hx2 n (y1 â‹… z)) as (y2&?&?);
- first by rewrite assoc (comm _ x2) -assoc.
- exists (y1 â‹… y2); split; last rewrite (comm _ y1) -assoc; auto.
+ intros Hx1 Hx2 Hy n mz ?.
+ destruct (Hx1 n (Some (x2 â‹…? mz))) as (y1&?&?).
+ { by rewrite /= -cmra_opM_assoc. }
+ destruct (Hx2 n (Some (y1 â‹…? mz))) as (y2&?&?).
+ { by rewrite /= -cmra_opM_assoc (comm _ x2) cmra_opM_assoc. }
+ exists (y1 â‹… y2); split; last rewrite (comm _ y1) cmra_opM_assoc; auto.
Qed.
Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
- x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
+ x1 ~~>: P1 → x2 ~~>: P2 →
+ x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
Proof. eauto 10 using cmra_updateP_op. Qed.
Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2.
Proof.
rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
Qed.
-Lemma cmra_update_id x : x ~~> x.
-Proof. intro. auto. Qed.
+
+Section total_updates.
+ Context `{CMRATotal A}.
+
+ Lemma cmra_total_updateP x (P : A → Prop) :
+ x ~~>: P ↔ ∀ n z, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
+ Proof.
+ split=> Hup; [intros n z; apply (Hup n (Some z))|].
+ intros n [z|] ?; simpl; [by apply Hup|].
+ destruct (Hup n (core x)) as (y&?&?); first by rewrite cmra_core_r.
+ eauto using cmra_validN_op_l.
+ Qed.
+ Lemma cmra_total_update x y : x ~~> y ↔ ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
+ Proof. rewrite cmra_update_updateP cmra_total_updateP. naive_solver. Qed.
+
+ Context `{CMRADiscrete A}.
+
+ Lemma cmra_discrete_updateP (x : A) (P : A → Prop) :
+ x ~~>: P ↔ ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
+ Proof.
+ rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff.
+ naive_solver eauto using 0.
+ Qed.
+ Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
+ x ~~> y ↔ ∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z).
+ Proof.
+ rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff.
+ naive_solver eauto using 0.
+ Qed.
+End total_updates.
End cmra.
(** * Properties about CMRAs with a unit element **)
Section ucmra.
-Context {A : ucmraT}.
-Implicit Types x y z : A.
+ Context {A : ucmraT}.
+ Implicit Types x y z : A.
+
+ Global Instance ucmra_unit_inhabited : Inhabited A := populate ∅.
+
+ Lemma ucmra_unit_validN n : ✓{n} (∅:A).
+ Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
+ Lemma ucmra_unit_leastN n x : ∅ ≼{n} x.
+ Proof. by exists x; rewrite left_id. Qed.
+ Lemma ucmra_unit_least x : ∅ ≼ x.
+ Proof. by exists x; rewrite left_id. Qed.
+ Global Instance ucmra_unit_right_id : RightId (≡) ∅ (@op A _).
+ Proof. by intros x; rewrite (comm op) left_id. Qed.
+ Global Instance ucmra_unit_persistent : Persistent (∅:A).
+ Proof. apply ucmra_pcore_unit. Qed.
+
+ Global Instance cmra_unit_total : CMRATotal A.
+ Proof.
+ intros x. destruct (cmra_pcore_preserving' ∅ x ∅) as (cx&->&?);
+ eauto using ucmra_unit_least, (persistent ∅).
+ Qed.
-Global Instance ucmra_unit_inhabited : Inhabited A := populate ∅.
-
-Lemma ucmra_unit_validN n : ✓{n} (∅:A).
-Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
-Lemma ucmra_unit_leastN n x : ∅ ≼{n} x.
-Proof. by exists x; rewrite left_id. Qed.
-Lemma ucmra_unit_least x : ∅ ≼ x.
-Proof. by exists x; rewrite left_id. Qed.
-Global Instance ucmra_unit_right_id : RightId (≡) ∅ (@op A _).
-Proof. by intros x; rewrite (comm op) left_id. Qed.
-Global Instance ucmra_unit_persistent : Persistent (∅:A).
-Proof. by rewrite /Persistent -{2}(cmra_core_l ∅) right_id. Qed.
-Lemma ucmra_core_unit : core (∅:A) ≡ ∅.
-Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed.
-
-Lemma ucmra_update_unit x : x ~~> ∅.
-Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
-Lemma ucmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
-Proof. split; [intros; trans ∅|]; auto using ucmra_update_unit. Qed.
+ Lemma ucmra_update_unit x : x ~~> ∅.
+ Proof.
+ apply cmra_total_update=> n z. rewrite left_id; apply cmra_validN_op_r.
+ Qed.
+ Lemma ucmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
+ Proof. split; [intros; trans ∅|]; auto using ucmra_update_unit. Qed.
End ucmra.
+Hint Immediate cmra_unit_total.
+
+(** * Constructing a CMRA with total core *)
+Section cmra_total.
+ Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
+ Context (total : ∀ x, is_Some (pcore x)).
+ Context (op_ne : ∀ n (x : A), Proper (dist n ==> dist n) (op x)).
+ Context (core_ne : ∀ n, Proper (dist n ==> dist n) (@core A _)).
+ Context (validN_ne : ∀ n, Proper (dist n ==> impl) (@validN A _ n)).
+ Context (valid_validN : ∀ (x : A), ✓ x ↔ ∀ n, ✓{n} x).
+ Context (validN_S : ∀ n (x : A), ✓{S n} x → ✓{n} x).
+ Context (op_assoc : Assoc (≡) (@op A _)).
+ Context (op_comm : Comm (≡) (@op A _)).
+ Context (core_l : ∀ x : A, core x ⋅ x ≡ x).
+ Context (core_idemp : ∀ x : A, core (core x) ≡ core x).
+ Context (core_preserving : ∀ x y : A, x ≼ y → core x ≼ core y).
+ Context (validN_op_l : ∀ n (x y : A), ✓{n} (x ⋅ y) → ✓{n} x).
+ Context (extend : ∀ n (x y1 y2 : A),
+ ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
+ { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }).
+ Lemma cmra_total_mixin : CMRAMixin A.
+ Proof.
+ split; auto.
+ - intros n x y ? Hcx%core_ne Hx; move: Hcx. rewrite /core /= Hx /=.
+ case (total y)=> [cy ->]; eauto.
+ - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
+ - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
+ case (total cx)=>[ccx ->]; by constructor.
+ - intros x y cx Hxy%core_preserving Hx. move: Hxy.
+ rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
+ Qed.
+End cmra_total.
(** * Properties about monotone functions *)
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
@@ -579,22 +769,24 @@ End cmra_transport.
(** * Instances *)
(** ** Discrete CMRA *)
-Record RAMixin A `{Equiv A, Core A, Op A, Valid A} := {
+Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
(* setoids *)
- ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x);
- ra_core_ne : Proper ((≡) ==> (≡)) core;
- ra_validN_ne : Proper ((≡) ==> impl) valid;
+ ra_op_proper (x : A) : Proper ((≡) ==> (≡)) (op x);
+ ra_core_proper x y cx :
+ x ≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡ cy;
+ ra_validN_proper : Proper ((≡) ==> impl) valid;
(* monoid *)
ra_assoc : Assoc (≡) (⋅);
ra_comm : Comm (≡) (⋅);
- ra_core_l x : core x ⋅ x ≡ x;
- ra_core_idemp x : core (core x) ≡ core x;
- ra_core_preserving x y : x ≼ y → core x ≼ core y;
+ ra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
+ ra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
+ ra_pcore_preserving x y cx :
+ x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x
}.
Section discrete.
- Context `{Equiv A, Core A, Op A, Valid A, @Equivalence A (≡)}.
+ Context `{Equiv A, PCore A, Op A, Valid A, @Equivalence A (≡)}.
Context (ra_mix : RAMixin A).
Existing Instances discrete_dist discrete_compl.
@@ -612,19 +804,43 @@ Notation discreteR A ra_mix :=
Notation discreteLeibnizR A ra_mix :=
(CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)).
-Global Instance discrete_cmra_discrete `{Equiv A, Core A, Op A, Valid A,
+Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A,
@Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
Proof. split. apply _. done. Qed.
+Section ra_total.
+ Context A `{Equiv A, PCore A, Op A, Valid A}.
+ Context (total : ∀ x, is_Some (pcore x)).
+ Context (op_proper : ∀ (x : A), Proper ((≡) ==> (≡)) (op x)).
+ Context (core_proper: Proper ((≡) ==> (≡)) (@core A _)).
+ Context (valid_proper : Proper ((≡) ==> impl) (@valid A _)).
+ Context (op_assoc : Assoc (≡) (@op A _)).
+ Context (op_comm : Comm (≡) (@op A _)).
+ Context (core_l : ∀ x : A, core x ⋅ x ≡ x).
+ Context (core_idemp : ∀ x : A, core (core x) ≡ core x).
+ Context (core_preserving : ∀ x y : A, x ≼ y → core x ≼ core y).
+ Context (valid_op_l : ∀ x y : A, ✓ (x ⋅ y) → ✓ x).
+ Lemma ra_total_mixin : RAMixin A.
+ Proof.
+ split; auto.
+ - intros x y ? Hcx%core_proper Hx; move: Hcx. rewrite /core /= Hx /=.
+ case (total y)=> [cy ->]; eauto.
+ - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
+ - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
+ case (total cx)=>[ccx ->]; by constructor.
+ - intros x y cx Hxy%core_preserving Hx. move: Hxy.
+ rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
+ Qed.
+End ra_total.
+
(** ** CMRA for the unit type *)
Section unit.
Instance unit_valid : Valid () := λ x, True.
Instance unit_validN : ValidN () := λ n x, True.
- Instance unit_core : Core () := λ x, x.
+ Instance unit_pcore : PCore () := λ x, Some x.
Instance unit_op : Op () := λ x y, ().
-
Lemma unit_cmra_mixin : CMRAMixin ().
- Proof. by split; last exists ((),()). Qed.
+ Proof. apply cmra_total_mixin; try done. eauto. by exists ((),()). Qed.
Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
Instance unit_empty : Empty () := ().
@@ -636,17 +852,34 @@ Section unit.
Global Instance unit_cmra_discrete : CMRADiscrete unitR.
Proof. done. Qed.
Global Instance unit_persistent (x : ()) : Persistent x.
- Proof. done. Qed.
+ Proof. by constructor. Qed.
End unit.
(** ** Product *)
Section prod.
Context {A B : cmraT}.
+ Local Arguments pcore _ _ !_ /.
+ Local Arguments cmra_pcore _ !_/.
+
Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
- Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)).
+ Instance prod_pcore : PCore (A * B) := λ x,
+ c1 ↠pcore (x.1); c2 ↠pcore (x.2); Some (c1, c2).
+ Arguments prod_pcore !_ /.
Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
+ Lemma prod_pcore_Some (x cx : A * B) :
+ pcore x = Some cx ↔ pcore (x.1) = Some (cx.1) ∧ pcore (x.2) = Some (cx.2).
+ Proof. destruct x, cx; by intuition simplify_option_eq. Qed.
+ Lemma prod_pcore_Some' (x cx : A * B) :
+ pcore x ≡ Some cx ↔ pcore (x.1) ≡ Some (cx.1) ∧ pcore (x.2) ≡ Some (cx.2).
+ Proof.
+ split; [by intros (cx'&[-> ->]%prod_pcore_Some&->)%equiv_Some_inv_r'|].
+ rewrite {3}/pcore /prod_pcore. (* TODO: use setoid rewrite *)
+ intros [Hx1 Hx2]; inversion_clear Hx1; simpl; inversion_clear Hx2.
+ by constructor.
+ Qed.
+
Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
Proof.
split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
@@ -662,7 +895,10 @@ Section prod.
Proof.
split; try apply _.
- by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
- - by intros n y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
+ - intros n x y cx; setoid_rewrite prod_pcore_Some=> -[??] [??].
+ destruct (cmra_pcore_ne n (x.1) (y.1) (cx.1)) as (z1&->&?); auto.
+ destruct (cmra_pcore_ne n (x.2) (y.2) (cx.2)) as (z2&->&?); auto.
+ exists (z1,z2); repeat constructor; auto.
- by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
- intros x; split.
+ intros [??] n; split; by apply cmra_valid_validN.
@@ -670,10 +906,14 @@ Section prod.
- by intros n x [??]; split; apply cmra_validN_S.
- by split; rewrite /= assoc.
- by split; rewrite /= comm.
- - by split; rewrite /= cmra_core_l.
- - by split; rewrite /= cmra_core_idemp.
- - intros x y; rewrite !prod_included.
- by intros [??]; split; apply cmra_core_preserving.
+ - intros x y [??]%prod_pcore_Some;
+ constructor; simpl; eauto using cmra_pcore_l.
+ - intros x y; rewrite prod_pcore_Some prod_pcore_Some'.
+ naive_solver eauto using cmra_pcore_idemp.
+ - intros x y cx; rewrite prod_included prod_pcore_Some=> -[??] [??].
+ destruct (cmra_pcore_preserving (x.1) (y.1) (cx.1)) as (z1&?&?); auto.
+ destruct (cmra_pcore_preserving (x.2) (y.2) (cx.2)) as (z2&?&?); auto.
+ exists (z1,z2). by rewrite prod_included prod_pcore_Some.
- intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
- intros n x y1 y2 [??] [??]; simpl in *.
destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
@@ -683,26 +923,36 @@ Section prod.
Canonical Structure prodR :=
CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
+ Global Instance prod_cmra_total : CMRATotal A → CMRATotal B → CMRATotal prodR.
+ Proof.
+ intros H1 H2 [a b]. destruct (H1 a) as [ca ?], (H2 b) as [cb ?].
+ exists (ca,cb); by simplify_option_eq.
+ Qed.
+
Global Instance prod_cmra_discrete :
CMRADiscrete A → CMRADiscrete B → CMRADiscrete prodR.
Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
Global Instance pair_persistent x y :
Persistent x → Persistent y → Persistent (x,y).
- Proof. by split. Qed.
+ Proof. by rewrite /Persistent prod_pcore_Some'. Qed.
- Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
- Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
Proof.
- intros Hx1 Hx2 HP n z [??]; simpl in *.
- destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto.
- exists (a,b); repeat split; auto.
+ intros Hx1 Hx2 HP n mz [??]; simpl in *.
+ destruct (Hx1 n (fst <$> mz)) as (a&?&?); first by destruct mz.
+ destruct (Hx2 n (snd <$> mz)) as (b&?&?); first by destruct mz.
+ exists (a,b); repeat split; destruct mz; auto.
Qed.
Lemma prod_updateP' P1 P2 x :
x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2).
Proof. eauto using prod_updateP. Qed.
+ Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
+ Proof.
+ rewrite !cmra_update_updateP.
+ destruct x, y; eauto using prod_updateP with subst.
+ Qed.
Global Instance prod_local_update
(LA : A → A) `{!LocalUpdate LvA LA} (LB : B → B) `{!LocalUpdate LvB LB} :
@@ -727,6 +977,7 @@ Section prod_unit.
- split; apply ucmra_unit_valid.
- by split; rewrite /=left_id.
- by intros ? [??]; split; apply (timeless _).
+ - rewrite prod_pcore_Some'; split; apply (persistent _).
Qed.
Canonical Structure prodUR :=
UCMRAT (A * B) prod_cofe_mixin prod_cmra_mixin prod_ucmra_mixin.
@@ -793,21 +1044,24 @@ Qed.
(** ** CMRA for the option type *)
Section option.
Context {A : cmraT}.
+ Local Arguments core _ _ !_ /.
+ Local Arguments pcore _ _ !_ /.
Instance option_valid : Valid (option A) := λ mx,
match mx with Some x => ✓ x | None => True end.
Instance option_validN : ValidN (option A) := λ n mx,
match mx with Some x => ✓{n} x | None => True end.
- Instance option_empty : Empty (option A) := None.
-
- Instance option_core : Core (option A) := fmap core.
+ Instance option_pcore : PCore (option A) := λ mx, Some (mx ≫= pcore).
+ Arguments option_pcore !_ /.
Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
+ Lemma Some_core `{CMRATotal A} a : Some (core a) = core (Some a).
+ Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
Lemma option_included (mx my : option A) :
- mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y.
+ mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ (x ≼ y ∨ x ≡ y).
Proof.
split.
- intros [mz Hmz].
@@ -815,24 +1069,33 @@ Section option.
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
setoid_subst; eauto using cmra_included_l.
- - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
- by exists (Some z); constructor.
+ - intros [->|(x&y&->&->&[[z Hz]|Hz])].
+ + exists my. by destruct my.
+ + exists (Some z); by constructor.
+ + exists None; by constructor.
Qed.
Lemma option_cmra_mixin : CMRAMixin (option A).
Proof.
- split.
+ apply cmra_total_mixin.
+ - eauto.
- by intros n [x|]; destruct 1; constructor; cofe_subst.
- - by destruct 1; constructor; cofe_subst.
+ - destruct 1; by cofe_subst.
- by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
- intros [x|]; [apply cmra_valid_validN|done].
- intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
- intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
- intros [x|] [y|]; constructor; rewrite 1?comm; auto.
- - by intros [x|]; constructor; rewrite cmra_core_l.
- - by intros [x|]; constructor; rewrite cmra_core_idemp.
- - intros mx my; rewrite !option_included ;intros [->|(x&y&->&->&?)]; auto.
- right; exists (core x), (core y); eauto using cmra_core_preserving.
+ - intros [x|]; simpl; auto.
+ destruct (pcore x) as [cx|] eqn:?; constructor; eauto using cmra_pcore_l.
+ - intros [x|]; simpl; auto.
+ destruct (pcore x) as [cx|] eqn:?; simpl; eauto using cmra_pcore_idemp.
+ - intros mx my; setoid_rewrite option_included.
+ intros [->|(x&y&->&->&[?|?])]; simpl; eauto.
+ + destruct (pcore x) as [cx|] eqn:?; eauto.
+ destruct (cmra_pcore_preserving x y cx) as (?&?&?); eauto 10.
+ + destruct (pcore x) as [cx|] eqn:?; eauto.
+ destruct (cmra_pcore_proper x y cx) as (?&?&?); eauto 10.
- intros n [x|] [y|]; rewrite /validN /option_validN /=;
eauto using cmra_validN_op_l.
- intros n mx my1 my2.
@@ -851,8 +1114,9 @@ Section option.
Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
+ Instance option_empty : Empty (option A) := None.
Lemma option_ucmra_mixin : UCMRAMixin optionR.
- Proof. split. done. by intros []. by inversion_clear 1. Qed.
+ Proof. split. done. by intros []. by inversion_clear 1. done. Qed.
Canonical Structure optionUR :=
UCMRAT (option A) option_cofe_mixin option_cmra_mixin option_ucmra_mixin.
@@ -872,16 +1136,16 @@ Section option.
Proof. by constructor. Qed.
Global Instance option_persistent (mx : option A) :
(∀ x : A, Persistent x) → Persistent mx.
- Proof. intros. destruct mx. apply _. constructor. Qed.
+ Proof. intros. destruct mx; apply _. Qed.
(** Updates *)
Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
Proof.
- intros Hx Hy n [y|] ?.
- { destruct (Hx n y) as (y'&?&?); auto. exists (Some y'); auto. }
- destruct (Hx n (core x)) as (y'&?&?); rewrite ?cmra_core_r; auto.
- by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
+ intros Hx Hy; apply cmra_total_updateP=> n [y|] ?.
+ { destruct (Hx n (Some y)) as (y'&?&?); auto. exists (Some y'); auto. }
+ destruct (Hx n None) as (y'&?&?); rewrite ?cmra_core_r; auto.
+ by exists (Some y'); auto.
Qed.
Lemma option_updateP' (P : A → Prop) x :
x ~~>: P → Some x ~~>: from_option P False.
@@ -901,7 +1165,8 @@ Proof.
split; first apply _.
- intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f).
- intros mx my; rewrite !option_included.
- intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @included_preserving.
+ intros [->|(x&y&->&->&[?|Hxy])]; simpl; eauto 10 using @included_preserving.
+ right; exists (f x), (f y). by rewrite {4}Hxy; eauto.
Qed.
Program Definition optionURF (F : rFunctor) : urFunctor := {|
urFunctor_car A B := optionUR (rFunctor_car F A B);
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 6ef5c1332e68716257ff3f93b34556a1999724be..dcfaa63558459411457966b8a864ed7f2640dee6 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -88,6 +88,8 @@ Section cofe_mixin.
Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.
+Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
+
(** Discrete COFEs and Timeless elements *)
(* TODO: On paper, We called these "discrete elements". I think that makes
more sense. *)
@@ -151,8 +153,7 @@ Section cofe.
Qed.
Lemma timeless_iff n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y.
Proof.
- split; intros; [by apply equiv_dist|].
- apply (timeless _), dist_le with n; auto with lia.
+ split; intros; auto. apply (timeless _), dist_le with n; auto with lia.
Qed.
End cofe.
@@ -569,6 +570,9 @@ Section option.
Proof. destruct 1; split; eauto. Qed.
Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
Proof. by inversion_clear 1. Qed.
+ Global Instance from_option_ne {B} (R : relation B) (f : A → B) n :
+ Proper (dist n ==> R) f → Proper (R ==> dist n ==> R) (from_option f).
+ Proof. destruct 3; simpl; auto. Qed.
Global Instance None_timeless : Timeless (@None A).
Proof. inversion_clear 1; constructor. Qed.
@@ -592,14 +596,9 @@ End option.
Typeclasses Opaque option_dist.
Arguments optionC : clear implicits.
-Instance from_option_ne {A B : cofeT} (f : A → B) n :
- Proper (dist n ==> dist n) f →
- Proper (dist n ==> dist n ==> dist n) (from_option f).
-Proof. destruct 3; simpl; auto. Qed.
-
-Instance option_fmap_ne {A B : cofeT} (f : A → B) n:
- Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
-Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
+Instance option_fmap_ne {A B : cofeT} n:
+ Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
+Proof. intros f f' Hf ?? []; constructor; auto. Qed.
Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
CofeMor (fmap f : optionC A → optionC B).
Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 07352633a70f500e7d48caf421a33381fe4d97b4..4fe1fba88d68a5b696726e114b874695636790be 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -2,7 +2,7 @@ From iris.algebra Require Export cmra.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
-Local Arguments core _ _ !_ /.
+Local Arguments pcore _ _ !_ /.
(* This is isomorphic to option, but has a very different RA structure. *)
Inductive dec_agree (A : Type) : Type :=
@@ -26,19 +26,19 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
| DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
| _, _ => DecAgreeBot
end.
-Instance dec_agree_core : Core (dec_agree A) := id.
+Instance dec_agree_pcore : PCore (dec_agree A) := Some.
Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof.
split.
- apply _.
- - apply _.
+ - intros x y cx ? [=<-]; eauto.
- apply _.
- intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
+ - intros [?|] ? [=<-]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- - intros [?|]; by repeat (simplify_eq/= || case_match).
- - by intros [?|] [?|] ?.
+ - intros [?|] [?|] ?? [=<-]; eauto.
- by intros [?|] [?|] ?.
Qed.
@@ -47,7 +47,7 @@ Canonical Structure dec_agreeR : cmraT :=
(* Some properties of this CMRA *)
Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
-Proof. done. Qed.
+Proof. by constructor. Qed.
Lemma dec_agree_ne a b : a ≠b → DecAgree a ⋅ DecAgree b = DecAgreeBot.
Proof. intros. by rewrite /= decide_False. Qed.
diff --git a/algebra/dra.v b/algebra/dra.v
index 6d2e9c893d5213475856f921e0a61b39b42259d2..e4e46c1eb91ebc494acd342ca42b8170b4415c70 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -142,8 +142,8 @@ Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
-Program Instance validity_core : Core (validity A) := λ x,
- Validity (core (validity_car x)) (✓ x) _.
+Program Instance validity_pcore : PCore (validity A) := λ x,
+ Some (Validity (core (validity_car x)) (✓ x) _).
Solve Obligations with naive_solver eauto using dra_core_valid.
Program Instance validity_op : Op (validity A) := λ x y,
Validity (validity_car x â‹… validity_car y)
@@ -152,7 +152,7 @@ Solve Obligations with naive_solver eauto using dra_op_valid.
Definition validity_ra_mixin : RAMixin (validity A).
Proof.
- split.
+ apply ra_total_mixin; first eauto.
- intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
split; intros (?&?&?); split_and!;
first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
@@ -176,6 +176,9 @@ Qed.
Canonical Structure validityR : cmraT :=
discreteR (validity A) validity_ra_mixin.
+Global Instance validity_cmra_total : CMRATotal validityR.
+Proof. rewrite /CMRATotal; eauto. Qed.
+
Lemma validity_update x y :
(∀ c, ✓ x → ✓ c → validity_car x ⊥ c → ✓ y ∧ validity_car y ⊥ c) → x ~~> y.
Proof.
diff --git a/algebra/excl.v b/algebra/excl.v
index 994f9ab9f45cdd7564e8b4041271fd9baed6b1b4..5e83c0e59a44fa3aa049249d3be553ea23cd5699 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -5,11 +5,13 @@ Local Arguments valid _ _ !_ /.
Inductive excl (A : Type) :=
| Excl : A → excl A
- | ExclUnit : excl A
| ExclBot : excl A.
Arguments Excl {_} _.
-Arguments ExclUnit {_}.
Arguments ExclBot {_}.
+
+Notation Excl' x := (Some (Excl x)).
+Notation ExclBot' := (Some ExclBot).
+
Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
match x with Excl a => Some a | _ => None end.
@@ -21,12 +23,10 @@ Implicit Types x y : excl A.
(* Cofe *)
Inductive excl_equiv : Equiv (excl A) :=
| Excl_equiv a b : a ≡ b → Excl a ≡ Excl b
- | ExclUnit_equiv : ExclUnit ≡ ExclUnit
| ExclBot_equiv : ExclBot ≡ ExclBot.
Existing Instance excl_equiv.
Inductive excl_dist : Dist (excl A) :=
| Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b
- | ExclUnit_dist n : ExclUnit ≡{n}≡ ExclUnit
| ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
Existing Instance excl_dist.
@@ -67,43 +67,31 @@ Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
Global Instance Excl_timeless a : Timeless a → Timeless (Excl a).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
-Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
-Proof. by inversion_clear 1; constructor. Qed.
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
(* CMRA *)
Instance excl_valid : Valid (excl A) := λ x,
- match x with Excl _ | ExclUnit => True | ExclBot => False end.
+ match x with Excl _ => True | ExclBot => False end.
Instance excl_validN : ValidN (excl A) := λ n x,
- match x with Excl _ | ExclUnit => True | ExclBot => False end.
-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
- | ExclUnit, ExclUnit => ExclUnit
- | _, _=> ExclBot
- end.
+ match x with Excl _ => True | ExclBot => False end.
+Instance excl_pcore : PCore (excl A) := λ _, None.
+Instance excl_op : Op (excl A) := λ x y, ExclBot.
Lemma excl_cmra_mixin : CMRAMixin (excl A).
Proof.
- split.
+ split; try discriminate.
- by intros n []; destruct 1; constructor.
- - constructor.
- by destruct 1; intros ?.
- intros x; split. done. by move=> /(_ 0).
- - intros n [?| |]; simpl; auto with lia.
- - by intros [?| |] [?| |] [?| |]; constructor.
- - by intros [?| |] [?| |]; constructor.
- - by intros [?| |]; constructor.
- - constructor.
- - by intros [?| |] [?| |]; exists ExclUnit.
- - by intros n [?| |] [?| |].
+ - intros n [?|]; simpl; auto with lia.
+ - by intros [?|] [?|] [?|]; constructor.
+ - by intros [?|] [?|]; constructor.
+ - by intros n [?|] [?|].
- intros n x y1 y2 ? Hx.
by exists match y1, y2 with
| Excl a1, Excl a2 => (Excl a1, Excl a2)
| ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
- | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
Qed.
Canonical Structure exclR :=
@@ -112,57 +100,49 @@ Canonical Structure exclR :=
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 = ∅.
-Proof. by destruct x. Qed.
-Lemma Excl_includedN n a x : ✓{n} x → Excl a ≼{n} x ↔ x ≡{n}≡ Excl a.
-Proof.
- intros Hvalid; split; [|by intros ->].
- intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a).
-Qed.
-
(** Internalized properties *)
Lemma excl_equivI {M} (x y : excl A) :
(x ≡ y) ⊣⊢ (match x, y with
| Excl a, Excl b => a ≡ b
- | ExclUnit, ExclUnit | ExclBot, ExclBot => True
+ | ExclBot, ExclBot => True
| _, _ => False
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma excl_validI {M} (x : excl A) :
- (✓ x) ⊣⊢ (if x is ExclBot then False else True : uPred M).
+ ✓ x ⊣⊢ (if x is ExclBot then False else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *)
Global Instance excl_local_update y :
LocalUpdate (λ x, if x is Excl _ then ✓ y else False) (λ _, y).
-Proof. split. apply _. by destruct y; intros n [a| |] [b'| |]. Qed.
+Proof. split. apply _. by destruct y; intros n [a|] [b'|]. Qed.
(** Updates *)
Lemma excl_update a y : ✓ y → Excl a ~~> y.
-Proof. destruct y; by intros ?? [?| |]. Qed.
+Proof. destruct y=> ? n [z|]; eauto. Qed.
Lemma excl_updateP (P : excl A → Prop) a y : ✓ y → P y → Excl a ~~>: P.
-Proof. intros ?? n z ?; exists y. by destruct y, z as [?| |]. Qed.
+Proof. destruct y=> ?? n [z|]; eauto. Qed.
+
+(** Option excl *)
+Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None.
+Proof. by destruct mx. Qed.
+Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None.
+Proof. by destruct mx. Qed.
+Lemma Excl_includedN n a mx : ✓{n} mx → Excl' a ≼{n} mx ↔ mx ≡{n}≡ Excl' a.
+Proof.
+ intros Hvalid; split; [|by intros ->].
+ intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a).
+Qed.
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 :=
- match x with
- | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
- end.
+ match x with Excl a => Excl (f a) | ExclBot => ExclBot end.
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
Proof. by destruct x. Qed.
Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
@@ -171,14 +151,14 @@ Proof. by destruct x. Qed.
Lemma excl_map_ext {A B : cofeT} (f g : A → B) x :
(∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
Proof. by destruct x; constructor. Qed.
-Instance excl_map_cmra_ne {A B : cofeT} n :
+Instance excl_map_ne {A B : cofeT} n :
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.
Instance excl_map_cmra_monotone {A B : cofeT} (f : A → B) :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f).
Proof.
split; try apply _.
- - by intros n [a| |].
+ - by intros n [a|].
- intros x y [z Hy]; exists (excl_map f z); apply equiv_dist=> n.
move: Hy=> /equiv_dist /(_ n) ->; by destruct x, z.
Qed.
@@ -187,9 +167,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 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)
+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.
intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
@@ -203,8 +183,8 @@ Next Obligation.
apply excl_map_ext=>y; apply cFunctor_compose.
Qed.
-Instance exclURF_contractive F :
- cFunctorContractive F → urFunctorContractive (exclURF F).
+Instance exclRF_contractive F :
+ cFunctorContractive F → rFunctorContractive (exclRF F).
Proof.
intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
Qed.
diff --git a/algebra/frac.v b/algebra/frac.v
index e4f7897d268a17804ad717698fbf942a2d1a7a6b..6581ce2534a0d5926a2290f0089c4f73d6b00860 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -1,15 +1,15 @@
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
+Local Arguments op _ _ !_ !_ /.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
-Inductive frac {A : Type} :=
- | Frac : Qp → A → frac
- | FracUnit : frac.
-Arguments frac _ : clear implicits.
-Instance maybe_Frac {A} : Maybe2 (@Frac A) := λ x,
- match x with Frac q a => Some (q,a) | _ => None end.
+Inductive frac A := Frac { frac_perm : Qp ; frac_car : A }.
+Add Printing Constructor frac.
+Arguments Frac {_} _ _.
+Arguments frac_perm {_} _.
+Arguments frac_car {_} _.
Instance: Params (@Frac) 2.
Section cofe.
@@ -18,37 +18,37 @@ Implicit Types a b : A.
Implicit Types x y : frac A.
(* Cofe *)
-Inductive frac_equiv : Equiv (frac A) :=
- | Frac_equiv q1 q2 a b : q1 = q2 → a ≡ b → Frac q1 a ≡ Frac q2 b
- | FracUnit_equiv : FracUnit ≡ FracUnit.
-Existing Instance frac_equiv.
-Inductive frac_dist : Dist (frac A) :=
- | Frac_dist q1 q2 a b n : q1 = q2 → a ≡{n}≡ b → Frac q1 a ≡{n}≡ Frac q2 b
- | FracUnit_dist n : FracUnit ≡{n}≡ FracUnit.
-Existing Instance frac_dist.
+Instance frac_equiv : Equiv (frac A) := λ x y,
+ frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y.
+Instance frac_dist : Dist (frac A) := λ n x y,
+ frac_perm x = frac_perm y ∧ frac_car x ≡{n}≡ frac_car y.
Global Instance Frac_ne q n : Proper (dist n ==> dist n) (@Frac A q).
Proof. by constructor. Qed.
Global Instance Frac_proper q : Proper ((≡) ==> (≡)) (@Frac A q).
Proof. by constructor. Qed.
Global Instance Frac_inj : Inj2 (=) (≡) (≡) (@Frac A).
-Proof. by inversion_clear 1. Qed.
+Proof. by destruct 1. Qed.
Global Instance Frac_dist_inj n : Inj2 (=) (dist n) (dist n) (@Frac A).
-Proof. by inversion_clear 1. Qed.
-
-Program Definition frac_chain (c : chain (frac A)) (q : Qp) (a : A)
- (H : maybe2 Frac (c 0) = Some (q,a)) : chain A :=
- {| chain_car n := match c n return _ with Frac _ b => b | _ => a end |}.
+Proof. by destruct 1. Qed.
+
+Global Instance frac_perm_ne n : Proper (dist n ==> (=)) (@frac_perm A).
+Proof. by destruct 1. Qed.
+Global Instance frac_car_ne n : Proper (dist n ==> dist n) (@frac_car A).
+Proof. by destruct 1. Qed.
+Global Instance frac_perm_proper : Proper ((≡) ==> (=)) (@frac_perm A).
+Proof. by destruct 1. Qed.
+Global Instance frac_car_proper : Proper ((≡) ==> (≡)) (@frac_car A).
+Proof. by destruct 1. Qed.
+
+Program Definition frac_chain (c : chain (frac A)) : chain A :=
+ {| chain_car n := match c n return _ with Frac _ b => b end |}.
Next Obligation.
- intros c q a ? n i ?; simpl.
- destruct (c 0) eqn:?; simplify_eq/=.
+ intros c n i ?; simpl. destruct (c 0) eqn:?; simplify_eq/=.
by feed inversion (chain_cauchy c n i).
Qed.
Instance frac_compl : Compl (frac A) := λ c,
- match Some_dec (maybe2 Frac (c 0)) with
- | inleft (exist (q,a) H) => Frac q (compl (frac_chain c q a H))
- | inright _ => c 0
- end.
+ Frac (frac_perm (c 0)) (compl (frac_chain c)).
Definition frac_cofe_mixin : CofeMixin (frac A).
Proof.
split.
@@ -57,40 +57,29 @@ Proof.
+ intros Hxy; feed inversion (Hxy 0); subst; constructor; try done.
apply equiv_dist=> n; by feed inversion (Hxy n).
- intros n; split.
- + by intros [q a|]; constructor.
+ + by intros [q a]; constructor.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; done || apply dist_S.
- - intros n c; unfold compl, frac_compl.
- destruct (Some_dec (maybe2 Frac (c 0))) as [[[q a] Hx]|].
- { assert (c 0 = Frac q a) by (by destruct (c 0); simplify_eq/=).
- assert (∃ b, c n = Frac q b) as [y Hy].
- { feed inversion (chain_cauchy c 0 n);
- eauto with lia congruence f_equal. }
- rewrite Hy; constructor; auto.
- by rewrite (conv_compl n (frac_chain c q a Hx)) /= Hy. }
- feed inversion (chain_cauchy c 0 n); first lia;
- constructor; destruct (c 0); simplify_eq/=.
+ - intros n c; constructor; simpl.
+ + destruct (chain_cauchy c 0 n); auto with lia.
+ + apply (conv_compl n (frac_chain c)).
Qed.
Canonical Structure fracC : cofeT := CofeT (frac A) frac_cofe_mixin.
Global Instance frac_discrete : Discrete A → Discrete fracC.
Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
Global Instance frac_leibniz : LeibnizEquiv A → LeibnizEquiv (frac A).
-Proof. by destruct 2; f_equal; done || apply leibniz_equiv. Qed.
+Proof. intros ? [??] [??] [??]; f_equal; done || by apply leibniz_equiv. Qed.
Global Instance Frac_timeless q (a : A) : Timeless a → Timeless (Frac q a).
Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
-Global Instance FracUnit_timeless : Timeless (@FracUnit A).
-Proof. by inversion_clear 1; constructor. Qed.
End cofe.
Arguments fracC : clear implicits.
(* Functor on COFEs *)
Definition frac_map {A B} (f : A → B) (x : frac A) : frac B :=
- match x with
- | Frac q a => Frac q (f a) | FracUnit => FracUnit
- end.
+ match x with Frac q a => Frac q (f a) end.
Instance: Params (@frac_map) 2.
Lemma frac_map_id {A} (x : frac A) : frac_map id x = x.
@@ -100,10 +89,10 @@ Lemma frac_map_compose {A B C} (f : A → B) (g : B → C) (x : frac A) :
Proof. by destruct x. Qed.
Lemma frac_map_ext {A B : cofeT} (f g : A → B) x :
(∀ x, f x ≡ g x) → frac_map f x ≡ frac_map g x.
-Proof. by destruct x; constructor. Qed.
+Proof. destruct x; constructor; simpl; auto. Qed.
Instance frac_map_cmra_ne {A B : cofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@frac_map A B).
-Proof. intros f f' Hf; destruct 1; constructor; by try apply Hf. Qed.
+Proof. intros f f' Hf [??] [??] [??]; constructor; by try apply Hf. Qed.
Definition fracC_map {A B} (f : A -n> B) : fracC A -n> fracC B :=
CofeMor (frac_map f).
Instance fracC_map_ne A B n : Proper (dist n ==> dist n) (@fracC_map A B).
@@ -114,131 +103,103 @@ Context {A : cmraT}.
Implicit Types a b : A.
Implicit Types x y : frac A.
-(* CMRA *)
Instance frac_valid : Valid (frac A) := λ x,
- match x with Frac q a => (q ≤ 1)%Qc ∧ ✓ a | FracUnit => True end.
+ (frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x.
+Global Arguments frac_valid !_/.
Instance frac_validN : ValidN (frac A) := λ n x,
- match x with Frac q a => (q ≤ 1)%Qc ∧ ✓{n} a | FracUnit => True end.
-Instance frac_core : Core (frac A) := λ _, FracUnit.
+ (frac_perm x ≤ 1)%Qc ∧ ✓{n} frac_car x.
+Global Arguments frac_validN _ !_/.
+Instance frac_pcore : PCore (frac A) := λ _, None.
Instance frac_op : Op (frac A) := λ x y,
- match x, y with
- | Frac q1 a, Frac q2 b => Frac (q1 + q2) (a â‹… b)
- | Frac q a, FracUnit | FracUnit, Frac q a => Frac q a
- | FracUnit, FracUnit => FracUnit
- end.
+ Frac (frac_perm x + frac_perm y) (frac_car x â‹… frac_car y).
+Global Arguments frac_op !_ !_ /.
Lemma Frac_op q1 q2 a b : Frac q1 a â‹… Frac q2 b = Frac (q1 + q2) (a â‹… b).
Proof. done. Qed.
Definition frac_cmra_mixin : CMRAMixin (frac A).
Proof.
- split.
- - intros n []; destruct 1; constructor; by cofe_subst.
- - constructor.
- - do 2 destruct 1; split; by cofe_subst.
- - intros [q a|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
- - intros n [q a|]; destruct 1; split; auto using cmra_validN_S.
- - intros [q1 a1|] [q2 a2|] [q3 a3|]; constructor; by rewrite ?assoc.
- - intros [q1 a1|] [q2 a2|]; constructor; by rewrite 1?comm ?[(q1+_)%Qp]comm.
- - intros []; by constructor.
- - done.
- - by exists FracUnit.
- - intros n [q1 a1|] [q2 a2|]; destruct 1; split; eauto using cmra_validN_op_l.
+ split; try discriminate.
+ - intros n [??] [??] [??] [??]; constructor; by cofe_subst.
+ - intros ? [??] [??] [??] [??]; split; by cofe_subst.
+ - intros [??]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
+ - intros n [q a]; destruct 1; split; auto using cmra_validN_S.
+ - intros [q1 a1] [q2 a2] [q3 a3]; constructor; by rewrite /= ?assoc.
+ - intros [q1 a1] [q2 a2]; constructor; by rewrite /= 1?comm ?[(q1+_)%Qp]comm.
+ - intros n [q1 a1] [q2 a2]; destruct 1; split; eauto using cmra_validN_op_l.
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 (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, FracUnit); inversion_clear Hx'; by repeat constructor.
- + exists (FracUnit, Frac q a); inversion_clear Hx'; by repeat constructor.
- + exfalso; inversion_clear Hx'.
+ - intros n [q a] y1 y2 Hx 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.
Qed.
-Canonical Structure fracR :=
- CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin.
+Canonical Structure fracR := CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin.
Global Instance frac_cmra_discrete : CMRADiscrete A → CMRADiscrete fracR.
Proof.
split; first apply _.
- intros [q a|]; destruct 1; split; auto using cmra_discrete_valid.
+ 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 = ∅.
+Lemma frac_validN_inv_l n x y : ✓{n} (x ⋅ y) → frac_perm x ≠1%Qp.
Proof.
- destruct y as [q b|]; [|done]=> -[Hq ?]; destruct (Qcle_not_lt _ _ Hq).
- by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
+ intros [Hq _] Hx; simpl in *; destruct (Qcle_not_lt _ _ Hq).
+ by rewrite Hx -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
Qed.
-Lemma frac_valid_inv_l y a : ✓ (Frac 1 a ⋅ y) → y = ∅.
-Proof. intros. by apply frac_validN_inv_l with 0 a, cmra_valid_validN. Qed.
+Lemma frac_valid_inv_l x y : ✓ (x ⋅ y) → frac_perm x ≠1%Qp.
+Proof. intros. by apply frac_validN_inv_l with 0 y, cmra_valid_validN. Qed.
(** Internalized properties *)
Lemma frac_equivI {M} (x y : frac A) :
- (x ≡ y) ⊣⊢ (match x, y with
- | Frac q1 a, Frac q2 b => q1 = q2 ∧ a ≡ b
- | FracUnit, FracUnit => True
- | _, _ => False
- end : uPred M).
-Proof.
- uPred.unseal; do 2 split; first by destruct 1.
- by destruct x, y; destruct 1; try constructor.
-Qed.
+ (x ≡ y) ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M).
+Proof. by uPred.unseal. Qed.
Lemma frac_validI {M} (x : frac A) :
- (✓ x) ⊣⊢ (if x is Frac q a then ■(q ≤ 1)%Qc ∧ ✓ a else True : uPred M).
-Proof. uPred.unseal. by destruct x. Qed.
+ ✓ x ⊣⊢ (■(frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x : uPred M).
+Proof. by uPred.unseal. Qed.
(** ** Local updates *)
Global Instance frac_local_update_full p a :
- LocalUpdate (λ x, if x is Frac q _ then q = 1%Qp else False) (λ _, Frac p a).
-Proof.
- split; first by intros ???.
- by intros n [q b|] y; [|done]=> -> /frac_validN_inv_l ->.
-Qed.
+ LocalUpdate (λ x, frac_perm x = 1%Qp) (λ _, Frac p a).
+Proof. split; first by intros ???. by intros n x y ? ?%frac_validN_inv_l. Qed.
Global Instance frac_local_update `{!LocalUpdate Lv L} :
- LocalUpdate (λ x, if x is Frac _ a then Lv a else False) (frac_map L).
+ LocalUpdate (λ x, Lv (frac_car x)) (frac_map L).
Proof.
- split; first apply _. intros n [p a|] [q b|]; simpl; try done.
+ split; first apply _. intros n [p a] [q b]; simpl.
intros ? [??]; constructor; [done|by apply (local_updateN L)].
Qed.
(** Updates *)
Lemma frac_update_full (a1 a2 : A) : ✓ a2 → Frac 1 a1 ~~> Frac 1 a2.
Proof.
- move=> ? n y /frac_validN_inv_l ->. split. done. by apply cmra_valid_validN.
+ move=> ? n [y|]; last (intros; by apply cmra_valid_validN).
+ by intros ?%frac_validN_inv_l.
Qed.
Lemma frac_update (a1 a2 : A) p : a1 ~~> a2 → Frac p a1 ~~> Frac p a2.
Proof.
- intros Ha n [q b|] [??]; split; auto.
- apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r.
+ intros Ha n mz [??]; split; first by destruct mz.
+ pose proof (Ha n (frac_car <$> mz)); destruct mz; naive_solver.
Qed.
End cmra.
Arguments fracR : clear implicits.
-Arguments fracUR : clear implicits.
(* Functor *)
Instance frac_map_cmra_monotone {A B : cmraT} (f : A → B) :
CMRAMonotone f → CMRAMonotone (frac_map f).
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: ucmra_unit_least; auto.
+ - intros n [p a]; destruct 1; split; simpl in *; auto using validN_preserving.
+ - intros [q1 a1] [q2 a2] [[q3 a3] [??]]; setoid_subst.
destruct (included_preserving f a1 (a1 â‹… a3)) as [b ?].
{ by apply cmra_included_l. }
by exists (Frac q3 b); constructor.
Qed.
-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)
+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)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_ne.
@@ -252,8 +213,8 @@ Next Obligation.
apply frac_map_ext=>y; apply rFunctor_compose.
Qed.
-Instance fracURF_contractive F :
- rFunctorContractive F → urFunctorContractive (fracURF F).
+Instance fracRF_contractive F :
+ rFunctorContractive F → rFunctorContractive (fracRF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive.
Qed.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index f209cf09c39d3435dc9867ca54d12842c533b38e..accb4f183b04d48e4a955a7f81279b348ace4ada 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -93,14 +93,14 @@ Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K A.
Instance gmap_op : Op (gmap K A) := merge op.
-Instance gmap_core : Core (gmap K A) := fmap core.
+Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
Instance gmap_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
Instance gmap_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_core m i : core m !! i = core (m !! i).
-Proof. by apply lookup_fmap. Qed.
+Proof. by apply lookup_omap. Qed.
Lemma lookup_included (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
Proof.
@@ -120,20 +120,21 @@ Qed.
Lemma gmap_cmra_mixin : CMRAMixin (gmap K A).
Proof.
- split.
- - by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
- - by intros n m1 m2 Hm i; rewrite !lookup_core (Hm i).
- - by intros n m1 m2 Hm ? i; rewrite -(Hm i).
+ 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; apply cmra_validN_S, Hm.
- by intros m1 m2 m3 i; rewrite !lookup_op assoc.
- by intros m1 m2 i; rewrite !lookup_op comm.
- - by intros m i; rewrite lookup_op !lookup_core cmra_core_l.
- - by intros m i; rewrite !lookup_core cmra_core_idemp.
- - intros x y; rewrite !lookup_included; intros Hm i.
- by rewrite !lookup_core; apply cmra_core_preserving.
+ - 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_preserving.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- intros n m m1 m2 Hm Hm12.
@@ -164,6 +165,7 @@ Proof.
- by intros i; rewrite lookup_empty.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- apply gmap_empty_timeless.
+ - constructor=> i. by rewrite lookup_omap lookup_empty.
Qed.
Canonical Structure gmapUR :=
UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
@@ -201,42 +203,51 @@ Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
Lemma insert_singleton_opN n m i x :
- m !! i = None ∨ m !! i ≡{n}≡ Some (core x) → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m.
+ m !! i = None → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m.
Proof.
- intros Hi j; destruct (decide (i = j)) as [->|];
- [|by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id].
- rewrite lookup_op lookup_insert lookup_singleton.
- by destruct Hi as [->| ->]; constructor; rewrite ?cmra_core_r.
+ intros Hi j; destruct (decide (i = j)) as [->|].
+ - by rewrite lookup_op lookup_insert lookup_singleton Hi right_id.
+ - by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id.
Qed.
-Lemma insert_singleton_op m i x :
- m !! i = None ∨ m !! i ≡ Some (core x) → <[i:=x]> m ≡ {[ i := x ]} ⋅ m.
+Lemma insert_singleton_op m i x : m !! i = None → <[i:=x]> m ≡ {[ i := x ]} ⋅ m.
Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed.
-Lemma core_singleton (i : K) (x : A) :
- core ({[ i := x ]} : gmap K A) = {[ i := core x ]}.
-Proof. apply map_fmap_singleton. Qed.
+Lemma core_singleton (i : K) (x : A) cx :
+ pcore x = Some cx → core ({[ i := x ]} : gmap K A) = {[ i := cx ]}.
+Proof. apply omap_singleton. Qed.
+Lemma core_singleton' (i : K) (x : A) cx :
+ pcore x ≡ Some cx → core ({[ i := x ]} : gmap K A) ≡ {[ i := cx ]}.
+Proof.
+ intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx').
+Qed.
Lemma op_singleton (i : K) (x y : A) :
{[ i := x ]} â‹… {[ i := y ]} = ({[ i := x â‹… y ]} : gmap K A).
Proof. by apply (merge_singleton _ _ _ x y). Qed.
Global Instance gmap_persistent m : (∀ x : A, Persistent x) → Persistent m.
-Proof. intros ? i. by rewrite lookup_core persistent. Qed.
+Proof.
+ intros; apply persistent_total=> i.
+ rewrite lookup_core. apply (persistent_core _).
+Qed.
Global Instance gmap_singleton_persistent i (x : A) :
Persistent x → Persistent {[ i := x ]}.
-Proof. intros. by rewrite /Persistent core_singleton persistent. Qed.
+Proof. intros. by apply persistent_total, core_singleton'. Qed.
Lemma singleton_includedN n m i x :
- {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ x ≼{n} y.
+ {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ (x ≼{n} y ∨ x ≡{n}≡ y).
Proof.
split.
- move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
case (m' !! i)=> [y|]=> Hm.
+ exists (x â‹… y); eauto using cmra_includedN_l.
- + by exists x.
- - intros (y&Hi&[z ?]).
- exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|].
- + rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
- + by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
+ + exists x; eauto.
+ - intros (y&Hi&[[z ?]| ->]).
+ + exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|].
+ * rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
+ * by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
+ + exists (delete i m)=> j; destruct (decide (i = j)) as [->|].
+ * by rewrite Hi lookup_op lookup_singleton lookup_delete.
+ * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
Qed.
Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2.
Proof.
@@ -248,8 +259,8 @@ 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 n mf Hm.
- destruct (Hx n (mf !! i)) as ([y|]&?&?); try done.
+ 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.
@@ -275,14 +286,15 @@ Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma updateP_alloc_strong (Q : gmap K A → Prop) (I : gset K) m x :
✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
Proof.
- intros ? HQ n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
+ intros ? HQ. apply cmra_total_updateP.
+ intros n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]].
{ rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
exists (<[i:=x]>m); split.
{ by apply HQ; last done; apply not_elem_of_dom. }
- rewrite insert_singleton_opN; last by left; apply not_elem_of_dom.
+ rewrite insert_singleton_opN; last by apply not_elem_of_dom.
rewrite -assoc -insert_singleton_opN;
- last by left; apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
+ last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
by apply insert_validN; [apply cmra_valid_validN|].
Qed.
Lemma updateP_alloc (Q : gmap K A → Prop) m x :
@@ -299,15 +311,15 @@ 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).
+ 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); simpl; first done. intros; by apply cmra_valid_validN. }
+ 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); first done.
- by rewrite /= (comm _ y) left_id right_id.
+ move:Hy; case _: (gf !! i)=>[x|]; rewrite /= ?right_id //.
- move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
Qed.
Lemma singleton_updateP_unit' (P: A → Prop) u i :
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 111b7d47eb4ec48fe7a34a87595c4e229087e81b..ecb2ac1cae3587fab8ede88576105c9b122b72b6 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -85,7 +85,7 @@ Section iprod_cmra.
Implicit Types f g : iprod B.
Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
- Instance iprod_core : Core (iprod B) := λ f x, core (f x).
+ Instance iprod_pcore : PCore (iprod B) := λ f, Some (λ x, core (f x)).
Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x.
Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
@@ -100,7 +100,8 @@ Section iprod_cmra.
Lemma iprod_cmra_mixin : CMRAMixin (iprod B).
Proof.
- split.
+ apply cmra_total_mixin.
+ - eauto.
- by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
- by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
- by intros n f1 f2 Hf ? x; rewrite -(Hf x).
@@ -132,6 +133,7 @@ Section iprod_cmra.
- intros x; apply ucmra_unit_valid.
- by intros f x; rewrite iprod_lookup_op left_id.
- intros f Hf x. by apply: timeless.
+ - constructor=> x. apply persistent_core, _.
Qed.
Canonical Structure iprodUR :=
UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
@@ -147,7 +149,8 @@ Section iprod_cmra.
y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) →
iprod_insert x y1 g ~~>: Q.
Proof.
- intros Hy1 HP n gf Hg. destruct (Hy1 n (gf x)) as (y2&?&?).
+ intros Hy1 HP; apply cmra_total_updateP.
+ intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
{ move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. }
exists (iprod_insert x y2 g); split; [auto|].
intros x'; destruct (decide (x' = x)) as [->|];
@@ -205,12 +208,12 @@ Section iprod_singleton.
Proof.
move=>x'; destruct (decide (x = x')) as [->|];
by rewrite iprod_lookup_core ?iprod_lookup_singleton
- ?iprod_lookup_singleton_ne // (persistent ∅).
+ ?iprod_lookup_singleton_ne // (persistent_core ∅).
Qed.
Global Instance iprod_singleton_persistent x (y : B x) :
Persistent y → Persistent (iprod_singleton x y).
- Proof. intros. rewrite /Persistent iprod_core_singleton. by f_equiv. Qed.
+ Proof. by rewrite !persistent_total iprod_core_singleton=> ->. Qed.
Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2).
@@ -235,7 +238,8 @@ Section iprod_singleton.
Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :
∅ ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q.
Proof.
- intros Hx HQ n gf Hg. destruct (Hx n (gf x)) as (y2&?&?); first apply Hg.
+ intros Hx HQ; apply cmra_total_updateP.
+ intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
exists (iprod_singleton x y2); split; [by apply HQ|].
intros x'; destruct (decide (x' = x)) as [->|].
- by rewrite iprod_lookup_op iprod_lookup_singleton.
diff --git a/algebra/list.v b/algebra/list.v
index eafa5210e18f6fcf989adafd867888464eb421b8..17f9b32ff847c601cde5be2484cf6fa9468e26be 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -124,7 +124,7 @@ Section cmra.
| _, [] => l1
| x :: l1, y :: l2 => x â‹… y :: l1 â‹… l2
end.
- Instance list_core : Core (list A) := fmap core.
+ Instance list_pcore : PCore (list A) := λ l, Some (core <$> l).
Instance list_valid : Valid (list A) := Forall (λ x, ✓ x).
Instance list_validN : ValidN (list A) := λ n, Forall (λ x, ✓{n} x).
@@ -147,7 +147,10 @@ Section cmra.
by rewrite /= ?left_id_L ?right_id_L.
Qed.
Lemma list_lookup_core l i : core l !! i = core (l !! i).
- Proof. revert i; induction l; intros [|i]; simpl; auto. Qed.
+ Proof.
+ rewrite /core /= list_lookup_fmap.
+ destruct (l !! i); by rewrite /= ?Some_core.
+ Qed.
Lemma list_lookup_included l1 l2 : l1 ≼ l2 ↔ ∀ i, l1 !! i ≼ l2 !! i.
Proof.
@@ -165,10 +168,11 @@ Section cmra.
Definition list_cmra_mixin : CMRAMixin (list A).
Proof.
- split.
+ apply cmra_total_mixin.
+ - eauto.
- intros n l l1 l2; rewrite !list_dist_lookup=> Hl i.
by rewrite !list_lookup_op Hl.
- - apply _.
+ - intros n l1 l2 Hl; by rewrite /core /= Hl.
- intros n l1 l2; rewrite !list_dist_lookup !list_lookup_validN=> Hl ? i.
by rewrite -Hl.
- intros l. rewrite list_lookup_valid. setoid_rewrite list_lookup_validN.
@@ -196,8 +200,7 @@ Section cmra.
[inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
Qed.
- Canonical Structure listR :=
- CMRAT (list A) list_cofe_mixin list_cmra_mixin.
+ Canonical Structure listR := CMRAT (list A) list_cofe_mixin list_cmra_mixin.
Global Instance empty_list : Empty (list A) := [].
Definition list_ucmra_mixin : UCMRAMixin (list A).
@@ -206,6 +209,7 @@ Section cmra.
- constructor.
- by intros l.
- by inversion_clear 1.
+ - by constructor.
Qed.
Canonical Structure listUR :=
UCMRAT (list A) list_cofe_mixin list_cmra_mixin list_ucmra_mixin.
@@ -218,8 +222,8 @@ Section cmra.
Global Instance list_persistent l : (∀ x : A, Persistent x) → Persistent l.
Proof.
- intros ?; apply list_equiv_lookup=> i.
- by rewrite list_lookup_core (persistent (l !! i)).
+ intros ?; constructor; apply list_equiv_lookup=> i.
+ by rewrite list_lookup_core (persistent_core (l !! i)).
Qed.
(** Internalized properties *)
@@ -294,8 +298,8 @@ Section properties.
Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
Proof.
- rewrite /singletonM /list_singletonM /=.
- induction i; constructor; auto using ucmra_core_unit.
+ rewrite /singletonM /list_singletonM.
+ by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ∅).
Qed.
Lemma list_op_singletonM i (x y : A) :
{[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
@@ -305,19 +309,19 @@ Section properties.
Qed.
Lemma list_alter_singletonM f i x : alter f i {[i := x]} = {[i := f x]}.
Proof.
- rewrite /singletonM /list_singletonM /=.
- induction i; f_equal/=; auto.
+ rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
Qed.
Global Instance list_singleton_persistent i (x : A) :
Persistent x → Persistent {[ i := x ]}.
- Proof. intros. by rewrite /Persistent list_core_singletonM persistent. Qed.
+ Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed.
(* Update *)
Lemma list_update_updateP (P : A → Prop) (Q : list A → Prop) l1 x l2 :
x ~~>: P → (∀ y, P y → Q (l1 ++ y :: l2)) → l1 ++ x :: l2 ~~>: Q.
Proof.
- intros Hx%option_updateP' HP n mf; rewrite list_lookup_validN=> Hm.
- destruct (Hx n (mf !! length l1)) as ([y|]&H1&H2); simpl in *; try done.
+ intros Hx%option_updateP' HP.
+ apply cmra_total_updateP=> n mf; rewrite list_lookup_validN=> Hm.
+ destruct (Hx n (Some (mf !! length l1))) as ([y|]&H1&H2); simpl in *; try done.
{ move: (Hm (length l1)). by rewrite list_lookup_op list_lookup_middle. }
exists (l1 ++ y :: l2); split; auto.
apply list_lookup_validN=> i.
diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index b156f57e6deca9cf2e252fecf858f6d857de2828..5c3f6f6a0c510d7e25261f902a2d71eb9c849bb0 100644
--- a/algebra/one_shot.v
+++ b/algebra/one_shot.v
@@ -1,17 +1,21 @@
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
+Local Arguments pcore _ _ !_ /.
+Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments cmra_validN _ _ !_ /.
Local Arguments cmra_valid _ !_ /.
(* TODO: Really, we should have sums, and then this should be just "excl unit + A". *)
-Inductive one_shot {A : Type} :=
- | OneShotPending : one_shot
- | Shot : A → one_shot
- | OneShotUnit : one_shot
- | OneShotBot : one_shot.
-Arguments one_shot _ : clear implicits.
+Inductive one_shot (A : Type) :=
+ | OneShotPending : one_shot A
+ | Shot : A → one_shot A
+ | OneShotBot : one_shot A.
+Arguments OneShotPending {_}.
+Arguments Shot {_} _.
+Arguments OneShotBot {_}.
+
Instance maybe_Shot {A} : Maybe (@Shot A) := λ x,
match x with Shot a => Some a | _ => None end.
Instance: Params (@Shot) 1.
@@ -25,13 +29,11 @@ Implicit Types x y : one_shot A.
Inductive one_shot_equiv : Equiv (one_shot A) :=
| OneShotPending_equiv : OneShotPending ≡ OneShotPending
| OneShot_equiv a b : a ≡ b → Shot a ≡ Shot b
- | OneShotUnit_equiv : OneShotUnit ≡ OneShotUnit
| OneShotBot_equiv : OneShotBot ≡ OneShotBot.
Existing Instance one_shot_equiv.
Inductive one_shot_dist : Dist (one_shot A) :=
| OneShotPending_dist n : OneShotPending ≡{n}≡ OneShotPending
| OneShot_dist n a b : a ≡{n}≡ b → Shot a ≡{n}≡ Shot b
- | OneShotUnit_dist n : OneShotUnit ≡{n}≡ OneShotUnit
| OneShotBot_dist n : OneShotBot ≡{n}≡ OneShotBot.
Existing Instance one_shot_dist.
@@ -57,7 +59,7 @@ Proof.
+ intros Hxy; feed inversion (Hxy 0); subst; constructor; try done.
apply equiv_dist=> n; by feed inversion (Hxy n).
- intros n; split.
- + by intros [|a| |]; constructor.
+ + by intros [|a|]; constructor.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; done || apply dist_S.
@@ -73,8 +75,6 @@ Proof. by destruct 2; f_equal; done || apply leibniz_equiv. Qed.
Global Instance Shot_timeless (a : A) : Timeless a → Timeless (Shot a).
Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
-Global Instance OneShotUnit_timeless : Timeless (@OneShotUnit A).
-Proof. by inversion_clear 1; constructor. Qed.
End cofe.
Arguments one_shotC : clear implicits.
@@ -84,7 +84,6 @@ Definition one_shot_map {A B} (f : A → B) (x : one_shot A) : one_shot B :=
match x with
| OneShotPending => OneShotPending
| Shot a => Shot (f a)
- | OneShotUnit => OneShotUnit
| OneShotBot => OneShotBot
end.
Instance: Params (@one_shot_map) 2.
@@ -115,106 +114,91 @@ Instance one_shot_valid : Valid (one_shot A) := λ x,
match x with
| OneShotPending => True
| Shot a => ✓ a
- | OneShotUnit => True
| OneShotBot => False
end.
Instance one_shot_validN : ValidN (one_shot A) := λ n x,
match x with
| OneShotPending => True
| Shot a => ✓{n} a
- | OneShotUnit => True
| OneShotBot => False
end.
-Instance one_shot_core : Core (one_shot A) := λ x,
+Instance one_shot_pcore : PCore (one_shot A) := λ x,
match x with
- | Shot a => Shot (core a)
- | OneShotBot => OneShotBot
- | _ => OneShotUnit
+ | OneShotPending => None
+ | Shot a => Shot <$> pcore a
+ | OneShotBot => Some OneShotBot
end.
Instance one_shot_op : Op (one_shot A) := λ x y,
match x, y with
| Shot a, Shot b => Shot (a â‹… b)
- | Shot a, OneShotUnit | OneShotUnit, Shot a => Shot a
- | OneShotUnit, OneShotPending | OneShotPending, OneShotUnit => OneShotPending
- | OneShotUnit, OneShotUnit => OneShotUnit
| _, _ => OneShotBot
end.
Lemma Shot_op a b : Shot a â‹… Shot b = Shot (a â‹… b).
Proof. done. Qed.
-Lemma Shot_core a : core (Shot a) = Shot (core a).
-Proof. done. Qed.
-Lemma Shot_incl a b : Shot a ≼ Shot b ↔ a ≼ b.
+Lemma one_shot_included x y :
+ x ≼ y ↔ y = OneShotBot ∨ ∃ a b, x = Shot a ∧ y = Shot b ∧ a ≼ b.
Proof.
- split; intros [c H].
- - destruct c; inversion_clear H; first by eexists.
- by rewrite (_ : b ≡ a).
- - exists (Shot c). constructor. done.
-Qed.
+ split.
+ - intros [z Hy]; destruct x as [|a|], z as [|b|]; inversion_clear Hy; auto.
+ right; eexists _, _; split_and!; eauto.
+ setoid_subst; eauto using cmra_included_l.
+ - intros [->|(a&b&->&->&c&?)].
+ + destruct x; exists OneShotBot; constructor.
+ + exists (Shot c); by constructor.
+Qed.
Lemma one_shot_cmra_mixin : CMRAMixin (one_shot A).
Proof.
split.
- intros n []; destruct 1; constructor; by cofe_subst.
- - intros ? [|a| |] [|b| |] H; inversion_clear H; constructor; by f_equiv.
- - intros ? [|a| |] [|b| |] H; inversion_clear H; cofe_subst; done.
- - intros [|a| |]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
- - intros n [|a| |]; simpl; auto using cmra_validN_S.
- - intros [|a1| |] [|a2| |] [|a3| |]; constructor; by rewrite ?assoc.
- - intros [|a1| |] [|a2| |]; constructor; by rewrite 1?comm.
- - intros [|a| |]; constructor; []. exact: cmra_core_l.
- - intros [|a| |]; constructor; []. exact: cmra_core_idemp.
- - intros [|a1| |] [|a2| |]; simpl;
- try solve [ by exists OneShotUnit; constructor
- | by exists OneShotBot; constructor
- | by intros [[|a3| |] H]; inversion_clear H ].
- + intros H%Shot_incl. apply Shot_incl, cmra_core_preserving. done.
- + intros _. exists (Shot (core a2)). by constructor.
- - intros n [|a1| |] [|a2| |]; simpl; eauto using cmra_validN_op_l; done.
- - intros n [|a| |] y1 y2 Hx Hx'; last 2 first.
- + by exists (OneShotUnit, OneShotUnit); destruct y1, y2; inversion_clear Hx'.
+ - intros ???? [n|n a b Hab|n] [=]; subst; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
+ destruct (cmra_pcore_ne n a b ca) as (cb&->&?); auto.
+ exists (Shot cb); by repeat constructor.
+ - intros ? [|a|] [|b|] H; inversion_clear H; cofe_subst; done.
+ - intros [|a|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
+ - intros n [|a|]; simpl; auto using cmra_validN_S.
+ - intros [|a1|] [|a2|] [|a3|]; constructor; by rewrite ?assoc.
+ - intros [|a1|] [|a2|]; constructor; by rewrite 1?comm.
+ - intros [|a|] ? [=]; subst; auto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
+ constructor; eauto using cmra_pcore_l.
+ - intros [|a|] ? [=]; subst; auto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
+ feed inversion (cmra_pcore_idemp a ca); repeat constructor; auto.
+ - intros x y ? [->|(a&b&->&->&?)]%one_shot_included [=].
+ { exists OneShotBot. rewrite one_shot_included; eauto. }
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
+ destruct (cmra_pcore_preserving a b ca) as (cb&->&?); auto.
+ exists (Shot cb). rewrite one_shot_included; eauto 10.
+ - intros n [|a1|] [|a2|]; simpl; eauto using cmra_validN_op_l; done.
+ - intros n [|a|] y1 y2 Hx Hx'.
+ + destruct y1, y2; exfalso; by inversion_clear Hx'.
+ + destruct y1 as [|b1|], y2 as [|b2|]; try (exfalso; by inversion_clear Hx').
+ apply (inj Shot) in Hx'.
+ destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto.
+ exists (Shot z1, Shot z2). by repeat constructor.
+ by exists (OneShotBot, OneShotBot); destruct y1, y2; inversion_clear Hx'.
- + destruct y1, y2; try (exfalso; by inversion_clear Hx').
- * by exists (OneShotPending, OneShotUnit).
- * by exists (OneShotUnit, OneShotPending).
- + destruct y1 as [|b1 | |], y2 as [|b2| |]; try (exfalso; by inversion_clear Hx').
- * apply (inj Shot) in Hx'.
- destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto.
- exists (Shot z1, Shot z2). by repeat constructor.
- * exists (Shot a, OneShotUnit). inversion_clear Hx'. by repeat constructor.
- * exists (OneShotUnit, Shot a). inversion_clear Hx'. by repeat constructor.
Qed.
Canonical Structure one_shotR :=
CMRAT (one_shot A) one_shot_cofe_mixin one_shot_cmra_mixin.
+
Global Instance one_shot_cmra_discrete : CMRADiscrete A → CMRADiscrete one_shotR.
Proof.
split; first apply _.
- intros [|a| |]; simpl; auto using cmra_discrete_valid.
+ intros [|a|]; simpl; auto using cmra_discrete_valid.
Qed.
-Instance one_shot_empty : Empty (one_shot A) := OneShotUnit.
-Lemma one_shot_ucmra_mixin : UCMRAMixin (one_shot A).
-Proof. split. done. by intros []. apply _. Qed.
-Canonical Structure one_shotUR :=
- UCMRAT (one_shot A) one_shot_cofe_mixin one_shot_cmra_mixin one_shot_ucmra_mixin.
-
Global Instance Shot_persistent a : Persistent a → Persistent (Shot a).
-Proof. by constructor. Qed.
-
-Lemma one_shot_validN_inv_l n y : ✓{n} (OneShotPending ⋅ y) → y = ∅.
-Proof. by destruct y; inversion_clear 1. Qed.
-Lemma one_shot_valid_inv_l y : ✓ (OneShotPending ⋅ y) → y = ∅.
-Proof. intros. by apply one_shot_validN_inv_l with 0, cmra_valid_validN. Qed.
-Lemma one_shot_bot_largest y : y ≼ OneShotBot.
-Proof. destruct y; exists OneShotBot; constructor. Qed.
+Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
(** Internalized properties *)
Lemma one_shot_equivI {M} (x y : one_shot A) :
(x ≡ y) ⊣⊢ (match x, y with
| OneShotPending, OneShotPending => True
| Shot a, Shot b => a ≡ b
- | OneShotUnit, OneShotUnit => True
| OneShotBot, OneShotBot => True
| _, _ => False
end : uPred M).
@@ -232,45 +216,35 @@ Proof. uPred.unseal. by destruct x. Qed.
(** Updates *)
Lemma one_shot_update_shoot (a : A) : ✓ a → OneShotPending ~~> Shot a.
-Proof.
- move=> ? n y /one_shot_validN_inv_l ->. by apply cmra_valid_validN.
-Qed.
+Proof. move=> ? n [y|] //= ?. by apply cmra_valid_validN. Qed.
Lemma one_shot_update (a1 a2 : A) : a1 ~~> a2 → Shot a1 ~~> Shot a2.
Proof.
- intros Ha n [|b| |] ?; simpl; auto.
- apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r.
+ intros Ha n [[|b|]|] ?; simpl in *; auto.
+ - by apply (Ha n (Some b)).
+ - by apply (Ha n None).
Qed.
Lemma one_shot_updateP (P : A → Prop) (Q : one_shot A → Prop) a :
a ~~>: P → (∀ b, P b → Q (Shot b)) → Shot a ~~>: Q.
Proof.
- intros Hx HP n mf Hm. destruct mf as [|b| |]; try by destruct Hm.
- - destruct (Hx n b) as (c&?&?); try done.
- exists (Shot c). auto.
- - destruct (Hx n (core a)) as (c&?&?); try done.
- { by rewrite cmra_core_r. }
- exists (Shot c). split; simpl; eauto using cmra_validN_op_l.
+ intros Hx HP n mf Hm. destruct mf as [[|b|]|]; try by destruct Hm.
+ - destruct (Hx n (Some b)) as (c&?&?); naive_solver.
+ - destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l.
Qed.
Lemma one_shot_updateP' (P : A → Prop) a :
a ~~>: P → Shot a ~~>: λ m', ∃ b, m' = Shot b ∧ P b.
Proof. eauto using one_shot_updateP. Qed.
-
End cmra.
Arguments one_shotR : clear implicits.
-Arguments one_shotUR : clear implicits.
(* Functor *)
Instance one_shot_map_cmra_monotone {A B : cmraT} (f : A → B) :
CMRAMonotone f → CMRAMonotone (one_shot_map f).
Proof.
split; try apply _.
- - intros n [|a| |]; simpl; auto using validN_preserving.
- - intros [|a1| |] [|a2| |] [[|a3| |] Hx];
- inversion Hx; setoid_subst; try apply: ucmra_unit_least;
- try apply one_shot_bot_largest; auto; [].
- destruct (included_preserving f a1 (a1 â‹… a3)) as [b ?].
- { by apply cmra_included_l. }
- by exists (Shot b); constructor.
+ - intros n [|a|]; simpl; auto using validN_preserving.
+ - intros x y; rewrite !one_shot_included.
+ intros [->|(a&b&->&->&?)]; simpl; eauto 10 using included_preserving.
Qed.
Program Definition one_shotRF (F : rFunctor) : rFunctor := {|
@@ -294,25 +268,3 @@ Instance one_shotRF_contractive F :
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_contractive.
Qed.
-
-Program Definition one_shotURF (F : rFunctor) : urFunctor := {|
- urFunctor_car A B := one_shotUR (rFunctor_car F A B);
- urFunctor_map A1 A2 B1 B2 fg := one_shotC_map (rFunctor_map F fg)
-|}.
-Next Obligation.
- by intros F A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_ne.
-Qed.
-Next Obligation.
- intros F A B x. rewrite /= -{2}(one_shot_map_id x).
- apply one_shot_map_ext=>y; apply rFunctor_id.
-Qed.
-Next Obligation.
- intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -one_shot_map_compose.
- apply one_shot_map_ext=>y; apply rFunctor_compose.
-Qed.
-
-Instance one_shotURF_contractive F :
- rFunctorContractive F → urFunctorContractive (one_shotURF F).
-Proof.
- by intros ? A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_contractive.
-Qed.
diff --git a/algebra/upred.v b/algebra/upred.v
index 3a46637b316c00c6aa2bc3fddab074324206278c..0a72da7b07a5f0c63b8aebaa0117409a61a7bd42 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -215,8 +215,10 @@ Definition uPred_wand_eq :
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (core x) |}.
-Next Obligation. naive_solver eauto using uPred_mono, cmra_core_preservingN. Qed.
-Next Obligation. naive_solver eauto using uPred_closed, cmra_core_validN. Qed.
+Next Obligation.
+ intros M; naive_solver eauto using uPred_mono, @cmra_core_preservingN.
+Qed.
+Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
Definition uPred_always {M} := proj1_sig uPred_always_aux M.
Definition uPred_always_eq :
@@ -431,7 +433,7 @@ Global Instance later_proper :
Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
Proof.
intros P1 P2 HP.
- unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
+ unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
Qed.
Global Instance always_proper :
Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M) := ne_proper _.
@@ -856,11 +858,11 @@ Proof. by unseal. Qed.
Lemma always_elim P : □ P ⊢ P.
Proof.
unseal; split=> n x ? /=.
- eauto using uPred_mono, cmra_included_core, cmra_included_includedN.
+ eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
Qed.
Lemma always_intro' P Q : □ P ⊢ Q → □ P ⊢ □ Q.
Proof.
- unseal=> HPQ; split=> n x ??; apply HPQ; simpl; auto using cmra_core_validN.
+ unseal=> HPQ; split=> n x ??; apply HPQ; simpl; auto using @cmra_core_validN.
by rewrite cmra_core_idemp.
Qed.
Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ (□ P ∧ □ Q).
@@ -1023,7 +1025,7 @@ Qed.
Lemma always_ownM (a : M) : Persistent a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl.
- rewrite -(persistent a). by apply cmra_core_preservingN.
+ rewrite -(persistent_core a). by apply cmra_core_preservingN.
Qed.
Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a.
Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 9a2cac7a9ea7ecdb26123b249dddfdaa4009c05c..c1e2c2a7afa9486704806c12aecbf3079a6c7a60 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -19,8 +19,7 @@ Class heapG Σ := HeapG {
Definition heapGF : gFunctor := authGF heapUR.
Definition to_heap : state → heapUR := fmap (λ v, Frac 1 (DecAgree v)).
-Definition of_heap : heapUR → state :=
- omap (mbind (maybe DecAgree ∘ snd) ∘ maybe2 Frac).
+Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ frac_car).
Section definitions.
Context `{i : heapG Σ}.
@@ -70,7 +69,7 @@ Section heap.
intros Hv. apply map_eq=> l'; destruct (decide (l' = l)) as [->|].
- move: (Hv l). rewrite /of_heap lookup_insert
lookup_omap (lookup_op _ h) lookup_singleton.
- case _:(h !! l)=>[[q' [v'|]|]|] //=; last by move=> [??].
+ case _:(h !! l)=>[[q' [v'|]]|] //=; last by move=> [??].
move=> [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp.
- rewrite /of_heap lookup_insert_ne // !lookup_omap.
by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
@@ -79,10 +78,10 @@ Section heap.
to_heap (<[l:=v]> σ) = <[l:=Frac 1 (DecAgree v)]> (to_heap σ).
Proof. by rewrite /to_heap -fmap_insert. Qed.
Lemma of_heap_None h l :
- ✓ h → of_heap h !! l = None → h !! l = None ∨ h !! l ≡ Some FracUnit.
+ ✓ h → of_heap h !! l = None → h !! l = None.
Proof.
move=> /(_ l). rewrite /of_heap lookup_omap.
- by case: (h !! l)=> [[q [v|]|]|] //=; destruct 1; auto.
+ by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto.
Qed.
Lemma heap_store_valid l h v1 v2 :
✓ ({[l := Frac 1 (DecAgree v1)]} ⋅ h) →
@@ -90,7 +89,7 @@ Section heap.
Proof.
intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
- rewrite !lookup_op !lookup_singleton.
- case: (h !! l)=>[x|]; [|done]=> /frac_valid_inv_l=>-> //.
+ by case: (h !! l)=> [x|] // /frac_valid_inv_l.
- by rewrite !lookup_op !lookup_singleton_ne.
Qed.
Hint Resolve heap_store_valid.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index dbc1f76f3795904f1b8420844ccf14a8ef0de06c..f5eab2f097c041d58c0345a7bc959454b6b7cfbc 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -75,9 +75,9 @@ Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
Proof.
intros Hv ? [k ?]%rtc_nsteps.
- eapply wp_adequacy_steps with (r1 := (Res ∅ (Excl σ1) m)); eauto; [|].
+ eapply wp_adequacy_steps with (r1 := (Res ∅ (Excl' σ1) m)); eauto; [|].
{ by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
- uPred.unseal; exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ m); split_and?.
+ uPred.unseal; exists (Res ∅ (Excl' σ1) ∅), (Res ∅ ∅ m); split_and?.
- by rewrite Res_op ?left_id ?right_id.
- rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
- by apply ownG_spec.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index e1c79a43679613ac3b26b54219c7ed11ce3821c9..0cdf20cab6db26f3bf9ea7a760672773ad34ee5b 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -58,7 +58,7 @@ Section auth.
▷ φ a ⊢ (|={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
Proof.
iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
- iPvs (own_alloc (Auth (Excl a) a)) as {γ} "Hγ"; first done.
+ iPvs (own_alloc (Auth (Excl' a) a)) as {γ} "Hγ"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
{ iNext. iExists a. by iFrame "Hφ". }
diff --git a/program_logic/model.v b/program_logic/model.v
index 5daecb065756b8523bebc17246e0b9507ea485a1..55cdb0ac6f870c12c7e3614ab91ac8afc1e19c41 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -19,7 +19,7 @@ Definition iGst (Λ : language) (Σ : iFunctor) : ucmraT := Σ (iPreProp Λ Σ).
Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iResUR Λ Σ := resUR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
-Definition iPst Λ := excl (state Λ).
+Definition iPst Λ := option (excl (state Λ)).
Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResUR Λ Σ).
Parameter iProp_unfold: ∀ {Λ Σ}, iProp Λ Σ -n> iPreProp Λ Σ.
@@ -40,7 +40,7 @@ Definition iGst (Λ : language) (Σ : iFunctor) : ucmraT := Σ (iPreProp Λ Σ).
Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iResUR Λ Σ := resUR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
-Definition iPst Λ := excl (state Λ).
+Definition iPst Λ := option (excl (state Λ)).
Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResUR Λ Σ).
Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ :=
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 3127a5b2b15e97817a9e67d012237d774db758fd..88368a6cf5ec4529a8225f835008e65fa469271d 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export model.
Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
uPred_ownM (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
Arguments ownI {_ _} _ _%I.
-Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_ownM (Res ∅ (Excl σ) ∅).
+Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_ownM (Res ∅ (Excl' σ) ∅).
Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownM (Res ∅ ∅ m).
Instance: Params (@ownI) 3.
Instance: Params (@ownP) 2.
@@ -64,11 +64,12 @@ Proof.
intros (?&?&?). rewrite /ownI; uPred.unseal.
rewrite /uPred_holds/=res_includedN/= singleton_includedN; split.
- intros [(P'&Hi&HP) _]; rewrite Hi.
- constructor; symmetry; apply agree_valid_includedN; last done.
- by apply lookup_validN_Some with (wld r) i.
+ constructor; symmetry; apply agree_valid_includedN.
+ + by apply lookup_validN_Some with (wld r) i.
+ + by destruct HP as [?| ->].
- intros ?; split_and?; try apply ucmra_unit_leastN; eauto.
Qed.
-Lemma ownP_spec n r σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡ Excl σ.
+Lemma ownP_spec n r σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡ Excl' σ.
Proof.
intros (?&?&?). rewrite /ownP; uPred.unseal.
rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index d03e671f5510b225c37c6355c56f4b0f5ec9b1a5..0304c1bc0c554953fbe4e84d533a52b5a3cf416b 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export language.
Record res (Λ : language) (A : cofeT) (M : cmraT) := Res {
wld : gmapR positive (agreeR A);
- pst : exclR (stateC Λ);
+ pst : optionR (exclR (stateC Λ));
gst : M;
}.
Add Printing Constructor res.
@@ -73,8 +73,8 @@ Proof. destruct 3; constructor; by apply (timeless _). Qed.
Instance res_op : Op (res Λ A M) := λ r1 r2,
Res (wld r1 â‹… wld r2) (pst r1 â‹… pst r2) (gst r1 â‹… gst r2).
-Instance res_core : Core (res Λ A M) := λ r,
- Res (core (wld r)) (core (pst r)) (core (gst r)).
+Instance res_pcore : PCore (res Λ A M) := λ r,
+ Some $ Res (core (wld r)) (core (pst r)) (core (gst r)).
Instance res_valid : Valid (res Λ A M) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
Instance res_validN : ValidN (res Λ A M) := λ n r,
✓{n} wld r ∧ ✓{n} pst r ∧ ✓{n} gst r.
@@ -95,7 +95,8 @@ Proof.
Qed.
Definition res_cmra_mixin : CMRAMixin (res Λ A M).
Proof.
- split.
+ apply cmra_total_mixin.
+ - eauto.
- by intros n x [???] ? [???]; constructor; cofe_subst.
- by intros n [???] ? [???]; constructor; cofe_subst.
- by intros n [???] ? [???] (?&?&?); split_and!; cofe_subst.
@@ -117,8 +118,7 @@ Proof.
(cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
by exists (Res w σ m, Res w' σ' m').
Qed.
-Canonical Structure resR :=
- CMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin.
+Canonical Structure resR := CMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin.
Instance res_empty : Empty (res Λ A M) := Res ∅ ∅ ∅.
Definition res_ucmra_mixin : UCMRAMixin (res Λ A M).
@@ -127,12 +127,13 @@ Proof.
- split_and!; apply ucmra_unit_valid.
- by split; rewrite /= left_id.
- apply _.
+ - do 2 constructor; simpl; apply (persistent_core _).
Qed.
Canonical Structure resUR :=
UCMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin res_ucmra_mixin.
Definition update_pst (σ : state Λ) (r : res Λ A M) : res Λ A M :=
- Res (wld r) (Excl σ) (gst r).
+ Res (wld r) (Excl' σ) (gst r).
Definition update_gst (m : M) (r : res Λ A M) : res Λ A M :=
Res (wld r) (pst r) m.
@@ -158,7 +159,7 @@ Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
Global Instance Res_timeless eσ m : Timeless m → Timeless (@Res Λ A M ∅ eσ m).
Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
Global Instance Res_persistent w m: Persistent m → Persistent (@Res Λ A M w ∅ m).
-Proof. constructor; apply (persistent _). Qed.
+Proof. do 2 constructor; apply (persistent_core _). Qed.
(** Internalized properties *)
Lemma res_equivI {M'} r1 r2 :
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 84fb2cde34707659ad42dc27af629784e12090b3..650238ddd5f910f70db52d1ad6c6e925b097d6a4 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -9,7 +9,7 @@ Local Hint Extern 1 (✓{_} wld _) => apply wld_validN.
Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
(σ : state Λ) (rs : gmap positive (iRes Λ Σ)) (r : iRes Λ Σ) := {
wsat_pre_valid : ✓{S n} r;
- wsat_pre_state : pst r ≡ Excl σ;
+ wsat_pre_state : pst r ≡ Excl' σ;
wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
wsat_pre_wld i P :
i ∈ E →
@@ -70,7 +70,7 @@ Proof.
destruct n; first done.
intros _ [rs ?]; eapply cmra_validN_op_l, wsat_pre_valid; eauto.
Qed.
-Lemma wsat_init k E σ m : ✓{S k} m → wsat (S k) E σ (Res ∅ (Excl σ) m).
+Lemma wsat_init k E σ m : ✓{S k} m → wsat (S k) E σ (Res ∅ (Excl' σ) m).
Proof.
intros Hv. exists ∅; constructor; auto.
- rewrite big_opM_empty right_id.
@@ -114,7 +114,7 @@ Proof.
exists r'; rewrite lookup_insert_ne; naive_solver.
Qed.
Lemma wsat_update_pst n E σ1 σ1' r rf :
- pst r ≡{S n}≡ Excl σ1 → wsat (S n) E σ1' (r ⋅ rf) →
+ pst r ≡{S n}≡ Excl' σ1 → wsat (S n) E σ1' (r ⋅ rf) →
σ1' = σ1 ∧ ∀ σ2, wsat (S n) E σ2 (update_pst σ2 r ⋅ rf).
Proof.
intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *.
@@ -122,7 +122,7 @@ Proof.
{ by apply: (excl_validN_inv_l (S n) _ σ1); rewrite -Hpst_r assoc. }
assert (σ1' = σ1) as ->.
{ apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
- apply (inj Excl).
+ apply (inj Excl), (inj Some).
by rewrite -Hpst_r -Hpst -assoc Hpst' right_id. }
split; [done|exists rs].
by constructor; first split_and!; try rewrite /= -assoc Hpst'.
@@ -132,7 +132,7 @@ Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
Proof.
intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
- destruct (Hup (S n) (mf â‹… gst (rf â‹… big_opM rs))) as (m2&?&Hval'); try done.
+ destruct (Hup (S n) (Some (mf â‹… gst (rf â‹… big_opM rs)))) as (m2&?&Hval'); try done.
{ by rewrite /= (assoc _ m1) -Hr assoc. }
exists m2; split; [exists rs|done].
by constructor; first split_and!; auto.