From cca375a0525aae3bc8e2a092b832a34c97c41124 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Jun 2016 09:54:45 +0200
Subject: [PATCH] Make local updates relational.
---
algebra/auth.v | 41 ++---------
algebra/cmra.v | 4 ++
algebra/gmap.v | 163 +++++++++++++++++++++++++-----------------
algebra/list.v | 31 +++++---
algebra/updates.v | 114 +++++++++++++++--------------
heap_lang/heap.v | 55 +++++++-------
program_logic/auth.v | 36 +++-------
program_logic/boxes.v | 9 +--
8 files changed, 225 insertions(+), 228 deletions(-)
diff --git a/algebra/auth.v b/algebra/auth.v
index 8ab3307cd..702dacff9 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -179,42 +179,15 @@ Proof. done. Qed.
Lemma auth_both_op a b : Auth (Excl' a) b ≡ ◠a ⋅ ◯ b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
-Lemma auth_update a a' b b' :
- (∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b) →
- â— a â‹… â—¯ a' ~~> â— b â‹… â—¯ b'.
+Lemma auth_update a af b :
+ a ~l~> b @ Some af →
+ â— (a â‹… af) â‹… â—¯ a ~~> â— (b â‹… af) â‹… â—¯ b.
Proof.
- intros Hab; apply cmra_total_update.
+ intros [Hab Hab']; apply cmra_total_update.
move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
- destruct (Hab n (bf1 â‹… bf2)) as [Ha' ?]; auto.
- { by rewrite Ha left_id assoc. }
- split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done].
-Qed.
-
-Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
- Lv a → ✓ L a' →
- â— a' â‹… â—¯ a ~~> â— L a' â‹… â—¯ L a.
-Proof.
- intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
- by rewrite EQ (local_updateN L) // -EQ.
-Qed.
-
-Lemma auth_update_op_l a a' b :
- ✓ (b ⋅ a) → ◠a ⋅ ◯ a' ~~> ◠(b ⋅ a) ⋅ ◯ (b ⋅ a').
-Proof. by intros; apply (auth_local_update _). Qed.
-Lemma auth_update_op_r a a' b :
- ✓ (a ⋅ b) → ◠a ⋅ ◯ a' ~~> ◠(a ⋅ b) ⋅ ◯ (a' ⋅ b).
-Proof. rewrite -!(comm _ b); apply auth_update_op_l. Qed.
-
-(* This does not seem to follow from auth_local_update.
- The trouble is that given ✓ (L a ⋅ a'), Lv a
- we need ✓ (a ⋅ a'). I think this should hold for every local update,
- but adding an extra axiom to local updates just for this is silly. *)
-Lemma auth_local_update_l L `{!LocalUpdate Lv L} a a' :
- Lv a → ✓ (L a ⋅ a') →
- â— (a â‹… a') â‹… â—¯ a ~~> â— (L a â‹… a') â‹… â—¯ L a.
-Proof.
- intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
- by rewrite -(local_updateN L) // EQ -(local_updateN L) // -EQ.
+ move: Ha; rewrite !left_id=> Hm; split; auto.
+ exists bf2. rewrite -assoc.
+ apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
Qed.
End cmra.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index e0f371e39..1b5323bb2 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -326,6 +326,8 @@ Lemma exclusive_l x `{!Exclusive x} y : ✓ (x ⋅ y) → False.
Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
Proof. rewrite comm. by apply exclusive_l. Qed.
+Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
+Proof. destruct my. move=> /(exclusiveN_l _ x) []. done. Qed.
(** ** Order *)
Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
@@ -965,6 +967,8 @@ Section option.
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 Some_op_opM x my : Some x â‹… my = Some (x â‹…? my).
+ Proof. by destruct my. Qed.
Lemma option_included (mx my : option A) :
mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ (x ≼ y ∨ x ≡ y).
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 58749181f..5b5c3bad8 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -184,7 +184,10 @@ Section properties.
Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K A.
Implicit Types i : K.
-Implicit Types a : A.
+Implicit Types x y : A.
+
+Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)).
+Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
Lemma lookup_validN_Some n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x.
Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
@@ -281,82 +284,108 @@ Proof. apply insert_updateP'. Qed.
Lemma singleton_update i (x y : A) : x ~~> y → {[ i := x ]} ~~> {[ i := y ]}.
Proof. apply insert_update. Qed.
-Section freshness.
-Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
- ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
+Lemma delete_update m i : m ~~> delete i m.
Proof.
- intros ? HQ. apply cmra_total_updateP.
- intros n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
- assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]].
- { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
- exists (<[i:=x]>m); split.
- { by apply HQ; last done; apply not_elem_of_dom. }
- rewrite insert_singleton_opN; last by apply not_elem_of_dom.
- rewrite -assoc -insert_singleton_opN;
- last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
- by apply insert_validN; [apply cmra_valid_validN|].
+ apply cmra_total_update=> n mf Hm j; destruct (decide (i = j)); subst.
+ - move: (Hm j). rewrite !lookup_op lookup_delete left_id.
+ apply cmra_validN_op_r.
+ - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
Qed.
-Lemma alloc_updateP (Q : gmap K A → Prop) m x :
- ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
-Proof. move=>??. eapply alloc_updateP_strong with (I:=∅); by eauto. Qed.
-Lemma alloc_updateP_strong' m x (I : gset K) :
- ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None.
-Proof. eauto using alloc_updateP_strong. Qed.
-Lemma alloc_updateP' m x :
- ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
-Proof. eauto using alloc_updateP. Qed.
-
-Lemma 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. apply cmra_total_updateP=> n gf Hg.
- destruct (Hx n (gf !! i)) as (y&?&Hy).
- { move:(Hg i). rewrite !left_id.
- case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
- intros; by apply cmra_valid_validN. }
- exists {[ i := y ]}; split; first by auto.
- intros i'; destruct (decide (i' = i)) as [->|].
- - rewrite lookup_op lookup_singleton.
- move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
- - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
-Qed.
-Lemma 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 ]}.
+
+Section freshness.
+ Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
+ Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
+ ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
+ Proof.
+ intros ? HQ. apply cmra_total_updateP.
+ intros n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
+ assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]].
+ { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
+ exists (<[i:=x]>m); split.
+ { by apply HQ; last done; apply not_elem_of_dom. }
+ rewrite insert_singleton_opN; last by apply not_elem_of_dom.
+ rewrite -assoc -insert_singleton_opN;
+ last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
+ by apply insert_validN; [apply cmra_valid_validN|].
+ Qed.
+ Lemma alloc_updateP (Q : gmap K A → Prop) m x :
+ ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
+ Proof. move=>??. eapply alloc_updateP_strong with (I:=∅); by eauto. Qed.
+ Lemma alloc_updateP_strong' m x (I : gset K) :
+ ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None.
+ Proof. eauto using alloc_updateP_strong. Qed.
+ Lemma alloc_updateP' m x :
+ ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
+ Proof. eauto using alloc_updateP. Qed.
+
+ Lemma 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. apply cmra_total_updateP=> n gf Hg.
+ destruct (Hx n (gf !! i)) as (y&?&Hy).
+ { move:(Hg i). rewrite !left_id.
+ case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
+ intros; by apply cmra_valid_validN. }
+ exists {[ i := y ]}; split; first by auto.
+ intros i'; destruct (decide (i' = i)) as [->|].
+ - rewrite lookup_op lookup_singleton.
+ move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
+ - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
+ Qed.
+ Lemma 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.
+
+Lemma insert_local_update m i x y mf :
+ x ~l~> y @ mf ≫= (!! i) → <[i:=x]>m ~l~> <[i:=y]>m @ mf.
Proof.
- rewrite !cmra_update_updateP; eauto using singleton_updateP_unit with subst.
+ intros [Hxy Hxy']; split.
+ - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
+ + rewrite !lookup_opM !lookup_insert !Some_op_opM. apply Hxy.
+ + by rewrite !lookup_opM !lookup_insert_ne.
+ - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
+ destruct (decide (i = j)); subst.
+ + rewrite !lookup_opM !lookup_insert !Some_op_opM !inj_iff. apply Hxy'.
+ + by rewrite !lookup_opM !lookup_insert_ne.
Qed.
-End freshness.
-(* Allocation is a local update: Just use composition with a singleton map. *)
+Lemma singleton_local_update i x y mf :
+ x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf.
+Proof. apply insert_local_update. Qed.
-Global Instance delete_local_update :
- LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Exclusive x) (delete i).
+Lemma alloc_singleton_local_update i x mf :
+ mf ≫= (!! i) = None → ✓ x → ∅ ~l~> {[ i := x ]} @ mf.
Proof.
- split; first apply _.
- intros n m1 m2 (x&Hix&Hv) Hm j; destruct (decide (i = j)) as [<-|].
- - rewrite lookup_delete !lookup_op lookup_delete.
- case Hiy: (m2 !! i)=> [y|]; last constructor.
- destruct (Hv y); apply cmra_validN_le with n; last omega.
- move: (Hm i). by rewrite lookup_op Hix Hiy.
- - by rewrite lookup_op !lookup_delete_ne // lookup_op.
+ intros Hi. split.
+ - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
+ + intros _; rewrite !lookup_opM !lookup_insert !Some_op_opM Hi /=.
+ by apply cmra_valid_validN.
+ + by rewrite !lookup_opM !lookup_insert_ne.
+ - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
+ destruct (decide (i = j)); subst.
+ + intros _. rewrite !lookup_opM !lookup_insert !Hi !lookup_empty !left_id_L.
+ by intros <-.
+ + by rewrite !lookup_opM !lookup_insert_ne.
Qed.
-(* Applying a local update at a position we own is a local update. *)
-Global Instance alter_local_update `{!LocalUpdate Lv L} i :
- LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Lv x) (alter L i).
+Lemma delete_local_update m i x `{!Exclusive x} mf :
+ m !! i = Some x → m ~l~> delete i m @ mf.
Proof.
- split; first apply _.
- intros n m1 m2 (x&Hix&?) Hm j; destruct (decide (i = j)) as [->|].
- - rewrite lookup_alter !lookup_op lookup_alter Hix /=.
- move: (Hm j); rewrite lookup_op Hix.
- case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN L).
- - by rewrite lookup_op !lookup_alter_ne // lookup_op.
+ intros Hx; split; [intros n; apply delete_update|].
+ intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
+ destruct (decide (i = j)); subst.
+ + rewrite !lookup_opM !lookup_delete Hx=> ? Hj.
+ rewrite (exclusiveN_Some_l n x (mf ≫= lookup j)) //.
+ by rewrite (exclusiveN_Some_l n x (mf' ≫= lookup j)) -?Hj.
+ + by rewrite !lookup_opM !lookup_delete_ne.
Qed.
End properties.
diff --git a/algebra/list.v b/algebra/list.v
index 558e4032b..269c65376 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -246,6 +246,9 @@ Section properties.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
+ Lemma list_lookup_opM l mk i : (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i)).
+ Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.
+
Lemma list_op_app l1 l2 l3 :
length l2 ≤ length l1 → (l1 ++ l3) ⋅ l2 = (l1 ⋅ l2) ++ l3.
Proof.
@@ -337,17 +340,25 @@ Section properties.
rewrite !cmra_update_updateP => H; eauto using list_middle_updateP with subst.
Qed.
- (* Applying a local update at a position we own is a local update. *)
- Global Instance list_alter_local_update `{LocalUpdate A Lv L} i :
- LocalUpdate (λ L, ∃ x, L !! i = Some x ∧ Lv x) (alter L i).
+ Lemma list_middle_local_update l1 l2 x y ml :
+ x ~l~> y @ ml ≫= (!! length l1) →
+ l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
Proof.
- split; [apply _|]; intros n l1 l2 (x&Hi1&?) Hm; apply list_dist_lookup=> j.
- destruct (decide (j = i)); subst; last first.
- { by rewrite list_lookup_op !list_lookup_alter_ne // list_lookup_op. }
- rewrite list_lookup_op !list_lookup_alter list_lookup_op Hi1.
- destruct (l2 !! i) as [y|] eqn:Hi2; rewrite Hi2; constructor; auto.
- eapply (local_updateN L), (list_lookup_validN_Some _ _ i); eauto.
- by rewrite list_lookup_op Hi1 Hi2.
+ intros [Hxy Hxy']; split.
+ - intros n; rewrite !list_lookup_validN=> Hl i; move: (Hl i).
+ destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
+ + by rewrite !list_lookup_opM !lookup_app_l.
+ + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM; apply (Hxy n).
+ + rewrite !(cons_middle _ l1 l2) !assoc.
+ rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
+ - intros n mk; rewrite !list_lookup_validN !list_dist_lookup => Hl Hl' i.
+ move: (Hl i) (Hl' i).
+ destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
+ + by rewrite !list_lookup_opM !lookup_app_l.
+ + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM !inj_iff.
+ apply (Hxy' n).
+ + rewrite !(cons_middle _ l1 l2) !assoc.
+ rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
Qed.
End properties.
diff --git a/algebra/updates.v b/algebra/updates.v
index cd85753a0..ab978f4e0 100644
--- a/algebra/updates.v
+++ b/algebra/updates.v
@@ -1,13 +1,13 @@
From iris.algebra Require Export cmra.
(** * Local updates *)
-(** The idea is that lemams taking this class will usually have L explicit,
- and leave Lv implicit - it will be inferred by the typeclass machinery. *)
-Class LocalUpdate {A : cmraT} (Lv : A → Prop) (L : A → A) := {
- local_update_ne n :> Proper (dist n ==> dist n) L;
- local_updateN n x y : Lv x → ✓{n} (x ⋅ y) → L (x ⋅ y) ≡{n}≡ L x ⋅ y
+Record local_update {A : cmraT} (mz : option A) (x y : A) := {
+ local_update_valid n : ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz);
+ local_update_go n mz' :
+ ✓{n} (x ⋅? mz) → x ⋅? mz ≡{n}≡ x ⋅? mz' → y ⋅? mz ≡{n}≡ y ⋅? mz'
}.
-Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
+Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
+Instance: Params (@local_update) 1.
(** * Frame preserving updates *)
Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
@@ -25,6 +25,13 @@ Section cmra.
Context {A : cmraT}.
Implicit Types x y : A.
+Global Instance local_update_proper :
+ Proper ((≡) ==> (≡) ==> (≡) ==> iff) (@local_update A).
+Proof.
+ cut (Proper ((≡) ==> (≡) ==> (≡) ==> impl) (@local_update A)).
+ { intros Hproper; split; by apply Hproper. }
+ intros mz mz' Hmz x x' Hx y y' Hy [Hv Hup]; constructor; setoid_subst; auto.
+Qed.
Global Instance cmra_updateP_proper :
Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
@@ -38,25 +45,35 @@ Proof.
Qed.
(** ** Local updates *)
-Global Instance local_update_proper (L : A → A) Lv :
- LocalUpdate Lv L → Proper ((≡) ==> (≡)) L.
-Proof. intros; apply (ne_proper _). Qed.
-
-Lemma local_update (L : A → A) `{!LocalUpdate Lv L} x y :
- Lv x → ✓ (x ⋅ y) → L (x ⋅ y) ≡ L x ⋅ y.
+Global Instance local_update_preorder mz : PreOrder (@local_update A mz).
Proof.
- by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
+ split.
+ - intros x; by split.
+ - intros x1 x2 x3 [??] [??]; split; eauto.
Qed.
-Global Instance op_local_update x : LocalUpdate (λ _, True) (op x).
-Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
+Lemma exclusive_local_update `{!Exclusive x} y mz : ✓ y → x ~l~> y @ mz.
+Proof.
+ split; intros n.
+ - move=> /exclusiveN_opM ->. by apply cmra_valid_validN.
+ - intros mz' ? Hmz.
+ by rewrite (exclusiveN_opM n x mz) // (exclusiveN_opM n x mz') -?Hmz.
+Qed.
-Global Instance id_local_update : LocalUpdate (λ _, True) (@id A).
-Proof. split; auto with typeclass_instances. Qed.
+Lemma op_local_update x1 x2 y mz :
+ x1 ~l~> x2 @ Some (y ⋅? mz) → x1 ⋅ y ~l~> x2 ⋅ y @ mz.
+Proof.
+ intros [Hv1 H1]; split.
+ - intros n. rewrite !cmra_opM_assoc. move=> /Hv1 /=; auto.
+ - intros n mz'. rewrite !cmra_opM_assoc. move=> Hv /(H1 _ (Some _) Hv) /=; auto.
+Qed.
-Global Instance exclusive_local_update y :
- LocalUpdate Exclusive (λ _, y) | 1000.
-Proof. split. apply _. by intros ?????%exclusiveN_l. Qed.
+Lemma alloc_local_update x y mz : ✓ (x ⋅ y ⋅? mz) → x ~l~> x ⋅ y @ mz.
+Proof.
+ split.
+ - intros n _. by apply cmra_valid_validN.
+ - intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->.
+Qed.
(** ** Frame preserving updates *)
Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
@@ -137,19 +154,7 @@ Section total_updates.
End total_updates.
End cmra.
-(** ** CMRAs with a unit *)
-Section ucmra.
- Context {A : ucmraT}.
- Implicit Types x y : A.
-
- Lemma ucmra_update_unit x : x ~~> ∅.
- Proof.
- apply cmra_total_update=> n z. rewrite left_id; apply cmra_validN_op_r.
- Qed.
- Lemma ucmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
- Proof. split; [intros; trans ∅|]; auto using ucmra_update_unit. Qed.
-End ucmra.
-
+(** * Transport *)
Section cmra_transport.
Context {A B : cmraT} (H : A = B).
Notation T := (cmra_transport H).
@@ -166,6 +171,17 @@ Section prod.
Context {A B : cmraT}.
Implicit Types x : A * B.
+ Lemma prod_local_update x y mz :
+ x.1 ~l~> y.1 @ fst <$> mz → x.2 ~l~> y.2 @ snd <$> mz →
+ x ~l~> y @ mz.
+ Proof.
+ intros [Hv1 H1] [Hv2 H2]; split.
+ - intros n [??]; destruct mz; split; auto.
+ - intros n mz' [??] [??].
+ specialize (H1 n (fst <$> mz')); specialize (H2 n (snd <$> mz')).
+ destruct mz, mz'; split; naive_solver.
+ Qed.
+
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
Proof.
@@ -182,16 +198,6 @@ Section prod.
rewrite !cmra_update_updateP.
destruct x, y; eauto using prod_updateP with subst.
Qed.
-
- Global Instance prod_local_update
- (LA : A → A) `{!LocalUpdate LvA LA} (LB : B → B) `{!LocalUpdate LvB LB} :
- LocalUpdate (λ x, LvA (x.1) ∧ LvB (x.2)) (prod_map LA LB).
- Proof.
- constructor.
- - intros n x y [??]; constructor; simpl; by apply local_update_ne.
- - intros n ?? [??] [??];
- constructor; simpl in *; eapply local_updateN; eauto.
- Qed.
End prod.
(** * Option *)
@@ -199,19 +205,13 @@ Section option.
Context {A : cmraT}.
Implicit Types x y : A.
- Global Instance option_fmap_local_update (L : A → A) Lv :
- LocalUpdate Lv L →
- LocalUpdate (λ mx, if mx is Some x then Lv x else False) (fmap L).
- Proof.
- split; first apply _.
- intros n [x|] [z|]; constructor; by eauto using (local_updateN L).
- Qed.
- Global Instance option_const_local_update Lv y :
- LocalUpdate Lv (λ _, y) →
- LocalUpdate (λ mx, if mx is Some x then Lv x else False) (λ _, Some y).
+ Lemma option_local_update x y mmz :
+ x ~l~> y @ mjoin mmz →
+ Some x ~l~> Some y @ mmz.
Proof.
- split; first apply _.
- intros n [x|] [z|]; constructor; by eauto using (local_updateN (λ _, y)).
+ intros [Hv H]; split; first destruct mmz as [[?|]|]; auto.
+ intros n mmz'. specialize (H n (mjoin mmz')).
+ destruct mmz as [[]|], mmz' as [[]|]; inversion_clear 2; constructor; auto.
Qed.
Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
@@ -226,7 +226,5 @@ Section option.
x ~~>: P → Some x ~~>: from_option P False.
Proof. eauto using option_updateP. Qed.
Lemma option_update x y : x ~~> y → Some x ~~> Some y.
- Proof.
- rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
- Qed.
+ Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed.
End option.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 3fb45d287..225faa58b 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -77,8 +77,7 @@ Section heap.
Lemma to_heap_insert l v σ :
to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
Proof. by rewrite /to_heap -fmap_insert. Qed.
- Lemma of_heap_None h l :
- ✓ h → of_heap h !! l = None → h !! l = None.
+ Lemma of_heap_None h l : ✓ h → of_heap h !! l = None → h !! l = None.
Proof.
move=> /(_ l). rewrite /of_heap lookup_omap.
by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto.
@@ -130,7 +129,8 @@ Section heap.
rewrite -auth_own_op op_singleton pair_op dec_agree_ne //.
apply (anti_symm (⊢)); last by apply const_elim_l.
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
- rewrite option_validI prod_validI frac_validI discrete_valid. by apply const_elim_r.
+ rewrite option_validI prod_validI frac_validI discrete_valid.
+ by apply const_elim_r.
Qed.
Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
@@ -139,19 +139,18 @@ Section heap.
(** Weakest precondition *)
Lemma wp_alloc N E e v Φ :
to_val e = Some v → nclose N ⊆ E →
- heap_ctx N ★ ▷ (∀ l, l ↦ v -★ Φ (LitV $ LitLoc l)) ⊢ WP Alloc e @ E {{ Φ }}.
+ heap_ctx N ★ ▷ (∀ l, l ↦ v -★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
Proof.
iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
- iApply (auth_fsa heap_inv (wp_fsa (Alloc e)) _ N); simpl; eauto.
- iFrame "Hinv Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id.
+ iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+ iFrame "Hinv Hheap". iIntros {h}. rewrite left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
- iIntros {l} "[% Hheap]". iExists (op {[ l := (1%Qp, DecAgree v) ]}), _, _.
- rewrite [{[ _ := _ ]} ⋅ ∅]right_id.
+ iIntros {l} "[% Hheap]". iExists {[ l := (1%Qp, DecAgree v) ]}.
rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
- iFrame "Hheap". iSplit.
- { iPureIntro; split; first done. by apply (insert_valid h). }
+ iFrame "Hheap". iSplit; first iPureIntro.
+ { by apply alloc_singleton_local_update; first apply of_heap_None. }
iIntros "Hheap". iApply "HΦ". by rewrite /heap_mapsto.
Qed.
@@ -161,12 +160,12 @@ Section heap.
⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
- iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
- heap_name {[ l := (q, DecAgree v) ]}); simpl; eauto.
+ iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
- rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
- iIntros "$"; eauto.
+ rewrite of_heap_singleton_op //. iFrame "Hl".
+ iIntros "> Hown". iExists _; iSplit; first done.
+ rewrite of_heap_singleton_op //. by iFrame.
Qed.
Lemma wp_store N E l v' e v Φ :
@@ -175,13 +174,13 @@ Section heap.
⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
- iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, (1%Qp, DecAgree v)) l) _
- N _ heap_name {[ l := (1%Qp, DecAgree v') ]}); simpl; eauto.
+ iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
- rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
- iFrame "Hl". iNext. iIntros "$". iFrame "HΦ".
- iPureIntro. eauto 10 with typeclass_instances.
+ rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
+ iIntros "> Hown". iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
+ { iPureIntro; by apply singleton_local_update, exclusive_local_update. }
+ rewrite of_heap_singleton_op //; eauto. by iFrame.
Qed.
Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
@@ -190,12 +189,12 @@ Section heap.
⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros {????} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
- iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
- heap_name {[ l := (q, DecAgree v') ]}); simpl; eauto 10.
+ iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
- rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
- iIntros "$"; eauto.
+ rewrite of_heap_singleton_op //. iFrame "Hl".
+ iIntros "> Hown". iExists _; iSplit; first done.
+ rewrite of_heap_singleton_op //. by iFrame.
Qed.
Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ :
@@ -204,12 +203,12 @@ Section heap.
⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros {???} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
- iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, (1%Qp, DecAgree v2)) l)
- _ N _ heap_name {[ l := (1%Qp, DecAgree v1) ]}); simpl; eauto 10.
+ iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
- rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
- iFrame "Hl". iNext. iIntros "$". iFrame "HΦ".
- iPureIntro. eauto 10 with typeclass_instances.
+ rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
+ iIntros "> Hown". iExists {[l := (1%Qp, DecAgree v2)]}; iSplit.
+ { iPureIntro; by apply singleton_local_update, exclusive_local_update. }
+ rewrite of_heap_singleton_op //; eauto. by iFrame.
Qed.
End heap.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 55d28ca7e..1dad62362 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -53,8 +53,7 @@ Section auth.
Implicit Types a b : A.
Implicit Types γ : gname.
- Lemma auth_own_op γ a b :
- auth_own γ (a ⋅ b) ⊣⊢ (auth_own γ a ★ auth_own γ b).
+ Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
@@ -87,11 +86,10 @@ Section auth.
Lemma auth_fsa E N (Ψ : V → iPropG Λ Σ) γ a :
fsaV → nclose N ⊆ E →
- auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a',
- ■✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
- fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
- ■(Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
- (auth_own γ (L a) -★ Ψ x)))
+ auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ af,
+ ■✓ (a ⋅ af) ★ ▷ φ (a ⋅ af) -★
+ fsa (E ∖ nclose N) (λ x, ∃ b,
+ ■(a ~l~> b @ Some af) ★ ▷ φ (b ⋅ af) ★ (auth_own γ b -★ Ψ x)))
⊢ fsa E Ψ.
Proof.
iIntros {??} "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
@@ -99,29 +97,13 @@ Section auth.
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
iDestruct (own_valid _ with "#Hγ") as "Hvalid".
iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
- iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
+ iDestruct "Ha'" as {af} "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ"; by iSplit. }
- iIntros {v} "HL". iDestruct "HL" as {L Lv ?} "(% & Hφ & HΨ)".
- iPvs (own_update _ with "Hγ") as "[Hγ Hγf]".
- { apply (auth_local_update_l L); tauto. }
+ iIntros {v} "Ha". iDestruct "Ha" as {b} "(% & Hφ & HΨ)".
+ iPvs (own_update _ with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
- iNext. iExists (L a â‹… b). by iFrame.
- Qed.
-
- Lemma auth_fsa' L `{!LocalUpdate Lv L} E N (Ψ : V → iPropG Λ Σ) γ a :
- fsaV → nclose N ⊆ E →
- auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a',
- ■✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
- fsa (E ∖ nclose N) (λ x,
- ■(Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
- (auth_own γ (L a) -★ Ψ x)))
- ⊢ fsa E Ψ.
- Proof.
- iIntros {??} "(#Ha & Hγf & HΨ)"; iApply (auth_fsa E N Ψ γ a); auto.
- iFrame "Ha Hγf". iIntros {a'} "H".
- iApply fsa_wand_r; iSplitL; first by iApply "HΨ".
- iIntros {v} "?"; by iExists L, Lv, _.
+ iNext. iExists (b â‹… af). by iFrame.
Qed.
End auth.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 84bc45374..ee8f117a8 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -45,7 +45,6 @@ Context `{boxG Λ Σ} (N : namespace).
Notation iProp := (iPropG Λ Σ).
Implicit Types P Q : iProp.
-(* FIXME: solve_proper picks the eq ==> instance for Next. *)
Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
Proof. solve_proper. Qed.
Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ).
@@ -69,9 +68,11 @@ Lemma box_own_auth_update E γ b1 b2 b3 :
box_own_auth γ (◠Excl' b1) ★ box_own_auth γ (◯ Excl' b2)
={E}=> box_own_auth γ (◠Excl' b3) ★ box_own_auth γ (◯ Excl' b3).
Proof.
- rewrite /box_own_prop -!own_op.
- apply own_update, prod_update; simpl; last reflexivity.
- apply (auth_local_update (λ _, Excl' b3)). apply _. done.
+ rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".
+ iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete.
+ iApply (own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
+ rewrite -{1}(right_id ∅ _ (Excl' b2)) -{1}(right_id ∅ _ (Excl' b3)).
+ by apply auth_update, option_local_update, exclusive_local_update.
Qed.
Lemma box_own_agree γ Q1 Q2 :
--
GitLab