Commit eb8dd726 authored by Robbert Krebbers's avatar Robbert Krebbers

Introduce a type class for Discrete COFEs and CMRAs.

parent b2c912d8
......@@ -14,7 +14,8 @@ Notation "● a" := (Auth (Excl a) ∅) (at level 20).
(* COFE *)
Section cofe.
Context {A : cofeT}.
Implicit Types a b : A.
Implicit Types a : excl A.
Implicit Types b : A.
Implicit Types x y : auth A.
Instance auth_equiv : Equiv (auth A) := λ x y,
......@@ -51,9 +52,12 @@ Proof.
apply (conv_compl n (chain_map own c)).
Qed.
Canonical Structure authC := CofeT auth_cofe_mixin.
Global Instance auth_timeless (x : auth A) :
Timeless (authoritative x) Timeless (own x) Timeless x.
Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
Global Instance Auth_timeless a b :
Timeless a Timeless b Timeless (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: timeless. Qed.
Global Instance auth_discrete : Discrete A Discrete authC.
Proof. intros ? [??]; apply _. Qed.
Global Instance auth_leibniz : LeibnizEquiv A LeibnizEquiv (auth A).
Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
End cofe.
......@@ -87,6 +91,7 @@ Instance auth_op : Op (auth A) := λ x y,
Auth (authoritative x authoritative y) (own x own y).
Instance auth_minus : Minus (auth A) := λ x y,
Auth (authoritative x authoritative y) (own x own y).
Lemma auth_included (x y : auth A) :
x y authoritative x authoritative y own x own y.
Proof.
......@@ -136,6 +141,12 @@ Proof.
by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
Qed.
Canonical Structure authRA : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
Global Instance auth_cmra_discrete : CMRADiscrete A CMRADiscrete authRA.
Proof.
split; first apply _.
intros [[] ?]; by rewrite /= /cmra_valid /cmra_validN /=
-?cmra_discrete_included_iff -?cmra_discrete_valid_iff.
Qed.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
......
......@@ -134,6 +134,12 @@ Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := {
}.
Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate .
(** * Discrete CMRAs *)
Class CMRADiscrete (A : cmraT) : Prop := {
cmra_discrete :> Discrete A;
cmra_discrete_valid (x : A) : {0} x x
}.
(** * Morphisms *)
Class CMRAMonotone {A B : cmraT} (f : A B) := {
includedN_preserving n x y : x {n} y f x {n} f y;
......@@ -319,6 +325,24 @@ Proof.
by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Qed.
(** ** Discrete *)
Lemma cmra_discrete_valid_iff `{CMRADiscrete A} n x : x {n} x.
Proof.
split; first by rewrite cmra_valid_validN.
eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
Lemma cmra_discrete_included_iff `{Discrete A} n x y : x y x {n} y.
Proof.
split; first by rewrite cmra_included_includedN.
intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
Qed.
Lemma cmra_discrete_updateP `{CMRADiscrete A} (x : A) (P : A Prop) :
( z, (x z) y, P y (y z)) x ~~>: P.
Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
( z, (x z) (y z)) x ~~> y.
Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
(** ** RAs with an empty element *)
Section identity.
Context `{Empty A, !CMRAIdentity A}.
......@@ -473,7 +497,7 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
}.
Section discrete.
Context {A : cofeT} `{ x : A, Timeless x}.
Context {A : cofeT} `{Discrete A}.
Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
Instance discrete_validN : ValidN A := λ n x, x.
......@@ -486,12 +510,8 @@ Section discrete.
apply (timeless _), dist_le with n; auto with lia.
Qed.
Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
Lemma discrete_updateP (x : discreteRA) (P : A Prop) :
( z, (x z) y, P y (y z)) x ~~>: P.
Proof. intros Hvalid n z; apply Hvalid. Qed.
Lemma discrete_update (x y : discreteRA) :
( z, (x z) (y z)) x ~~> y.
Proof. intros Hvalid n z; apply Hvalid. Qed.
Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
End discrete.
(** ** CMRA for the unit type *)
......@@ -506,7 +526,8 @@ Section unit.
Canonical Structure unitRA : cmraT :=
Eval cbv [unitC discreteRA cofe_car] in discreteRA unit_ra.
Global Instance unit_cmra_identity : CMRAIdentity unitRA.
Proof. by split. Qed.
Global Instance unit_cmra_discrete : CMRADiscrete unitRA.
Proof. by apply discrete_cmra_discrete. Qed.
End unit.
(** ** Product *)
......@@ -563,6 +584,10 @@ Section prod.
- by split; rewrite /=left_id.
- by intros ? [??]; split; apply (timeless _).
Qed.
Global Instance prod_cmra_discrete :
CMRADiscrete A CMRADiscrete B CMRADiscrete prodRA.
Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. 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 :
......
......@@ -90,6 +90,11 @@ Section cofe_mixin.
Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.
(** Discrete COFEs and Timeless elements *)
Class Timeless {A : cofeT} (x : A) := timeless y : x {0} y x y.
Arguments timeless {_} _ {_} _ _.
Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x.
(** General properties *)
Section cofe.
Context {A : cofeT}.
......@@ -136,6 +141,12 @@ Section cofe.
Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
Global Instance contractive_proper {B : cofeT} (f : A B) `{!Contractive f} :
Proper (() ==> ()) f | 100 := _.
Lemma timeless_iff n (x : A) `{!Timeless x} y : x y x {n} y.
Proof.
split; intros; [by apply equiv_dist|].
apply (timeless _), dist_le with n; auto with lia.
Qed.
End cofe.
(** Mapping a chain *)
......@@ -144,15 +155,6 @@ Program Definition chain_map `{Dist A, Dist B} (f : A → B)
{| chain_car n := f (c n) |}.
Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
(** Timeless elements *)
Class Timeless {A : cofeT} (x : A) := timeless y : x {0} y x y.
Arguments timeless {_} _ {_} _ _.
Lemma timeless_iff {A : cofeT} n (x : A) `{!Timeless x} y : x y x {n} y.
Proof.
split; intros; [by apply equiv_dist|].
apply (timeless _), dist_le with n; auto with lia.
Qed.
(** Fixpoint *)
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
......@@ -256,7 +258,7 @@ Section unit.
Definition unit_cofe_mixin : CofeMixin unit.
Proof. by repeat split; try exists 0. Qed.
Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
Global Instance unit_timeless (x : ()) : Timeless x.
Global Instance unit_discrete_cofe : Discrete unitC.
Proof. done. Qed.
End unit.
......@@ -285,6 +287,8 @@ Section product.
Global Instance pair_timeless (x : A) (y : B) :
Timeless x Timeless y Timeless (x,y).
Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
Global Instance prod_discrete_cofe : Discrete A Discrete B Discrete prodC.
Proof. intros ?? [??]; apply _. Qed.
End product.
Arguments prodC : clear implicits.
......@@ -315,8 +319,8 @@ Section discrete_cofe.
symmetry; apply (chain_cauchy c 0 (S n)); omega.
Qed.
Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
Proof. by intros y. Qed.
Global Instance discrete_discrete_cofe : Discrete discreteC.
Proof. by intros x y. Qed.
End discrete_cofe.
Arguments discreteC _ {_ _}.
......
......@@ -131,26 +131,20 @@ Proof.
intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
Qed.
Definition validityRA : cmraT := discreteRA validity_ra.
Instance validity_cmra_discrete :
CMRADiscrete validityRA := discrete_cmra_discrete _.
Lemma validity_update (x y : validityRA) :
( z, x z validity_car x z y validity_car y z) x ~~> y.
Proof.
intros Hxy. apply discrete_update.
intros z (?&?&?); split_and!; try eapply Hxy; eauto.
intros Hxy; apply cmra_discrete_update=> z [?[??]].
split_and!; try eapply Hxy; eauto.
Qed.
Lemma to_validity_valid (x : A) :
to_validity x x.
Proof. intros. done. Qed.
Lemma to_validity_op (x y : A) :
( (x y) x y x y)
to_validity (x y) to_validity x to_validity y.
Proof.
intros Hvd. split; [split | done].
- simpl. auto.
- clear Hvd. simpl. intros (? & ? & ?).
auto using dra_op_valid, to_validity_valid.
Qed.
Proof. split; naive_solver auto using dra_op_valid. Qed.
Lemma to_validity_included x y:
( y to_validity x to_validity y)%C ( x x y).
......@@ -158,7 +152,7 @@ Proof.
split.
- move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
destruct Hvl' as [? [? ?]].
split; first by apply to_validity_valid.
split; first done.
exists (validity_car z). split_and!; last done.
+ apply EQ. assumption.
+ by apply validity_valid_car_valid.
......@@ -169,5 +163,4 @@ Proof.
+ intros _. setoid_subst. by apply dra_op_valid.
+ intros _. rewrite /= EQ //.
Qed.
End dra.
......@@ -69,6 +69,10 @@ Proof.
constructor; destruct (c 1); simplify_eq/=.
Qed.
Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
Global Instance excl_discrete : Discrete A Discrete exclC.
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
Global Instance Excl_timeless (x : A) : Timeless x Timeless (Excl x).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
......@@ -76,11 +80,6 @@ Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
Proof. by inversion_clear 1; constructor. Qed.
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
Global Instance excl_timeless :
( x : A, Timeless x) x : excl A, Timeless x.
Proof. intros ? []; apply _. Qed.
Global Instance excl_leibniz : LeibnizEquiv A LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
(* CMRA *)
Instance excl_valid : Valid (excl A) := λ x,
......@@ -127,6 +126,9 @@ Qed.
Canonical Structure exclRA : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin.
Global Instance excl_cmra_identity : CMRAIdentity exclRA.
Proof. split. done. by intros []. apply _. Qed.
Global Instance excl_cmra_discrete : Discrete A CMRADiscrete exclRA.
Proof. split. apply _. by intros []. Qed.
Lemma excl_validN_inv_l n x y : {n} (Excl x y) y = .
Proof. by destruct y. Qed.
Lemma excl_validN_inv_r n x y : {n} (x Excl y) x = .
......
......@@ -29,7 +29,8 @@ Proof.
by rewrite conv_compl /=; apply reflexive_eq.
Qed.
Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.
Global Instance map_discrete : Discrete A Discrete mapC.
Proof. intros ? m m' ? i. by apply (timeless _). Qed.
(* why doesn't this go automatic? *)
Global Instance mapC_leibniz: LeibnizEquiv A LeibnizEquiv mapC.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
......@@ -61,9 +62,6 @@ Proof.
[by constructor|by apply lookup_ne].
Qed.
Global Instance map_timeless `{ a : A, Timeless a} m : Timeless m.
Proof. by intros m' ? i; apply: timeless. Qed.
Instance map_empty_timeless : Timeless ( : gmap K A).
Proof.
intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
......@@ -168,8 +166,8 @@ Proof.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- apply map_empty_timeless.
Qed.
Global Instance mapRA_leibniz : LeibnizEquiv A LeibnizEquiv mapRA.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
Global Instance map_cmra_discrete : CMRADiscrete A CMRADiscrete mapRA.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
(** Internalized properties *)
Lemma map_equivI {M} m1 m2 : (m1 m2)%I ( i, m1 !! i m2 !! i : uPred M)%I.
......
......@@ -41,6 +41,9 @@ Proof.
constructor.
Qed.
Canonical Structure optionC := CofeT option_cofe_mixin.
Global Instance option_discrete : Discrete A Discrete optionC.
Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
Proof. by constructor. Qed.
Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
......@@ -51,8 +54,6 @@ Global Instance None_timeless : Timeless (@None A).
Proof. inversion_clear 1; constructor. Qed.
Global Instance Some_timeless x : Timeless x Timeless (Some x).
Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
Global Instance option_timeless `{! a : A, Timeless a} (mx : option A) : Timeless mx.
Proof. destruct mx; auto with typeclass_instances. Qed.
End cofe.
Arguments optionC : clear implicits.
......@@ -121,6 +122,8 @@ Qed.
Canonical Structure optionRA := CMRAT option_cofe_mixin option_cmra_mixin.
Global Instance option_cmra_identity : CMRAIdentity optionRA.
Proof. split. done. by intros []. by inversion_clear 1. Qed.
Global Instance option_cmra_discrete : CMRADiscrete A CMRADiscrete optionRA.
Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
(** Misc *)
Lemma op_is_Some mx my : is_Some (mx my) is_Some mx is_Some my.
......
......@@ -318,6 +318,9 @@ Implicit Types s : state sts.
Implicit Types S : states sts.
Implicit Types T : tokens sts.
Global Instance sts_cmra_discrete : CMRADiscrete (stsRA sts).
Proof. apply validity_cmra_discrete. Qed.
(** Setoids *)
Global Instance sts_auth_proper s : Proper (() ==> ()) (sts_auth s).
Proof. (* this proof is horrible *)
......
......@@ -896,7 +896,7 @@ Proof. split=> n x _; apply cmra_validN_op_l. Qed.
Lemma ownM_invalid (a : M) : ¬ {0} a uPred_ownM a False.
Proof. by intros; rewrite ownM_valid valid_elim. Qed.
Global Instance ownM_mono : Proper (flip () ==> ()) (@uPred_ownM M).
Proof. intros x y [z ->]. rewrite ownM_op. eauto. Qed.
Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
(* Products *)
Lemma prod_equivI {A B : cofeT} (x y : A * B) :
......@@ -912,11 +912,16 @@ Lemma later_equivI {A : cofeT} (x y : later A) :
Proof. done. Qed.
(* Discrete *)
(* For equality, there already is timeless_eq *)
Lemma discrete_validI {A : cofeT} `{ x : A, Timeless x}
`{Op A, Valid A, Unit A, Minus A} (ra : RA A) (x : discreteRA ra) :
( x)%I ( x : uPred M)%I.
Proof. done. Qed.
Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) :
( a)%I ( a : uPred M)%I.
Proof. split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
Lemma timeless_eq {A : cofeT} (a b : A) :
Timeless a (a b)%I ( (a b) : uPred M)%I.
Proof.
intros ?. apply (anti_symm ()).
- split=> n x ? ? /=. by apply (timeless_iff n a).
- eapply const_elim; first done. move=>->. apply eq_refl.
Qed.
(* Timeless *)
Lemma timelessP_spec P : TimelessP P n x, {n} x P 0 x P n x.
......@@ -927,13 +932,17 @@ Proof.
- move=> HP; split=> -[|n] x /=; auto; left.
apply HP, uPred_weaken with n x; eauto using cmra_validN_le.
Qed.
Global Instance const_timeless φ : TimelessP ( φ : uPred M)%I.
Proof. by apply timelessP_spec=> -[|n] x. Qed.
Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
TimelessP ( a : uPred M)%I.
Proof. apply timelessP_spec=> n x /=. by rewrite -!cmra_discrete_valid_iff. Qed.
Global Instance and_timeless P Q: TimelessP P TimelessP Q TimelessP (P Q).
Proof. by intros ??; rewrite /TimelessP later_and or_and_r; apply and_mono. Qed.
Global Instance or_timeless P Q : TimelessP P TimelessP Q TimelessP (P Q).
Proof.
intros; rewrite /TimelessP later_or (timelessP P) (timelessP Q); eauto 10.
intros; rewrite /TimelessP later_or (timelessP _) (timelessP Q); eauto 10.
Qed.
Global Instance impl_timeless P Q : TimelessP Q TimelessP (P Q).
Proof.
......@@ -975,13 +984,6 @@ Proof.
intros ?; apply timelessP_spec=> n x ??; apply cmra_included_includedN,
cmra_timeless_included_l; eauto using cmra_validN_le.
Qed.
Lemma timeless_eq {A : cofeT} (a b : A) :
Timeless a (a b)%I ((a b) : uPred M)%I.
Proof.
intros ?. apply (anti_symm ()).
- split=> n x ? ? /=. by apply (timeless_iff n a).
- eapply const_elim; first done. move=>->. apply eq_refl.
Qed.
(* Always stable *)
Local Notation AS := AlwaysStable.
......
......@@ -123,7 +123,7 @@ Section heap.
apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
with N heap_name ; simpl; eauto with I.
rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
rewrite -assoc left_id; apply const_elim_sep_l=> ?.
rewrite -assoc left_id discrete_valid; apply const_elim_sep_l=> ?.
rewrite -(wp_alloc_pst _ (of_heap h)) //.
apply sep_mono_r; rewrite HP; apply later_mono.
apply forall_mono=> l; apply wand_intro_l.
......@@ -147,7 +147,7 @@ Section heap.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Excl v ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
rewrite const_equiv // left_id.
rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
......@@ -165,7 +165,7 @@ Section heap.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
with N heap_name {[ l := Excl v' ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
rewrite /heap_inv alter_singleton insert_insert.
rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
......@@ -185,7 +185,7 @@ Section heap.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
rewrite const_equiv // left_id.
rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
......@@ -204,7 +204,7 @@ Section heap.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) ?lookup_insert //.
rewrite /heap_inv alter_singleton insert_insert.
rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
......
......@@ -5,13 +5,12 @@ Import uPred.
Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
auth_inG :> inG Λ Σ (authRA A);
auth_identity :> CMRAIdentity A;
(* TODO: Once we switched to RAs, this can be removed. *)
auth_timeless (a : A) :> Timeless a;
auth_timeless :> CMRADiscrete A;
}.
Definition authGF (A : cmraT) : iFunctor := constF (authRA A).
Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
`{CMRAIdentity A, a : A, Timeless a} : authG Λ Σ A.
`{CMRAIdentity A, CMRADiscrete A} : authG Λ Σ A.
Proof. split; try apply _. apply: inGF_inG. Qed.
Definition auth_own_def `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
......@@ -26,11 +25,11 @@ Module Export AuthOwn : AuthOwnSig.
Definition auth_own_eq := Logic.eq_refl (@auth_own).
End AuthOwn.
(* TODO: Once we switched to RAs, it is no longer necessary to remember that a
is constantly valid. *)
Definition auth_inv`{authG Λ Σ A} (γ : gname) (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
( a, ( a own γ ( a)) φ a)%I.
Definition auth_ctx`{authG Λ Σ A} (γ : gname) (N : namespace) (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
Definition auth_inv `{authG Λ Σ A}
(γ : gname) (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
( a, ( a own γ ( a)) φ a)%I.
Definition auth_ctx`{authG Λ Σ A}
(γ : gname) (N : namespace) (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
inv N (auth_inv γ φ).
Instance: Params (@auth_inv) 6.
......@@ -68,7 +67,7 @@ Section auth.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
trans ( auth_inv γ φ auth_own γ a)%I.
{ rewrite /auth_inv -(exist_intro a) later_sep.
rewrite const_equiv // left_id. ecancel [ φ _]%I.
rewrite -valid_intro // left_id. ecancel [ φ _]%I.
by rewrite -later_intro auth_own_eq -own_op auth_both_op. }
rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
by rewrite always_and_sep_l.
......@@ -79,20 +78,19 @@ Section auth.
Lemma auth_opened E γ a :
( auth_inv γ φ auth_own γ a)
(|={E}=> a', (a a') φ (a a') own γ ( (a a') a)).
(|={E}=> a', (a a') φ (a a') own γ ( (a a') a)).
Proof.
rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
rewrite later_sep [((_ _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
rewrite always_and_sep_l -!assoc. apply const_elim_sep_l=>Hv.
rewrite always_and_sep_l -!assoc discrete_valid. apply const_elim_sep_l=>Hv.
rewrite auth_own_eq [(▷φ _ _)%I]comm assoc -own_op.
rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
apply exist_elim=>a'.
rewrite left_id -(exist_intro a').
apply (eq_rewrite b (a a') (λ x, x φ x own γ ( x a))%I).
{ by move=>n ? ? /timeless_iff ->. }
apply (eq_rewrite b (a a') (λ x, x φ x own γ ( x a))%I).
{ by move=>n x y /timeless_iff ->. }
{ by eauto with I. }
rewrite const_equiv // left_id comm.
apply sep_mono_r. by rewrite sep_elim_l.
rewrite -valid_intro // left_id comm. auto with I.
Qed.
Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
......@@ -103,8 +101,8 @@ Section auth.
intros HL Hv. rewrite /auth_inv auth_own_eq -(exist_intro (L a a')).
(* TODO it would be really nice to use cancel here *)
rewrite later_sep [(_ ▷φ _)%I]comm -assoc.
rewrite -pvs_frame_l. apply sep_mono; first done.
rewrite const_equiv // left_id -later_intro -own_op.
rewrite -pvs_frame_l. apply sep_mono_r.
rewrite -valid_intro // left_id -later_intro -own_op.
by apply own_update, (auth_local_update_l L).
Qed.
......@@ -118,7 +116,7 @@ Section auth.
nclose N E
P auth_ctx γ N φ
P ( auth_own γ a a',
(a a') φ (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)))
......@@ -150,7 +148,7 @@ Section auth.
nclose N E
P auth_ctx γ N φ
P ( auth_own γ a ( a',
(a a') φ (a a') -
(a a') φ (a a') -
fsa (E nclose N) (λ x,
(Lv a (L a a')) φ (L a a')
(auth_own γ (L a) - Ψ x))))
......
......@@ -123,7 +123,7 @@ Section sts.
rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
rewrite -(exist_intro s).
rewrite [(_ ▷φ _)%I]comm -!assoc -own_op -[(▷φ _ _)%I]comm.
rewrite own_valid_l discrete_validI.
rewrite own_valid_l discrete_valid.
rewrite -!assoc. apply const_elim_sep_l=> Hvalid.
assert (s S) by eauto using sts_auth_frag_valid_inv.
rewrite const_equiv // left_id comm sts_op_auth_frag //.
......@@ -138,7 +138,7 @@ Section sts.
(* TODO it would be really nice to use cancel here *)
rewrite [(_ φ _)%I]comm -assoc.
rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
rewrite own_valid_l discrete_valid. apply const_elim_sep_l=>Hval.
trans (|={E}=> own γ (sts_auth s' T'))%I.
{ by apply own_update, sts_update_auth. }
by rewrite -own_op sts_op_auth_frag_up.
......
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