diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 40eae66f244cdca473a3bb9c5d903732a2d2eab0..3f826b1b2f781c9cbaf07c227ec420e7aaf2bd94 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -4,7 +4,6 @@ From iris.prelude Require Import options.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
-Local Arguments pcore _ _ !_ /.
(** Define an agreement construction such that Agree A is discrete when A is discrete.
Notice that this construction is NOT complete. The following is due to Aleš:
@@ -89,7 +88,6 @@ Local Instance agree_valid_instance : Valid (agree A) := λ x, ∀ n, ✓{n} x.
Local Program Instance agree_op_instance : Op (agree A) := λ x y,
{| agree_car := agree_car x ++ agree_car y |}.
Next Obligation. by intros [[|??]] y. Qed.
-Local Instance agree_pcore_instance : PCore (agree A) := Some.
Lemma agree_validN_def n x :
✓{n} x ↔ ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b.
@@ -140,7 +138,6 @@ Definition agree_cmra_mixin : CmraMixin (agree A).
Proof.
apply cmra_total_mixin; try apply _ || by eauto.
- intros n x; rewrite !agree_validN_def; eauto using dist_le.
- - intros x. apply agree_idemp.
- intros n x y; rewrite !agree_validN_def /=.
setoid_rewrite elem_of_app; naive_solver.
- intros n x y1 y2 Hval Hx; exists x, x; simpl; split.
@@ -154,9 +151,9 @@ Qed.
Canonical Structure agreeR : cmra := Cmra (agree A) agree_cmra_mixin.
Global Instance agree_cmra_total : CmraTotal agreeR.
-Proof. rewrite /CmraTotal; eauto. Qed.
+Proof. intros x. exists x. by split; [exists x|]; rewrite agree_idemp. Qed.
Global Instance agree_core_id x : CoreId x.
-Proof. by constructor. Qed.
+Proof. by rewrite /CoreId agree_idemp. Qed.
Global Instance agree_cmra_discrete : OfeDiscrete A → CmraDiscrete agreeR.
Proof.
@@ -308,7 +305,6 @@ Section agree_map.
- intros n x. rewrite !agree_validN_def=> Hv b b' /=.
intros (a&->&?)%elem_of_list_fmap (a'&->&?)%elem_of_list_fmap.
apply Hf; eauto.
- - done.
- intros x y n; split=> b /=;
rewrite !fmap_app; setoid_rewrite elem_of_app; eauto.
Qed.
diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 6725b52f04137b9b17a6ea62a2cfba735d7d7375..021b4fda6250633bd5b24bd18e926e8c6a210cc7 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -124,21 +124,11 @@ Section auth.
Proof. apply view_frag_op. Qed.
Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
Proof. apply view_frag_mono. Qed.
- Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
- Proof. apply view_frag_core. Qed.
- Lemma auth_both_core_discarded a b :
- core (â—â–¡ a â‹… â—¯ b) ≡ â—â–¡ a â‹… â—¯ (core b).
- Proof. apply view_both_core_discarded. Qed.
- Lemma auth_both_core_frac q a b :
- core (â—{#q} a â‹… â—¯ b) ≡ â—¯ (core b).
- Proof. apply view_both_core_frac. Qed.
Global Instance auth_auth_core_id a : CoreId (â—â–¡ a).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
Proof. rewrite /auth_frag. apply _. Qed.
- Global Instance auth_both_core_id a1 a2 : CoreId a2 → CoreId (â—â–¡ a1 â‹… â—¯ a2).
- Proof. rewrite /auth_auth /auth_frag. apply _. Qed.
Global Instance auth_frag_is_op a b1 b2 :
IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
Proof. rewrite /auth_frag. apply _. Qed.
diff --git a/iris/algebra/category/morphism.v b/iris/algebra/category/morphism.v
index 9b19b75d20c444cb4aeda25cdee41eea97ba8a3d..f197eeb0f27c1e4a8ef6fe8c9b69163c71f38c57 100644
--- a/iris/algebra/category/morphism.v
+++ b/iris/algebra/category/morphism.v
@@ -14,35 +14,13 @@ Proof.
naive_solver.
Qed.
-Class Morphism {A B : cmra} (f : A → B) := {
- #[global] morph_ne :: NonExpansive f;
- morph_validN n (x : A) : ✓{n} x → ✓{n} (f x);
- morph_op (x y : A) : f (x ⋅ y) ≡ f x ⋅ f y;
-}.
-Global Hint Mode Morphism - - ! : typeclass_instances.
-Global Arguments morph_validN {_ _} _ {_} _ _ _.
-Global Arguments morph_op {_ _} _ {_} _ _.
-
Class PerservesUnit {A B : ucmra} (f : A → B) :=
morph_unit : f ε ≡ ε.
Global Hint Mode PerservesUnit - - ! : typeclass_instances.
-Global Arguments morph_op {_ _} _ {_}.
-
-Section morph.
-Context {A B : cmra} (f : A → B) `{!Morphism f}.
-
-Global Instance morph_proper : Proper ((≡) ==> (≡)) f.
-Proof using Type*. apply ne_proper, _. Qed.
-
-Lemma morph_valid (x : A) : ✓ x → ✓ (f x).
-Proof using Type*.
- rewrite !cmra_valid_validN. eauto using morph_validN.
-Qed.
-End morph.
Record morph (A B : cmra) := Morph {
morph_car :> A → B;
- #[global] morph_morphism :: Morphism morph_car;
+ #[global] morph_morphism :: CmraMorphism morph_car;
}.
Global Arguments Morph {_ _} _ {_}.
Global Arguments morph_car {_ _} _ _.
@@ -80,7 +58,7 @@ Notation "A -r> B" := (morphO A B) (at level 99, B at level 200, right associati
Record umorph (A B : ucmra) := UMorph {
umorph_car :> A → B;
- #[global] umorph_morphism :: Morphism umorph_car;
+ #[global] umorph_morphism :: CmraMorphism umorph_car;
#[global] umorph_unit :: PerservesUnit umorph_car;
}.
Global Arguments UMorph {_ _} _ {_ _}.
@@ -125,20 +103,9 @@ Global Arguments umorphO : clear implicits.
Notation "A -ur> B" := (umorphO A B) (at level 99, B at level 200, right associativity).
(** Category *)
-Global Instance id_morph {A : cmra} : Morphism (@id A).
-Proof. split=>//. apply _. Qed.
Global Instance id_umorph {A : ucmra} : PerservesUnit (@id A).
Proof. by red. Qed.
-Global Instance comp_morph {A B C : cmra} (f : B → C) (g : A → B) : Morphism f → Morphism g → Morphism (f ∘ g).
-Proof.
- split=>/=.
- - apply _.
- - intros n x Hx.
- by do 2 apply (morph_validN _).
- - intros x y.
- by rewrite !morph_op.
-Qed.
-Global Instance ucomp_morph {A B C : ucmra} (f : B → C) (g : A → B) : Morphism f → PerservesUnit f → PerservesUnit g → PerservesUnit (f ∘ g).
+Global Instance ucomp_morph {A B C : ucmra} (f : B → C) (g : A → B) : CmraMorphism f → PerservesUnit f → PerservesUnit g → PerservesUnit (f ∘ g).
Proof.
intros ???; red=>/=.
by rewrite !morph_unit.
@@ -155,7 +122,7 @@ Global Instance compM_ne {A B C} : NonExpansive2 (@compM A B C).
Proof.
intros n f1 f2 Hf g1 g2 Hg m x Hm Hx=>/=.
trans (f2 (g1 x)).
- - by apply Hf, (morph_validN g1).
+ - by apply Hf, (cmra_morphism_validN g1).
- f_equiv. by apply Hg.
Qed.
Global Instance compM_proper {A B C} : Proper ((≡) ==> (≡) ==> (≡)) (@compM A B C).
@@ -191,7 +158,7 @@ Proof. done. Qed.
(** Terminal *)
Definition to_unit {A} (_ : A) : () := ().
-Global Instance to_unit_morph {A : cmra} : Morphism (@to_unit A).
+Global Instance to_unit_morph {A : cmra} : CmraMorphism (@to_unit A).
Proof. by split. Qed.
Global Instance to_unit_umorph {A : ucmra} : PerservesUnit (@to_unit A).
Proof. done. Qed.
@@ -205,12 +172,12 @@ Proof. apply to_unit_unique. Qed.
(** Product *)
Definition fpair {A B C} (f : A → B) (g : A → C) (x : A) := (f x, g x).
-Global Instance fpair_morph {A B C : cmra} (f : A → B) (g : A → C) : Morphism f → Morphism g → Morphism (fpair f g).
+Global Instance fpair_morph {A B C : cmra} (f : A → B) (g : A → C) : CmraMorphism f → CmraMorphism g → CmraMorphism (fpair f g).
Proof.
intros ??. split.
- solve_proper.
- - intros n x ?; split=>/=; by apply morph_validN.
- - intros x y; split=>/=; by apply morph_op.
+ - intros n x ?; split=>/=; by apply cmra_morphism_validN.
+ - intros x y; split=>/=; by apply cmra_morphism_op.
Qed.
Global Instance fpair_umorph {A B C : ucmra} (f : A → B) (g : A → C) : PerservesUnit f → PerservesUnit g → PerservesUnit (fpair f g).
Proof. intros ??. by split. Qed.
@@ -229,7 +196,7 @@ Proof. exact fpairM_ne. Qed.
Global Instance fpairUM_proper {A B C} : Proper ((≡) ==> (≡) ==> (≡)) (@fpairUM A B C).
Proof. apply ne_proper_2, _. Qed.
-Global Instance fst_morph {A B : cmra} : Morphism (@fst A B).
+Global Instance fst_morph {A B : cmra} : CmraMorphism (@fst A B).
Proof.
split.
- apply _.
@@ -241,7 +208,7 @@ Proof. by red. Qed.
Canonical fstM {A B : cmra} := Morph (@fst A B).
Canonical fstUM {A B : ucmra} := UMorph (@fst A B).
-Global Instance snd_morph {A B : cmra} : Morphism (@snd A B).
+Global Instance snd_morph {A B : cmra} : CmraMorphism (@snd A B).
Proof.
split.
- apply _.
@@ -294,14 +261,14 @@ Proof. apply fpairM_ump. Qed.
(*Infinite Product*)
Definition flam {I} {A} {B : I → ucmra} (f : ∀ i, A → B i) (a : A) : discrete_funUR B :=
λ i, f i a.
-Global Instance flam_morph {I} {A : cmra} {B : I → ucmra} (f : ∀ i, A → B i) : (∀ i, Morphism (f i)) → Morphism (flam f).
+Global Instance flam_morph {I} {A : cmra} {B : I → ucmra} (f : ∀ i, A → B i) : (∀ i, CmraMorphism (f i)) → CmraMorphism (flam f).
Proof.
split.
- solve_proper.
- intros n a ? i.
- by apply (morph_validN (f i)).
+ by apply (cmra_morphism_validN (f i)).
- intros a1 a2 i.
- apply (morph_op (f i)).
+ apply (cmra_morphism_op (f i)).
Qed.
Global Instance flam_umorph {I} {A : ucmra} {B : I → ucmra} (f : ∀ i, A → B i) : (∀ i, PerservesUnit (f i)) → PerservesUnit (flam f).
Proof. intros ? i. apply morph_unit. Qed.
@@ -326,7 +293,7 @@ Proof. exact flamM_proper. Qed.
Definition fproj {I} {B : I → ucmra} (i : I) (f : discrete_funUR B) : B i :=
f i.
-Global Instance fproj_morph {I} {B : I → ucmra} (i : I) : Morphism (@fproj I B i).
+Global Instance fproj_morph {I} {B : I → ucmra} (i : I) : CmraMorphism (@fproj I B i).
Proof.
split.
- intros n f g Hfg.
@@ -376,19 +343,19 @@ Lemma flamUM_ump {I A} {B : I → ucmra} (f : A -ur> discrete_funUR B) (g : ∀
Proof. exact: flamM_ump. Qed.
(** option *)
-Global Instance Some_morph {A : cmra} : Morphism (@Some A).
+Global Instance Some_morph {A : cmra} : CmraMorphism (@Some A).
Proof. split=>//. apply _. Qed.
Canonical SomeM {A : cmra} := Morph (@Some A).
-Global Instance option_fmap_morph {A B : cmra} (f : A → B) : Morphism f → Morphism (fmap (M:=option) f).
+Global Instance option_fmap_morph {A B : cmra} (f : A → B) : CmraMorphism f → CmraMorphism (fmap (M:=option) f).
Proof.
intros ?; split.
- apply _.
- intros n [x|]=>//.
- apply (morph_validN f).
+ apply (cmra_morphism_validN f).
- intros [x|] [y|]=>//=.
constructor.
- apply (morph_op f).
+ apply (cmra_morphism_op f).
Qed.
Global Instance option_fmap_umorph {A B : cmra} (f : A → B) : PerservesUnit (fmap (M:=option) f).
Proof. by red. Qed.
@@ -404,7 +371,7 @@ Lemma option_fmapM_SomeM {A B} (f : A -r> B) : umorph_morph (option_fmapUM f) ®
Proof. by intros n x. Qed.
Definition option_elim {A : ucmra} : option A → A := default ε.
-Global Instance option_elim_morph {A} : Morphism (@option_elim A).
+Global Instance option_elim_morph {A} : CmraMorphism (@option_elim A).
Proof.
split.
- solve_proper.
@@ -548,63 +515,6 @@ Next Obligation.
intros f g. apply NoDup_list_union; apply dsum_support_no_dup.
Qed.
-Definition dsum_core_cond (f : dsum B) : Prop :=
- is_Some (head (filter (λ a, is_Some (core (f a))) (dsum_support f))).
-Global Instance dsum_core_cond_decide (f : dsum B) : Decision (dsum_core_cond f) := _.
-Global Instance dsum_core_cond_proof_irrel (f : dsum B) : ProofIrrel (dsum_core_cond f) := _.
-
-Lemma dsum_core_cond_alt (f : dsum B) : dsum_core_cond f ↔ ∃ a, is_Some (core (f a)).
-Proof.
- rewrite /dsum_core_cond head_is_Some.
- trans (∃ a, a ∈ filter (λ a : A, is_Some (core (f a))) (dsum_support f)).
- {
- destruct filter; split=>//.
- - intros [? []%elem_of_nil].
- - intros _. exists a. by left.
- }
- f_equiv=> a.
- rewrite elem_of_list_filter dsum_support_strict.
- destruct (f a); naive_solver.
-Qed.
-
-Program Definition dsum_core (f : dsum B) (Hf : dsum_core_cond f) : dsum B := {|
- dsum_car a := core (f a);
- dsum_support := filter (λ a, is_Some (core (f a))) (dsum_support f);
-|}.
-Next Obligation.
- intros f Hf a.
- rewrite elem_of_list_filter dsum_support_strict.
- destruct (f a); naive_solver.
-Qed.
-Next Obligation.
- intros f (a & ? & ?)%dsum_core_cond_alt.
- exists a.
- rewrite elem_of_list_filter dsum_support_strict.
- destruct (f a); naive_solver.
-Qed.
-Next Obligation.
- intros f _. apply NoDup_filter, dsum_support_no_dup.
-Qed.
-
-Local Instance dsum_pcore_instance : PCore (dsum B) := λ f,
- match (decide (dsum_core_cond f)) with
- | left Hf => Some $ dsum_core f Hf
- | right _ => None
- end.
-
-Lemma dsum_pcore_Some (f cf : dsum B) : pcore f = Some cf ↔ ∃ Hf, dsum_core f Hf = cf.
-Proof.
- rewrite /pcore /dsum_pcore_instance.
- destruct decide as [Hf|Hf]; split.
- - intros [= <-].
- by exists Hf.
- - intros [Hf' <-].
- do 2 f_equal.
- apply proof_irrel.
- - done.
- - by intros [? _].
-Qed.
-
Lemma dsum_includedN_1 n (f g : dsum B) a : f ≼{n} g → f a ≼{n} g a.
Proof.
intros [h H].
@@ -616,19 +526,6 @@ Proof.
split.
- intros f n g1 g2 Hg a=>/=.
f_equiv. apply Hg.
- - intros n f g _ H [Hf <-]%dsum_pcore_Some.
- assert (dsum_core_cond g) as Hg.
- {
- rewrite !dsum_core_cond_alt in Hf |- *.
- destruct Hf as [a Hf].
- exists a.
- by rewrite -(H a).
- }
- exists (dsum_core g Hg); split.
- { apply dsum_pcore_Some. by exists Hg. }
- intros a=>/=.
- f_equiv.
- apply H.
- intros n f g H Hf a.
by rewrite -(H a).
- intros f; split.
@@ -643,38 +540,6 @@ Proof.
apply assoc, _.
- intros f g a=>/=.
apply comm, _.
- - intros f _ [Hf <-]%dsum_pcore_Some a=>/=.
- apply cmra_core_l.
- - intros f _ [Hf <-]%dsum_pcore_Some.
- assert (dsum_core_cond (dsum_core f Hf)) as Hcf.
- {
- rewrite /dsum_core_cond list_filter_filter_r //=.
- intros x ?.
- by rewrite cmra_core_idemp.
- }
- rewrite /pcore /dsum_pcore_instance.
- rewrite decide_True_pi.
- constructor=> a /=.
- apply cmra_core_idemp.
- - intros f g _ [h H] [Hf <-]%dsum_pcore_Some.
- assert (dsum_core_cond g) as Hg.
- {
- rewrite !dsum_core_cond_alt in Hf |- *.
- destruct Hf as (a & cx & Hf).
- exists a.
- rewrite (H a) /=.
- destruct (f a) as [x|] eqn:Hx=>//.
- rewrite /core /= in Hf.
- destruct (h a) as [y|]=>//.
- rewrite /core /=.
- by destruct (cmra_pcore_mono x (x â‹… y) cx) as (? & -> & _).
- }
- exists (dsum_core g Hg); split.
- { apply dsum_pcore_Some. by exists Hg. }
- exists (dsum_core g Hg)=> a /=.
- destruct (cmra_core_mono (f a) (g a)) as [y Hc].
- { exists (h a). apply H. }
- by rewrite Hc assoc -cmra_core_dup.
- intros n f g H a.
eapply cmra_validN_op_l, H.
- intros n f g1 g2 Hf H.
@@ -748,7 +613,7 @@ Proof.
{ by apply dsum_includedN_1. }
by rewrite assoc -{1}(Hh a).
+ right.
- intros m h ? Hhf Hh.
+ intros h Hhf Hh.
contradict Ha.
apply Exists_exists.
destruct (dsum_support_inhab h) as [a [x Ha]%dsum_support_strict].
@@ -757,9 +622,9 @@ Proof.
destruct Hhf as [i Hi].
rewrite (Hi a) /= Ha.
by destruct (i a).
- * assert (h a ≼{m} g a) as [Ha'|(_ & y & _ & ? & _)]%option_includedN=>//.
+ * assert (h a ≼{0} g a) as [Ha'|(_ & y & _ & ? & _)]%option_includedN=>//.
{
- apply H=>//.
+ apply H, Hh; first lia.
by apply dsum_includedN_1.
}
by rewrite Ha in Ha'.
@@ -769,7 +634,7 @@ Canonical dsumR := Cmra (dsum B) dsum_cmra_mixin.
Lemma elem_of_dsum_op a (f g : dsum B) : a ∈ f ⋅ g ↔ a ∈ f ∨ a ∈ g.
Proof. apply elem_of_list_union. Qed.
-Global Instance DSum_morph a : Morphism (DSum a).
+Global Instance DSum_morph a : CmraMorphism (DSum a).
Proof.
split.
- solve_proper.
@@ -822,7 +687,7 @@ Proof.
Qed.
Lemma dsum_fold_op {C : cmra} (f : ∀ a, B a → C) (g1 g2 : dsum B) :
- (∀ a, Morphism (f a)) →
+ (∀ a, CmraMorphism (f a)) →
dsum_fold f (g1 ⋅ g2) ≡ dsum_fold f g1 ⋅ dsum_fold f g2.
Proof.
intros Hf.
@@ -837,7 +702,7 @@ Proof.
f_equiv=> _ a /=.
destruct (g1 a) as [x|], (g2 a) as [y|]=>//=.
constructor.
- apply morph_op, _.
+ apply cmra_morphism_op, _.
}
f_equiv.
- rewrite /= list_union_comm; [|apply dsum_support_no_dup..].
@@ -935,15 +800,9 @@ Local Instance coProd_valid_instance : Valid (coProd B) := λ f,
Local Program Instance coProd_op_instance : Op (coProd B) := λ f g,
CoProd' (coProd_car f â‹… coProd_car g).
-Local Instance coProd_pcore_instance : PCore (coProd B) := λ f,
- CoProd' <$> pcore (coProd_car f).
-
Lemma coProd_cmra_mixin : CmraMixin (coProd B).
Proof.
apply (iso_cmra_mixin_restrict_validity CoProd' coProd_car)=>//.
- - intros f.
- rewrite {2}/pcore /coProd_pcore_instance.
- by destruct pcore.
- by intros n f [_ ?].
- intros n f g H [Hf1 Hf].
split.
@@ -964,17 +823,17 @@ Proof.
Qed.
Canonical coProdR := Cmra (coProd B) coProd_cmra_mixin.
-Global Instance CoProd_morph a : Morphism (CoProd a).
+Global Instance CoProd_morph a : CmraMorphism (CoProd a).
Proof.
split.
- solve_proper.
- intros n b Hb.
split=>/=.
+ by intros a1 a2 ->%elem_of_DSum ->%elem_of_DSum.
- + by apply (morph_validN _).
+ + by apply (cmra_morphism_validN _).
- intros b1 b2.
do 5 red. simpl.
- apply morph_op, _.
+ apply cmra_morphism_op, _.
Qed.
Canonical Structure CoProdM a := Morph (CoProd a).
@@ -1001,7 +860,7 @@ Proof.
+ specialize (Hf a).
by rewrite Hb in Hf.
- intros (a & b & -> & Hb).
- by apply (morph_validN _).
+ by apply (cmra_morphism_validN _).
Qed.
Lemma coProd_valid (f : coProd B) : ✓ f ↔ ∃ a b, f ≡ CoProd a b ∧ ✓ b.
Proof.
@@ -1025,7 +884,7 @@ Proof.
+ specialize (Hf a).
by rewrite Hb in Hf.
- intros (a & b & -> & Hb).
- by apply (morph_valid _).
+ by apply (cmra_morphism_valid _).
Qed.
End coProd_cmra.
@@ -1034,7 +893,7 @@ Global Arguments coProdR {_ _} _.
Definition fmatch {A} `{!EqDecision A} {B : A → cmra} {C : cmra} (f : ∀ a, B a → C) (g : coProd B) : C :=
dsum_fold f (coProd_car g).
-Global Instance fmatch_morph {A} `{!EqDecision A} {B : A → cmra} {C : cmra} (f : ∀ a, B a → C) : (∀ a, Morphism (f a)) → Morphism (fmatch f).
+Global Instance fmatch_morph {A} `{!EqDecision A} {B : A → cmra} {C : cmra} (f : ∀ a, B a → C) : (∀ a, CmraMorphism (f a)) → CmraMorphism (fmatch f).
Proof.
intros Hf.
assert (NonExpansive (fmatch f)) by solve_proper.
@@ -1042,7 +901,7 @@ Proof.
split=>//.
- intros n g (a & b & -> & ?)%coProd_validN.
rewrite /fmatch /= dsum_fold_DSum.
- by apply (morph_validN _).
+ by apply (cmra_morphism_validN _).
- intros g1 g2.
rewrite /fmatch /=.
apply dsum_fold_op, _.
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index f4d7d6f3f22b1372479c4632594f1edf4d814824..86986bd1d4a75207249e391137b11942dffb4c98 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -3,10 +3,6 @@ From iris.algebra Require Export ofe monoid.
From iris.prelude Require Import options.
Local Set Primitive Projections.
-Class PCore (A : Type) := pcore : A → option A.
-Global Hint Mode PCore ! : typeclass_instances.
-Global Instance: Params (@pcore) 2 := {}.
-
Class Op (A : Type) := op : A → A → A.
Global Hint Mode Op ! : typeclass_instances.
Global Instance: Params (@op) 2 := {}.
@@ -51,11 +47,9 @@ Global Instance: Params (@includedN) 4 := {}.
Global Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
Section mixin.
- Record CmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A} := {
+ Record CmraMixin A `{!Dist A, !Equiv A, !Op A, !Valid A, !ValidN A} := {
(* setoids *)
mixin_cmra_op_ne (x : A) : NonExpansive (op x);
- mixin_cmra_pcore_ne n (x y : A) cx :
- x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
mixin_cmra_validN_ne n : Proper (dist (A := A) n ==> impl) (validN n);
(* valid *)
mixin_cmra_valid_validN (x : A) : ✓ x ↔ ∀ n, ✓{n} x;
@@ -63,10 +57,6 @@ Section mixin.
(* monoid *)
mixin_cmra_assoc : Assoc (≡@{A}) (⋅);
mixin_cmra_comm : Comm (≡@{A}) (⋅);
- mixin_cmra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
- mixin_cmra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
- mixin_cmra_pcore_mono (x y : A) cx :
- x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
mixin_cmra_validN_op_l n (x y : A) : ✓{n} (x ⋅ y) → ✓{n} x;
mixin_cmra_extend n (x y1 y2 : A) :
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
@@ -84,14 +74,13 @@ Structure cmra := Cmra' {
cmra_car :> Type;
cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car;
- cmra_pcore : PCore cmra_car;
cmra_op : Op cmra_car;
cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CmraMixin cmra_car;
}.
-Global Arguments Cmra' _ {_ _ _ _ _ _} _ _.
+Global Arguments Cmra' _ {_ _ _ _ _} _ _.
(* Given [m : CmraMixin A], the notation [Cmra A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
@@ -100,7 +89,6 @@ Notation Cmra A m := (Cmra' A (ofe_mixin_of A%type) m) (only parsing).
Global Arguments cmra_car : simpl never.
Global Arguments cmra_equiv : simpl never.
Global Arguments cmra_dist : simpl never.
-Global Arguments cmra_pcore : simpl never.
Global Arguments cmra_op : simpl never.
Global Arguments cmra_valid : simpl never.
Global Arguments cmra_validN : simpl never.
@@ -108,7 +96,6 @@ Global Arguments cmra_ofe_mixin : simpl never.
Global Arguments cmra_mixin : simpl never.
Add Printing Constructor cmra.
(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
-Global Hint Extern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_instances.
Global Hint Extern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.
Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.
@@ -125,7 +112,7 @@ Canonical Structure cmra_ofeO.
problem with canonical structure inference. Additionally, we make Coq
eagerly expand the coercions that go from one structure to another, like
[cmra_ofeO] in this case. *)
-Global Strategy expand [cmra_ofeO cmra_equiv cmra_dist cmra_pcore cmra_op
+Global Strategy expand [cmra_ofeO cmra_equiv cmra_dist cmra_op
cmra_valid cmra_validN cmra_ofe_mixin cmra_mixin].
Definition cmra_mixin_of' A {Ac : cmra} (f : Ac → A) : CmraMixin Ac := cmra_mixin Ac.
@@ -138,9 +125,6 @@ Section cmra_mixin.
Implicit Types x y : A.
Global Instance cmra_op_ne (x : A) : NonExpansive (op x).
Proof. apply (mixin_cmra_op_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.
@@ -151,13 +135,6 @@ 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_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_mono x y cx :
- x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
- Proof. apply (mixin_cmra_pcore_mono _ (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 :
@@ -171,7 +148,7 @@ Section cmra_mixin.
End cmra_mixin.
(** * CoreId elements *)
-Class CoreId {A : cmra} (x : A) := core_id : pcore x ≡ Some x.
+Class CoreId {A : cmra} (x : A) := core_id : x ≡ x ⋅ x.
Global Arguments core_id {_} _ {_}.
Global Hint Mode CoreId + ! : typeclass_instances.
Global Instance: Params (@CoreId) 1 := {}.
@@ -197,24 +174,17 @@ Global Hint Mode IdFree + ! : typeclass_instances.
Global Instance: Params (@IdFree) 1 := {}.
(** * CMRAs whose core is total *)
-Class CmraTotal (A : cmra) := cmra_total (x : A) : is_Some (pcore x).
+Class CmraTotal (A : cmra) := cmra_total (x : A) : ∃ cx, cx ≼ x ∧ cx ≡ cx ⋅ cx.
Global Hint Mode CmraTotal ! : typeclass_instances.
-(** The function [core] returns a dummy when used on CMRAs without total
-core. We only ever use this for [CmraTotal] CMRAs, but it is more convenient
-to not require that proof to be able to call this function. *)
-Definition core {A} `{!PCore A} (x : A) : A := default x (pcore x).
-Global Instance: Params (@core) 2 := {}.
-
(** * CMRAs with a unit element *)
Class Unit (A : Type) := ε : A.
Global Hint Mode Unit ! : typeclass_instances.
Global Arguments ε {_ _}.
-Record UcmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A} := {
+Record UcmraMixin A `{!Dist A, !Equiv A, !Op A, !Valid A, !Unit A} := {
mixin_ucmra_unit_valid : ✓ (ε : A);
mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
- mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
}.
#[projections(primitive=no)] (* FIXME: making this primitive leads to strange
@@ -223,7 +193,6 @@ Structure ucmra := Ucmra' {
ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car;
- ucmra_pcore : PCore ucmra_car;
ucmra_op : Op ucmra_car;
ucmra_valid : Valid ucmra_car;
ucmra_validN : ValidN ucmra_car;
@@ -232,13 +201,12 @@ Structure ucmra := Ucmra' {
ucmra_cmra_mixin : CmraMixin ucmra_car;
ucmra_mixin : UcmraMixin ucmra_car;
}.
-Global Arguments Ucmra' _ {_ _ _ _ _ _ _} _ _ _.
+Global Arguments Ucmra' _ {_ _ _ _ _ _} _ _ _.
Notation Ucmra A m :=
(Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
Global Arguments ucmra_car : simpl never.
Global Arguments ucmra_equiv : simpl never.
Global Arguments ucmra_dist : simpl never.
-Global Arguments ucmra_pcore : simpl never.
Global Arguments ucmra_op : simpl never.
Global Arguments ucmra_valid : simpl never.
Global Arguments ucmra_validN : simpl never.
@@ -259,7 +227,7 @@ Canonical Structure ucmra_cmraR.
problem with canonical structure inference. Additionally, we make Coq
eagerly expand the coercions that go from one structure to another, like
[ucmra_cmraR] and [ucmra_ofeO] in this case. *)
-Global Strategy expand [ucmra_cmraR ucmra_ofeO ucmra_equiv ucmra_dist ucmra_pcore
+Global Strategy expand [ucmra_cmraR ucmra_ofeO ucmra_equiv ucmra_dist
ucmra_op ucmra_valid ucmra_validN ucmra_unit
ucmra_ofe_mixin ucmra_cmra_mixin].
@@ -271,8 +239,6 @@ Section ucmra_mixin.
Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
Global Instance ucmra_unit_left_id : LeftId (≡) ε (@op A _).
Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
- Lemma ucmra_pcore_unit : pcore (ε:A) ≡ Some ε.
- Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
End ucmra_mixin.
(** * Discrete CMRAs *)
@@ -288,12 +254,10 @@ Global Hint Mode CmraDiscrete ! : typeclass_instances.
Class CmraMorphism {A B : cmra} (f : A → B) := {
#[global] cmra_morphism_ne :: NonExpansive f;
cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
- cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
}.
Global Hint Mode CmraMorphism - - ! : typeclass_instances.
Global Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
-Global Arguments cmra_morphism_pcore {_ _} _ {_} _.
Global Arguments cmra_morphism_op {_ _} _ {_} _ _.
(** * Properties **)
@@ -303,22 +267,6 @@ Implicit Types x y z : A.
Implicit Types xs ys zs : list A.
(** ** Setoids *)
-Global Instance cmra_pcore_ne' : NonExpansive (@pcore A _).
-Proof.
- intros n 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. 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' : NonExpansive2 (@op A _).
Proof. intros n x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
Global Instance cmra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
@@ -379,28 +327,6 @@ Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
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_pcore_l' x cx : pcore x ≡ Some cx → cx ⋅ x ≡ x.
-Proof. intros (cx'&?&<-)%Some_equiv_eq. 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'&?&<-)%Some_equiv_eq. by apply cmra_pcore_r. Qed.
-Lemma cmra_pcore_idemp' x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx.
-Proof. intros (cx'&?&<-)%Some_equiv_eq. eauto using cmra_pcore_idemp. Qed.
-Lemma cmra_pcore_dup x cx : pcore x = Some cx → cx ≡ cx ⋅ cx.
-Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
-Lemma cmra_pcore_dup' x cx : pcore x ≡ Some cx → cx ≡ cx ⋅ cx.
-Proof. intros; symmetry; 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.
-
(** ** Exclusive elements *)
Lemma exclusiveN_l n x `{!Exclusive x} y : ✓{n} (x ⋅ y) → False.
Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed.
@@ -449,27 +375,6 @@ 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_pcore_mono' x y cx :
- x ≼ y → pcore x ≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
-Proof.
- intros ? (cx'&?&Hcx)%Some_equiv_eq.
- destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
- exists cy; by rewrite -Hcx.
-Qed.
-Lemma cmra_pcore_monoN' n x y cx :
- x ≼{n} y → pcore x ≡{n}≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼{n} cy.
-Proof.
- intros [z Hy] (cx'&?&Hcx)%dist_Some_inv_r'.
- destruct (cmra_pcore_mono 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_pcore x cx : pcore x = Some cx → cx ≼ x.
-Proof. exists x. by rewrite cmra_pcore_l. Qed.
-
Lemma cmra_monoN_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_mono_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
@@ -498,16 +403,18 @@ Proof.
Qed.
(** ** CoreId elements *)
-Lemma core_id_dup x `{!CoreId x} : x ≡ x ⋅ x.
-Proof. by apply cmra_pcore_dup' with x. Qed.
-
Lemma core_id_extract x y `{!CoreId x} :
x ≼ y → y ≡ y ⋅ x.
Proof.
- intros ?.
- destruct (cmra_pcore_mono' x y x) as (cy & Hcy & [x' Hx']); [done|exact: core_id|].
- rewrite -(cmra_pcore_r y) //. rewrite Hx' -!assoc. f_equiv.
- rewrite [x' â‹… x]comm assoc -core_id_dup. done.
+ intros [z ->].
+ by rewrite (comm _ _ x) assoc -core_id.
+Qed.
+
+Global Instance op_core_id x y : CoreId x → CoreId y → CoreId (x ⋅ y).
+Proof.
+ rewrite /CoreId. intros Hx Hy.
+ rewrite assoc -(assoc _ x) (comm _ y) assoc -assoc.
+ by f_equiv.
Qed.
(** ** Total core *)
@@ -515,82 +422,32 @@ Section total_core.
Local Set Default Proof Using "Type*".
Context `{!CmraTotal A}.
- Lemma cmra_pcore_core x : pcore x = Some (core x).
- Proof.
- rewrite /core. destruct (cmra_total x) as [cx ->]. done.
- Qed.
- 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_mono x y : x ≼ y → core x ≼ core y.
- Proof.
- intros; destruct (cmra_total x) as [cx Hcx].
- destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
- by rewrite /core /= Hcx Hcy.
- Qed.
-
- Global Instance cmra_core_ne : NonExpansive (@core A _).
- Proof.
- intros n 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_dup x : core x ≡ core x ⋅ core x.
- Proof. by rewrite -{3}(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 core_id_total x : CoreId x ↔ core x ≡ x.
- Proof.
- split; [intros; by rewrite /core /= (core_id x)|].
- rewrite /CoreId /core /=.
- destruct (cmra_total x) as [? ->]. by constructor.
- Qed.
- Lemma core_id_core x `{!CoreId x} : core x ≡ x.
- Proof. by apply core_id_total. Qed.
-
- (** Not an instance since TC search cannot solve the premise. *)
- Lemma cmra_pcore_core_id x y : pcore x = Some y → CoreId y.
- Proof. rewrite /CoreId. eauto using cmra_pcore_idemp. Qed.
-
- Global Instance cmra_core_core_id x : CoreId (core x).
- Proof. eapply cmra_pcore_core_id. rewrite cmra_pcore_core. done. 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.
+ split; last apply _.
+ intros x.
+ destruct (cmra_total x) as (cx & [y ->] & Hcx).
+ exists cx.
+ by rewrite (comm _ _ cx) assoc -Hcx.
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_monoN n x y : x ≼{n} y → core x ≼{n} core y.
- Proof.
- intros [z ->].
- apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
+ split; last apply _.
+ intros x.
+ destruct (cmra_total x) as (cx & [y ->] & Hcx).
+ exists cx.
+ by rewrite (comm _ _ cx) assoc -Hcx.
Qed.
Lemma cmra_maximum_idemp_total n (x : A) : ✓{n} x →
{ cx | cx ≼{n} x ∧ cx ⋅ cx ≡{n}≡ cx ∧ ∀ m (y : A), m ≤ n → y ≼{m} x → y ⋅ y ≡{m}≡ y → y ≼{m} cx }.
Proof.
intros Hx.
destruct (cmra_maximum_idemp n x Hx) as [?|H]; first done.
- destruct (H (core x))=>//.
- + exists x.
- by rewrite cmra_core_l.
- + by rewrite -cmra_core_dup.
+ exfalso.
+ destruct (cmra_total x) as (cx & ? & ?).
+ destruct (H cx).
+ - by apply cmra_included_includedN.
+ - by apply equiv_dist.
Qed.
End total_core.
@@ -699,11 +556,11 @@ Section ucmra.
Global Instance ucmra_unit_right_id : RightId (≡) ε (@op A _).
Proof. by intros x; rewrite (comm op) left_id. Qed.
Global Instance ucmra_unit_core_id : CoreId (ε:A).
- Proof. apply ucmra_pcore_unit. Qed.
+ Proof. rewrite /CoreId. by rewrite left_id. Qed.
Global Instance cmra_unit_cmra_total : CmraTotal A.
Proof.
- intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?); [..|by eauto].
+ intros x. exists ε; split.
- apply ucmra_unit_least.
- apply (core_id _).
Qed.
@@ -728,41 +585,9 @@ Section cmra_leibniz.
Global Instance cmra_comm_L : Comm (=) (@op A _).
Proof. intros x y. unfold_leibniz. by rewrite comm. Qed.
- Lemma cmra_pcore_l_L x cx : pcore x = Some cx → cx ⋅ x = x.
- Proof. unfold_leibniz. apply cmra_pcore_l'. Qed.
- Lemma cmra_pcore_idemp_L x cx : pcore x = Some cx → pcore cx = Some cx.
- Proof. unfold_leibniz. apply cmra_pcore_idemp'. Qed.
-
- Lemma cmra_op_opM_assoc_L x y mz : (x â‹… y) â‹…? mz = x â‹… (y â‹…? mz).
- Proof. unfold_leibniz. apply cmra_op_opM_assoc. Qed.
-
- (** ** Core *)
- Lemma cmra_pcore_r_L x cx : pcore x = Some cx → x ⋅ cx = x.
- Proof. unfold_leibniz. apply cmra_pcore_r'. Qed.
- Lemma cmra_pcore_dup_L x cx : pcore x = Some cx → cx = cx ⋅ cx.
- Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.
-
(** ** CoreId elements *)
- Lemma core_id_dup_L x `{!CoreId x} : x = x â‹… x.
- Proof. unfold_leibniz. by apply core_id_dup. Qed.
-
- (** ** Total core *)
- Section total_core.
- Context `{!CmraTotal A}.
-
- Lemma cmra_core_r_L x : x â‹… core x = x.
- Proof. unfold_leibniz. apply cmra_core_r. Qed.
- Lemma cmra_core_l_L x : core x â‹… x = x.
- Proof. unfold_leibniz. apply cmra_core_l. Qed.
- Lemma cmra_core_idemp_L x : core (core x) = core x.
- Proof. unfold_leibniz. apply cmra_core_idemp. Qed.
- Lemma cmra_core_dup_L x : core x = core x â‹… core x.
- Proof. unfold_leibniz. apply cmra_core_dup. Qed.
- Lemma core_id_total_L x : CoreId x ↔ core x = x.
- Proof. unfold_leibniz. apply core_id_total. Qed.
- Lemma core_id_core_L x `{!CoreId x} : core x = x.
- Proof. by apply core_id_total_L. Qed.
- End total_core.
+ Lemma core_id_L x `{!CoreId x} : x = x â‹… x.
+ Proof. unfold_leibniz. by apply (core_id x). Qed.
End cmra_leibniz.
Section ucmra_leibniz.
@@ -778,18 +603,13 @@ End ucmra_leibniz.
(** * 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 : A, is_Some (pcore x)).
+ Context A `{!Dist A, !Equiv A, !Op A, !Valid A, !ValidN A}.
Context (op_ne : ∀ x : A, NonExpansive (op x)).
- Context (core_ne : NonExpansive (@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_mono : ∀ 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 →
@@ -799,13 +619,6 @@ Section cmra_total.
Lemma cmra_total_mixin : CmraMixin A.
Proof using Type*.
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_mono Hx. move: Hxy.
- rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
Qed.
End cmra_total.
@@ -815,7 +628,6 @@ Proof.
split => /=.
- apply _.
- done.
- - intros. by rewrite option_fmap_id.
- done.
Qed.
Global Instance cmra_morphism_proper {A B : cmra} (f : A → B) `{!CmraMorphism f} :
@@ -826,15 +638,12 @@ Proof.
split.
- apply _.
- move=> n x Hx /=. by apply cmra_morphism_validN, cmra_morphism_validN.
- - move=> x /=. by rewrite option_fmap_compose !cmra_morphism_pcore.
- move=> x y /=. by rewrite !cmra_morphism_op.
Qed.
Section cmra_morphism.
Local Set Default Proof Using "Type*".
Context {A B : cmra} (f : A → B) `{!CmraMorphism f}.
- Lemma cmra_morphism_core x : f (core x) ≡ core (f x).
- Proof. unfold core. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
Lemma cmra_morphism_monotone x y : x ≼ y → f x ≼ f y.
Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
Lemma cmra_morphism_monotoneN n x y : x ≼{n} y → f x ≼{n} f y.
@@ -1048,8 +857,6 @@ Section cmra_transport.
Proof. by intros ???; destruct H. Qed.
Lemma cmra_transport_op x y : T (x â‹… y) = T x â‹… T y.
Proof. by destruct H. Qed.
- Lemma cmra_transport_core x : T (core x) = core (T x).
- Proof. by destruct H. Qed.
Lemma cmra_transport_validN n x : ✓{n} T x ↔ ✓{n} x.
Proof. by destruct H. Qed.
Lemma cmra_transport_valid x : ✓ T x ↔ ✓ x.
@@ -1062,19 +869,13 @@ End cmra_transport.
(** * Instances *)
(** ** Discrete CMRA *)
-Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
+Record RAMixin A `{Equiv A, Op A, Valid A} := {
(* setoids *)
ra_op_proper (x : A) : Proper ((≡) ==> (≡)) (op x);
- ra_core_proper (x y : A) cx :
- x ≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡ cy;
ra_validN_proper : Proper ((≡@{A}) ==> impl) valid;
(* monoid *)
ra_assoc : Assoc (≡@{A}) (⋅);
ra_comm : Comm (≡@{A}) (⋅);
- ra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
- ra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
- ra_pcore_mono (x y : A) cx :
- x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
ra_valid_op_l (x y : A) : ✓ (x ⋅ y) → ✓ x;
ra_maximum_idemp (x : A) : ✓ x →
{ cx | cx ≼ x ∧ cx ⋅ cx ≡ cx ∧ ∀ (y : A), y ≼ x → y ⋅ y ≡ y → y ≼ cx } +
@@ -1083,14 +884,14 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
Section discrete.
Local Set Default Proof Using "Type*".
- Context `{!Equiv A, !PCore A, !Op A, !Valid A} (Heq : @Equivalence A (≡)).
+ Context `{!Equiv A, !Op A, !Valid A} (Heq : @Equivalence A (≡)).
Context (ra_mix : RAMixin A).
Existing Instances discrete_dist.
Local Instance discrete_validN_instance : ValidN A := λ n x, ✓ x.
Definition discrete_cmra_mixin : CmraMixin A.
Proof.
- destruct ra_mix as [????????? maximum_idemp]; split; try done.
+ destruct ra_mix as [????? maximum_idemp]; split; try done.
- intros x; split; first done. by move=> /(_ 0).
- intros n x y1 y2 ??; by exists y1, y2.
- intros n x ?.
@@ -1114,37 +915,22 @@ Notation discreteR A ra_mix :=
Section ra_total.
Local Set Default Proof Using "Type*".
- Context A `{Equiv A, PCore A, Op A, Valid A}.
- Context (total : ∀ x : A, is_Some (pcore x)).
+ Context A `{Equiv A, Op A, Valid A}.
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_mono : ∀ x y : A, x ≼ y → core x ≼ core y).
Context (valid_op_l : ∀ x y : A, ✓ (x ⋅ y) → ✓ x).
Context (maximum_idemp : ∀ x : A, ✓ x →
{ cx | cx ≼ x ∧ cx ⋅ cx ≡ cx ∧ ∀ (y : A), y ≼ x → y ⋅ y ≡ y → y ≼ cx }).
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_mono Hx. move: Hxy.
- rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
- Qed.
+ Proof. split; auto. Qed.
End ra_total.
(** ** CMRA for the unit type *)
Section unit.
Local Instance unit_valid_instance : Valid () := λ x, True.
Local Instance unit_validN_instance : ValidN () := λ n x, True.
- Local Instance unit_pcore_instance : PCore () := λ x, Some x.
Local Instance unit_op_instance : Op () := λ x y, ().
Lemma unit_cmra_mixin : CmraMixin ().
Proof.
@@ -1172,7 +958,6 @@ End unit.
Section empty.
Local Instance Empty_set_valid_instance : Valid Empty_set := λ x, False.
Local Instance Empty_set_validN_instance : ValidN Empty_set := λ n x, False.
- Local Instance Empty_set_pcore_instance : PCore Empty_set := λ x, Some x.
Local Instance Empty_set_op_instance : Op Empty_set := λ x y, x.
Lemma Empty_set_cmra_mixin : CmraMixin Empty_set.
Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
@@ -1189,28 +974,11 @@ End empty.
(** ** Product *)
Section prod.
Context {A B : cmra}.
- Local Arguments pcore _ _ !_ /.
- Local Arguments cmra_pcore _ !_/.
Local Instance prod_op_instance : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
- Local Instance prod_pcore_instance : PCore (A * B) := λ x,
- c1 ↠pcore (x.1); c2 ↠pcore (x.2); Some (c1, c2).
- Local Arguments prod_pcore_instance !_ /.
Local Instance prod_valid_instance : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
Local Instance prod_validN_instance : 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&<-)%Some_equiv_eq|].
- rewrite {3}/pcore /prod_pcore_instance. (* 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|].
@@ -1226,10 +994,6 @@ Section prod.
Proof.
split; try apply _.
- by intros n x 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.
@@ -1237,14 +1001,6 @@ Section prod.
- by intros n x [??]; split; apply cmra_validN_S.
- by split; rewrite /= assoc.
- by split; rewrite /= comm.
- - 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_mono (x.1) (y.1) (cx.1)) as (z1&?&?); auto.
- destruct (cmra_pcore_mono (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 (z11&z12&?&?&?); auto.
@@ -1285,20 +1041,13 @@ Section prod.
Lemma pair_includedN (a a' : A) (b b' : B) n :
(a, b) ≼{n} (a', b') ↔ a ≼{n} a' ∧ b ≼{n} b'.
Proof. apply prod_includedN. Qed.
- Lemma pair_pcore (a : A) (b : B) :
- pcore (a, b) = c1 ↠pcore a; c2 ↠pcore b; Some (c1, c2).
- Proof. done. Qed.
- Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
- core (a, b) = (core a, core b).
- Proof.
- rewrite /core {1}/pcore /=.
- rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
- Qed.
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.
+ intros H1 H2 [a b]. destruct (H1 a) as (ca & ? & ?), (H2 b) as (cb & ? & ?).
+ exists (ca, cb); split.
+ - by apply prod_included.
+ - done.
Qed.
Global Instance prod_cmra_discrete :
@@ -1309,7 +1058,7 @@ Section prod.
unification. *)
Lemma pair_core_id x y :
CoreId x → CoreId y → CoreId (x,y).
- Proof. by rewrite /CoreId prod_pcore_Some'. Qed.
+ Proof. by rewrite /CoreId. Qed.
Global Instance pair_exclusive_l x y : Exclusive x → Exclusive (x,y).
Proof. by intros ?[][?%exclusive0_l]. Qed.
@@ -1341,7 +1090,6 @@ Section prod_unit.
split.
- split; apply ucmra_unit_valid.
- by split; rewrite /=left_id.
- - rewrite prod_pcore_Some'; split; apply (core_id _).
Qed.
Canonical Structure prodUR := Ucmra (prod A B) prod_ucmra_mixin.
@@ -1374,12 +1122,6 @@ Global Instance prod_map_cmra_morphism {A A' B B' : cmra} (f : A → A') (g : B
Proof.
split; first apply _.
- by intros n x [??]; split; simpl; apply cmra_morphism_validN.
- - intros [x1 x2]. rewrite /= !pair_pcore. simpl.
- pose proof (Hf := cmra_morphism_pcore f (x1)).
- destruct (pcore (f (x1))), (pcore (x1)); inversion_clear Hf=>//=.
- pose proof (Hg := cmra_morphism_pcore g (x2)).
- destruct (pcore (g (x2))), (pcore (x2)); inversion_clear Hg=>//=.
- by setoid_subst.
- intros. by rewrite /prod_map /= !cmra_morphism_op.
Qed.
@@ -1436,26 +1178,17 @@ Section option.
Context {A : cmra}.
Implicit Types a b : A.
Implicit Types ma mb : option A.
- Local Arguments core _ _ !_ /.
- Local Arguments pcore _ _ !_ /.
Local Instance option_valid_instance : Valid (option A) := λ ma,
match ma with Some a => ✓ a | None => True end.
Local Instance option_validN_instance : ValidN (option A) := λ n ma,
match ma with Some a => ✓{n} a | None => True end.
- Local Instance option_pcore_instance : PCore (option A) := λ ma,
- Some (ma ≫= pcore).
- Local Arguments option_pcore_instance !_ /.
Local Instance option_op_instance : Op (option A) :=
union_with (λ a b, Some (a ⋅ b)).
Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} 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 pcore_Some a : pcore (Some a) = Some (pcore a).
- Proof. done. Qed.
Lemma Some_op_opM a ma : Some a â‹… ma = Some (a â‹…? ma).
Proof. by destruct ma. Qed.
@@ -1509,25 +1242,13 @@ Section option.
Lemma option_cmra_mixin : CmraMixin (option A).
Proof.
apply cmra_total_mixin.
- - eauto.
- by intros [a|] n; destruct 1; constructor; ofe_subst.
- - destruct 1; by ofe_subst.
- by destruct 1; rewrite /validN /option_validN_instance //=; ofe_subst.
- intros [a|]; [apply cmra_valid_validN|done].
- intros n [a|];
unfold validN, option_validN_instance; eauto using cmra_validN_S.
- intros [a|] [b|] [c|]; constructor; rewrite ?assoc; auto.
- intros [a|] [b|]; constructor; rewrite 1?comm; auto.
- - intros [a|]; simpl; auto.
- destruct (pcore a) as [ca|] eqn:?; constructor; eauto using cmra_pcore_l.
- - intros [a|]; simpl; auto.
- destruct (pcore a) as [ca|] eqn:?; simpl; eauto using cmra_pcore_idemp.
- - intros ma mb; setoid_rewrite option_included.
- intros [->|(a&b&->&->&[?|?])]; simpl; eauto.
- + destruct (pcore a) as [ca|] eqn:?; eauto.
- destruct (cmra_pcore_proper a b ca) as (?&?&?); eauto 10.
- + destruct (pcore a) as [ca|] eqn:?; eauto.
- destruct (cmra_pcore_mono a b ca) as (?&?&?); eauto 10.
- intros n [a|] [b|]; rewrite /validN /option_validN_instance /=;
eauto using cmra_validN_op_l.
- intros n ma mb1 mb2.
@@ -1578,7 +1299,7 @@ Section option.
Local Instance option_unit_instance : Unit (option A) := None.
Lemma option_ucmra_mixin : UcmraMixin optionR.
- Proof. split; [done| |done]. by intros []. Qed.
+ Proof. split; first done. by intros []. Qed.
Canonical Structure optionUR := Ucmra (option A) option_ucmra_mixin.
(** Misc *)
@@ -1751,7 +1472,6 @@ Global Instance option_fmap_cmra_morphism {A B : cmra} (f: A → B) `{!CmraMorph
Proof.
split; first apply _.
- intros n [a|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
- - move=> [a|] //. by apply Some_proper, cmra_morphism_pcore.
- move=> [a|] [b|] //=. by rewrite (cmra_morphism_op f).
Qed.
@@ -1797,15 +1517,12 @@ Section discrete_fun_cmra.
Local Instance discrete_fun_op_instance : Op (discrete_fun B) := λ f g x,
f x â‹… g x.
- Local Instance discrete_fun_pcore_instance : PCore (discrete_fun B) := λ f,
- Some (λ x, core (f x)).
Local Instance discrete_fun_valid_instance : Valid (discrete_fun B) := λ f,
∀ x, ✓ f x.
Local Instance discrete_fun_validN_instance : ValidN (discrete_fun B) := λ n f,
∀ x, ✓{n} f x.
Definition discrete_fun_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
- Definition discrete_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
Lemma discrete_fun_included_spec_1 (f g : discrete_fun B) x : f ≼ g → f x ≼ g x.
Proof.
@@ -1822,9 +1539,7 @@ Section discrete_fun_cmra.
Lemma discrete_fun_cmra_mixin : CmraMixin (discrete_fun B).
Proof.
apply cmra_total_mixin.
- - eauto.
- intros n f1 f2 f3 Hf x. by rewrite discrete_fun_lookup_op (Hf x).
- - intros n f1 f2 Hf x. by rewrite discrete_fun_lookup_core (Hf x).
- intros n f1 f2 Hf ? x. by rewrite -(Hf x).
- intros g; split.
+ intros Hg n i; apply cmra_valid_validN, Hg.
@@ -1832,13 +1547,6 @@ Section discrete_fun_cmra.
- intros n f Hf x; apply cmra_validN_S, Hf.
- intros f1 f2 f3 x. by rewrite discrete_fun_lookup_op assoc.
- intros f1 f2 x. by rewrite discrete_fun_lookup_op comm.
- - intros f x.
- by rewrite discrete_fun_lookup_op discrete_fun_lookup_core cmra_core_l.
- - intros f x. by rewrite discrete_fun_lookup_core cmra_core_idemp.
- - intros f1 f2 Hf12. exists (core f2)=>x. rewrite discrete_fun_lookup_op.
- apply (discrete_fun_included_spec_1 _ _ x), (cmra_core_mono (f1 x)) in Hf12.
- rewrite !discrete_fun_lookup_core. destruct Hf12 as [? ->].
- rewrite assoc -cmra_core_dup //.
- intros n f1 f2 Hf x. apply cmra_validN_op_l with (f2 x), Hf.
- intros n f f1 f2 Hf Hf12.
assert (FUN := λ x, cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
@@ -1874,7 +1582,6 @@ Section discrete_fun_cmra.
split.
- intros x. apply ucmra_unit_valid.
- intros f x. by rewrite discrete_fun_lookup_op left_id.
- - constructor=> x. apply core_id_core, _.
Qed.
Canonical Structure discrete_funUR :=
Ucmra (discrete_fun B) discrete_fun_ucmra_mixin.
@@ -1894,7 +1601,6 @@ Proof.
split; first apply _.
- intros n g Hg x. rewrite /discrete_fun_map.
apply (cmra_morphism_validN (f _)), Hg.
- - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
- intros g1 g2 i.
by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
Qed.
@@ -1934,7 +1640,7 @@ prove that if the composition of two elements is valid, then so are both of the
elements. The "domain" is the image of [g] in [A], or equivalently the part of
[A] where [f] returns [Some]. *)
Lemma inj_cmra_mixin_restrict_validity {A : cmra} {B : ofe}
- `{!PCore B, !Op B, !Valid B, !ValidN B}
+ `{!Op B, !Valid B, !ValidN B}
(f : A → option B) (g : B → A)
(* [g] is proper/non-expansive and injective w.r.t. OFE equality *)
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
@@ -1942,8 +1648,6 @@ Lemma inj_cmra_mixin_restrict_validity {A : cmra} {B : ofe}
(and [f] its inverse) *)
(gf_dist : ∀ (x : A) (y : B) n, f x ≡{n}≡ Some y ↔ g y ≡{n}≡ x)
(* [g] commutes with [pcore] (on the part where it is defined) and [op] *)
- (g_pcore_dist : ∀ (y cy : B) n,
- pcore y ≡{n}≡ Some cy ↔ pcore (g y) ≡{n}≡ Some (g cy))
(g_op : ∀ (y1 y2 : B), g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
(* [g] also commutes with [opM] when the right-hand side is produced by [f],
and cancels the [f]. In particular this axiom implies that when taking an
@@ -1970,51 +1674,20 @@ Proof.
(* Some general derived facts that will be useful later. *)
assert (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2).
{ intros ??. rewrite !equiv_dist. naive_solver. }
- assert (g_pcore : ∀ (y cy : B),
- pcore y ≡ Some cy ↔ pcore (g y) ≡ Some (g cy)).
- { intros. rewrite !equiv_dist. naive_solver. }
assert (gf : ∀ x y, f x ≡ Some y ↔ g y ≡ x).
{ intros. rewrite !equiv_dist. naive_solver. }
assert (fg : ∀ y, f (g y) ≡ Some y).
{ intros. apply gf. done. }
assert (g_ne : NonExpansive g).
{ intros n ???. apply g_dist. done. }
- (* Some of the CMRA properties are useful in proving the others. *)
- assert (b_pcore_l' : ∀ y cy : B, pcore y ≡ Some cy → cy ⋅ y ≡ y).
- { intros y cy Hy. apply g_equiv. rewrite g_op. apply cmra_pcore_l'.
- apply g_pcore. done. }
- assert (b_pcore_idemp : ∀ y cy : B, pcore y ≡ Some cy → pcore cy ≡ Some cy).
- { intros y cy Hy. eapply g_pcore, cmra_pcore_idemp', g_pcore. done. }
(* Now prove all the mixin laws. *)
split.
- intros y n z1 z2 Hz%g_dist. apply g_dist. by rewrite !g_op Hz.
- - intros n y1 y2 cy Hy%g_dist Hy1.
- assert (g <$> pcore y2 ≡{n}≡ Some (g cy))
- as (cx & (cy'&->&->)%fmap_Some_1 & ?%g_dist)%dist_Some_inv_r'; [|by eauto].
- assert (Hgcy : pcore (g y1) ≡ Some (g cy)).
- { apply g_pcore. rewrite Hy1. done. }
- rewrite equiv_dist in Hgcy. specialize (Hgcy n).
- rewrite Hy in Hgcy. apply g_pcore_dist in Hgcy. rewrite Hgcy. done.
- done.
- done.
- done.
- intros y1 y2 y3. apply g_equiv. by rewrite !g_op assoc.
- intros y1 y2. apply g_equiv. by rewrite !g_op comm.
- - intros y cy Hcy. apply b_pcore_l'. by rewrite Hcy.
- - intros y cy Hcy. eapply b_pcore_idemp. by rewrite -Hcy.
- - intros y1 y2 cy [z Hy2] Hy1.
- destruct (cmra_pcore_mono' (g y1) (g y2) (g cy)) as (cx&Hcgy2&[x Hcx]).
- { exists (g z). rewrite -g_op. by apply g_equiv. }
- { apply g_pcore. rewrite Hy1 //. }
- apply (reflexive_eq (R:=equiv)) in Hcgy2.
- rewrite -g_opM_f in Hcx. rewrite Hcx in Hcgy2.
- apply g_pcore in Hcgy2.
- apply Some_equiv_eq in Hcgy2 as [cy' [-> Hcy']].
- eexists. split; first done.
- destruct (f x) as [y|].
- + exists y. done.
- + exists cy. apply (reflexive_eq (R:=equiv)), b_pcore_idemp, b_pcore_l' in Hy1.
- rewrite Hy1 //.
- done.
- intros n y z1 z2 ?%g_validN ?.
destruct (cmra_extend n (g y) (g z1) (g z2)) as (x1&x2&Hgy&Hx1&Hx2).
@@ -2073,14 +1746,13 @@ Qed.
(** Constructing a CMRA through an isomorphism that may restrict validity. *)
Lemma iso_cmra_mixin_restrict_validity {A : cmra} {B : ofe}
- `{!PCore B, !Op B, !Valid B, !ValidN B}
+ `{!Op B, !Valid B, !ValidN B}
(f : A → B) (g : B → A)
(* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
(* [g] is surjective (and [f] its inverse) *)
(gf : ∀ x : A, g (f x) ≡ x)
- (* [g] commutes with [pcore] and [op] *)
- (g_pcore : ∀ y : B, pcore (g y) ≡ g <$> pcore y)
+ (* [g] commutes with [op] *)
(g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
(* The validity predicate on [B] restricts the one on [A] *)
(g_validN : ∀ n y, ✓{n} y → ✓{n} (g y))
@@ -2100,22 +1772,18 @@ Proof.
- intros. split.
+ intros Hy%(inj Some). rewrite -Hy gf //.
+ intros ?. f_equiv. apply g_dist. rewrite gf. done.
- - intros. rewrite g_pcore. split.
- + intros ->. done.
- + intros (? & -> & ->%g_dist)%fmap_Some_dist. done.
- intros ??. simpl. rewrite g_op gf //.
Qed.
(** * Constructing a camera through an isomorphism *)
Lemma iso_cmra_mixin {A : cmra} {B : ofe}
- `{!PCore B, !Op B, !Valid B, !ValidN B}
+ `{!Op B, !Valid B, !ValidN B}
(f : A → B) (g : B → A)
(* [g] is proper/non-expansive and injective w.r.t. OFE equality *)
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
(* [g] is surjective (and [f] its inverse) *)
(gf : ∀ x : A, g (f x) ≡ x)
- (* [g] commutes with [pcore], [op], [valid], and [validN] *)
- (g_pcore : ∀ y : B, pcore (g y) ≡ g <$> pcore y)
+ (* [g] commutes with [op], [valid], and [validN] *)
(g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
(g_valid : ∀ y, ✓ (g y) ↔ ✓ y)
(g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
diff --git a/iris/algebra/coPset.v b/iris/algebra/coPset.v
index 414eea193285dad285e4616faff4dc4daed7bad3..b0b9f0cfdb40160805f2b80149f4d2d911cfd54c 100644
--- a/iris/algebra/coPset.v
+++ b/iris/algebra/coPset.v
@@ -14,12 +14,9 @@ Section coPset.
Local Instance coPset_valid_instance : Valid coPset := λ _, True.
Local Instance coPset_unit_instance : Unit coPset := (∅ : coPset).
Local Instance coPset_op_instance : Op coPset := union.
- Local Instance coPset_pcore_instance : PCore coPset := Some.
Lemma coPset_op X Y : X ⋅ Y = X ∪ Y.
Proof. done. Qed.
- Lemma coPset_core X : core X = X.
- Proof. done. Qed.
Lemma coPset_included X Y : X ≼ Y ↔ X ⊆ Y.
Proof.
split.
@@ -32,10 +29,8 @@ Section coPset.
apply ra_total_mixin; eauto.
- solve_proper.
- solve_proper.
- - solve_proper.
- intros X1 X2 X3. by rewrite !coPset_op assoc_L.
- intros X1 X2. by rewrite !coPset_op comm_L.
- - intros X. by rewrite coPset_core idemp_L.
- intros X _.
exists X; split_and! =>//.
+ apply coPset_included. set_solver.
@@ -47,7 +42,7 @@ Section coPset.
Proof. apply discrete_cmra_discrete. Qed.
Lemma coPset_ucmra_mixin : UcmraMixin coPset.
- Proof. split; [done | | done]. intros X. by rewrite coPset_op left_id_L. Qed.
+ Proof. split; first done. intros X. by rewrite coPset_op left_id_L. Qed.
Canonical Structure coPsetUR := Ucmra coPset coPset_ucmra_mixin.
Lemma coPset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
@@ -81,7 +76,6 @@ Section coPset_disj.
| CoPset X, CoPset Y => if decide (X ## Y) then CoPset (X ∪ Y) else CoPsetBot
| _, _ => CoPsetBot
end.
- Local Instance coPset_disj_pcore_instance : PCore coPset_disj := λ _, Some ε.
Ltac coPset_disj_solve :=
repeat (simpl || case_decide);
@@ -106,13 +100,10 @@ Section coPset_disj.
Proof.
apply ra_total_mixin; eauto.
- intros [?|]; destruct 1; coPset_disj_solve.
- - by constructor.
- by destruct 1.
- intros [X1|] [X2|] [X3|]; coPset_disj_solve.
- intros [X1|] [X2|]; coPset_disj_solve.
- intros [X|]; coPset_disj_solve.
- - exists (CoPset ∅); coPset_disj_solve.
- - intros [X1|] [X2|]; coPset_disj_solve.
- intros [X|]=>// _.
exists ε; split_and!.
+ apply coPset_disj_included. set_solver.
@@ -131,6 +122,6 @@ Section coPset_disj.
Proof. apply discrete_cmra_discrete. Qed.
Lemma coPset_disj_ucmra_mixin : UcmraMixin coPset_disj.
- Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
+ Proof. split; first done. intros [X|]; coPset_disj_solve. Qed.
Canonical Structure coPset_disjUR := Ucmra coPset_disj coPset_disj_ucmra_mixin.
End coPset_disj.
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index ac09b23f53370b3c2b140bed4f348e76a309c49d..2785667b17a29161ac3f546d9f31d1e945ef50e8 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -2,8 +2,6 @@ From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Import options.
-Local Arguments pcore _ _ !_ /.
-Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments cmra_validN _ _ !_ /.
@@ -160,12 +158,6 @@ Local Instance csum_validN_instance : ValidN (csum A B) := λ n x,
| Cinr b => ✓{n} b
| CsumBot => False
end.
-Local Instance csum_pcore_instance : PCore (csum A B) := λ x,
- match x with
- | Cinl a => Cinl <$> pcore a
- | Cinr b => Cinr <$> pcore b
- | CsumBot => Some CsumBot
- end.
Local Instance csum_op_instance : Op (csum A B) := λ x y,
match x, y with
| Cinl a, Cinl a' => Cinl (a â‹… a')
@@ -226,36 +218,11 @@ Lemma csum_cmra_mixin : CmraMixin (csum A B).
Proof.
split.
- intros [] n; destruct 1; constructor; by ofe_subst.
- - intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto.
- + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
- destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto.
- exists (Cinl ca'); by repeat constructor.
- + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
- destruct (cmra_pcore_ne n b b' cb) as (cb'&->&?); auto.
- exists (Cinr cb'); by repeat constructor.
- intros ? [a|b|] [a'|b'|] H; inversion_clear H; ofe_subst; done.
- intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
- intros n [a|b|]; simpl; auto using cmra_validN_S.
- intros [a1|b1|] [a2|b2|] [a3|b3|]; constructor; by rewrite ?assoc.
- intros [a1|b1|] [a2|b2|]; constructor; by rewrite 1?comm.
- - intros [a|b|] ? [=]; subst; auto.
- + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
- constructor; eauto using cmra_pcore_l.
- + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
- constructor; eauto using cmra_pcore_l.
- - intros [a|b|] ? [=]; subst; auto.
- + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
- oinversion (cmra_pcore_idemp a ca); repeat constructor; auto.
- + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
- oinversion (cmra_pcore_idemp b cb); repeat constructor; auto.
- - intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
- + exists CsumBot. rewrite csum_included; eauto.
- + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
- destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
- exists (Cinl ca'). rewrite csum_included; eauto 10.
- + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
- destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto.
- exists (Cinr cb'). rewrite csum_included; eauto 10.
- intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
- intros n [a|b|] y1 y2 Hx Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'.
@@ -299,9 +266,9 @@ Proof.
Qed.
Global Instance Cinl_core_id a : CoreId a → CoreId (Cinl a).
-Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed.
+Proof. by constructor. Qed.
Global Instance Cinr_core_id b : CoreId b → CoreId (Cinr b).
-Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed.
+Proof. by constructor. Qed.
Global Instance Cinl_exclusive a : Exclusive a → Exclusive (Cinl a).
Proof. by move=> H[]? =>[/H||]. Qed.
@@ -410,7 +377,6 @@ Global Instance csum_map_cmra_morphism {A A' B B' : cmra} (f : A → A') (g : B
Proof.
split; try apply _.
- intros n [a|b|]; simpl; auto using cmra_morphism_validN.
- - move=> [a|b|]=>//=; rewrite -cmra_morphism_pcore; by destruct pcore.
- intros [xa|ya|] [xb|yb|]=>//=; by rewrite cmra_morphism_op.
Qed.
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 8190ff19f42e47e9b96fc8eec43fb0f541911f25..b5beba24d3b2cfe3af243586e8058ac1fada3707 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -79,16 +79,6 @@ Section dfrac.
| DfracBoth q => q < 1
end%Qp.
- (** As in the fractional camera the core is undefined for elements denoting
- ownership of a fraction. For elements denoting the knowledge that a fraction has
- been discarded the core is the identity function. *)
- Local Instance dfrac_pcore_instance : PCore dfrac := λ dq,
- match dq with
- | DfracOwn q => None
- | DfracDiscarded => Some DfracDiscarded
- | DfracBoth q => Some DfracDiscarded
- end.
-
(** When elements are combined, ownership is added together and knowledge of
discarded fractions is preserved. *)
Local Instance dfrac_op_instance : Op dfrac := λ dq dp,
@@ -134,16 +124,10 @@ Section dfrac.
Definition dfrac_ra_mixin : RAMixin dfrac.
Proof.
split; try apply _.
- - intros [?| |?] ? dq <-; intros [= <-]; eexists _; done.
- intros [?| |?] [?| |?] [?| |?];
rewrite /op /dfrac_op_instance 1?assoc_L 1?assoc_L; done.
- intros [?| |?] [?| |?];
rewrite /op /dfrac_op_instance 1?(comm_L Qp.add); done.
- - intros [?| |?] dq; rewrite /pcore /dfrac_pcore_instance; intros [= <-];
- rewrite /op /dfrac_op_instance; done.
- - intros [?| |?] ? [= <-]; done.
- - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
- apply dfrac_discarded_included.
- intros [q| |q] [q'| |q']; rewrite /op /dfrac_op_instance /valid /dfrac_valid_instance //.
+ intros. trans (q + q')%Qp; [|done]. apply Qp.le_add_l.
+ apply Qp.lt_le_incl.
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index d2fc1a02d0b0e222fb5ef89c693318594a8e1e4d..a1a4f9317470cde7640194ff05499095c12e7bb5 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -74,12 +74,11 @@ Local Instance excl_valid_instance : Valid (excl A) := λ x,
match x with Excl _ => True | ExclBot => False end.
Local Instance excl_validN_instance : ValidN (excl A) := λ n x,
match x with Excl _ => True | ExclBot => False end.
-Local Instance excl_pcore_instance : PCore (excl A) := λ _, None.
Local Instance excl_op_instance : Op (excl A) := λ x y, ExclBot.
Lemma excl_cmra_mixin : CmraMixin (excl A).
Proof.
- split; try discriminate.
+ split.
- by intros n []; destruct 1; constructor.
- by destruct 1; intros ?.
- intros x; split; [done|]. by move=> /(_ 0).
diff --git a/iris/algebra/frac.v b/iris/algebra/frac.v
index 68372fc85bf25d577efdda299fe76546aa1b89e9..f0c7a1aed933642101a7d2f90649bc6fc0b2399e 100644
--- a/iris/algebra/frac.v
+++ b/iris/algebra/frac.v
@@ -16,7 +16,6 @@ Section frac.
Canonical Structure fracO := leibnizO frac.
Local Instance frac_valid_instance : Valid frac := λ x, (x ≤ 1)%Qp.
- Local Instance frac_pcore_instance : PCore frac := λ _, None.
Local Instance frac_op_instance : Op frac := λ x y, (x + y)%Qp.
Lemma frac_valid p : ✓ p ↔ (p ≤ 1)%Qp.
diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v
index 4b0c2dc031ae5b554b493b6af9bbc40e45e82ba4..498f611c67c6be7baec48e42e21a1bde32f33cb9 100644
--- a/iris/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -97,18 +97,6 @@ Section cmra.
by rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne.
Qed.
- Lemma discrete_fun_singleton_core x (y : B x) :
- core (discrete_fun_singleton x y) ≡ discrete_fun_singleton x (core y).
- Proof.
- move=>x'; destruct (decide (x = x')) as [->|];
- by rewrite discrete_fun_lookup_core ?discrete_fun_lookup_singleton
- ?discrete_fun_lookup_singleton_ne // (core_id_core _).
- Qed.
-
- Global Instance discrete_fun_singleton_core_id x (y : B x) :
- CoreId y → CoreId (discrete_fun_singleton x y).
- Proof. by rewrite !core_id_total discrete_fun_singleton_core=> ->. Qed.
-
Lemma discrete_fun_singleton_op (x : A) (y1 y2 : B x) :
discrete_fun_singleton x y1 ⋅ discrete_fun_singleton x y2 ≡ discrete_fun_singleton x (y1 ⋅ y2).
Proof.
@@ -117,6 +105,10 @@ Section cmra.
- by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton_ne // left_id.
Qed.
+ Global Instance discrete_fun_singleton_core_id x (y : B x) :
+ CoreId y → CoreId (discrete_fun_singleton x y).
+ Proof. rewrite /CoreId. intros Hy. by rewrite discrete_fun_singleton_op -Hy. Qed.
+
Lemma discrete_fun_insert_updateP x (P : B x → Prop) (Q : discrete_fun B → Prop) g y1 :
y1 ~~>: P → (∀ y2, P y2 → Q (discrete_fun_insert x y2 g)) →
discrete_fun_insert x y1 g ~~>: Q.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 65e1b83eb679da75f386f787d6617ed94cee4134..9ca7c439c7a219dac41d22b6acfad6a417c2d777 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -181,7 +181,6 @@ Implicit Types m : gmap K A.
Local Instance gmap_unit_instance : Unit (gmap K A) := (∅ : gmap K A).
Local Instance gmap_op_instance : Op (gmap K A) := merge op.
-Local Instance gmap_pcore_instance : PCore (gmap K A) := λ m, Some (omap pcore m).
Local Instance gmap_valid_instance : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
Local Instance gmap_validN_instance : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
@@ -189,8 +188,6 @@ Lemma gmap_op m1 m2 : m1 â‹… m2 = merge op m1 m2.
Proof. done. Qed.
Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
Proof. rewrite lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
-Lemma lookup_core m i : core m !! i = core (m !! i).
-Proof. by apply lookup_omap. Qed.
Lemma lookup_includedN n (m1 m2 : gmap K A) : m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
Proof.
@@ -229,9 +226,7 @@ Qed.
Lemma gmap_cmra_mixin : CmraMixin (gmap K A).
Proof.
apply cmra_total_mixin.
- - eauto.
- intros n m1 m2 m3 Hm i; by rewrite !lookup_op (Hm i).
- - intros n m1 m2 Hm i; by rewrite !lookup_core (Hm i).
- intros n m1 m2 Hm ? i; by rewrite -(Hm i).
- intros m; split.
+ by intros ? n i; apply cmra_valid_validN.
@@ -239,10 +234,6 @@ Proof.
- 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.
- - intros m i. by rewrite lookup_op lookup_core cmra_core_l.
- - intros m i. by rewrite !lookup_core cmra_core_idemp.
- - intros m1 m2; rewrite !lookup_included=> Hm i.
- rewrite !lookup_core. by apply cmra_core_mono.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- intros n m y1 y2 Hm Heq.
@@ -292,7 +283,6 @@ Proof.
split.
- by intros i; rewrite lookup_empty.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- - constructor=> i. by rewrite lookup_omap lookup_empty.
Qed.
Canonical Structure gmapUR := Ucmra (gmap K A) gmap_ucmra_mixin.
@@ -348,17 +338,6 @@ Proof.
- by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id_L.
Qed.
-Lemma singleton_core (i : K) (x : A) cx :
- pcore x = Some cx → core {[ i := x ]} =@{gmap K A} {[ i := cx ]}.
-Proof. apply omap_singleton_Some. Qed.
-Lemma singleton_core' (i : K) (x : A) cx :
- pcore x ≡ Some cx → core {[ i := x ]} ≡@{gmap K A} {[ i := cx ]}.
-Proof.
- intros (cx'&?&<-)%Some_equiv_eq. by rewrite (singleton_core _ _ cx').
-Qed.
-Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) :
- core {[ i := x ]} =@{gmap K A} {[ i := core x ]}.
-Proof. apply singleton_core. rewrite cmra_pcore_core //. Qed.
Lemma singleton_op (i : K) (x y : A) :
{[ i := x ]} â‹… {[ i := y ]} =@{gmap K A} {[ i := x â‹… y ]}.
Proof. by apply (merge_singleton _ _ _ x y). Qed.
@@ -368,16 +347,17 @@ Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -singleton_op. Qed.
Lemma gmap_core_id m : (∀ i x, m !! i = Some x → CoreId x) → CoreId m.
Proof.
- intros Hcore; apply core_id_total=> i.
- rewrite lookup_core. destruct (m !! i) as [x|] eqn:Hix; rewrite Hix; [|done].
- by eapply Hcore.
+ rewrite /CoreId=> Hx i.
+ rewrite lookup_op.
+ destruct (m !! i) as [x|] eqn:Hix; rewrite Hix; last done.
+ constructor. by eapply Hx.
Qed.
Global Instance gmap_core_id' m : (∀ x : A, CoreId x) → CoreId m.
Proof. auto using gmap_core_id. Qed.
Global Instance gmap_singleton_core_id i (x : A) :
CoreId x → CoreId {[ i := x ]}.
-Proof. intros. by apply core_id_total, singleton_core'. Qed.
+Proof. rewrite /CoreId. intros Hx. by rewrite singleton_op -Hx. Qed.
Lemma singleton_includedN_l n m i x :
{[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ Some x ≼{n} Some y.
@@ -754,8 +734,6 @@ Global Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmra} (f : A → B
Proof.
split; try apply _.
- by intros n m ? i; rewrite lookup_fmap; apply (cmra_morphism_validN _).
- - intros m. apply Some_proper=>i. rewrite lookup_fmap !lookup_omap lookup_fmap.
- case: (m!!i)=>//= ?. apply cmra_morphism_pcore, _.
- intros m1 m2 i. by rewrite lookup_op !lookup_fmap lookup_op cmra_morphism_op.
Qed.
Definition gmapO_map `{Countable K} {A B} (f: A -n> B) :
diff --git a/iris/algebra/gset.v b/iris/algebra/gset.v
index 7560008f195259ee00120c32cbae12a0188004eb..18d8b86118ba9b8d366a04fd9b5e8694bc1f89bd 100644
--- a/iris/algebra/gset.v
+++ b/iris/algebra/gset.v
@@ -13,12 +13,9 @@ Section gset.
Local Instance gset_valid_instance : Valid (gset K) := λ _, True.
Local Instance gset_unit_instance : Unit (gset K) := (∅ : gset K).
Local Instance gset_op_instance : Op (gset K) := union.
- Local Instance gset_pcore_instance : PCore (gset K) := λ X, Some X.
Lemma gset_op X Y : X ⋅ Y = X ∪ Y.
Proof. done. Qed.
- Lemma gset_core X : core X = X.
- Proof. done. Qed.
Lemma gset_included X Y : X ≼ Y ↔ X ⊆ Y.
Proof.
split.
@@ -29,7 +26,6 @@ Section gset.
Lemma gset_ra_mixin : RAMixin (gset K).
Proof.
apply ra_total_mixin; apply _ || eauto.
- - intros X. by rewrite gset_core idemp_L.
- intros X _.
exists X; split_and!; [exists X| |done]; by rewrite idemp.
Qed.
@@ -39,7 +35,7 @@ Section gset.
Proof. apply discrete_cmra_discrete. Qed.
Lemma gset_ucmra_mixin : UcmraMixin (gset K).
- Proof. split; [ done | | done ]. intros X. by rewrite gset_op left_id_L. Qed.
+ Proof. split; first done. intros X. by rewrite gset_op left_id_L. Qed.
Canonical Structure gsetUR := Ucmra (gset K) gset_ucmra_mixin.
Lemma gset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
@@ -56,7 +52,7 @@ Section gset.
Qed.
Global Instance gset_core_id X : CoreId X.
- Proof. by apply core_id_total; rewrite gset_core. Qed.
+ Proof. rewrite /CoreId gset_op. set_solver. Qed.
Lemma big_opS_singletons X :
([^op set] x ∈ X, {[ x ]}) = X.
@@ -103,7 +99,6 @@ Section gset_disj.
| GSet X, GSet Y => if decide (X ## Y) then GSet (X ∪ Y) else GSetBot
| _, _ => GSetBot
end.
- Local Instance gset_disj_pcore_instance : PCore (gset_disj K) := λ _, Some ε.
Ltac gset_disj_solve :=
repeat (simpl || case_decide);
@@ -127,13 +122,10 @@ Section gset_disj.
Proof.
apply ra_total_mixin; eauto.
- intros [?|]; destruct 1; gset_disj_solve.
- - by constructor.
- by destruct 1.
- intros [X1|] [X2|] [X3|]; gset_disj_solve.
- intros [X1|] [X2|]; gset_disj_solve.
- intros [X|]; gset_disj_solve.
- - exists (GSet ∅); gset_disj_solve.
- - intros [X1|] [X2|]; gset_disj_solve.
- intros [X|]=>// _.
exists (GSet ε); split_and! =>//.
+ exists (GSet X).
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index 7020038338a41eb94e958aa52af84b798310feda..a967c6880fd599f27187b9c6bf912861a6e8debf 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -34,7 +34,7 @@ Section mono_nat.
Proof.
rewrite /mono_nat_auth auth_auth_dfrac_op.
rewrite (comm _ (â—{dq2} _)) -!assoc (assoc _ (â—¯ _)).
- by rewrite -core_id_dup (comm _ (â—¯ _)).
+ by rewrite -core_id (comm _ (â—¯ _)).
Qed.
Lemma mono_nat_lb_op n1 n2 :
@@ -76,7 +76,7 @@ Section mono_nat.
rewrite /mono_nat_auth (comm _ (â—{dq2} _)) -!assoc (assoc _ (â—¯ _)).
rewrite -auth_frag_op (comm _ (â—¯ _)) assoc. split.
- move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
- - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
+ - intros [? ->]. rewrite -core_id -auth_auth_dfrac_op.
by apply auth_both_dfrac_valid_discrete.
Qed.
Lemma mono_nat_auth_op_valid n1 n2 :
diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index 638a33484a0c64f5f07ad29a61e196d98b8bf091..60c2b4289b8314d28b2e7469e91fedd367cd6d53 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -5,7 +5,6 @@ From iris.prelude Require Import options.
Section nat.
Local Instance nat_valid_instance : Valid nat := λ x, True.
Local Instance nat_validN_instance : ValidN nat := λ n x, True.
- Local Instance nat_pcore_instance : PCore nat := λ x, Some 0.
Local Instance nat_op_instance : Op nat := plus.
Definition nat_op x y : x â‹… y = x + y := eq_refl.
Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
@@ -16,7 +15,6 @@ Section nat.
- solve_proper.
- intros x y z. apply Nat.add_assoc.
- intros x y. apply Nat.add_comm.
- - by exists 0.
- intros x _.
exists 0; split_and! =>//.
{ by exists x. }
@@ -62,7 +60,6 @@ Section max_nat.
Local Instance max_nat_unit_instance : Unit max_nat := MaxNat 0.
Local Instance max_nat_valid_instance : Valid max_nat := λ x, True.
Local Instance max_nat_validN_instance : ValidN max_nat := λ n x, True.
- Local Instance max_nat_pcore_instance : PCore max_nat := Some.
Local Instance max_nat_op_instance : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
Definition max_nat_op x y : MaxNat x â‹… MaxNat y = MaxNat (x `max` y) := eq_refl.
@@ -77,7 +74,6 @@ Section max_nat.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite max_nat_op. by rewrite Nat.max_assoc.
- intros [x] [y]. by rewrite max_nat_op Nat.max_comm.
- - intros [x]. by rewrite max_nat_op Nat.max_id.
- intros [x] _.
exists (MaxNat x); split_and! =>//.
+ by apply max_nat_included.
@@ -93,7 +89,7 @@ Section max_nat.
Canonical Structure max_natUR : ucmra := Ucmra max_nat max_nat_ucmra_mixin.
Global Instance max_nat_core_id (x : max_nat) : CoreId x.
- Proof. by constructor. Qed.
+ Proof. destruct x as [n]. rewrite /CoreId /op /cmra_op /= /max_nat_op_instance /=. f_equal. lia. Qed.
Lemma max_nat_local_update (x y x' : max_nat) :
max_nat_car x ≤ max_nat_car x' → (x,y) ~l~> (x',x').
@@ -121,7 +117,6 @@ Canonical Structure min_natO := leibnizO min_nat.
Section min_nat.
Local Instance min_nat_valid_instance : Valid min_nat := λ x, True.
Local Instance min_nat_validN_instance : ValidN min_nat := λ n x, True.
- Local Instance min_nat_pcore_instance : PCore min_nat := Some.
Local Instance min_nat_op_instance : Op min_nat := λ n m, MinNat (min_nat_car n `min` min_nat_car m).
Definition min_nat_op_min x y : MinNat x â‹… MinNat y = MinNat (x `min` y) := eq_refl.
@@ -136,7 +131,6 @@ Section min_nat.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite min_nat_op_min. by rewrite Nat.min_assoc.
- intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
- - intros [x]. by rewrite min_nat_op_min Nat.min_id.
- intros [x] _.
exists (MinNat x); split_and! =>//.
+ by apply min_nat_included.
@@ -148,7 +142,7 @@ Section min_nat.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance min_nat_core_id (x : min_nat) : CoreId x.
- Proof. by constructor. Qed.
+ Proof. destruct x as [n]. rewrite /CoreId /op /cmra_op /= /min_nat_op_instance /=. f_equal. lia. Qed.
Lemma min_nat_local_update (x y x' : min_nat) :
min_nat_car x' ≤ min_nat_car x → (x,y) ~l~> (x',x').
@@ -177,7 +171,6 @@ End min_nat.
Section positive.
Local Instance pos_valid_instance : Valid positive := λ x, True.
Local Instance pos_validN_instance : ValidN positive := λ n x, True.
- Local Instance pos_pcore_instance : PCore positive := λ x, None.
Local Instance pos_op_instance : Op positive := Pos.add.
Definition pos_op_add x y : x â‹… y = (x + y)%positive := eq_refl.
Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
@@ -216,7 +209,6 @@ Section Z.
Local Open Scope Z_scope.
Local Instance Z_valid_instance : Valid Z := λ x, True.
Local Instance Z_validN_instance : ValidN Z := λ n x, True.
- Local Instance Z_pcore_instance : PCore Z := λ x, Some 0.
Local Instance Z_op_instance : Op Z := Z.add.
Definition Z_op x y : x â‹… y = x + y := eq_refl.
Lemma Z_ra_mixin : RAMixin Z.
@@ -225,7 +217,6 @@ Section Z.
- solve_proper.
- intros x y z. apply Z.add_assoc.
- intros x y. apply Z.add_comm.
- - by exists 0.
- intros x _.
exists 0; split_and! =>//.
+ exists x. by rewrite left_id.
@@ -273,7 +264,6 @@ Section max_Z.
Local Instance max_Z_unit_instance : Unit max_Z := MaxZ 0.
Local Instance max_Z_valid_instance : Valid max_Z := λ x, True.
Local Instance max_Z_validN_instance : ValidN max_Z := λ n x, True.
- Local Instance max_Z_pcore_instance : PCore max_Z := Some.
Local Instance max_Z_op_instance : Op max_Z := λ n m,
MaxZ (max_Z_car n `max` max_Z_car m).
Definition max_Z_op x y : MaxZ x â‹… MaxZ y = MaxZ (x `max` y) := eq_refl.
@@ -290,7 +280,6 @@ Section max_Z.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite max_Z_op. by rewrite Z.max_assoc.
- intros [x] [y]. by rewrite max_Z_op Z.max_comm.
- - intros [x]. by rewrite max_Z_op Z.max_id.
- intros [x] _.
exists (MaxZ x); split_and! =>//.
+ by apply max_Z_included.
@@ -299,13 +288,13 @@ Section max_Z.
Canonical Structure max_ZR : cmra := discreteR max_Z max_Z_ra_mixin.
Global Instance max_Z_cmra_total : CmraTotal max_ZR.
- Proof. intros x. eauto. Qed.
+ Proof. intros [x]. exists (MaxZ x). rewrite max_Z_included max_Z_op. split=>//=. f_equal. lia. Qed.
Global Instance max_Z_cmra_discrete : CmraDiscrete max_ZR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance max_Z_core_id (x : max_Z) : CoreId x.
- Proof. by constructor. Qed.
+ Proof. destruct x as [x]. rewrite /CoreId max_Z_op. f_equal. lia. Qed.
Lemma max_Z_local_update (x y x' : max_Z) :
max_Z_car x ≤ max_Z_car x' → (x,y) ~l~> (x',x').
diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index 05ca50a3c146ce938807f6d4ab83b8f99c863807..0595a5ad01b7e6c3ab53324189f23eeb3c43ea74 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -53,10 +53,10 @@ Global Instance is_op_pair {A B : cmra} (a b1 b2 : A) (a' b1' b2' : B) :
Proof. by constructor. Qed.
Global Instance is_op_pair_core_id_l {A B : cmra} (a : A) (a' b1' b2' : B) :
CoreId a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
-Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
+Proof. constructor=> //=. Qed.
Global Instance is_op_pair_core_id_r {A B : cmra} (a b1 b2 : A) (a' : B) :
CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
-Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
+Proof. constructor=> //=. Qed.
Global Instance is_op_Some {A : cmra} (a : A) b1 b2 :
IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
diff --git a/iris/algebra/reservation_map.v b/iris/algebra/reservation_map.v
index d616b974018bc208e842f34555b9b86ba94703e8..b064bd90c9c6568ef563d930fab8a99a97ef3674 100644
--- a/iris/algebra/reservation_map.v
+++ b/iris/algebra/reservation_map.v
@@ -118,8 +118,6 @@ Section cmra.
| CoPsetBot => False
end.
Global Arguments reservation_map_validN_instance !_ /.
- Local Instance reservation_map_pcore_instance : PCore (reservation_map A) := λ x,
- Some (ReservationMap (core (reservation_map_data_proj x)) ε).
Local Instance reservation_map_op_instance : Op (reservation_map A) := λ x y,
ReservationMap (reservation_map_data_proj x â‹… reservation_map_data_proj y)
(reservation_map_token_proj x â‹… reservation_map_token_proj y).
@@ -166,9 +164,7 @@ Section cmra.
Lemma reservation_map_cmra_mixin : CmraMixin (reservation_map A).
Proof.
apply cmra_total_mixin.
- - eauto.
- by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- - solve_proper.
- intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[??]; split; simplify_eq/=.
+ by rewrite -Hm.
+ intros i. by rewrite -(dist_None n) -Hm dist_None.
@@ -178,10 +174,6 @@ Section cmra.
naive_solver eauto using cmra_validN_S.
- split; simpl; [by rewrite assoc|by rewrite assoc_L].
- split; simpl; [by rewrite comm|by rewrite comm_L].
- - split; simpl; [by rewrite cmra_core_l|by rewrite left_id_L].
- - split; simpl; [by rewrite cmra_core_idemp|done].
- - intros ??; rewrite! reservation_map_included; intros [??].
- by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
- intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite reservation_map_validN_eq /=.
rewrite {1}/op /cmra_op /=. case_decide; last done.
intros [Hm Hdisj]; split; first by eauto using cmra_validN_op_l.
@@ -224,14 +216,13 @@ Section cmra.
split; simpl.
- rewrite reservation_map_valid_eq /=. split; [apply ucmra_unit_valid|]. set_solver.
- split; simpl; [by rewrite left_id|by rewrite left_id_L].
- - do 2 constructor; [apply (core_id_core _)|done].
Qed.
Canonical Structure reservation_mapUR :=
Ucmra (reservation_map A) reservation_map_ucmra_mixin.
Global Instance reservation_map_data_core_id k a :
CoreId a → CoreId (reservation_map_data k a).
- Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
+ Proof. constructor; [apply core_id, _ | apply core_id_L, _]. Qed.
Lemma reservation_map_data_valid k a : ✓ (reservation_map_data k a) ↔ ✓ a.
Proof. rewrite reservation_map_valid_eq /= singleton_valid. set_solver. Qed.
diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index 066d602ccf5de3b4cc9b266ef62323dacb49ff39..d8bb08129ea76fce6fa8d21e6415d46eef397819 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -125,8 +125,11 @@ Lemma cmra_total_updateP `{!CmraTotal A} x (P : A → Prop) :
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.
+ destruct (cmra_total x) as (cx&[z Hx]&Hcx).
+ destruct (Hup n cx) as (y&?&?).
+ - by rewrite Hx (comm _ _ cx) assoc -Hcx -Hx.
+ - exists y; split; first done.
+ by eapply cmra_validN_op_l.
Qed.
Lemma cmra_total_update `{!CmraTotal A} x y :
x ~~> y ↔ ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 93026bb89accc7fc1fd91cbab3a3cdc02f87c8dc..ef5e7b13f0f9869f86decc979de9bac005ef5a6d 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -187,8 +187,6 @@ Section cmra.
✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
| None => ∃ a, rel n a (view_frag_proj x)
end.
- Local Instance view_pcore_instance : PCore (view rel) := λ x,
- Some (View (core (view_auth_proj x)) (core (view_frag_proj x))).
Local Instance view_op_instance : Op (view rel) := λ x y,
View (view_auth_proj x â‹… view_auth_proj y) (view_frag_proj x â‹… view_frag_proj y).
@@ -205,12 +203,6 @@ Section cmra.
| Some (dq, ag) => ✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
| None => ∃ a, rel n a (view_frag_proj x)
end := eq_refl _.
- Local Definition view_pcore_eq :
- pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x))) :=
- eq_refl _.
- Local Definition view_core_eq :
- core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x)) :=
- eq_refl _.
Local Definition view_op_eq :
op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y)
(view_frag_proj x â‹… view_frag_proj y) :=
@@ -221,7 +213,6 @@ Section cmra.
apply (iso_cmra_mixin_restrict_validity
(λ x : option (dfrac * agree A) * B, View x.1 x.2)
(λ x, (view_auth_proj x, view_frag_proj x))); try done.
- - intros [x b]. by rewrite /= pair_pcore !cmra_pcore_core.
- intros n [[[dq ag]|] b]; rewrite /= view_validN_eq /=.
+ intros (?&a&->&?). repeat split; simpl; [done|]. by eapply view_rel_validN.
+ intros [a ?]. repeat split; simpl. by eapply view_rel_validN.
@@ -271,7 +262,6 @@ Section cmra.
split; simpl.
- rewrite view_valid_eq /=. apply view_rel_unit.
- by intros x; constructor; rewrite /= left_id.
- - do 2 constructor; [done| apply (core_id_core _)].
Qed.
Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.
@@ -289,21 +279,15 @@ Section cmra.
Proof. done. Qed.
Lemma view_frag_mono b1 b2 : b1 ≼ b2 → ◯V b1 ≼ ◯V b2.
Proof. intros [c ->]. by rewrite view_frag_op. Qed.
- Lemma view_frag_core b : core (â—¯V b) = â—¯V (core b).
- Proof. done. Qed.
- Lemma view_both_core_discarded a b :
- core (â—Vâ–¡ a â‹… â—¯V b) ≡ â—Vâ–¡ a â‹… â—¯V (core b).
- Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
- Lemma view_both_core_frac q a b :
- core (â—V{#q} a â‹… â—¯V b) ≡ â—¯V (core b).
- Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
Global Instance view_auth_core_id a : CoreId (â—Vâ–¡ a).
- Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
+ Proof.
+ constructor; simpl; last by rewrite left_id.
+ do 2 constructor; simpl; first done.
+ by rewrite agree_idemp.
+ Qed.
Global Instance view_frag_core_id b : CoreId b → CoreId (◯V b).
- Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
- Global Instance view_both_core_id a b : CoreId b → CoreId (â—Vâ–¡ a â‹… â—¯V b).
- Proof. do 2 constructor; simpl; auto. rewrite !left_id. apply: core_id_core. Qed.
+ Proof. by constructor. Qed.
Global Instance view_frag_is_op b b1 b2 :
IsOp b b1 b2 → IsOp' (◯V b) (◯V b1) (◯V b2).
Proof. done. Qed.
@@ -680,8 +664,6 @@ Proof.
[|naive_solver eauto using cmra_morphism_validN].
intros [? [a' [Hag ?]]]. split; [done|]. exists (f a'). split; [|by auto].
by rewrite -agree_map_to_agree -Hag.
- - intros [o bf]. apply Some_proper; rewrite /view_map /=.
- f_equiv; by rewrite cmra_morphism_core.
- intros [[[dq1 ag1]|] bf1] [[[dq2 ag2]|] bf2];
try apply View_proper=> //=; by rewrite cmra_morphism_op.
Qed.
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 9077f0feb05865932ba6914c42b082342d73346c..b1c30a8683a14bf01d0e370d554d4eafbe3e974a 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -209,7 +209,7 @@ Section restate.
Lemma ownM_op (a1 a2 : M) :
uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
Proof. exact: uPred_primitive.ownM_op. Qed.
- Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
+ Lemma persistently_ownM_core (a : M) : uPred_ownM a ∧ a ⋅ a ≡ a ⊢ <pers> uPred_ownM a.
Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
Proof. exact: uPred_primitive.ownM_unit. Qed.
diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index 335bd5a534be02e894f32323f1c90b7e1e718078..664c4c7d5096b184366c4851951e18277845f858 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -30,7 +30,9 @@ Section derived.
Proof.
rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
[by rewrite persistently_elim|].
- by rewrite {1}persistently_ownM_core core_id_core.
+ rewrite -persistently_ownM_core -core_id.
+ apply and_intro; first done.
+ apply internal_eq_refl.
Qed.
Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
Proof. intros. rewrite ownM_valid cmra_valid_elim. by apply pure_elim'. Qed.
@@ -83,7 +85,7 @@ Section derived.
Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
Proof.
- intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
+ intros. rewrite -intuitionistically_ownM. apply _.
Qed.
(** For big ops *)
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 121576384336e66e63379f4d946b5f62f0cd839f..2c00d50290efcbb26db2b38313b7be7e5fb3fcae 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -131,7 +131,7 @@ Local Instance iRes_singleton_core_id γ a :
CoreId a → CoreId (iRes_singleton γ a).
Proof.
intros. apply discrete_fun_singleton_core_id, gmap_singleton_core_id.
- by rewrite /CoreId -cmra_morphism_pcore core_id.
+ by rewrite /CoreId -cmra_morphism_op -cmra_transport_op -core_id.
Qed.
Local Lemma later_internal_eq_iRes_singleton γ a r :
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index a8da44d40f208a71f3b0a94beaab6d71df0e5157..6bb231e6da9c8786c39722be97ee2f1d4cef8bf4 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -282,7 +282,7 @@ Local Definition uPred_or_unseal :
Local Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ n' x',
- x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}.
+ x ≼{n'} x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}.
Next Obligation.
intros M P Q n1 n1' x1 x1' HPQ [x2 Hx1'] Hn1 n2 x3 [x4 Hx3] ?; simpl in *.
rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
@@ -362,8 +362,15 @@ Local Definition uPred_plainly_unseal :
@uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
Local Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
- {| uPred_holds n x := P n (core x) |}.
-Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
+ {| uPred_holds n x := ∃ y, y ≼{n} x ∧ y ≡{n}≡ y ⋅ y ∧ P n y |}.
+Next Obligation.
+ intros M P n1 n2 x1 x2 (y & ? & Hy & HP) ??.
+ exists y; split_and!.
+ - trans x1; last done.
+ by eapply cmra_includedN_le.
+ - by eapply dist_le.
+ - by eapply uPred_mono.
+Qed.
Local Definition uPred_persistently_aux : seal (@uPred_persistently_def).
Proof. by eexists. Qed.
Definition uPred_persistently := uPred_persistently_aux.(unseal).
@@ -565,7 +572,8 @@ Section primitive.
Lemma persistently_ne : NonExpansive (@uPred_persistently M).
Proof.
intros n P1 P2 HP.
- unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
+ unseal; split=> n' x ?? /=; f_equiv=> y.
+ split; intros (?&?&?); split_and! =>//; apply HP=>//; by eapply cmra_validN_includedN.
Qed.
Lemma ownM_ne : NonExpansive (@uPred_ownM M).
@@ -642,7 +650,7 @@ Section primitive.
Qed.
Lemma True_sep_1 P : P ⊢ True ∗ P.
Proof.
- unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l.
+ unseal; split; intros n x ??. exists ε, x. by rewrite left_id.
Qed.
Lemma True_sep_2 P : True ∗ P ⊢ P.
Proof.
@@ -674,31 +682,57 @@ Section primitive.
(** Persistently *)
Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
- Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
+ Proof.
+ intros HP; unseal; split=> n x ? /= -[y [? [??]]].
+ exists y; split_and! =>//.
+ apply HP=>//.
+ by eapply cmra_validN_includedN.
+ Qed.
Lemma persistently_elim P : □ P ⊢ P.
Proof.
- unseal; split=> n x ? /=.
- eauto using uPred_mono, cmra_included_core, cmra_included_includedN.
+ unseal; split=> n x ? /= -[y [? [??]]].
+ by eapply uPred_mono.
Qed.
Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
- Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
+ Proof.
+ unseal; split=> n x ? -[y [? [??]]] /=.
+ exists y; split_and! =>//.
+ by exists y.
+ Qed.
Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
- Proof. by unseal. Qed.
+ Proof.
+ unseal; split=> n x ? /= HΨ.
+ destruct (cmra_maximum_idemp_total n x) as (y & ? & ? & Hy); first done.
+ exists y; split_and! =>// a.
+ destruct (HΨ a) as (z & ? & ? & ?).
+ eapply uPred_mono=>//.
+ by apply Hy.
+ Qed.
Lemma persistently_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
- Proof. by unseal. Qed.
+ Proof.
+ unseal; split; intros n x ? (y & ? & ? & a & ?).
+ by exists a, y.
+ Qed.
Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ P ∗ Q.
Proof.
- unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
- by rewrite cmra_core_l.
+ unseal; split; intros n x ? [(y & [z Hx] & Hy & ?) ?].
+ exists y, x; split; last done.
+ by rewrite Hx assoc -Hy.
Qed.
(** Plainly *)
Lemma plainly_mono P Q : (P ⊢ Q) → ■P ⊢ ■Q.
Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed.
Lemma plainly_elim_persistently P : ■P ⊢ □ P.
- Proof. unseal; split; simpl; eauto using uPred_mono, ucmra_unit_leastN. Qed.
+ Proof.
+ unseal; split=> n x ? HP.
+ exists ε; split_and!.
+ - apply ucmra_unit_leastN.
+ - by rewrite right_id.
+ - done.
+ Qed.
Lemma plainly_idemp_2 P : ■P ⊢ ■■P.
Proof. unseal; split=> n x ?? //. Qed.
@@ -716,15 +750,20 @@ Section primitive.
and ■, but for any modality defined as `M P n x := ∀ y, R x y → P n y`. *)
Lemma persistently_impl_plainly P Q : (■P → □ Q) ⊢ □ (■P → Q).
Proof.
- unseal; split=> /= n x ? HPQ n' x' ????.
- eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
- apply (HPQ n' x); eauto using cmra_validN_le.
+ unseal; split=> /= n x ? HPQ.
+ destruct (cmra_maximum_idemp_total n x) as (y & ? & ? & Hy); first done.
+ exists y; split_and! =>// n' x' ????.
+ destruct (HPQ n' x) as (z & ? & ? & ?)=>//.
+ { by eapply cmra_validN_le. }
+ eapply uPred_mono=>//.
+ trans y; last done.
+ by apply Hy.
Qed.
Lemma plainly_impl_plainly P Q : (■P → ■Q) ⊢ ■(■P → Q).
Proof.
unseal; split=> /= n x ? HPQ n' x' ????.
- eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
+ eapply uPred_mono with n' ε=>//.
apply (HPQ n' x); eauto using cmra_validN_le.
Qed.
@@ -747,7 +786,7 @@ Section primitive.
Proof.
unseal; split=> n x ?.
destruct n as [|n]; simpl.
- { by exists x, (core x); rewrite cmra_core_r. }
+ { exists ε, x. by rewrite left_id. }
intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
@@ -766,9 +805,26 @@ Section primitive.
Qed.
Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P.
- Proof. by unseal. Qed.
+ Proof.
+ unseal; split=> /= -[|n] x ?.
+ - intros _. exists ε; split_and!.
+ + apply ucmra_unit_leastN.
+ + by rewrite right_id.
+ + done.
+ - intros (y & ? & ? & ?).
+ destruct (cmra_maximum_idemp_total (S n) x) as (z&?&?&Hz)=>//.
+ exists z; split_and! =>//.
+ eapply uPred_mono=>//.
+ apply Hz=>//. lia.
+ Qed.
Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
- Proof. by unseal. Qed.
+ Proof.
+ unseal; split; intros [|n] x ? (y & ? & ? & ?)=>//=.
+ exists y; split_and!.
+ - by apply cmra_includedN_S.
+ - by apply dist_S.
+ - done.
+ Qed.
Lemma later_plainly_1 P : ▷ ■P ⊢ ■▷ P.
Proof. by unseal. Qed.
Lemma later_plainly_2 P : ■▷ P ⊢ ▷ ■P.
@@ -852,16 +908,16 @@ Section primitive.
Proof.
unseal; split=> n x ?; split.
- intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
- split.
- + by exists (core a1); rewrite cmra_core_r.
+ split=>/=.
+ + done.
+ by exists z.
- intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
- Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
+ Lemma persistently_ownM_core (a : M) : uPred_ownM a ∧ a ⋅ a ≡ a ⊢ □ uPred_ownM a.
Proof.
- split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
+ unseal; split=> n x /= ? [??]. by exists a.
Qed.
Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
diff --git a/iris/bi/lib/cmra.v b/iris/bi/lib/cmra.v
index 65fca318a02bc042656e7618ea54ab226a2102dd..65cb14e126557a85c919d0f2d6461433dd4a7924 100644
--- a/iris/bi/lib/cmra.v
+++ b/iris/bi/lib/cmra.v
@@ -56,7 +56,11 @@ Section internal_included_laws.
Proof. rewrite /internal_included. apply _. Qed.
Lemma internal_included_refl `{!CmraTotal A} (x : A) : ⊢@{PROP} x ≼ x.
- Proof. iExists (core x). by rewrite cmra_core_r. Qed.
+ Proof.
+ destruct (cmra_total x) as (c & [y Hx] & Hc).
+ iExists c.
+ by rewrite Hx (comm _ _ c) assoc -Hc.
+ Qed.
Lemma internal_included_trans {A} (x y z : A) :
⊢@{PROP} x ≼ y -∗ y ≼ z -∗ x ≼ z.
Proof.