Commit bee413b8 authored by Robbert Krebbers's avatar Robbert Krebbers

No longer use option for local updates.

Instead, I separate it into a total function and a predicate
describe whether the action is allowed or not. This has some
advantages:

* It is much easier to deal with total functions and predicates
  in Coq than with functions into option.
* Already existing functions do not need to be wrapped. Instead,
  when using a local update you end up with a sensible side
  condition as a Coq Prop.
* The definition of local updates (and all CMRA instances) no
  longer depend on option.
parent a21fb68f
Require Export algebra.excl.
Require Import algebra.functor algebra.option.
Require Import algebra.functor.
Local Arguments validN _ _ _ !_ /.
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
......@@ -148,7 +148,7 @@ Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
(* FIXME tentative name. Or maybe remove this notion entirely. *)
Definition auth_step a a' b b' :=
Definition auth_step (a a' b b' : A) : Prop :=
n af, {n} a a {n} a' af b {n} b' af {n} b.
Lemma auth_update a a' b b' :
......@@ -160,27 +160,31 @@ Proof.
{ by rewrite Ha left_id associative. }
split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
Qed.
Lemma auth_update_op_l a a' b :
(b a) a a' ~~> (b a) (b a').
(* FIXME: are the following lemmas derivable from each other? *)
Lemma auth_local_update_l f `{!LocalUpdate P f} a a' :
P a (f a a')
(a a') a ~~> (f a a') f a.
Proof.
intros; apply auth_update=>n af ? EQ; split; last done.
by rewrite -(local_updateN f) // EQ -(local_updateN f) // -EQ.
Qed.
Lemma auth_local_update f `{!LocalUpdate P f} a a' :
P a (f a')
a' a ~~> f a' f a.
Proof.
intros; apply auth_update.
by intros n af ? Ha; split; [by rewrite Ha associative|].
intros; apply auth_update=>n af ? EQ; split; last done.
by rewrite EQ (local_updateN f) // -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 -!(commutative _ b); apply auth_update_op_l. Qed.
Lemma auth_local_update (L : LocalUpdate A) `{!LocalUpdateSpec L} a a' b :
L a = Some b (b a')
(a a') a ~~> (b a') b.
Proof.
intros Hlv Hv. apply auth_update=>n af Hab EQ.
split; last done.
apply (injective (R:=()) Some).
rewrite !Some_op -Hlv.
rewrite -!local_update_spec //; eauto; last by rewrite -EQ; [].
by rewrite EQ.
Qed.
End cmra.
Arguments authRA : clear implicits.
......
......@@ -135,6 +135,13 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
validN_preserving n x : {n} x {n} (f x)
}.
(** * Local updates *)
Class LocalUpdate {A : cmraT} (P : A Prop) (f : A A) := {
local_update_ne n :> Proper (dist n ==> dist n) f;
local_updateN n x y : P x {n} (x y) f (x y) {n} f x y
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
(** * Frame preserving updates *)
Definition cmra_updateP {A : cmraT} (x : A) (P : A Prop) := z n,
{n} (x z) y, P y {n} (y z).
......@@ -313,6 +320,18 @@ Section identity.
Proof. by rewrite -{2}(cmra_unit_l ) right_id. Qed.
End identity.
(** ** Local updates *)
Global Instance local_update_proper P (f : A A) :
LocalUpdate P f Proper (() ==> ()) f.
Proof. intros; apply (ne_proper _). Qed.
Lemma local_update f `{!LocalUpdate P f} x y :
P x (x y) f (x y) f x y.
Proof. by rewrite equiv_dist=>?? n; apply (local_updateN f). Qed.
Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
Proof. split. apply _. by intros n y1 y2 _ _; rewrite associative. Qed.
(** ** Updates *)
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
......
Require Export algebra.cmra.
Require Import algebra.functor algebra.option.
Require Import algebra.functor.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
......@@ -138,23 +138,16 @@ Proof.
by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
Qed.
(* Updates *)
(** ** Local updates *)
Global Instance excl_local_update b :
LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).
Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
(** Updates *)
Lemma excl_update (x : A) y : y Excl x ~~> y.
Proof. by destruct y; intros ? [?| |]. Qed.
Lemma excl_updateP (P : excl A Prop) x y : y P y Excl x ~~>: P.
Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
Definition excl_local_update_to (b : A) : LocalUpdate exclRA :=
λ a, if a is Excl _ then Some (Excl b) else None.
Global Instance excl_local_update_to_spec b :
LocalUpdateSpec (excl_local_update_to b).
Proof.
split.
- move=>? a a' EQ. destruct EQ; done.
- move=>a a' n [b' Hlv] Hv /=. destruct a; try discriminate Hlv; [].
destruct a'; try contradiction Hv; []. reflexivity.
Qed.
End excl.
Arguments exclC : clear implicits.
......
......@@ -34,6 +34,12 @@ Global Instance lookup_ne n k :
Proof. by intros m1 m2. Qed.
Global Instance lookup_proper k :
Proper (() ==> ()) (lookup k : gmap K A option A) := _.
Global Instance alter_ne f k n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (alter f k).
Proof.
intros ? m m' Hm k'.
by destruct (decide (k = k')); simplify_map_equality; rewrite (Hm k').
Qed.
Global Instance insert_ne i n :
Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
Proof.
......@@ -280,47 +286,22 @@ Lemma map_updateP_alloc' m x :
Proof. eauto using map_updateP_alloc. Qed.
End freshness.
Section local.
Definition map_local_alloc i x : LocalUpdate (mapRA K A) :=
local_update_op {[ i x ]}.
(* Deallocation is not a local update. The trouble is that if we own {[ i ↦ x ]},
then the frame could always own "unit x", and prevent deallocation. *)
Context (L : LocalUpdate A) `{!LocalUpdateSpec L}.
Definition map_local_update i : LocalUpdate (mapRA K A) :=
λ m, x m !! i; y L x; Some (<[i:=y]>m).
Global Instance map_local_update_spec i : LocalUpdateSpec (map_local_update i).
(*
Lemma option_fmap_op {B : cmraT} (f : A → B) (mx my : option A) : f <$> mx ⋅ my = (f <$> mx) ⋅ (f <$> my).
Proof. destruct mx, my; simpl; try done.
*)
Global Instance map_alter_update `{!LocalUpdate P f} i :
LocalUpdate (λ m, x, m !! i = Some x P x) (alter f i).
Proof.
rewrite /map_local_update. split.
- (* FIXME Oh wow, this is harder than expected... *)
move=>n f g EQ. move:(EQ i).
case _:(f !! i)=>[fi|]; case _:(g !! i)=>[gi|]; move=>EQi;
inversion EQi; subst; simpl; last done.
assert (EQL : L fi {n} L gi) by (by apply local_update_ne). move: EQL.
case _:(L fi)=>[Lfi|] /=; case _:(L gi)=>[Lgi|]; move=>EQL;
inversion EQL; subst; simpl; last done.
apply Some_ne, insert_ne; done.
- move=>f g n [b Hlv] Hv. rewrite lookup_op. move:Hlv.
case EQf:(f !! i)=>[fi|]; simpl; last discriminate.
case EQL:(L fi)=>[Lfi|]; simpl; last discriminate.
case=>?. subst b.
case EQg:(g !! i)=>[gi|]; simpl.
+ assert (L (fi gi) {n} L fi Some gi) as EQLi.
{ apply local_update_spec; first by eauto.
move:(Hv i). rewrite lookup_op EQf EQg -Some_op. done. }
rewrite EQL -Some_op in EQLi.
destruct (L (fi gi)) as [Lfgi|]; inversion EQLi; subst; simpl.
rewrite -Some_op. apply Some_ne. move=>j. rewrite lookup_op.
destruct (decide (i = j)); simplify_map_equality; last by rewrite lookup_op.
rewrite EQg -Some_op. apply Some_ne. done.
+ rewrite EQL /=.
rewrite -Some_op. apply Some_ne. move=>j. rewrite lookup_op.
destruct (decide (i = j)); simplify_map_equality; last by rewrite lookup_op.
by rewrite EQg.
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 f).
- by rewrite lookup_op !lookup_alter_ne // lookup_op.
Qed.
End local.
End properties.
(** Functor *)
......@@ -358,4 +339,3 @@ Next Obligation.
intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
Qed.
......@@ -187,28 +187,3 @@ Next Obligation.
intros Σ A B C f g x. rewrite /= -option_fmap_compose.
apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
Qed.
(** * Local CMRA Updates *)
(* FIXME: These need the CMRA structure on option, hence they are defined here. Or maybe moe option to cmra.v? *)
(* TODO: Probably needs some more magic flags. What about notation? *)
Section local_update.
Context {A : cmraT}.
(* Do we need more step-indexing here? *)
Definition LocalUpdate := A option A.
Class LocalUpdateSpec (L : LocalUpdate) := {
local_update_ne n :> Proper ((dist n) ==> (dist n)) L;
local_update_spec a b n : is_Some (L a) {n}(a b) L (a b) {n} (L a) Some b
}.
Definition local_update_op (b : A) : LocalUpdate
:= λ a, Some (b a).
Global Instance local_update_op_spec b : LocalUpdateSpec (local_update_op b).
Proof.
rewrite /local_update_op. split.
- move=>? ? ? EQ /=. by rewrite EQ.
- move=>a a' n Hlv Hv /=. by rewrite associative.
Qed.
End local_update.
Arguments LocalUpdate : clear implicits.
......@@ -14,16 +14,16 @@ Section auth.
(* TODO: Need this to be proven somewhere. *)
(* FIXME ✓ binds too strong, I need parenthesis here. *)
Hypothesis auth_valid :
forall a b, ((Auth (Excl a) b) : iProp Λ (globalC Σ)) ( b', a b b').
forall a b, ( (Auth (Excl a) b) : iProp Λ (globalC Σ)) ( b', a b b').
(* FIXME how much would break if we had a global instance from ∅ to Inhabited? *)
Local Instance auth_inhabited : Inhabited A.
Proof. split. exact . Qed.
Definition auth_inv (γ : gname) : iProp Λ (globalC Σ) :=
( a, own AuthI γ (a) φ a)%I.
Definition auth_own (γ : gname) (a : A) := own AuthI γ (a).
Definition auth_ctx (γ : gname) := inv N (auth_inv γ).
( a, own AuthI γ ( a) φ a)%I.
Definition auth_own (γ : gname) (a : A) : iProp Λ (globalC Σ) := own AuthI γ ( a).
Definition auth_ctx (γ : gname) : iProp Λ (globalC Σ) := inv N (auth_inv γ).
Lemma auth_alloc a :
a φ a pvs N N ( γ, auth_ctx γ auth_own γ a).
......@@ -58,18 +58,15 @@ Section auth.
by rewrite sep_elim_l.
Qed.
Context (L : LocalUpdate A) `{!LocalUpdateSpec L}.
Lemma auth_closing a a' b γ :
L a = Some b (b a')
(φ (b a') own AuthI γ ( (a a') a))
pvs N N (auth_inv γ auth_own γ b).
Lemma auth_closing `{!LocalUpdate φf f} a a' γ :
φf a (f a a')
(φ (f a a') own AuthI γ ( (a a') a))
pvs N N (auth_inv γ auth_own γ (f a)).
Proof.
intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (b a')).
intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (f a a')).
rewrite [(_ φ _)%I]commutative -associative.
rewrite -pvs_frame_l. apply sep_mono; first done.
rewrite -own_op. apply own_update.
by apply (auth_local_update L).
rewrite -pvs_frame_l -own_op; apply sep_mono; first done.
by apply own_update, (auth_local_update_l f).
Qed.
End auth.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment