Commit f5f9e7ff authored by Robbert Krebbers's avatar Robbert Krebbers

Timelessness of ownership.

parent 9460ce23
......@@ -9,9 +9,12 @@ Instance: Params (@inv) 2.
Instance: Params (@ownP) 1.
Instance: Params (@ownG) 1.
Typeclasses Opaque inv ownG ownP.
Section ownership.
Context {Σ : iParam}.
Implicit Types r : res' Σ.
Implicit Types σ : istate Σ.
Implicit Types P : iProp Σ.
Implicit Types m : icmra' Σ.
......@@ -38,6 +41,8 @@ Proof.
rewrite /ownP -uPred.own_op Res_op.
by apply uPred.own_invalid; intros (_&?&_).
Qed.
Global Instance ownP_timeless σ : TimelessP (ownP σ).
Proof. rewrite /ownP; apply _. Qed.
(* ghost state *)
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Σ).
......@@ -51,6 +56,8 @@ Proof.
Qed.
Lemma ownG_valid m : (ownG m) ( m).
Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
Global Instance ownG_timeless m : Timeless m TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
(* inversion lemmas *)
Lemma inv_spec r n i P :
......
......@@ -8,6 +8,7 @@ Record iParam := IParam {
ilanguage : Language iexpr ival istate;
icmra_empty A : Empty (icmra A);
icmra_empty_spec A : RAIdentity (icmra A);
icmra_empty_timeless A : Timeless ( : icmra A);
icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B;
icmra_map_ne {A B} n : Proper (dist n ==> dist n) (@icmra_map A B);
icmra_map_id {A : cofeT} (x : icmra A) : icmra_map cid x x;
......@@ -16,7 +17,8 @@ Record iParam := IParam {
icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
}.
Existing Instances ilanguage.
Existing Instances icmra_empty icmra_empty_spec icmra_map_ne icmra_map_mono.
Existing Instances icmra_empty icmra_empty_spec icmra_empty_timeless.
Existing Instances icmra_map_ne icmra_map_mono.
Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
( x, f x g x) icmra_map Σ f m icmra_map Σ g m.
......
......@@ -161,6 +161,8 @@ Lemma lookup_wld_op_r n r1 r2 i P :
Proof.
rewrite (commutative _ r1) (commutative _ (wld r1)); apply lookup_wld_op_l.
Qed.
Global Instance Res_timeless eσ m : Timeless m Timeless (Res eσ m).
Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
End res.
Arguments resRA : clear implicits.
......
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