From 69d67c60ffd5c084348e9d0e4a15bb8f63525092 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 27 May 2016 14:51:17 +0200
Subject: [PATCH] Introduce a canonical structure for CMRAs with a unit
element.
---
algebra/auth.v | 50 +++----
algebra/cmra.v | 241 +++++++++++++++++++++++---------
algebra/cmra_big_op.v | 17 +--
algebra/cmra_tactics.v | 6 +-
algebra/cofe.v | 4 +-
algebra/excl.v | 29 ++--
algebra/frac.v | 33 +++--
algebra/gmap.v | 71 ++++++----
algebra/iprod.v | 164 +++++++++++-----------
algebra/list.v | 142 ++++++++++---------
algebra/one_shot.v | 46 ++++--
algebra/upred.v | 47 +++----
algebra/upred_big_op.v | 2 +-
algebra/upred_tactics.v | 4 +-
heap_lang/heap.v | 18 +--
heap_lang/proofmode.v | 2 +-
program_logic/auth.v | 9 +-
program_logic/ghost_ownership.v | 31 ++--
program_logic/global_functor.v | 2 +-
program_logic/model.v | 27 ++--
program_logic/ownership.v | 8 +-
program_logic/resources.v | 62 ++++----
program_logic/viewshifts.v | 4 +-
proofmode/coq_tactics.v | 4 +-
tests/proofmode.v | 14 +-
25 files changed, 594 insertions(+), 443 deletions(-)
diff --git a/algebra/auth.v b/algebra/auth.v
index a1ffd49f3..21012546f 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -66,11 +66,10 @@ Arguments authC : clear implicits.
(* CMRA *)
Section cmra.
-Context {A : cmraT}.
+Context {A : ucmraT}.
Implicit Types a b : A.
Implicit Types x y : auth A.
-Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
Instance auth_valid : Valid (auth A) := λ x,
match authoritative x with
| Excl a => (∀ n, own x ≼{n} a) ∧ ✓ a
@@ -101,7 +100,7 @@ Proof. by destruct x as [[]]. Qed.
Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} own x.
Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
-Definition auth_cmra_mixin : CMRAMixin (auth A).
+Lemma auth_cmra_mixin : CMRAMixin (auth A).
Proof.
split.
- by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
@@ -128,7 +127,7 @@ Proof.
as (b&?&?&?); auto using own_validN.
by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
Qed.
-Canonical Structure authR : cmraT :=
+Canonical Structure authR :=
CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
Proof.
@@ -139,6 +138,17 @@ Proof.
- by rewrite -cmra_discrete_valid_iff.
Qed.
+Instance auth_empty : Empty (auth A) := Auth ∅ ∅.
+Lemma auth_ucmra_mixin : UCMRAMixin (auth A).
+Proof.
+ split; simpl.
+ - apply (@ucmra_unit_valid A).
+ - by intros x; constructor; rewrite /= left_id.
+ - apply _.
+Qed.
+Canonical Structure authUR :=
+ UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
+
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
(x ≡ y) ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M).
@@ -151,17 +161,6 @@ Lemma auth_validI {M} (x : auth A) :
end : uPred M).
Proof. uPred.unseal. by destruct x as [[]]. Qed.
-(** The notations â—¯ and â— only work for CMRAs with an empty element. So, in
-what follows, we assume we have an empty element. *)
-Context `{Empty A, !CMRAUnit A}.
-
-Global Instance auth_cmra_unit : CMRAUnit authR.
-Proof.
- split; simpl.
- - by apply (@cmra_unit_valid A _).
- - by intros x; constructor; rewrite /= left_id.
- - apply _.
-Qed.
Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed.
Lemma auth_both_op a b : Auth (Excl a) b ≡ ◠a ⋅ ◯ b.
@@ -206,6 +205,7 @@ Qed.
End cmra.
Arguments authR : clear implicits.
+Arguments authUR : clear implicits.
(* Functor *)
Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
@@ -223,7 +223,7 @@ Instance auth_map_cmra_ne {A B : cofeT} n :
Proof.
intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf].
Qed.
-Instance auth_map_cmra_monotone {A B : cmraT} (f : A → B) :
+Instance auth_map_cmra_monotone {A B : ucmraT} (f : A → B) :
CMRAMonotone f → CMRAMonotone (auth_map f).
Proof.
split; try apply _.
@@ -237,24 +237,24 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.
-Program Definition authRF (F : rFunctor) : rFunctor := {|
- rFunctor_car A B := authR (rFunctor_car F A B);
- rFunctor_map A1 A2 B1 B2 fg := authC_map (rFunctor_map F fg)
+Program Definition authURF (F : urFunctor) : urFunctor := {|
+ urFunctor_car A B := authUR (urFunctor_car F A B);
+ urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
|}.
Next Obligation.
- by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_ne.
+ by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(auth_map_id x).
- apply auth_map_ext=>y; apply rFunctor_id.
+ apply auth_map_ext=>y; apply urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
- apply auth_map_ext=>y; apply rFunctor_compose.
+ apply auth_map_ext=>y; apply urFunctor_compose.
Qed.
-Instance authRF_contractive F :
- rFunctorContractive F → rFunctorContractive (authRF F).
+Instance authURF_contractive F :
+ urFunctorContractive F → urFunctorContractive (authURF F).
Proof.
- by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_contractive.
+ by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
Qed.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 7ebdfca0b..e15086715 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -113,12 +113,57 @@ End cmra_mixin.
(** * CMRAs with a unit element *)
(** We use the notation ∅ because for most instances (maps, sets, etc) the
`empty' element is the unit. *)
-Class CMRAUnit (A : cmraT) `{Empty A} := {
- cmra_unit_valid : ✓ ∅;
- cmra_unit_left_id :> LeftId (≡) ∅ (⋅);
- cmra_unit_timeless :> Timeless ∅
+Record UCMRAMixin A `{Dist A, Equiv A, Op A, Valid A, Empty A} := {
+ mixin_ucmra_unit_valid : ✓ ∅;
+ mixin_ucmra_unit_left_id : LeftId (≡) ∅ (⋅);
+ mixin_ucmra_unit_timeless : Timeless ∅
}.
-Instance cmra_unit_inhabited `{CMRAUnit A} : Inhabited A := populate ∅.
+
+Structure ucmraT := UCMRAT {
+ ucmra_car :> Type;
+ ucmra_equiv : Equiv ucmra_car;
+ ucmra_dist : Dist ucmra_car;
+ ucmra_compl : Compl ucmra_car;
+ ucmra_core : Core ucmra_car;
+ ucmra_op : Op ucmra_car;
+ ucmra_valid : Valid ucmra_car;
+ ucmra_validN : ValidN ucmra_car;
+ ucmra_empty : Empty ucmra_car;
+ ucmra_cofe_mixin : CofeMixin ucmra_car;
+ ucmra_cmra_mixin : CMRAMixin ucmra_car;
+ ucmra_mixin : UCMRAMixin ucmra_car
+}.
+Arguments UCMRAT _ {_ _ _ _ _ _ _ _} _ _ _.
+Arguments ucmra_car : simpl never.
+Arguments ucmra_equiv : simpl never.
+Arguments ucmra_dist : simpl never.
+Arguments ucmra_compl : simpl never.
+Arguments ucmra_core : simpl never.
+Arguments ucmra_op : simpl never.
+Arguments ucmra_valid : simpl never.
+Arguments ucmra_validN : simpl never.
+Arguments ucmra_cofe_mixin : simpl never.
+Arguments ucmra_cmra_mixin : simpl never.
+Arguments ucmra_mixin : simpl never.
+Add Printing Constructor ucmraT.
+Existing Instances ucmra_empty.
+Coercion ucmra_cofeC (A : ucmraT) : cofeT := CofeT A (ucmra_cofe_mixin A).
+Canonical Structure ucmra_cofeC.
+Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
+ CMRAT A (ucmra_cofe_mixin A) (ucmra_cmra_mixin A).
+Canonical Structure ucmra_cmraR.
+
+(** Lifting properties from the mixin *)
+Section ucmra_mixin.
+ Context {A : ucmraT}.
+ Implicit Types x y : A.
+ Lemma ucmra_unit_valid : ✓ (∅ : A).
+ 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.
+ Global Instance ucmra_unit_timeless : Timeless (∅ : A).
+ Proof. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed.
+End ucmra_mixin.
(** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : core x ≡ x.
@@ -331,23 +376,6 @@ Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
(∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y.
Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
-(** ** RAs with a unit element *)
-Section unit.
- Context `{Empty A, !CMRAUnit A}.
- Lemma cmra_unit_validN n : ✓{n} ∅.
- Proof. apply cmra_valid_validN, cmra_unit_valid. Qed.
- Lemma cmra_unit_leastN n x : ∅ ≼{n} x.
- Proof. by exists x; rewrite left_id. Qed.
- Lemma cmra_unit_least x : ∅ ≼ x.
- Proof. by exists x; rewrite left_id. Qed.
- Global Instance cmra_unit_right_id : RightId (≡) ∅ (⋅).
- Proof. by intros x; rewrite (comm op) left_id. Qed.
- Global Instance cmra_unit_persistent : Persistent ∅.
- Proof. by rewrite /Persistent -{2}(cmra_core_l ∅) right_id. Qed.
- Lemma cmra_core_unit : core (∅:A) ≡ ∅.
- Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed.
-End unit.
-
(** ** Local updates *)
Global Instance local_update_proper Lv (L : A → A) :
LocalUpdate Lv L → Proper ((≡) ==> (≡)) L.
@@ -407,16 +435,34 @@ Proof.
Qed.
Lemma cmra_update_id x : x ~~> x.
Proof. intro. auto. Qed.
-
-Section unit_updates.
- Context `{Empty A, !CMRAUnit A}.
- Lemma cmra_update_unit x : x ~~> ∅.
- Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
- Lemma cmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
- Proof. split; [intros; trans ∅|]; auto using cmra_update_unit. Qed.
-End unit_updates.
End cmra.
+(** * Properties about CMRAs with a unit element **)
+Section ucmra.
+Context {A : ucmraT}.
+Implicit Types x y z : A.
+
+Global Instance ucmra_unit_inhabited : Inhabited A := populate ∅.
+
+Lemma ucmra_unit_validN n : ✓{n} (∅:A).
+Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
+Lemma ucmra_unit_leastN n x : ∅ ≼{n} x.
+Proof. by exists x; rewrite left_id. Qed.
+Lemma ucmra_unit_least x : ∅ ≼ x.
+Proof. by exists x; rewrite left_id. Qed.
+Global Instance ucmra_unit_right_id : RightId (≡) ∅ (@op A _).
+Proof. by intros x; rewrite (comm op) left_id. Qed.
+Global Instance ucmra_unit_persistent : Persistent (∅:A).
+Proof. by rewrite /Persistent -{2}(cmra_core_l ∅) right_id. Qed.
+Lemma ucmra_core_unit : core (∅:A) ≡ ∅.
+Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed.
+
+Lemma ucmra_update_unit x : x ~~> ∅.
+Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
+Lemma ucmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
+Proof. split; [intros; trans ∅|]; auto using ucmra_update_unit. Qed.
+End ucmra.
+
(** * Properties about monotone functions *)
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Proof. repeat split; by try apply _. Qed.
@@ -471,6 +517,35 @@ Solve Obligations with done.
Instance constRF_contractive B : rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed.
+Structure urFunctor := URFunctor {
+ urFunctor_car : cofeT → cofeT → ucmraT;
+ urFunctor_map {A1 A2 B1 B2} :
+ ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
+ urFunctor_ne A1 A2 B1 B2 n :
+ Proper (dist n ==> dist n) (@urFunctor_map A1 A2 B1 B2);
+ urFunctor_id {A B} (x : urFunctor_car A B) : urFunctor_map (cid,cid) x ≡ x;
+ urFunctor_compose {A1 A2 A3 B1 B2 B3}
+ (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
+ urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
+ urFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
+ CMRAMonotone (urFunctor_map fg)
+}.
+Existing Instances urFunctor_ne urFunctor_mono.
+Instance: Params (@urFunctor_map) 5.
+
+Class urFunctorContractive (F : urFunctor) :=
+ urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
+
+Definition urFunctor_diag (F: urFunctor) (A: cofeT) : ucmraT := urFunctor_car F A A.
+Coercion urFunctor_diag : urFunctor >-> Funclass.
+
+Program Definition constURF (B : ucmraT) : urFunctor :=
+ {| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}.
+Solve Obligations with done.
+
+Instance constURF_contractive B : urFunctorContractive (constURF B).
+Proof. rewrite /urFunctorContractive; apply _. Qed.
+
(** * Transporting a CMRA equality *)
Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
eq_rect A id x _ H.
@@ -547,11 +622,17 @@ Section unit.
Instance unit_validN : ValidN () := λ n x, True.
Instance unit_core : Core () := λ x, x.
Instance unit_op : Op () := λ x y, ().
- Global Instance unit_empty : Empty () := ().
- Definition unit_cmra_mixin : CMRAMixin ().
+
+ Lemma unit_cmra_mixin : CMRAMixin ().
Proof. by split; last exists ((),()). Qed.
Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
- Global Instance unit_cmra_unit : CMRAUnit unitR.
+
+ Instance unit_empty : Empty () := ().
+ Lemma unit_ucmra_mixin : UCMRAMixin ().
+ Proof. done. Qed.
+ Canonical Structure unitUR : ucmraT :=
+ UCMRAT () unit_cofe_mixin unit_cmra_mixin unit_ucmra_mixin.
+
Global Instance unit_cmra_discrete : CMRADiscrete unitR.
Proof. done. Qed.
Global Instance unit_persistent (x : ()) : Persistent x.
@@ -562,10 +643,10 @@ End unit.
Section prod.
Context {A B : cmraT}.
Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
- Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)).
Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
+
Lemma prod_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|].
@@ -576,6 +657,7 @@ Section prod.
split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
Qed.
+
Definition prod_cmra_mixin : CMRAMixin (A * B).
Proof.
split; try apply _.
@@ -598,16 +680,9 @@ Section prod.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
by exists ((z1.1,z2.1),(z1.2,z2.2)).
Qed.
- Canonical Structure prodR : cmraT :=
+ Canonical Structure prodR :=
CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
- Global Instance prod_cmra_unit `{Empty A, Empty B} :
- CMRAUnit A → CMRAUnit B → CMRAUnit prodR.
- Proof.
- split.
- - split; apply cmra_unit_valid.
- - by split; rewrite /=left_id.
- - by intros ? [??]; split; apply (timeless _).
- Qed.
+
Global Instance prod_cmra_discrete :
CMRADiscrete A → CMRADiscrete B → CMRADiscrete prodR.
Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
@@ -616,10 +691,6 @@ Section prod.
Persistent x → Persistent y → Persistent (x,y).
Proof. by split. Qed.
- Lemma pair_split `{CMRAUnit A, CMRAUnit B} (x : A) (y : B) :
- (x, y) ≡ (x, ∅) ⋅ (∅, y).
- Proof. constructor; by rewrite /= ?left_id ?right_id. Qed.
-
Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
@@ -646,6 +717,26 @@ End prod.
Arguments prodR : clear implicits.
+Section prod_unit.
+ Context {A B : ucmraT}.
+
+ Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
+ Lemma prod_ucmra_mixin : UCMRAMixin (A * B).
+ Proof.
+ split.
+ - split; apply ucmra_unit_valid.
+ - by split; rewrite /=left_id.
+ - by intros ? [??]; split; apply (timeless _).
+ Qed.
+ Canonical Structure prodUR :=
+ UCMRAT (A * B) prod_cofe_mixin prod_cmra_mixin prod_ucmra_mixin.
+
+ Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y).
+ Proof. constructor; by rewrite /= ?left_id ?right_id. Qed.
+End prod_unit.
+
+Arguments prodUR : clear implicits.
+
Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B') :
CMRAMonotone f → CMRAMonotone g → CMRAMonotone (prod_map f g).
Proof.
@@ -654,13 +745,14 @@ Proof.
- intros x y; rewrite !prod_included=> -[??] /=.
by split; apply included_preserving.
Qed.
+
Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
rFunctor_map A1 A2 B1 B2 fg :=
prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
|}.
Next Obligation.
- intros F1 F2 A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply rFunctor_ne.
+ intros F1 F2 A1 A2 B1 B2 n ???. by apply prodC_map_ne; apply rFunctor_ne.
Qed.
Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed.
Next Obligation.
@@ -676,6 +768,28 @@ Proof.
by apply prodC_map_ne; apply rFunctor_contractive.
Qed.
+Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
+ urFunctor_car A B := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
+ urFunctor_map A1 A2 B1 B2 fg :=
+ prodC_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
+|}.
+Next Obligation.
+ intros F1 F2 A1 A2 B1 B2 n ???. by apply prodC_map_ne; apply urFunctor_ne.
+Qed.
+Next Obligation. by intros F1 F2 A B [??]; rewrite /= !urFunctor_id. Qed.
+Next Obligation.
+ intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
+ by rewrite !urFunctor_compose.
+Qed.
+
+Instance prodURF_contractive F1 F2 :
+ urFunctorContractive F1 → urFunctorContractive F2 →
+ urFunctorContractive (prodURF F1 F2).
+Proof.
+ intros ?? A1 A2 B1 B2 n ???;
+ by apply prodC_map_ne; apply urFunctor_contractive.
+Qed.
+
(** ** CMRA for the option type *)
Section option.
Context {A : cmraT}.
@@ -684,7 +798,8 @@ Section option.
match mx with Some x => ✓ x | None => True end.
Instance option_validN : ValidN (option A) := λ n mx,
match mx with Some x => ✓{n} x | None => True end.
- Global Instance option_empty : Empty (option A) := None.
+ Instance option_empty : Empty (option A) := None.
+
Instance option_core : Core (option A) := fmap core.
Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
@@ -704,7 +819,7 @@ Section option.
by exists (Some z); constructor.
Qed.
- Definition option_cmra_mixin : CMRAMixin (option A).
+ Lemma option_cmra_mixin : CMRAMixin (option A).
Proof.
split.
- by intros n [x|]; destruct 1; constructor; cofe_subst.
@@ -732,11 +847,15 @@ Section option.
Qed.
Canonical Structure optionR :=
CMRAT (option A) option_cofe_mixin option_cmra_mixin.
- Global Instance option_cmra_unit : CMRAUnit optionR.
- Proof. split. done. by intros []. by inversion_clear 1. Qed.
+
Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
+ Lemma option_ucmra_mixin : UCMRAMixin optionR.
+ Proof. split. done. by intros []. by inversion_clear 1. Qed.
+ Canonical Structure optionUR :=
+ UCMRAT (option A) option_cofe_mixin option_cmra_mixin option_ucmra_mixin.
+
(** Misc *)
Global Instance Some_cmra_monotone : CMRAMonotone Some.
Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
@@ -753,7 +872,7 @@ Section option.
Proof. by constructor. Qed.
Global Instance option_persistent (mx : option A) :
(∀ x : A, Persistent x) → Persistent mx.
- Proof. intros. destruct mx. apply _. apply cmra_unit_persistent. Qed.
+ Proof. intros. destruct mx. apply _. constructor. Qed.
(** Updates *)
Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
@@ -771,14 +890,10 @@ Section option.
Proof.
rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
Qed.
- Lemma option_update_None `{Empty A, !CMRAUnit A} : ∅ ~~> Some ∅.
- Proof.
- intros n [x|] ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id;
- auto using cmra_unit_validN.
- Qed.
End option.
Arguments optionR : clear implicits.
+Arguments optionUR : clear implicits.
Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} :
CMRAMonotone (fmap f : option A → option B).
@@ -788,9 +903,9 @@ Proof.
- intros mx my; rewrite !option_included.
intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @included_preserving.
Qed.
-Program Definition optionRF (F : rFunctor) : rFunctor := {|
- rFunctor_car A B := optionR (rFunctor_car F A B);
- rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
+Program Definition optionURF (F : rFunctor) : urFunctor := {|
+ urFunctor_car A B := optionUR (rFunctor_car F A B);
+ urFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
@@ -804,8 +919,8 @@ Next Obligation.
apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
Qed.
-Instance optionRF_contractive F :
- rFunctorContractive F → rFunctorContractive (optionRF F).
+Instance optionURF_contractive F :
+ rFunctorContractive F → urFunctorContractive (optionURF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
Qed.
diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 65f9f9256..030ddb25f 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -1,31 +1,32 @@
From iris.algebra Require Export cmra list.
From iris.prelude Require Import gmap.
-Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
+Fixpoint big_op {A : ucmraT} (xs : list A) : A :=
match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
-Arguments big_op _ _ !_ /.
-Instance: Params (@big_op) 2.
-Definition big_opM `{Countable K} {A : cmraT} `{Empty A} (m : gmap K A) : A :=
+Arguments big_op _ !_ /.
+Instance: Params (@big_op) 1.
+Definition big_opM `{Countable K} {A : ucmraT} (m : gmap K A) : A :=
big_op (snd <$> map_to_list m).
-Instance: Params (@big_opM) 5.
+Instance: Params (@big_opM) 4.
(** * Properties about big ops *)
Section big_op.
-Context `{CMRAUnit A}.
+Context {A : ucmraT}.
+Implicit Types xs : list A.
(** * Big ops *)
Lemma big_op_nil : big_op (@nil A) = ∅.
Proof. done. Qed.
Lemma big_op_cons x xs : big_op (x :: xs) = x â‹… big_op xs.
Proof. done. Qed.
-Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
+Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) (@big_op A).
Proof.
induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ x).
- by trans (big_op xs2).
Qed.
-Global Instance big_op_ne n : Proper (dist n ==> dist n) big_op.
+Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op A).
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op := ne_proper _.
Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
diff --git a/algebra/cmra_tactics.v b/algebra/cmra_tactics.v
index 227e789b5..cdb25704a 100644
--- a/algebra/cmra_tactics.v
+++ b/algebra/cmra_tactics.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import cmra_big_op.
(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
- Context `{CMRAUnit A}.
+ Context {A : ucmraT}.
Inductive expr :=
| EVar : nat → expr
@@ -24,8 +24,8 @@ Module ra_reflection. Section ra_reflection.
Lemma eval_flatten Σ e :
eval Σ e ≡ big_op ((λ n, from_option id ∅ (Σ !! n)) <$> flatten e).
Proof.
- by induction e as [| |e1 IH1 e2 IH2];
- rewrite /= ?right_id ?fmap_app ?big_op_app ?IH1 ?IH2.
+ induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
+ by rewrite fmap_app IH1 IH2 big_op_app.
Qed.
Lemma flatten_correct Σ e1 e2 :
flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 9df1334e7..6ef5c1332 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -91,8 +91,8 @@ End cofe_mixin.
(** Discrete COFEs and Timeless elements *)
(* TODO: On paper, We called these "discrete elements". I think that makes
more sense. *)
-Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
-Arguments timeless {_} _ {_} _ _.
+Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
+Arguments timeless {_ _ _} _ {_} _ _.
Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x.
(** General properties *)
diff --git a/algebra/excl.v b/algebra/excl.v
index 356f06d84..994f9ab9f 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -77,8 +77,7 @@ Instance excl_valid : Valid (excl A) := λ x,
match x with Excl _ | ExclUnit => True | ExclBot => False end.
Instance excl_validN : ValidN (excl A) := λ n x,
match x with Excl _ | ExclUnit => True | ExclBot => False end.
-Global Instance excl_empty : Empty (excl A) := ExclUnit.
-Instance excl_core : Core (excl A) := λ _, ∅.
+Instance excl_core : Core (excl A) := λ _, ExclUnit.
Instance excl_op : Op (excl A) := λ x y,
match x, y with
| Excl a, ExclUnit | ExclUnit, Excl a => Excl a
@@ -86,7 +85,7 @@ Instance excl_op : Op (excl A) := λ x y,
| _, _=> ExclBot
end.
-Definition excl_cmra_mixin : CMRAMixin (excl A).
+Lemma excl_cmra_mixin : CMRAMixin (excl A).
Proof.
split.
- by intros n []; destruct 1; constructor.
@@ -98,7 +97,7 @@ Proof.
- by intros [?| |] [?| |]; constructor.
- by intros [?| |]; constructor.
- constructor.
- - by intros [?| |] [?| |]; exists ∅.
+ - by intros [?| |] [?| |]; exists ExclUnit.
- by intros n [?| |] [?| |].
- intros n x y1 y2 ? Hx.
by exists match y1, y2 with
@@ -107,13 +106,18 @@ Proof.
| ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
Qed.
-Canonical Structure exclR : cmraT :=
+Canonical Structure exclR :=
CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
-Global Instance excl_cmra_unit : CMRAUnit exclR.
-Proof. split. done. by intros []. apply _. Qed.
+
Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR.
Proof. split. apply _. by intros []. Qed.
+Instance excl_empty : Empty (excl A) := ExclUnit.
+Lemma excl_ucmra_mixin : UCMRAMixin (excl A).
+Proof. split. done. by intros []. apply _. Qed.
+Canonical Structure exclUR :=
+ UCMRAT (excl A) excl_cofe_mixin excl_cmra_mixin excl_ucmra_mixin.
+
Lemma excl_validN_inv_l n x a : ✓{n} (Excl a ⋅ x) → x = ∅.
Proof. by destruct x. Qed.
Lemma excl_validN_inv_r n x a : ✓{n} (x ⋅ Excl a) → x = ∅.
@@ -152,6 +156,7 @@ End excl.
Arguments exclC : clear implicits.
Arguments exclR : clear implicits.
+Arguments exclUR : clear implicits.
(* Functor *)
Definition excl_map {A B} (f : A → B) (x : excl A) : excl B :=
@@ -182,9 +187,9 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
-Program Definition exclRF (F : cFunctor) : rFunctor := {|
- rFunctor_car A B := exclR (cFunctor_car F A B);
- rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
+Program Definition exclURF (F : cFunctor) : urFunctor := {|
+ urFunctor_car A B := (exclUR (cFunctor_car F A B) : ucmraT);
+ urFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
|}.
Next Obligation.
intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
@@ -198,8 +203,8 @@ Next Obligation.
apply excl_map_ext=>y; apply cFunctor_compose.
Qed.
-Instance exclRF_contractive F :
- cFunctorContractive F → rFunctorContractive (exclRF F).
+Instance exclURF_contractive F :
+ cFunctorContractive F → urFunctorContractive (exclURF F).
Proof.
intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
Qed.
diff --git a/algebra/frac.v b/algebra/frac.v
index ede01ba39..e4f7897d2 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -119,8 +119,7 @@ Instance frac_valid : Valid (frac A) := λ x,
match x with Frac q a => (q ≤ 1)%Qc ∧ ✓ a | FracUnit => True end.
Instance frac_validN : ValidN (frac A) := λ n x,
match x with Frac q a => (q ≤ 1)%Qc ∧ ✓{n} a | FracUnit => True end.
-Global Instance frac_empty : Empty (frac A) := FracUnit.
-Instance frac_core : Core (frac A) := λ _, ∅.
+Instance frac_core : Core (frac A) := λ _, FracUnit.
Instance frac_op : Op (frac A) := λ x y,
match x, y with
| Frac q1 a, Frac q2 b => Frac (q1 + q2) (a â‹… b)
@@ -148,25 +147,30 @@ Proof.
trans (q1 + q2)%Qp; simpl; last done.
rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak.
- intros n [q a|] y1 y2 Hx Hx'; last first.
- { by exists (∅, ∅); destruct y1, y2; inversion_clear Hx'. }
+ { by exists (FracUnit, FracUnit); destruct y1, y2; inversion_clear Hx'. }
destruct Hx, y1 as [q1 b1|], y2 as [q2 b2|].
+ apply (inj2 Frac) in Hx'; destruct Hx' as [-> ?].
destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto.
exists (Frac q1 z1,Frac q2 z2); by repeat constructor.
- + exists (Frac q a, ∅); inversion_clear Hx'; by repeat constructor.
- + exists (∅, Frac q a); inversion_clear Hx'; by repeat constructor.
+ + exists (Frac q a, FracUnit); inversion_clear Hx'; by repeat constructor.
+ + exists (FracUnit, Frac q a); inversion_clear Hx'; by repeat constructor.
+ exfalso; inversion_clear Hx'.
Qed.
-Canonical Structure fracR : cmraT :=
+Canonical Structure fracR :=
CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin.
-Global Instance frac_cmra_unit : CMRAUnit fracR.
-Proof. split. done. by intros []. apply _. Qed.
+
Global Instance frac_cmra_discrete : CMRADiscrete A → CMRADiscrete fracR.
Proof.
split; first apply _.
intros [q a|]; destruct 1; split; auto using cmra_discrete_valid.
Qed.
+Instance frac_empty : Empty (frac A) := FracUnit.
+Definition frac_ucmra_mixin : UCMRAMixin (frac A).
+Proof. split. done. by intros []. apply _. Qed.
+Canonical Structure fracUR :=
+ UCMRAT (frac A) frac_cofe_mixin frac_cmra_mixin frac_ucmra_mixin.
+
Lemma frac_validN_inv_l n y a : ✓{n} (Frac 1 a ⋅ y) → y = ∅.
Proof.
destruct y as [q b|]; [|done]=> -[Hq ?]; destruct (Qcle_not_lt _ _ Hq).
@@ -217,6 +221,7 @@ Qed.
End cmra.
Arguments fracR : clear implicits.
+Arguments fracUR : clear implicits.
(* Functor *)
Instance frac_map_cmra_monotone {A B : cmraT} (f : A → B) :
@@ -225,15 +230,15 @@ Proof.
split; try apply _.
- intros n [p a|]; destruct 1; split; auto using validN_preserving.
- intros [q1 a1|] [q2 a2|] [[q3 a3|] Hx];
- inversion Hx; setoid_subst; try apply: cmra_unit_least; auto.
+ inversion Hx; setoid_subst; try apply: ucmra_unit_least; auto.
destruct (included_preserving f a1 (a1 â‹… a3)) as [b ?].
{ by apply cmra_included_l. }
by exists (Frac q3 b); constructor.
Qed.
-Program Definition fracRF (F : rFunctor) : rFunctor := {|
- rFunctor_car A B := fracR (rFunctor_car F A B);
- rFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg)
+Program Definition fracURF (F : rFunctor) : urFunctor := {|
+ urFunctor_car A B := fracUR (rFunctor_car F A B);
+ urFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_ne.
@@ -247,8 +252,8 @@ Next Obligation.
apply frac_map_ext=>y; apply rFunctor_compose.
Qed.
-Instance fracRF_contractive F :
- rFunctorContractive F → rFunctorContractive (fracRF F).
+Instance fracURF_contractive F :
+ rFunctorContractive F → urFunctorContractive (fracURF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive.
Qed.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index a37719e1b..f209cf09c 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -109,7 +109,7 @@ Proof.
{ exists m2. by rewrite left_id. }
destruct (IH (delete i m2)) as [m2' Hm2'].
{ intros j. move: (Hm j); destruct (decide (i = j)) as [->|].
- - intros _. rewrite Hi. apply: cmra_unit_least.
+ - intros _. rewrite Hi. apply: ucmra_unit_least.
- rewrite lookup_insert_ne // lookup_delete_ne //. }
destruct (Hm i) as [my Hi']; simplify_map_eq.
exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|].
@@ -118,7 +118,7 @@ Proof.
lookup_insert_ne // lookup_partial_alter_ne.
Qed.
-Definition gmap_cmra_mixin : CMRAMixin (gmap K A).
+Lemma gmap_cmra_mixin : CMRAMixin (gmap K A).
Proof.
split.
- by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
@@ -152,17 +152,21 @@ Proof.
pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
by symmetry; apply option_op_positive_dist_r with (m1 !! i).
Qed.
-Canonical Structure gmapR : cmraT :=
+Canonical Structure gmapR :=
CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
-Global Instance gmap_cmra_unit : CMRAUnit gmapR.
+
+Global Instance gmap_cmra_discrete : CMRADiscrete A → CMRADiscrete gmapR.
+Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
+
+Lemma gmap_ucmra_mixin : UCMRAMixin (gmap K A).
Proof.
split.
- by intros i; rewrite lookup_empty.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- apply gmap_empty_timeless.
Qed.
-Global Instance gmap_cmra_discrete : CMRADiscrete A → CMRADiscrete gmapR.
-Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
+Canonical Structure gmapUR :=
+ UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
(** Internalized properties *)
Lemma gmap_equivI {M} m1 m2 : (m1 ≡ m2) ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
@@ -172,6 +176,7 @@ Proof. by uPred.unseal. Qed.
End cmra.
Arguments gmapR _ {_ _} _.
+Arguments gmapUR _ {_ _} _.
Section properties.
Context `{Countable K} {A : cmraT}.
@@ -189,7 +194,7 @@ Lemma insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m.
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
Lemma singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x.
Proof.
- split; [|by intros; apply insert_validN, cmra_unit_validN].
+ split; [|by intros; apply insert_validN, ucmra_unit_validN].
by move=>/(_ i); simplify_map_eq.
Qed.
Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
@@ -265,25 +270,6 @@ Proof. apply insert_updateP'. Qed.
Lemma singleton_update i (x y : A) : x ~~> y → {[ i := x ]} ~~> {[ i := y ]}.
Proof. apply insert_update. Qed.
-Lemma singleton_updateP_empty `{Empty A, !CMRAUnit A}
- (P : A → Prop) (Q : gmap K A → Prop) i :
- ∅ ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
-Proof.
- intros Hx HQ n gf Hg.
- destruct (Hx n (from_option id ∅ (gf !! i))) as (y&?&Hy).
- { move:(Hg i). rewrite !left_id.
- case _: (gf !! i); simpl; auto using cmra_unit_validN. }
- exists {[ i := y ]}; split; first by auto.
- intros i'; destruct (decide (i' = i)) as [->|].
- - rewrite lookup_op lookup_singleton.
- move:Hy; case _: (gf !! i); first done.
- by rewrite right_id.
- - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
-Qed.
-Lemma singleton_updateP_empty' `{Empty A, !CMRAUnit A} (P: A → Prop) i :
- ∅ ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
-Proof. eauto using singleton_updateP_empty. Qed.
-
Section freshness.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma updateP_alloc_strong (Q : gmap K A → Prop) (I : gset K) m x :
@@ -308,6 +294,31 @@ Proof. eauto using updateP_alloc_strong. Qed.
Lemma updateP_alloc' m x :
✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
Proof. eauto using updateP_alloc. Qed.
+
+Lemma singleton_updateP_unit (P : A → Prop) (Q : gmap K A → Prop) u i :
+ ✓ u → LeftId (≡) u (⋅) →
+ u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
+Proof.
+ intros ?? Hx HQ n gf Hg.
+ destruct (Hx n (from_option id u (gf !! i))) as (y&?&Hy).
+ { move:(Hg i). rewrite !left_id.
+ case _: (gf !! i); simpl; first done. intros; by apply cmra_valid_validN. }
+ exists {[ i := y ]}; split; first by auto.
+ intros i'; destruct (decide (i' = i)) as [->|].
+ - rewrite lookup_op lookup_singleton.
+ move:Hy; case _: (gf !! i); first done.
+ by rewrite /= (comm _ y) left_id right_id.
+ - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
+Qed.
+Lemma singleton_updateP_unit' (P: A → Prop) u i :
+ ✓ u → LeftId (≡) u (⋅) →
+ u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
+Proof. eauto using singleton_updateP_unit. Qed.
+Lemma singleton_update_unit u i (y : A) :
+ ✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}.
+Proof.
+ rewrite !cmra_update_updateP; eauto using singleton_updateP_unit with subst.
+Qed.
End freshness.
(* Allocation is a local update: Just use composition with a singleton map. *)
@@ -370,9 +381,9 @@ Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
Qed.
-Program Definition gmapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
- rFunctor_car A B := gmapR K (rFunctor_car F A B);
- rFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg)
+Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
+ urFunctor_car A B := gmapUR K (rFunctor_car F A B);
+ urFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
@@ -386,7 +397,7 @@ Next Obligation.
apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
Qed.
Instance gmapRF_contractive K `{Countable K} F :
- rFunctorContractive F → rFunctorContractive (gmapRF K F).
+ rFunctorContractive F → urFunctorContractive (gmapURF K F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
Qed.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 3a3883e93..111b7d47e 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -4,20 +4,14 @@ From iris.prelude Require Import finite.
(** * Indexed product *)
(** Need to put this in a definition to make canonical structures to work. *)
-Definition iprod {A} (B : A → cofeT) := ∀ x, B x.
-Definition iprod_insert {A} {B : A → cofeT} `{∀ x x' : A, Decision (x = x')}
+Definition iprod `{Finite A} (B : A → cofeT) := ∀ x, B x.
+Definition iprod_insert `{Finite A} {B : A → cofeT}
(x : A) (y : B x) (f : iprod B) : iprod B := λ x',
match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
-Global Instance iprod_empty {A} {B : A → cofeT}
- `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅.
-Definition iprod_singleton {A} {B : A → cofeT}
- `{∀ x x' : A, Decision (x = x'), ∀ x : A, Empty (B x)}
- (x : A) (y : B x) : iprod B := iprod_insert x y ∅.
-Instance: Params (@iprod_insert) 4.
-Instance: Params (@iprod_singleton) 5.
+Instance: Params (@iprod_insert) 5.
Section iprod_cofe.
- Context {A} {B : A → cofeT}.
+ Context `{Finite A} {B : A → cofeT}.
Implicit Types x : A.
Implicit Types f g : iprod B.
@@ -44,15 +38,6 @@ Section iprod_cofe.
Qed.
Canonical Structure iprodC : cofeT := CofeT (iprod B) iprod_cofe_mixin.
- (** Properties of empty *)
- Section empty.
- Context `{∀ x, Empty (B x)}.
- Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl.
- Global Instance iprod_empty_timeless :
- (∀ x : A, Timeless (∅ : B x)) → Timeless (∅ : iprod B).
- Proof. intros ? f Hf x. by apply: timeless. Qed.
- End empty.
-
(** Properties of iprod_insert. *)
Context `{∀ x x' : A, Decision (x = x')}.
@@ -79,8 +64,8 @@ Section iprod_cofe.
intros ? y ?.
cut (f ≡ iprod_insert x y f).
{ by move=> /(_ x)->; rewrite iprod_lookup_insert. }
- by apply: timeless=>x'; destruct (decide (x = x')) as [->|];
- rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
+ apply (timeless _)=> x'; destruct (decide (x = x')) as [->|];
+ by rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
Qed.
Global Instance iprod_insert_timeless f x y :
Timeless f → Timeless y → Timeless (iprod_insert x y f).
@@ -91,30 +76,12 @@ Section iprod_cofe.
- rewrite iprod_lookup_insert_ne //.
apply: timeless. by rewrite -(Heq x') iprod_lookup_insert_ne.
Qed.
-
- (** Properties of iprod_singletom. *)
- Context `{∀ x : A, Empty (B x)}.
-
- Global Instance iprod_singleton_ne n x :
- Proper (dist n ==> dist n) (iprod_singleton x).
- Proof. by intros y1 y2 Hy; rewrite /iprod_singleton Hy. Qed.
- Global Instance iprod_singleton_proper x :
- Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
-
- Lemma iprod_lookup_singleton x y : (iprod_singleton x y) x = y.
- Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
- Lemma iprod_lookup_singleton_ne x x' y: x ≠x' → (iprod_singleton x y) x' = ∅.
- Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
-
- Global Instance iprod_singleton_timeless x (y : B x) :
- (∀ x : A, Timeless (∅ : B x)) → Timeless y → Timeless (iprod_singleton x y).
- Proof. eauto using iprod_insert_timeless, iprod_empty_timeless. Qed.
End iprod_cofe.
-Arguments iprodC {_} _.
+Arguments iprodC {_ _ _} _.
Section iprod_cmra.
- Context `{Finite A} {B : A → cmraT}.
+ Context `{Finite A} {B : A → ucmraT}.
Implicit Types f g : iprod B.
Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
@@ -131,7 +98,7 @@ Section iprod_cmra.
intros [h ?]%finite_choice. by exists h.
Qed.
- Definition iprod_cmra_mixin : CMRAMixin (iprod B).
+ Lemma iprod_cmra_mixin : CMRAMixin (iprod B).
Proof.
split.
- by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
@@ -153,16 +120,21 @@ Section iprod_cmra.
exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
split_and?; intros x; apply (proj2_sig (g x)).
Qed.
- Canonical Structure iprodR : cmraT :=
+ Canonical Structure iprodR :=
CMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin.
- Global Instance iprod_cmra_unit `{∀ x, Empty (B x)} :
- (∀ x, CMRAUnit (B x)) → CMRAUnit iprodR.
+
+ Instance iprod_empty : Empty (iprod B) := λ x, ∅.
+ Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl.
+
+ Lemma iprod_ucmra_mixin : UCMRAMixin (iprod B).
Proof.
- intros ?; split.
- - intros x; apply cmra_unit_valid.
+ split.
+ - intros x; apply ucmra_unit_valid.
- by intros f x; rewrite iprod_lookup_op left_id.
- - by apply _.
+ - intros f Hf x. by apply: timeless.
Qed.
+ Canonical Structure iprodUR :=
+ UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
(** Internalized properties *)
Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2) ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
@@ -171,8 +143,6 @@ Section iprod_cmra.
Proof. by uPred.unseal. Qed.
(** Properties of iprod_insert. *)
- Context `{∀ x x' : A, Decision (x = x')}.
-
Lemma iprod_insert_updateP x (P : B x → Prop) (Q : iprod B → Prop) g y1 :
y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) →
iprod_insert x y1 g ~~>: Q.
@@ -194,16 +164,40 @@ Section iprod_cmra.
Proof.
rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
Qed.
+End iprod_cmra.
+
+Arguments iprodR {_ _ _} _.
+Arguments iprodUR {_ _ _} _.
+
+Definition iprod_singleton `{Finite A} {B : A → ucmraT}
+ (x : A) (y : B x) : iprod B := iprod_insert x y ∅.
+Instance: Params (@iprod_singleton) 5.
+
+Section iprod_singleton.
+ Context `{Finite A} {B : A → ucmraT}.
+ Implicit Types x : A.
+
+ Global Instance iprod_singleton_ne n x :
+ Proper (dist n ==> dist n) (iprod_singleton x : B x → _).
+ Proof. intros y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed.
+ Global Instance iprod_singleton_proper x :
+ Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
- (** Properties of iprod_singleton. *)
- Context `{∀ x, Empty (B x), ∀ x, CMRAUnit (B x)}.
+ Lemma iprod_lookup_singleton x (y : B x) : (iprod_singleton x y) x = y.
+ Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
+ Lemma iprod_lookup_singleton_ne x x' (y : B x) :
+ x ≠x' → (iprod_singleton x y) x' = ∅.
+ Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
- Lemma iprod_singleton_validN n x (y: B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
+ Global Instance iprod_singleton_timeless x (y : B x) :
+ Timeless y → Timeless (iprod_singleton x y) := _.
+
+ Lemma iprod_singleton_validN n x (y : B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
Proof.
split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
move=>Hx x'; destruct (decide (x = x')) as [->|];
rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
- by apply cmra_unit_validN.
+ by apply ucmra_unit_validN.
Qed.
Lemma iprod_core_singleton x (y : B x) :
@@ -234,7 +228,7 @@ Section iprod_cmra.
y1 ~~>: P →
iprod_singleton x y1 ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
Proof. eauto using iprod_singleton_updateP. Qed.
- Lemma iprod_singleton_update x y1 y2 :
+ Lemma iprod_singleton_update x (y1 y2 : B x) :
y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
Proof. eauto using iprod_insert_update. Qed.
@@ -250,30 +244,35 @@ Section iprod_cmra.
Lemma iprod_singleton_updateP_empty' x (P : B x → Prop) :
∅ ~~>: P → ∅ ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
Proof. eauto using iprod_singleton_updateP_empty. Qed.
-End iprod_cmra.
-
-Arguments iprodR {_ _ _} _.
+ Lemma iprod_singleton_update_empty x (y : B x) :
+ ∅ ~~> y → ∅ ~~> iprod_singleton x y.
+ Proof.
+ rewrite !cmra_update_updateP;
+ eauto using iprod_singleton_updateP_empty with subst.
+ Qed.
+End iprod_singleton.
(** * Functor *)
-Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
+Definition iprod_map `{Finite A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
(g : iprod B1) : iprod B2 := λ x, f _ (g x).
-Lemma iprod_map_ext {A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) g :
+Lemma iprod_map_ext `{Finite A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) (g : iprod B1) :
(∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
Proof. done. Qed.
-Lemma iprod_map_id {A} {B: A → cofeT} (g : iprod B) : iprod_map (λ _, id) g = g.
+Lemma iprod_map_id `{Finite A} {B : A → cofeT} (g : iprod B) :
+ iprod_map (λ _, id) g = g.
Proof. done. Qed.
-Lemma iprod_map_compose {A} {B1 B2 B3 : A → cofeT}
+Lemma iprod_map_compose `{Finite A} {B1 B2 B3 : A → cofeT}
(f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
Proof. done. Qed.
-Instance iprod_map_ne {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
+Instance iprod_map_ne `{Finite A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
(∀ x, Proper (dist n ==> dist n) (f x)) →
Proper (dist n ==> dist n) (iprod_map f).
Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
-Instance iprod_map_cmra_monotone `{Finite A}
- {B1 B2: A → cmraT} (f : ∀ x, B1 x → B2 x) :
+Instance iprod_map_cmra_monotone
+ `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
(∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f).
Proof.
split; first apply _.
@@ -282,53 +281,54 @@ Proof.
rewrite /iprod_map; apply (included_preserving _), Hf.
Qed.
-Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
+Definition iprodC_map `{Finite A} {B1 B2 : A → cofeT}
+ (f : iprod (λ x, B1 x -n> B2 x)) :
iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance iprodC_map_ne {A} {B1 B2 : A → cofeT} n :
- Proper (dist n ==> dist n) (@iprodC_map A B1 B2).
+Instance iprodC_map_ne `{Finite A} {B1 B2 : A → cofeT} n :
+ Proper (dist n ==> dist n) (@iprodC_map A _ _ B1 B2).
Proof. intros f1 f2 Hf g x; apply Hf. Qed.
-Program Definition iprodCF {C} (F : C → cFunctor) : cFunctor := {|
+Program Definition iprodCF `{Finite C} (F : C → cFunctor) : cFunctor := {|
cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
|}.
Next Obligation.
- intros C F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne.
+ intros C ?? F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne.
Qed.
Next Obligation.
- intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
+ intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
apply iprod_map_ext=> y; apply cFunctor_id.
Qed.
Next Obligation.
- intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
+ intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
apply iprod_map_ext=>y; apply cFunctor_compose.
Qed.
-Instance iprodCF_contractive {C} (F : C → cFunctor) :
+Instance iprodCF_contractive `{Finite C} (F : C → cFunctor) :
(∀ c, cFunctorContractive (F c)) → cFunctorContractive (iprodCF F).
Proof.
intros ? A1 A2 B1 B2 n ?? g.
by apply iprodC_map_ne=>c; apply cFunctor_contractive.
Qed.
-Program Definition iprodRF `{Finite C} (F : C → rFunctor) : rFunctor := {|
- rFunctor_car A B := iprodR (λ c, rFunctor_car (F c) A B);
- rFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, rFunctor_map (F c) fg)
+Program Definition iprodURF `{Finite C} (F : C → urFunctor) : urFunctor := {|
+ urFunctor_car A B := iprodUR (λ c, urFunctor_car (F c) A B);
+ urFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, urFunctor_map (F c) fg)
|}.
Next Obligation.
intros C ?? F A1 A2 B1 B2 n ?? g.
- by apply iprodC_map_ne=>?; apply rFunctor_ne.
+ by apply iprodC_map_ne=>?; apply urFunctor_ne.
Qed.
Next Obligation.
intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
- apply iprod_map_ext=> y; apply rFunctor_id.
+ apply iprod_map_ext=> y; apply urFunctor_id.
Qed.
Next Obligation.
intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-iprod_map_compose.
- apply iprod_map_ext=>y; apply rFunctor_compose.
+ apply iprod_map_ext=>y; apply urFunctor_compose.
Qed.
-Instance iprodRF_contractive `{Finite C} (F : C → rFunctor) :
- (∀ c, rFunctorContractive (F c)) → rFunctorContractive (iprodRF F).
+Instance iprodURF_contractive `{Finite C} (F : C → urFunctor) :
+ (∀ c, urFunctorContractive (F c)) → urFunctorContractive (iprodURF F).
Proof.
intros ? A1 A2 B1 B2 n ?? g.
- by apply iprodC_map_ne=>c; apply rFunctor_contractive.
+ by apply iprodC_map_ne=>c; apply urFunctor_contractive.
Qed.
diff --git a/algebra/list.v b/algebra/list.v
index 7ff0a57fb..eafa5210e 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -113,7 +113,7 @@ Qed.
(* CMRA *)
Section cmra.
- Context {A : cmraT}.
+ Context {A : ucmraT}.
Implicit Types l : list A.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
@@ -196,17 +196,19 @@ Section cmra.
[inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
Qed.
- Canonical Structure listR : cmraT :=
+ Canonical Structure listR :=
CMRAT (list A) list_cofe_mixin list_cmra_mixin.
Global Instance empty_list : Empty (list A) := [].
- Global Instance list_cmra_unit : CMRAUnit listR.
+ Definition list_ucmra_mixin : UCMRAMixin (list A).
Proof.
split.
- constructor.
- by intros l.
- by inversion_clear 1.
Qed.
+ Canonical Structure listUR :=
+ UCMRAT (list A) list_cofe_mixin list_cmra_mixin list_ucmra_mixin.
Global Instance list_cmra_discrete : CMRADiscrete A → CMRADiscrete listR.
Proof.
@@ -228,13 +230,15 @@ Section cmra.
End cmra.
Arguments listR : clear implicits.
+Arguments listUR : clear implicits.
-Global Instance list_singletonM `{Empty A} : SingletonM nat A (list A) := λ n x,
+Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
replicate n ∅ ++ [x].
Section properties.
- Context {A : cmraT}.
+ Context {A : ucmraT}.
Implicit Types l : list A.
+ Implicit Types x y z : A.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
@@ -255,64 +259,58 @@ Section properties.
Lemma replicate_valid n (x : A) : ✓ x → ✓ replicate n x.
Proof. apply Forall_replicate. Qed.
+ Global Instance list_singletonM_ne n i :
+ Proper (dist n ==> dist n) (@list_singletonM A i).
+ Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
+ Global Instance list_singletonM_proper i :
+ Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
- (* Singleton lists *)
- Section singleton.
- Context `{CMRAUnit A}.
-
- Global Instance list_singletonM_ne n i :
- Proper (dist n ==> dist n) (list_singletonM i).
- Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
- Global Instance list_singletonM_proper i :
- Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
-
- Lemma elem_of_list_singletonM i z x : z ∈ {[i := x]} → z = ∅ ∨ z = x.
- Proof.
- rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
- Qed.
- Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x.
- Proof. induction i; by f_equal/=. Qed.
- Lemma list_lookup_singletonM_ne i j x :
- i ≠j → {[ i := x ]} !! j = None ∨ {[ i := x ]} !! j = Some ∅.
- Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
- Lemma list_singletonM_validN n i x : ✓{n} {[ i := x ]} ↔ ✓{n} x.
- Proof.
- rewrite list_lookup_validN. split.
- { move=> /(_ i). by rewrite list_lookup_singletonM. }
- intros Hx j; destruct (decide (i = j)); subst.
- - by rewrite list_lookup_singletonM.
- - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
- rewrite Hi; by try apply (cmra_unit_validN (A:=A)).
- Qed.
- Lemma list_singleton_valid i x : ✓ {[ i := x ]} ↔ ✓ x.
- Proof.
- rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
- Qed.
- Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
- Proof.
- rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
- Qed.
-
- Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
- Proof.
- rewrite /singletonM /list_singletonM /=.
- induction i; constructor; auto using cmra_core_unit.
- Qed.
- Lemma list_op_singletonM i (x y : A) :
- {[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
- Proof.
- rewrite /singletonM /list_singletonM /=.
- induction i; constructor; rewrite ?left_id; auto.
- Qed.
- Lemma list_alter_singletonM f i x : alter f i {[i := x]} = {[i := f x]}.
- Proof.
- rewrite /singletonM /list_singletonM /=.
- induction i; f_equal/=; auto.
- Qed.
- Global Instance list_singleton_persistent i (x : A) :
- Persistent x → Persistent {[ i := x ]}.
- Proof. intros. by rewrite /Persistent list_core_singletonM persistent. Qed.
- End singleton.
+ Lemma elem_of_list_singletonM i z x : z ∈ {[i := x]} → z = ∅ ∨ z = x.
+ Proof.
+ rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
+ Qed.
+ Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x.
+ Proof. induction i; by f_equal/=. Qed.
+ Lemma list_lookup_singletonM_ne i j x :
+ i ≠j → {[ i := x ]} !! j = None ∨ {[ i := x ]} !! j = Some ∅.
+ Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
+ Lemma list_singletonM_validN n i x : ✓{n} {[ i := x ]} ↔ ✓{n} x.
+ Proof.
+ rewrite list_lookup_validN. split.
+ { move=> /(_ i). by rewrite list_lookup_singletonM. }
+ intros Hx j; destruct (decide (i = j)); subst.
+ - by rewrite list_lookup_singletonM.
+ - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
+ rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
+ Qed.
+ Lemma list_singleton_valid i x : ✓ {[ i := x ]} ↔ ✓ x.
+ Proof.
+ rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
+ Qed.
+ Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
+ Proof.
+ rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
+ Qed.
+
+ Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
+ Proof.
+ rewrite /singletonM /list_singletonM /=.
+ induction i; constructor; auto using ucmra_core_unit.
+ Qed.
+ Lemma list_op_singletonM i (x y : A) :
+ {[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
+ Proof.
+ rewrite /singletonM /list_singletonM /=.
+ induction i; constructor; rewrite ?left_id; auto.
+ Qed.
+ Lemma list_alter_singletonM f i x : alter f i {[i := x]} = {[i := f x]}.
+ Proof.
+ rewrite /singletonM /list_singletonM /=.
+ induction i; f_equal/=; auto.
+ Qed.
+ Global Instance list_singleton_persistent i (x : A) :
+ Persistent x → Persistent {[ i := x ]}.
+ Proof. intros. by rewrite /Persistent list_core_singletonM persistent. Qed.
(* Update *)
Lemma list_update_updateP (P : A → Prop) (Q : list A → Prop) l1 x l2 :
@@ -350,7 +348,7 @@ Section properties.
End properties.
(** Functor *)
-Instance list_fmap_cmra_monotone {A B : cmraT} (f : A → B)
+Instance list_fmap_cmra_monotone {A B : ucmraT} (f : A → B)
`{!CMRAMonotone f} : CMRAMonotone (fmap f : list A → list B).
Proof.
split; try apply _.
@@ -360,24 +358,24 @@ Proof.
by apply (included_preserving (fmap f : option A → option B)).
Qed.
-Program Definition listRF (F : rFunctor) : rFunctor := {|
- rFunctor_car A B := listR (rFunctor_car F A B);
- rFunctor_map A1 A2 B1 B2 fg := listC_map (rFunctor_map F fg)
+Program Definition listURF (F : urFunctor) : urFunctor := {|
+ urFunctor_car A B := listUR (urFunctor_car F A B);
+ urFunctor_map A1 A2 B1 B2 fg := listC_map (urFunctor_map F fg)
|}.
Next Obligation.
- by intros F ???? n f g Hfg; apply listC_map_ne, rFunctor_ne.
+ by intros F ???? n f g Hfg; apply listC_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(list_fmap_id x).
- apply list_fmap_setoid_ext=>y. apply rFunctor_id.
+ apply list_fmap_setoid_ext=>y. apply urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
- apply list_fmap_setoid_ext=>y; apply rFunctor_compose.
+ apply list_fmap_setoid_ext=>y; apply urFunctor_compose.
Qed.
-Instance listRF_contractive F :
- rFunctorContractive F → rFunctorContractive (listRF F).
+Instance listURF_contractive F :
+ urFunctorContractive F → urFunctorContractive (listURF F).
Proof.
- by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, rFunctor_contractive.
+ by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive.
Qed.
diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index 72588fd9c..b156f57e6 100644
--- a/algebra/one_shot.v
+++ b/algebra/one_shot.v
@@ -125,12 +125,11 @@ Instance one_shot_validN : ValidN (one_shot A) := λ n x,
| OneShotUnit => True
| OneShotBot => False
end.
-Global Instance one_shot_empty : Empty (one_shot A) := OneShotUnit.
Instance one_shot_core : Core (one_shot A) := λ x,
match x with
| Shot a => Shot (core a)
| OneShotBot => OneShotBot
- | _ => ∅
+ | _ => OneShotUnit
end.
Instance one_shot_op : Op (one_shot A) := λ x y,
match x, y with
@@ -154,7 +153,7 @@ Proof.
- exists (Shot c). constructor. done.
Qed.
-Definition one_shot_cmra_mixin : CMRAMixin (one_shot A).
+Lemma one_shot_cmra_mixin : CMRAMixin (one_shot A).
Proof.
split.
- intros n []; destruct 1; constructor; by cofe_subst.
@@ -174,7 +173,7 @@ Proof.
+ intros _. exists (Shot (core a2)). by constructor.
- intros n [|a1| |] [|a2| |]; simpl; eauto using cmra_validN_op_l; done.
- intros n [|a| |] y1 y2 Hx Hx'; last 2 first.
- + by exists (∅, ∅); destruct y1, y2; inversion_clear Hx'.
+ + by exists (OneShotUnit, OneShotUnit); destruct y1, y2; inversion_clear Hx'.
+ by exists (OneShotBot, OneShotBot); destruct y1, y2; inversion_clear Hx'.
+ destruct y1, y2; try (exfalso; by inversion_clear Hx').
* by exists (OneShotPending, OneShotUnit).
@@ -183,19 +182,23 @@ Proof.
* apply (inj Shot) in Hx'.
destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto.
exists (Shot z1, Shot z2). by repeat constructor.
- * exists (Shot a, ∅). inversion_clear Hx'. by repeat constructor.
- * exists (∅, Shot a). inversion_clear Hx'. by repeat constructor.
+ * exists (Shot a, OneShotUnit). inversion_clear Hx'. by repeat constructor.
+ * exists (OneShotUnit, Shot a). inversion_clear Hx'. by repeat constructor.
Qed.
-Canonical Structure one_shotR : cmraT :=
+Canonical Structure one_shotR :=
CMRAT (one_shot A) one_shot_cofe_mixin one_shot_cmra_mixin.
-Global Instance one_shot_cmra_unit : CMRAUnit one_shotR.
-Proof. split. done. by intros []. apply _. Qed.
Global Instance one_shot_cmra_discrete : CMRADiscrete A → CMRADiscrete one_shotR.
Proof.
split; first apply _.
intros [|a| |]; simpl; auto using cmra_discrete_valid.
Qed.
+Instance one_shot_empty : Empty (one_shot A) := OneShotUnit.
+Lemma one_shot_ucmra_mixin : UCMRAMixin (one_shot A).
+Proof. split. done. by intros []. apply _. Qed.
+Canonical Structure one_shotUR :=
+ UCMRAT (one_shot A) one_shot_cofe_mixin one_shot_cmra_mixin one_shot_ucmra_mixin.
+
Global Instance Shot_persistent a : Persistent a → Persistent (Shot a).
Proof. by constructor. Qed.
@@ -254,6 +257,7 @@ Proof. eauto using one_shot_updateP. Qed.
End cmra.
Arguments one_shotR : clear implicits.
+Arguments one_shotUR : clear implicits.
(* Functor *)
Instance one_shot_map_cmra_monotone {A B : cmraT} (f : A → B) :
@@ -262,7 +266,7 @@ Proof.
split; try apply _.
- intros n [|a| |]; simpl; auto using validN_preserving.
- intros [|a1| |] [|a2| |] [[|a3| |] Hx];
- inversion Hx; setoid_subst; try apply cmra_unit_least;
+ inversion Hx; setoid_subst; try apply: ucmra_unit_least;
try apply one_shot_bot_largest; auto; [].
destruct (included_preserving f a1 (a1 â‹… a3)) as [b ?].
{ by apply cmra_included_l. }
@@ -290,3 +294,25 @@ Instance one_shotRF_contractive F :
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_contractive.
Qed.
+
+Program Definition one_shotURF (F : rFunctor) : urFunctor := {|
+ urFunctor_car A B := one_shotUR (rFunctor_car F A B);
+ urFunctor_map A1 A2 B1 B2 fg := one_shotC_map (rFunctor_map F fg)
+|}.
+Next Obligation.
+ by intros F A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_ne.
+Qed.
+Next Obligation.
+ intros F A B x. rewrite /= -{2}(one_shot_map_id x).
+ apply one_shot_map_ext=>y; apply rFunctor_id.
+Qed.
+Next Obligation.
+ intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -one_shot_map_compose.
+ apply one_shot_map_ext=>y; apply rFunctor_compose.
+Qed.
+
+Instance one_shotURF_contractive F :
+ rFunctorContractive F → urFunctorContractive (one_shotURF F).
+Proof.
+ by intros ? A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_contractive.
+Qed.
diff --git a/algebra/upred.v b/algebra/upred.v
index 046b13b39..c576c0cc1 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -3,7 +3,7 @@ Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
Local Hint Extern 10 (_ ≤ _) => omega.
-Record uPred (M : cmraT) : Type := IProp {
+Record uPred (M : ucmraT) : Type := IProp {
uPred_holds :> nat → M → Prop;
uPred_ne n x1 x2 : uPred_holds n x1 → x1 ≡{n}≡ x2 → uPred_holds n x2;
uPred_weaken n1 n2 x1 x2 :
@@ -18,7 +18,7 @@ Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.
Section cofe.
- Context {M : cmraT}.
+ Context {M : ucmraT}.
Inductive uPred_equiv' (P Q : uPred M) : Prop :=
{ uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
@@ -64,32 +64,32 @@ Lemma uPred_weaken' {M} (P : uPred M) n1 n2 x1 x2 :
Proof. eauto using uPred_weaken. Qed.
(** functor *)
-Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
+Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
`{!CMRAMonotone f} (P : uPred M1) :
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
Next Obligation.
naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Qed.
-Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
+Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
`{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
intros x1 x2 Hx; split=> n' y ??.
split; apply Hx; auto using validN_preserving.
Qed.
-Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P ≡ P.
+Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P ≡ P.
Proof. by split=> n x ?. Qed.
-Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
+Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
`{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
Proof. by split=> n x Hx. Qed.
-Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
+Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
`{!CMRAMonotone f} `{!CMRAMonotone g}:
(∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
-Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
+Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
-Lemma uPredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
+Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
`{!CMRAMonotone f, !CMRAMonotone g} n :
f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
Proof.
@@ -97,28 +97,28 @@ Proof.
rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Qed.
-Program Definition uPredCF (F : rFunctor) : cFunctor := {|
- cFunctor_car A B := uPredC (rFunctor_car F B A);
- cFunctor_map A1 A2 B1 B2 fg := uPredC_map (rFunctor_map F (fg.2, fg.1))
+Program Definition uPredCF (F : urFunctor) : cFunctor := {|
+ cFunctor_car A B := uPredC (urFunctor_car F B A);
+ cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
|}.
Next Obligation.
intros F A1 A2 B1 B2 n P Q HPQ.
- apply uPredC_map_ne, rFunctor_ne; split; by apply HPQ.
+ apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
Qed.
Next Obligation.
intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
- apply uPred_map_ext=>y. by rewrite rFunctor_id.
+ apply uPred_map_ext=>y. by rewrite urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
- apply uPred_map_ext=>y; apply rFunctor_compose.
+ apply uPred_map_ext=>y; apply urFunctor_compose.
Qed.
Instance uPredCF_contractive F :
- rFunctorContractive F → cFunctorContractive (uPredCF F).
+ urFunctorContractive F → cFunctorContractive (uPredCF F).
Proof.
intros ? A1 A2 B1 B2 n P Q HPQ.
- apply uPredC_map_ne, rFunctor_contractive=> i ?; split; by apply HPQ.
+ apply uPredC_map_ne, urFunctor_contractive=> i ?; split; by apply HPQ.
Qed.
(** logical entailement *)
@@ -249,7 +249,7 @@ Definition uPred_later {M} := proj1_sig uPred_later_aux M.
Definition uPred_later_eq :
@uPred_later = @uPred_later_def := proj2_sig uPred_later_aux.
-Program Definition uPred_ownM_def {M : cmraT} (a : M) : uPred M :=
+Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
{| uPred_holds n x := a ≼{n} x |}.
Next Obligation. by intros M a n x1 x2 [a' ?] Hx; exists a'; rewrite -Hx. Qed.
Next Obligation.
@@ -261,7 +261,7 @@ Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M.
Definition uPred_ownM_eq :
@uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux.
-Program Definition uPred_valid_def {M A : cmraT} (a : A) : uPred M :=
+Program Definition uPred_valid_def {M : ucmraT} {A : cmraT} (a : A) : uPred M :=
{| uPred_holds n x := ✓{n} a |}.
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Definition uPred_valid_aux : { x | x = @uPred_valid_def }. by eexists. Qed.
@@ -324,7 +324,7 @@ Definition unseal :=
Ltac unseal := rewrite !unseal.
Section uPred_logic.
-Context {M : cmraT}.
+Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
@@ -511,11 +511,10 @@ Proof.
- by symmetry; apply Hab with x.
- by apply Ha.
Qed.
-Lemma eq_equiv `{Empty M, !CMRAUnit M} {A : cofeT} (a b : A) :
- True ⊢ (a ≡ b) → a ≡ b.
+Lemma eq_equiv {A : cofeT} (a b : A) : True ⊢ (a ≡ b) → a ≡ b.
Proof.
unseal=> Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
- apply cmra_valid_validN, cmra_unit_valid.
+ apply cmra_valid_validN, ucmra_unit_valid.
Qed.
Lemma eq_rewrite_contractive {A : cofeT} a b (Ψ : A → uPred M) P
{HΨ : Contractive Ψ} : P ⊢ ▷ (a ≡ b) → P ⊢ Ψ a → P ⊢ Ψ b.
@@ -1045,7 +1044,7 @@ Lemma always_ownM (a : M) : Persistent a → (□ uPred_ownM a) ⊣⊢ uPred_own
Proof. intros. by rewrite -(persistent a) always_ownM_core. Qed.
Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a.
Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
-Lemma ownM_empty `{Empty M, !CMRAUnit M} : True ⊢ uPred_ownM ∅.
+Lemma ownM_empty : True ⊢ uPred_ownM ∅.
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
(* Valid *)
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index d7b34262d..f76f90338 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -48,7 +48,7 @@ Arguments persistentL {_} _ {_}.
(** * Properties *)
Section big_op.
-Context {M : cmraT}.
+Context {M : ucmraT}.
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.
diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index 7a360b638..89210107e 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -3,7 +3,7 @@ From iris.algebra Require Export upred_big_op.
Import uPred.
Module uPred_reflection. Section uPred_reflection.
- Context {M : cmraT}.
+ Context {M : ucmraT}.
Inductive expr :=
| ETrue : expr
@@ -210,7 +210,7 @@ Class StripLaterL {M} (P Q : uPred M) := strip_later_l : ▷ Q ⊢ P.
Arguments strip_later_l {_} _ _ {_}.
Section strip_later.
-Context {M : cmraT}.
+Context {M : ucmraT}.
Implicit Types P Q : uPred M.
Global Instance strip_later_r_fallthrough P : StripLaterR P P | 1000.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index cd105a28b..9a2cac7a9 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -8,18 +8,18 @@ Import uPred.
a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
predicates over finmaps instead of just ownP. *)
-Definition heapR : cmraT := gmapR loc (fracR (dec_agreeR val)).
+Definition heapUR : ucmraT := gmapUR loc (fracR (dec_agreeR val)).
(** The CMRA we need. *)
Class heapG Σ := HeapG {
- heap_inG :> authG heap_lang Σ heapR;
+ heap_inG :> authG heap_lang Σ heapUR;
heap_name : gname
}.
(** The Functor we need. *)
-Definition heapGF : gFunctor := authGF heapR.
+Definition heapGF : gFunctor := authGF heapUR.
-Definition to_heap : state → heapR := fmap (λ v, Frac 1 (DecAgree v)).
-Definition of_heap : heapR → state :=
+Definition to_heap : state → heapUR := fmap (λ v, Frac 1 (DecAgree v)).
+Definition of_heap : heapUR → state :=
omap (mbind (maybe DecAgree ∘ snd) ∘ maybe2 Frac).
Section definitions.
@@ -27,7 +27,7 @@ Section definitions.
Definition heap_mapsto (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l := Frac q (DecAgree v) ]}.
- Definition heap_inv (h : heapR) : iPropG heap_lang Σ :=
+ Definition heap_inv (h : heapUR) : iPropG heap_lang Σ :=
ownP (of_heap h).
Definition heap_ctx (N : namespace) : iPropG heap_lang Σ :=
auth_ctx heap_name N heap_inv.
@@ -49,7 +49,7 @@ Section heap.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
Implicit Types σ : state.
- Implicit Types h g : heapR.
+ Implicit Types h g : heapUR.
(** Conversion to heaps and back *)
Global Instance of_heap_proper : Proper ((≡) ==> (=)) of_heap.
@@ -73,7 +73,7 @@ Section heap.
case _:(h !! l)=>[[q' [v'|]|]|] //=; last by move=> [??].
move=> [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp.
- rewrite /of_heap lookup_insert_ne // !lookup_omap.
- by rewrite (lookup_op _ h) lookup_singleton_ne // left_id.
+ by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
Qed.
Lemma to_heap_insert l v σ :
to_heap (<[l:=v]> σ) = <[l:=Frac 1 (DecAgree v)]> (to_heap σ).
@@ -97,7 +97,7 @@ Section heap.
(** Allocation *)
Lemma heap_alloc N E σ :
- authG heap_lang Σ heapR → nclose N ⊆ E →
+ authG heap_lang Σ heapUR → nclose N ⊆ E →
ownP σ ⊢ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ [★ map] l↦v ∈ σ, l ↦ v).
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index b57a9ea5c..9cf514794 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -10,7 +10,7 @@ Context {Σ : gFunctors} `{heapG Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
-Implicit Types Δ : envs (iResR heap_lang (globalF Σ)).
+Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
Global Instance sep_destruct_mapsto l q v :
SepDestruct false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 460f89b10..e1c79a436 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -4,16 +4,15 @@ From iris.proofmode Require Import invariants ghost_ownership.
Import uPred.
(* The CMRA we need. *)
-Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
+Class authG Λ Σ (A : ucmraT) := AuthG {
auth_inG :> inG Λ Σ (authR A);
- auth_identity :> CMRAUnit A;
auth_timeless :> CMRADiscrete A;
}.
(* The Functor we need. *)
-Definition authGF (A : cmraT) : gFunctor := GFunctor (constRF (authR A)).
+Definition authGF (A : ucmraT) : gFunctor := GFunctor (constRF (authR A)).
(* Show and register that they match. *)
-Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
- `{CMRAUnit A, CMRADiscrete A} : authG Λ Σ A.
+Instance authGF_inGF (A : ucmraT) `{inGF Λ Σ (authGF A)}
+ `{CMRADiscrete A} : authG Λ Σ A.
Proof. split; try apply _. apply: inGF_inG. Qed.
Section definitions.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 8ffab0a81..dab866204 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -14,19 +14,6 @@ Section global.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.
-(** * Transport empty *)
-Instance inG_empty `{Empty A} :
- Empty (projT2 Σ (inG_id i) (iPreProp Λ (globalF Σ))) :=
- cmra_transport inG_prf ∅.
-Instance inG_empty_spec `{Empty A} :
- CMRAUnit A → CMRAUnit (projT2 Σ (inG_id i) (iPreProp Λ (globalF Σ))).
-Proof.
- split.
- - apply cmra_transport_valid, cmra_unit_valid.
- - intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
- - apply _.
-Qed.
-
(** * Properties of own *)
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
Proof. solve_proper. Qed.
@@ -90,13 +77,17 @@ Proof.
intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
Qed.
+End global.
-Lemma own_empty `{Empty A, !CMRAUnit A} γ E : True ⊢ (|={E}=> own γ ∅).
+Section global_empty.
+Context `{i : inG Λ Σ (A:ucmraT)}.
+Implicit Types a : A.
+
+Lemma own_empty γ E : True ⊢ (|={E}=> own γ ∅).
Proof.
- rewrite ownG_empty /own. apply pvs_ownG_update, cmra_update_updateP.
- eapply iprod_singleton_updateP_empty;
- first by eapply singleton_updateP_empty', cmra_transport_updateP',
- cmra_update_updateP, cmra_update_unit.
- naive_solver.
+ rewrite ownG_empty /own. apply pvs_ownG_update, iprod_singleton_update_empty.
+ apply (singleton_update_unit (cmra_transport inG_prf ∅)); last done.
+ - apply cmra_transport_valid, ucmra_unit_valid.
+ - intros x; destruct inG_prf. by rewrite left_id.
Qed.
-End global.
+End global_empty.
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index 002255015..b9cdfe063 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -18,7 +18,7 @@ Definition gid (Σ : gFunctors) := fin (projT1 Σ).
Definition gname := positive.
Definition globalF (Σ : gFunctors) : iFunctor :=
- IFunctor (iprodRF (λ i, gmapRF gname (projT2 Σ i))).
+ IFunctor (iprodURF (λ i, gmapURF gname (projT2 Σ i))).
Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
diff --git a/program_logic/model.v b/program_logic/model.v
index 8c8a0aea5..5daecb065 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -7,22 +7,20 @@ from the category of COFEs to the category of CMRAs, which is instantiated
with [iProp]. The [iProp] can be used to construct impredicate CMRAs, such as
the stored propositions using the agreement CMRA. *)
Structure iFunctor := IFunctor {
- iFunctor_F :> rFunctor;
- iFunctor_contractive : rFunctorContractive iFunctor_F;
- iFunctor_empty (A : cofeT) : Empty (iFunctor_F A);
- iFunctor_identity (A : cofeT) : CMRAUnit (iFunctor_F A);
+ iFunctor_F :> urFunctor;
+ iFunctor_contractive : urFunctorContractive iFunctor_F
}.
-Arguments IFunctor _ {_ _ _}.
-Existing Instances iFunctor_contractive iFunctor_empty iFunctor_identity.
+Arguments IFunctor _ {_}.
+Existing Instances iFunctor_contractive.
Module Type iProp_solution_sig.
Parameter iPreProp : language → iFunctor → cofeT.
-Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ).
+Definition iGst (Λ : language) (Σ : iFunctor) : ucmraT := Σ (iPreProp Λ Σ).
Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
-Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
+Definition iResUR Λ Σ := resUR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
Definition iPst Λ := excl (state Λ).
-Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ).
+Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResUR Λ Σ).
Parameter iProp_unfold: ∀ {Λ Σ}, iProp Λ Σ -n> iPreProp Λ Σ.
Parameter iProp_fold: ∀ {Λ Σ}, iPreProp Λ Σ -n> iProp Λ Σ.
@@ -35,16 +33,16 @@ End iProp_solution_sig.
Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver.
Definition iProp_result (Λ : language) (Σ : iFunctor) :
- solution (uPredCF (resRF Λ (▶ ∙) Σ)) := solver.result _.
+ solution (uPredCF (resURF Λ (▶ ∙) Σ)) := solver.result _.
Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp_result Λ Σ.
-Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ).
+Definition iGst (Λ : language) (Σ : iFunctor) : ucmraT := Σ (iPreProp Λ Σ).
Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
-Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
+Definition iResUR Λ Σ := resUR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
Definition iPst Λ := excl (state Λ).
-Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ).
+Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResUR Λ Σ).
Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ :=
solution_fold (iProp_result Λ Σ).
Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
@@ -59,6 +57,5 @@ Bind Scope uPred_scope with iProp.
Instance iProp_fold_inj n Λ Σ : Inj (dist n) (dist n) (@iProp_fold Λ Σ).
Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
-Instance iProp_unfold_inj n Λ Σ :
- Inj (dist n) (dist n) (@iProp_unfold Λ Σ).
+Instance iProp_unfold_inj n Λ Σ : Inj (dist n) (dist n) (@iProp_unfold Λ Σ).
Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index cffff257a..3127a5b2b 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -50,7 +50,7 @@ Proof. rewrite /ownG uPred.ownM_valid res_validI /=; auto with I. Qed.
Lemma ownG_valid_r m : ownG m ⊢ (ownG m ★ ✓ m).
Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
Lemma ownG_empty : True ⊢ (ownG ∅ : iProp Λ Σ).
-Proof. apply uPred.ownM_empty. Qed.
+Proof. apply: uPred.ownM_empty. Qed.
Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownG_persistent m : Persistent m → PersistentP (ownG m).
@@ -66,17 +66,17 @@ Proof.
- intros [(P'&Hi&HP) _]; rewrite Hi.
constructor; symmetry; apply agree_valid_includedN; last done.
by apply lookup_validN_Some with (wld r) i.
- - intros ?; split_and?; try apply cmra_unit_leastN; eauto.
+ - intros ?; split_and?; try apply ucmra_unit_leastN; eauto.
Qed.
Lemma ownP_spec n r σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡ Excl σ.
Proof.
intros (?&?&?). rewrite /ownP; uPred.unseal.
rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
- rewrite (timeless_iff n). naive_solver (apply cmra_unit_leastN).
+ rewrite (timeless_iff n). naive_solver (apply ucmra_unit_leastN).
Qed.
Lemma ownG_spec n r m : (ownG m) n r ↔ m ≼{n} gst r.
Proof.
rewrite /ownG; uPred.unseal.
- rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_unit_leastN).
+ rewrite /uPred_holds /= res_includedN; naive_solver (apply ucmra_unit_leastN).
Qed.
End ownership.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index c07686035..d03e671f5 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -18,7 +18,7 @@ Instance: Params (@pst) 3.
Instance: Params (@gst) 3.
Section res.
-Context {Λ : language} {A : cofeT} {M : cmraT}.
+Context {Λ : language} {A : cofeT} {M : ucmraT}.
Implicit Types r : res Λ A M.
Inductive res_equiv' (r1 r2 : res Λ A M) := Res_equiv :
@@ -69,11 +69,10 @@ Qed.
Canonical Structure resC : cofeT := CofeT (res Λ A M) res_cofe_mixin.
Global Instance res_timeless r :
Timeless (wld r) → Timeless (gst r) → Timeless r.
-Proof. by destruct 3; constructor; try apply: timeless. Qed.
+Proof. destruct 3; constructor; by apply (timeless _). Qed.
Instance res_op : Op (res Λ A M) := λ r1 r2,
Res (wld r1 â‹… wld r2) (pst r1 â‹… pst r2) (gst r1 â‹… gst r2).
-Global Instance res_empty `{Empty M} : Empty (res Λ A M) := Res ∅ ∅ ∅.
Instance res_core : Core (res Λ A M) := λ r,
Res (core (wld r)) (core (pst r)) (core (gst r)).
Instance res_valid : Valid (res Λ A M) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
@@ -118,15 +117,19 @@ Proof.
(cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
by exists (Res w σ m, Res w' σ' m').
Qed.
-Canonical Structure resR : cmraT :=
+Canonical Structure resR :=
CMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin.
-Global Instance res_cmra_unit `{CMRAUnit M} : CMRAUnit resR.
+
+Instance res_empty : Empty (res Λ A M) := Res ∅ ∅ ∅.
+Definition res_ucmra_mixin : UCMRAMixin (res Λ A M).
Proof.
split.
- - split_and!; apply cmra_unit_valid.
+ - split_and!; apply ucmra_unit_valid.
- by split; rewrite /= left_id.
- apply _.
Qed.
+Canonical Structure resUR :=
+ UCMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin res_ucmra_mixin.
Definition update_pst (σ : state Λ) (r : res Λ A M) : res Λ A M :=
Res (wld r) (Excl σ) (gst r).
@@ -153,7 +156,7 @@ Lemma lookup_wld_op_r n r1 r2 i P :
✓{n} (r1⋅r2) → wld r2 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
Global Instance Res_timeless eσ m : Timeless m → Timeless (@Res Λ A M ∅ eσ m).
-Proof. by intros ? ? [???]; constructor; apply: timeless. Qed.
+Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
Global Instance Res_persistent w m: Persistent m → Persistent (@Res Λ A M w ∅ m).
Proof. constructor; apply (persistent _). Qed.
@@ -170,38 +173,39 @@ End res.
Arguments resC : clear implicits.
Arguments resR : clear implicits.
+Arguments resUR : clear implicits.
(* Functor *)
Definition res_map {Λ} {A A' : cofeT} {M M' : cmraT}
(f : A → A') (g : M → M') (r : res Λ A M) : res Λ A' M' :=
Res (agree_map f <$> wld r) (pst r) (g $ gst r).
-Instance res_map_ne {Λ} {A A': cofeT} {M M' : cmraT} (f : A → A') (g : M → M') :
+Instance res_map_ne {Λ} {A A': cofeT} {M M' : ucmraT} (f : A → A') (g : M → M'):
(∀ n, Proper (dist n ==> dist n) f) → (∀ n, Proper (dist n ==> dist n) g) →
∀ n, Proper (dist n ==> dist n) (@res_map Λ _ _ _ _ f g).
Proof. intros Hf n [] ? [???]; constructor; by cofe_subst. Qed.
-Lemma res_map_id {Λ A M} (r : res Λ A M) : res_map id id r ≡ r.
+Lemma res_map_id {Λ A} {M : ucmraT} (r : res Λ A M) : res_map id id r ≡ r.
Proof.
constructor; rewrite /res_map /=; f_equal.
- - rewrite -{2}(map_fmap_id (wld r)). apply map_fmap_setoid_ext=> i y ? /=.
- by rewrite -{2}(agree_map_id y).
+ rewrite -{2}(map_fmap_id (wld r)). apply map_fmap_setoid_ext=> i y ? /=.
+ by rewrite -{2}(agree_map_id y).
Qed.
-Lemma res_map_compose {Λ} {A1 A2 A3 : cofeT} {M1 M2 M3 : cmraT}
+Lemma res_map_compose {Λ} {A1 A2 A3 : cofeT} {M1 M2 M3 : ucmraT}
(f : A1 → A2) (f' : A2 → A3) (g : M1 → M2) (g' : M2 → M3) (r : res Λ A1 M1) :
res_map (f' ∘ f) (g' ∘ g) r ≡ res_map f' g' (res_map f g r).
Proof.
constructor; rewrite /res_map /=; f_equal.
- - rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
- by rewrite -agree_map_compose.
+ rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
+ by rewrite -agree_map_compose.
Qed.
-Lemma res_map_ext {Λ} {A A' : cofeT} {M M' : cmraT}
+Lemma res_map_ext {Λ} {A A' : cofeT} {M M' : ucmraT}
(f f' : A → A') (g g' : M → M') (r : res Λ A M) :
(∀ x, f x ≡ f' x) → (∀ m, g m ≡ g' m) → res_map f g r ≡ res_map f' g' r.
Proof.
intros Hf Hg; split; simpl; auto.
- - by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
+ by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
Qed.
Instance res_map_cmra_monotone {Λ}
- {A A' : cofeT} {M M': cmraT} (f: A → A') (g: M → M') :
+ {A A' : cofeT} {M M': ucmraT} (f: A → A') (g: M → M') :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone g →
CMRAMonotone (@res_map Λ _ _ _ _ f g).
Proof.
@@ -210,40 +214,40 @@ Proof.
- by intros r1 r2; rewrite !res_included;
intros (?&?&?); split_and!; simpl; try apply: included_preserving.
Qed.
-Definition resC_map {Λ} {A A' : cofeT} {M M' : cmraT}
+Definition resC_map {Λ} {A A' : cofeT} {M M' : ucmraT}
(f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=
CofeMor (res_map f g : resC Λ A M → resC Λ A' M').
Instance resC_map_ne {Λ A A' M M'} n :
Proper (dist n ==> dist n ==> dist n) (@resC_map Λ A A' M M').
Proof.
intros f g Hfg r; split; simpl; auto.
- - by apply (gmapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
+ by apply (gmapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
Qed.
-Program Definition resRF (Λ : language)
- (F1 : cFunctor) (F2 : rFunctor) : rFunctor := {|
- rFunctor_car A B := resR Λ (cFunctor_car F1 A B) (rFunctor_car F2 A B);
- rFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F1 fg) (rFunctor_map F2 fg)
+Program Definition resURF (Λ : language)
+ (F1 : cFunctor) (F2 : urFunctor) : urFunctor := {|
+ urFunctor_car A B := resUR Λ (cFunctor_car F1 A B) (urFunctor_car F2 A B);
+ urFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F1 fg) (urFunctor_map F2 fg)
|}.
Next Obligation.
intros Λ F1 F2 A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
- by apply cFunctor_ne.
- - by apply rFunctor_ne.
+ - by apply urFunctor_ne.
Qed.
Next Obligation.
intros Λ F Σ A B x. rewrite /= -{2}(res_map_id x).
- apply res_map_ext=>y. apply cFunctor_id. apply rFunctor_id.
+ apply res_map_ext=>y. apply cFunctor_id. apply urFunctor_id.
Qed.
Next Obligation.
intros Λ F Σ A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -res_map_compose.
- apply res_map_ext=>y. apply cFunctor_compose. apply rFunctor_compose.
+ apply res_map_ext=>y. apply cFunctor_compose. apply urFunctor_compose.
Qed.
Instance resRF_contractive Λ F1 F2 :
- cFunctorContractive F1 → rFunctorContractive F2 →
- rFunctorContractive (resRF Λ F1 F2).
+ cFunctorContractive F1 → urFunctorContractive F2 →
+ urFunctorContractive (resURF Λ F1 F2).
Proof.
intros ?? A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
- by apply cFunctor_contractive.
- - by apply rFunctor_contractive.
+ - by apply urFunctor_contractive.
Qed.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index aff248a17..2f3fdd2c8 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -112,7 +112,7 @@ Proof. by intros; apply vs_alt, own_updateP. Qed.
Lemma vs_update E γ a a' : a ~~> a' → own γ a ={E}=> own γ a'.
Proof. by intros; apply vs_alt, own_update. Qed.
+End vs_ghost.
-Lemma vs_own_empty `{Empty A, !CMRAUnit A} E γ : True ={E}=> own γ ∅.
+Lemma vs_own_empty `{inG Λ Σ (A:ucmraT)} E γ : True ={E}=> own γ ∅.
Proof. by intros; eapply vs_alt, own_empty. Qed.
-End vs_ghost.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 9a9a4dfb3..7a308038c 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -11,7 +11,7 @@ Local Notation "' ( x1 , x2 ) ↠y ; z" :=
Local Notation "' ( x1 , x2 , x3 ) ↠y ; z" :=
(match y with Some (x1,x2,x3) => z | None => None end).
-Record envs (M : cmraT) :=
+Record envs (M : ucmraT) :=
Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
Add Printing Constructor envs.
Arguments Envs {_} _ _.
@@ -96,7 +96,7 @@ Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
(* Coq versions of the tactics *)
Section tactics.
-Context {M : cmraT}.
+Context {M : ucmraT}.
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index a74ee879e..e82db494e 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import pviewshifts invariants.
-Lemma demo_0 {M : cmraT} (P Q : uPred M) :
+Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
□ (P ∨ Q) ⊢ ((∀ x, x = 0 ∨ x = 1) → (Q ∨ P)).
Proof.
iIntros "#H #H2".
@@ -11,7 +11,7 @@ Proof.
iDestruct ("H2" $! 10) as "[%|%]". done. done.
Qed.
-Lemma demo_1 (M : cmraT) (P1 P2 P3 : nat → uPred M) :
+Lemma demo_1 (M : ucmraT) (P1 P2 P3 : nat → uPred M) :
True ⊢ (∀ (x y : nat) a b,
x ≡ y →
□ (uPred_ownM (a ⋅ b) -★
@@ -36,7 +36,7 @@ Proof.
- done.
Qed.
-Lemma demo_2 (M : cmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat → uPredC M):
+Lemma demo_2 (M : ucmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat → uPredC M):
(P2 ★ (P3 ★ Q) ★ True ★ P1 ★ P2 ★ (P4 ★ (∃ x:nat, P5 x ∨ P3)) ★ True)
⊢ (P1 -★ (True ★ True) -★ (((P2 ∧ False ∨ P2 ∧ 0 = 0) ★ P3) ★ Q ★ P1 ★ True) ∧
(P2 ∨ False) ∧ (False → P5 0)).
@@ -53,17 +53,17 @@ Proof.
* iSplitL "HQ". iAssumption. by iSplitL "H1".
Qed.
-Lemma demo_3 (M : cmraT) (P1 P2 P3 : uPred M) :
+Lemma demo_3 (M : ucmraT) (P1 P2 P3 : uPred M) :
(P1 ★ P2 ★ P3) ⊢ (▷ P1 ★ ▷ (P2 ★ ∃ x, (P3 ∧ x = 0) ∨ P3)).
Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.
Definition foo {M} (P : uPred M) := (P → P)%I.
Definition bar {M} : uPred M := (∀ P, foo P)%I.
-Lemma demo_4 (M : cmraT) : True ⊢ @bar M.
+Lemma demo_4 (M : ucmraT) : True ⊢ @bar M.
Proof. iIntros. iIntros {P} "HP". done. Qed.
-Lemma demo_5 (M : cmraT) (x y : M) (P : uPred M) :
+Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
(∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)).
Proof.
iIntros "H1 H2".
@@ -72,7 +72,7 @@ Proof.
iApply uPred.eq_refl.
Qed.
-Lemma demo_6 (M : cmraT) (P Q : uPred M) :
+Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
True ⊢ (∀ x y z : nat,
x = plus 0 x → y = 0 → z = 0 → P → □ Q → foo (x ≡ x)).
Proof.
--
GitLab