Commit 9fd1f58e authored by Robbert Krebbers's avatar Robbert Krebbers

More timeless stuff.

Also introduce a notion for valid to be timeless.
parent ee8b3ce8
...@@ -25,7 +25,6 @@ Proof. by destruct 1. Qed. ...@@ -25,7 +25,6 @@ Proof. by destruct 1. Qed.
Instance auth_compl `{Cofe A} : Compl (auth A) := λ c, Instance auth_compl `{Cofe A} : Compl (auth A) := λ c,
Auth (compl (chain_map authoritative c)) (compl (chain_map own c)). Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
Local Instance auth_cofe `{Cofe A} : Cofe (auth A). Local Instance auth_cofe `{Cofe A} : Cofe (auth A).
Proof. Proof.
split. split.
...@@ -40,6 +39,9 @@ Proof. ...@@ -40,6 +39,9 @@ Proof.
* intros c n; split. apply (conv_compl (chain_map authoritative c) n). * intros c n; split. apply (conv_compl (chain_map authoritative c) n).
apply (conv_compl (chain_map own c) n). apply (conv_compl (chain_map own c) n).
Qed. Qed.
Instance Auth_timeless `{Dist A, Equiv A} (x : excl A) (y : A) :
Timeless x Timeless y Timeless (Auth x y).
Proof. by intros ?? [??] [??]; split; apply (timeless _). Qed.
(* CMRA *) (* CMRA *)
Instance auth_empty `{Empty A} : Empty (auth A) := Auth . Instance auth_empty `{Empty A} : Empty (auth A) := Auth .
...@@ -122,6 +124,14 @@ Proof. ...@@ -122,6 +124,14 @@ Proof.
split; [apply (ra_empty_valid (A:=A))|]. split; [apply (ra_empty_valid (A:=A))|].
by intros x; constructor; simpl; rewrite (left_id _ _). by intros x; constructor; simpl; rewrite (left_id _ _).
Qed. Qed.
Instance auth_frag_valid_timeless `{CMRA A} (x : A) :
ValidTimeless x ValidTimeless ( x).
Proof. by intros ??; apply (valid_timeless x). Qed.
Instance auth_valid_timeless `{CMRA A, Empty A, !RAEmpty A} (x : A) :
ValidTimeless x ValidTimeless ( x).
Proof.
by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)].
Qed.
Lemma auth_frag_op `{CMRA A} a b : (a b) a b. Lemma auth_frag_op `{CMRA A} a b : (a b) a b.
Proof. done. Qed. Proof. done. Qed.
......
...@@ -83,6 +83,11 @@ Definition cmra_update `{Op A, ValidN A} (x y : A) := ∀ z n, ...@@ -83,6 +83,11 @@ Definition cmra_update `{Op A, ValidN A} (x y : A) := ∀ z n,
Infix "⇝" := cmra_update (at level 70). Infix "⇝" := cmra_update (at level 70).
Instance: Params (@cmra_update) 3. Instance: Params (@cmra_update) 3.
(** Timeless elements *)
Class ValidTimeless `{Valid A, ValidN A} (x : A) :=
valid_timeless : validN 1 x valid x.
Arguments valid_timeless {_ _ _} _ {_} _.
(** Properties **) (** Properties **)
Section cmra. Section cmra.
Context `{cmra : CMRA A}. Context `{cmra : CMRA A}.
...@@ -122,12 +127,23 @@ Proof. ...@@ -122,12 +127,23 @@ Proof.
Qed. Qed.
Lemma cmra_unit_valid x n : {n} x {n} (unit x). Lemma cmra_unit_valid x n : {n} x {n} (unit x).
Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed. Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed.
(* Timeless *)
Lemma cmra_timeless_included_l `{!CMRAExtend A} x y :
Timeless x {1} y x {1} y x y.
Proof.
intros ?? [x' ?].
destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
by exists z'; rewrite Hy, (timeless x z) by done.
Qed.
Lemma cmra_timeless_included_r n x y : Timeless y x {1} y x {n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 : Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 :
{1} (x1 x2) Timeless x1 Timeless x2 Timeless (x1 x2). (x1 x2) Timeless x1 Timeless x2 Timeless (x1 x2).
Proof. Proof.
intros ??? z Hz. intros ??? z Hz.
destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
{ by rewrite <-?Hz. } { by rewrite <-?Hz; apply cmra_valid_validN. }
by rewrite Hz', (timeless x1 y1), (timeless x2 y2). by rewrite Hz', (timeless x1 y1), (timeless x2 y2).
Qed. Qed.
...@@ -223,6 +239,8 @@ Section discrete. ...@@ -223,6 +239,8 @@ Section discrete.
intros [|n] x y1 y2 ??; [|by exists (y1,y2)]. intros [|n] x y1 y2 ??; [|by exists (y1,y2)].
by exists (x,unit x); simpl; rewrite ra_unit_r. by exists (x,unit x); simpl; rewrite ra_unit_r.
Qed. Qed.
Global Instance discrete_timeless (x : A) : ValidTimeless x.
Proof. by intros ?. Qed.
Definition discreteRA : cmraT := CMRAT A. Definition discreteRA : cmraT := CMRAT A.
Lemma discrete_updateP (x : A) (P : A Prop) `{!Inhabited (sig P)} : Lemma discrete_updateP (x : A) (P : A Prop) `{!Inhabited (sig P)} :
( z, (x z) y, P y (y z)) x : P. ( z, (x z) y, P y (y z)) x : P.
...@@ -291,6 +309,9 @@ Proof. ...@@ -291,6 +309,9 @@ Proof.
destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto. destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
by exists ((z1.1,z2.1),(z1.2,z2.2)). by exists ((z1.1,z2.1),(z1.2,z2.2)).
Qed. Qed.
Instance pair_timeless `{Valid A, ValidN A, Valid B, ValidN B} (x : A) (y : B) :
ValidTimeless x ValidTimeless y ValidTimeless (x,y).
Proof. by intros ?? [??]; split; apply (valid_timeless _). Qed.
Canonical Structure prodRA (A B : cmraT) : cmraT := CMRAT (A * B). Canonical Structure prodRA (A B : cmraT) : cmraT := CMRAT (A * B).
Instance prod_map_cmra_monotone `{CMRA A, CMRA A', CMRA B, CMRA B'} Instance prod_map_cmra_monotone `{CMRA A, CMRA A', CMRA B, CMRA B'}
(f : A A') (g : B B') `{!CMRAMonotone f, !CMRAMonotone g} : (f : A A') (g : B B') `{!CMRAMonotone f, !CMRAMonotone g} :
......
...@@ -10,6 +10,17 @@ Instance option_unit `{Unit A} : Unit (option A) := fmap unit. ...@@ -10,6 +10,17 @@ Instance option_unit `{Unit A} : Unit (option A) := fmap unit.
Instance option_op `{Op A} : Op (option A) := union_with (λ x y, Some (x y)). Instance option_op `{Op A} : Op (option A) := union_with (λ x y, Some (x y)).
Instance option_minus `{Minus A} : Minus (option A) := Instance option_minus `{Minus A} : Minus (option A) :=
difference_with (λ x y, Some (x y)). difference_with (λ x y, Some (x y)).
Lemma option_included `{CMRA A} mx my :
mx my mx = None x y, mx = Some x my = Some y x y.
Proof.
split.
* intros [mz Hmz]; destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
setoid_subst; eauto using ra_included_l.
* intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
Qed.
Lemma option_includedN `{CMRA A} n mx my : Lemma option_includedN `{CMRA A} n mx my :
mx {n} my n = 0 mx = None x y, mx = Some x my = Some y x {n} y. mx {n} my n = 0 mx = None x y, mx = Some x my = Some y x {n} y.
Proof. Proof.
...@@ -17,9 +28,8 @@ Proof. ...@@ -17,9 +28,8 @@ Proof.
* intros [mz Hmz]; destruct n as [|n]; [by left|right]. * intros [mz Hmz]; destruct n as [|n]; [by left|right].
destruct mx as [x|]; [right|by left]. destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz]. destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_ands; auto. destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
+ by exists z. cofe_subst; auto using cmra_included_l.
+ by cofe_subst.
* intros [->|[->|(x&y&->&->&z&Hz)]]; * intros [->|[->|(x&y&->&->&z&Hz)]];
try (by exists my; destruct my; constructor). try (by exists my; destruct my; constructor).
by exists (Some z); constructor. by exists (Some z); constructor.
...@@ -65,6 +75,11 @@ Proof. ...@@ -65,6 +75,11 @@ Proof.
* by exists (None,Some x); inversion Hx'; repeat constructor. * by exists (None,Some x); inversion Hx'; repeat constructor.
* exists (None,None); repeat constructor. * exists (None,None); repeat constructor.
Qed. Qed.
Instance None_valid_timeless `{Valid A, ValidN A} : ValidTimeless (@None A).
Proof. done. Qed.
Instance Some_valid_timeless `{Valid A, ValidN A} x :
ValidTimeless x ValidTimeless (Some x).
Proof. by intros ? y; apply (valid_timeless x). Qed.
Instance option_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A B) Instance option_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A B)
`{!CMRAMonotone f} : CMRAMonotone (fmap f : option A option B). `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A option B).
Proof. Proof.
...@@ -154,6 +169,25 @@ Section map. ...@@ -154,6 +169,25 @@ Section map.
pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''. by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
Qed. Qed.
Global Instance map_empty_valid_timeless `{Valid A, ValidN A} :
ValidTimeless ( : M A).
Proof. by intros ??; rewrite lookup_empty. Qed.
Global Instance map_ra_insert_valid_timeless `{Valid A,ValidN A} (m: M A) i x:
ValidTimeless x ValidTimeless m m !! i = None
ValidTimeless (<[i:=x]>m).
Proof.
intros ?? Hi Hm j; destruct (decide (i = j)); simplify_map_equality.
{ specialize (Hm j); simplify_map_equality. by apply (valid_timeless _). }
generalize j; clear dependent j; rapply (valid_timeless m).
intros j; destruct (decide (i = j)); simplify_map_equality;[by rewrite Hi|].
by specialize (Hm j); simplify_map_equality.
Qed.
Global Instance map_ra_singleton_timeless `{Valid A, ValidN A} (i : K) x :
ValidTimeless x ValidTimeless ({[ i, x ]} : M A).
Proof.
intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _); simpl.
by rewrite lookup_empty.
Qed.
Definition mapRA (A : cmraT) : cmraT := CMRAT (M A). Definition mapRA (A : cmraT) : cmraT := CMRAT (M A).
Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A B) Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A B)
`{!CMRAMonotone f} : CMRAMonotone (fmap f : M A M B). `{!CMRAMonotone f} : CMRAMonotone (fmap f : M A M B).
......
...@@ -61,6 +61,13 @@ Proof. ...@@ -61,6 +61,13 @@ Proof.
feed inversion (chain_cauchy c 1 n); auto with lia; constructor. feed inversion (chain_cauchy c 1 n); auto with lia; constructor.
destruct (c 1); simplify_equality'. destruct (c 1); simplify_equality'.
Qed. Qed.
Instance Excl_timeless `{Equiv A, Dist A} (x : excl A) :
Timeless x Timeless (Excl x).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Instance ExclUnit_timeless `{Equiv A, Dist A} : Timeless (@ExclUnit A).
Proof. by inversion_clear 1; constructor. Qed.
Instance ExclBot_timeless `{Equiv A, Dist A} : Timeless (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
(* CMRA *) (* CMRA *)
Instance excl_valid {A} : Valid (excl A) := λ x, Instance excl_valid {A} : Valid (excl A) := λ x,
...@@ -112,6 +119,8 @@ Proof. ...@@ -112,6 +119,8 @@ Proof.
| ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit) | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
end; destruct y1, y2; inversion_clear Hx; repeat constructor. end; destruct y1, y2; inversion_clear Hx; repeat constructor.
Qed. Qed.
Instance excl_valid_timeless {A} (x : excl A) : ValidTimeless x.
Proof. by destruct x; intros ?. Qed.
(* Updates *) (* Updates *)
Lemma excl_update {A} (x : A) y : y Excl x y. Lemma excl_update {A} (x : A) y : y Excl x y.
......
...@@ -692,6 +692,14 @@ Lemma uPred_own_valid (a : M) : uPred_own a ⊆ (✓ a)%I. ...@@ -692,6 +692,14 @@ Lemma uPred_own_valid (a : M) : uPred_own a ⊆ (✓ a)%I.
Proof. Proof.
intros x n Hv [a' Hx]; simpl; rewrite Hx in Hv; eauto using cmra_valid_op_l. intros x n Hv [a' Hx]; simpl; rewrite Hx in Hv; eauto using cmra_valid_op_l.
Qed. Qed.
Lemma uPred_valid_intro (a : M) : a True%I ( a)%I.
Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
Lemma uPred_valid_elim_timess (a : M) :
ValidTimeless a ¬ a ( a)%I False%I.
Proof.
intros ? Hvalid x [|n] ??; [done|apply Hvalid].
apply (valid_timeless _), cmra_valid_le with (S n); auto with lia.
Qed.
(* Timeless *) (* Timeless *)
Global Instance uPred_const_timeless (P : Prop) : TimelessP (@uPred_const M P). Global Instance uPred_const_timeless (P : Prop) : TimelessP (@uPred_const M P).
...@@ -733,11 +741,10 @@ Proof. intros ? x n ??; simpl; apply timelessP; auto using cmra_unit_valid. Qed. ...@@ -733,11 +741,10 @@ Proof. intros ? x n ??; simpl; apply timelessP; auto using cmra_unit_valid. Qed.
Global Instance uPred_eq_timeless {A : cofeT} (a b : A) : Global Instance uPred_eq_timeless {A : cofeT} (a b : A) :
Timeless a TimelessP (a b : uPred M). Timeless a TimelessP (a b : uPred M).
Proof. by intros ? x n ??; apply equiv_dist, timeless. Qed. Proof. by intros ? x n ??; apply equiv_dist, timeless. Qed.
Global Instance uPred_own_timeless (a : M) :
Timeless a TimelessP (uPred_own a). (** Timeless elements *)
Global Instance uPred_own_timeless (a: M): Timeless a TimelessP (uPred_own a).
Proof. Proof.
intros ? x n ? [a' ?]. by intros ? x n ??; apply cmra_included_includedN, cmra_timeless_included_l.
destruct (cmra_extend_op 1 x a a') as ([b b']&Hx&Hb&Hb'); auto; simpl in *.
by exists b'; rewrite Hx, (timeless a b) by done.
Qed. Qed.
End logic. End logic.
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