Commit a3d0a338 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak the algebraic hierarchy.

- Make the carrier argument of the constructors for the canonical structures
  cofeT and cmraT explicit. This way we make sure the carrier is properly
  exposed, instead of some alias of the carrier.
- Make derived constructions (such as discreteC and discreteR) notations
  instead of definitions. This is yet again to make sure that the carrier is
  properly exposed.
- Turn DRA into a canonical structure (it used to be a type class).

This fixes some issues, notably it fixes some broken rewrites in algebra/sts
and it makes canonical structures work properly with dec_agree.
parent 93792f5c
Pipeline #1142 passed with stage
......@@ -49,7 +49,7 @@ Proof.
- intros n c; apply and_wlog_r; intros;
symmetry; apply (chain_cauchy c); naive_solver.
Qed.
Canonical Structure agreeC := CofeT agree_cofe_mixin.
Canonical Structure agreeC := CofeT (agree A) agree_cofe_mixin.
Lemma agree_car_ne n (x y : agree A) : {n} x x {n} y x n {n} y n.
Proof. by intros [??] Hxy; apply Hxy. Qed.
......@@ -116,7 +116,8 @@ Proof.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
Qed.
Canonical Structure agreeR : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin.
Canonical Structure agreeR : cmraT :=
CMRAT (agree A) agree_cofe_mixin agree_cmra_mixin.
Global Instance agree_persistent (x : agree A) : Persistent x.
Proof. done. Qed.
......
......@@ -51,7 +51,7 @@ Proof.
- intros n c; split. apply (conv_compl n (chain_map authoritative c)).
apply (conv_compl n (chain_map own c)).
Qed.
Canonical Structure authC := CofeT auth_cofe_mixin.
Canonical Structure authC := CofeT (auth A) auth_cofe_mixin.
Global Instance Auth_timeless a b :
Timeless a Timeless b Timeless (Auth a b).
......@@ -128,7 +128,8 @@ Proof.
as (b&?&?&?); auto using own_validN.
by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
Qed.
Canonical Structure authR : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
Canonical Structure authR : cmraT :=
CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
Global Instance auth_cmra_discrete : CMRADiscrete A CMRADiscrete authR.
Proof.
split; first apply _.
......
......@@ -62,7 +62,7 @@ Structure cmraT := CMRAT {
cmra_cofe_mixin : CofeMixin cmra_car;
cmra_mixin : CMRAMixin cmra_car
}.
Arguments CMRAT {_ _ _ _ _ _ _ _} _ _.
Arguments CMRAT _ {_ _ _ _ _ _ _} _ _.
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
......@@ -75,7 +75,7 @@ Arguments cmra_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Add Printing Constructor cmraT.
Existing Instances cmra_core cmra_op cmra_valid cmra_validN.
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
Canonical Structure cmra_cofeC.
(** Lifting properties from the mixin *)
......@@ -474,14 +474,14 @@ End cmra_transport.
(** * Instances *)
(** ** Discrete CMRA *)
Class RA A `{Equiv A, Core A, Op A, Valid A} := {
Record RAMixin A `{Equiv A, Core A, Op A, Valid A} := {
(* setoids *)
ra_op_ne (x : A) : Proper (() ==> ()) (op x);
ra_core_ne :> Proper (() ==> ()) core;
ra_validN_ne :> Proper (() ==> impl) valid;
ra_core_ne : Proper (() ==> ()) core;
ra_validN_ne : Proper (() ==> impl) valid;
(* monoid *)
ra_assoc :> Assoc () ();
ra_comm :> Comm () ();
ra_assoc : Assoc () ();
ra_comm : Comm () ();
ra_core_l x : core x x x;
ra_core_idemp x : core (core x) core x;
ra_core_preserving x y : x y core x core y;
......@@ -489,36 +489,41 @@ Class RA A `{Equiv A, Core A, Op A, Valid A} := {
}.
Section discrete.
Context {A : cofeT} `{Discrete A}.
Context `{Core A, Op A, Valid A} (ra : RA A).
Context `{Equiv A, Core A, Op A, Valid A, @Equivalence A ()}.
Context (ra_mix : RAMixin A).
Existing Instances discrete_dist discrete_compl.
Instance discrete_validN : ValidN A := λ n x, x.
Definition discrete_cmra_mixin : CMRAMixin A.
Proof.
destruct ra; split; unfold Proper, respectful, includedN;
try setoid_rewrite <-(timeless_iff _ _); try done.
destruct ra_mix; split; try done.
- intros x; split; first done. by move=> /(_ 0).
- intros n x y1 y2 ??; exists (y1,y2); split_and?; auto.
apply (timeless _), dist_le with n; auto with lia.
- intros n x y1 y2 ??; by exists (y1,y2).
Qed.
Definition discreteR : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
Global Instance discrete_cmra_discrete : CMRADiscrete discreteR.
Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
End discrete.
Notation discreteR A ra_mix :=
(CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
Notation discreteLeibnizR A ra_mix :=
(CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)).
Global Instance discrete_cmra_discrete `{Equiv A, Core A, Op A, Valid A,
@Equivalence A ()} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
Proof. split. apply _. done. Qed.
(** ** CMRA for the unit type *)
Section unit.
Instance unit_valid : Valid () := λ x, True.
Instance unit_validN : ValidN () := λ n x, True.
Instance unit_core : Core () := λ x, x.
Instance unit_op : Op () := λ x y, ().
Global Instance unit_empty : Empty () := ().
Definition unit_ra : RA ().
Proof. by split. Qed.
Canonical Structure unitR : cmraT :=
Eval cbv [unitC discreteR cofe_car] in discreteR unit_ra.
Definition unit_cmra_mixin : CMRAMixin ().
Proof. by split; last exists ((),()). Qed.
Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
Global Instance unit_cmra_unit : CMRAUnit unitR.
Global Instance unit_cmra_discrete : CMRADiscrete unitR.
Proof. by apply discrete_cmra_discrete. Qed.
Proof. done. Qed.
Global Instance unit_persistent (x : ()) : Persistent x.
Proof. done. Qed.
End unit.
......@@ -563,7 +568,8 @@ Section prod.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
by exists ((z1.1,z2.1),(z1.2,z2.2)).
Qed.
Canonical Structure prodR : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin.
Canonical Structure prodR : cmraT :=
CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
Global Instance prod_cmra_unit `{Empty A, Empty B} :
CMRAUnit A CMRAUnit B CMRAUnit prodR.
Proof.
......
......@@ -65,7 +65,7 @@ Structure cofeT := CofeT {
cofe_compl : Compl cofe_car;
cofe_mixin : CofeMixin cofe_car
}.
Arguments CofeT {_ _ _ _} _.
Arguments CofeT _ {_ _ _} _.
Add Printing Constructor cofeT.
Existing Instances cofe_equiv cofe_dist cofe_compl.
Arguments cofe_car : simpl never.
......@@ -239,7 +239,7 @@ Section cofe_mor.
- intros n c x; simpl.
by rewrite (conv_compl n (fun_chain c x)) /=.
Qed.
Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
Canonical Structure cofe_mor : cofeT := CofeT (cofeMor A B) cofe_mor_cofe_mixin.
Global Instance cofe_mor_car_ne n :
Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
......@@ -291,7 +291,7 @@ Section unit.
Instance unit_compl : Compl unit := λ _, ().
Definition unit_cofe_mixin : CofeMixin unit.
Proof. by repeat split; try exists 0. Qed.
Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
Canonical Structure unitC : cofeT := CofeT unit unit_cofe_mixin.
Global Instance unit_discrete_cofe : Discrete unitC.
Proof. done. Qed.
End unit.
......@@ -317,7 +317,7 @@ Section product.
- intros n c; split. apply (conv_compl n (chain_map fst c)).
apply (conv_compl n (chain_map snd c)).
Qed.
Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin.
Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin.
Global Instance pair_timeless (x : A) (y : B) :
Timeless x Timeless y Timeless (x,y).
Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
......@@ -436,15 +436,16 @@ Section discrete_cofe.
- intros n c. rewrite /compl /discrete_compl /=;
symmetry; apply (chain_cauchy c 0 n). omega.
Qed.
Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
Global Instance discrete_discrete_cofe : Discrete discreteC.
Proof. by intros x y. Qed.
End discrete_cofe.
Arguments discreteC _ {_ _}.
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
Proof. by intros A x y. Qed.
Notation discreteC A := (CofeT A discrete_cofe_mixin).
Notation leibnizC A := (CofeT A (@discrete_cofe_mixin _ equivL _)).
Instance discrete_discrete_cofe `{Equiv A, @Equivalence A ()} :
Discrete (discreteC A).
Proof. by intros x y. Qed.
Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A).
Proof. by intros x y. Qed.
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
......@@ -478,7 +479,7 @@ Section later.
- intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
- intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
Qed.
Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
Canonical Structure laterC : cofeT := CofeT (later A) later_cofe_mixin.
Global Instance Next_contractive : Contractive (@Next A).
Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
......
......@@ -71,7 +71,7 @@ Proof.
- intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
apply (chain_cauchy c); lia.
Qed.
Definition T : cofeT := CofeT tower_cofe_mixin.
Definition T : cofeT := CofeT tower tower_cofe_mixin.
Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
match i with 0 => cid | S i => f (i + k) ff i end.
......
......@@ -28,7 +28,7 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
end.
Instance dec_agree_core : Core (dec_agree A) := id.
Definition dec_agree_ra : RA (dec_agree A).
Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof.
split.
- apply _.
......@@ -42,7 +42,8 @@ Proof.
- by intros [?|] [?|] ?.
Qed.
Canonical Structure dec_agreeR : cmraT := discreteR dec_agree_ra.
Canonical Structure dec_agreeR : cmraT :=
discreteR (dec_agree A) dec_agree_ra_mixin.
(* Some properties of this CMRA *)
Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
......
This diff is collapsed.
......@@ -59,7 +59,7 @@ Proof.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
Qed.
Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
Canonical Structure exclC : cofeT := CofeT (excl A) 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).
......@@ -107,7 +107,8 @@ Proof.
| ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
Qed.
Canonical Structure exclR : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin.
Canonical Structure exclR : cmraT :=
CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
Global Instance excl_cmra_unit : CMRAUnit exclR.
Proof. split. done. by intros []. apply _. Qed.
Global Instance excl_cmra_discrete : Discrete A CMRADiscrete exclR.
......
......@@ -72,7 +72,7 @@ Proof.
feed inversion (chain_cauchy c 0 n); first lia;
constructor; destruct (c 0); simplify_eq/=.
Qed.
Canonical Structure fracC : cofeT := CofeT frac_cofe_mixin.
Canonical Structure fracC : cofeT := CofeT (frac A) frac_cofe_mixin.
Global Instance frac_discrete : Discrete A Discrete fracC.
Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
Global Instance frac_leibniz : LeibnizEquiv A LeibnizEquiv (frac A).
......@@ -157,7 +157,8 @@ Proof.
+ exists (, Frac q a); inversion_clear Hx'; by repeat constructor.
+ exfalso; inversion_clear Hx'.
Qed.
Canonical Structure fracR : cmraT := CMRAT frac_cofe_mixin frac_cmra_mixin.
Canonical Structure fracR : cmraT :=
CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin.
Global Instance frac_cmra_unit : CMRAUnit fracR.
Proof. split. done. by intros []. apply _. Qed.
Global Instance frac_cmra_discrete : CMRADiscrete A CMRADiscrete fracR.
......
......@@ -28,7 +28,7 @@ Proof.
feed inversion (λ H, chain_cauchy c 0 n H k); simpl; auto with lia.
by rewrite conv_compl /=; apply reflexive_eq.
Qed.
Canonical Structure gmapC : cofeT := CofeT gmap_cofe_mixin.
Canonical Structure gmapC : cofeT := CofeT (gmap K A) gmap_cofe_mixin.
Global Instance gmap_discrete : Discrete A Discrete gmapC.
Proof. intros ? m m' ? i. by apply (timeless _). Qed.
(* why doesn't this go automatic? *)
......@@ -152,7 +152,8 @@ Proof.
pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
by symmetry; apply option_op_positive_dist_r with (m1 !! i).
Qed.
Canonical Structure gmapR : cmraT := CMRAT gmap_cofe_mixin gmap_cmra_mixin.
Canonical Structure gmapR : cmraT :=
CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
Global Instance gmap_cmra_unit : CMRAUnit gmapR.
Proof.
split.
......
......@@ -42,7 +42,7 @@ Section iprod_cofe.
rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)).
apply (chain_cauchy c); lia.
Qed.
Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin.
Canonical Structure iprodC : cofeT := CofeT (iprod B) iprod_cofe_mixin.
(** Properties of empty *)
Section empty.
......@@ -153,7 +153,8 @@ Section iprod_cmra.
exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
split_and?; intros x; apply (proj2_sig (g x)).
Qed.
Canonical Structure iprodR : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin.
Canonical Structure iprodR : cmraT :=
CMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin.
Global Instance iprod_cmra_unit `{ x, Empty (B x)} :
( x, CMRAUnit (B x)) CMRAUnit iprodR.
Proof.
......
......@@ -68,7 +68,7 @@ Proof.
rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->].
Qed.
Canonical Structure listC := CofeT list_cofe_mixin.
Canonical Structure listC := CofeT (list A) list_cofe_mixin.
Global Instance list_discrete : Discrete A Discrete listC.
Proof. induction 2; constructor; try apply (timeless _); auto. Qed.
......@@ -196,7 +196,8 @@ Section cmra.
[inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
Qed.
Canonical Structure listR : cmraT := CMRAT list_cofe_mixin list_cmra_mixin.
Canonical Structure listR : cmraT :=
CMRAT (list A) list_cofe_mixin list_cmra_mixin.
Global Instance empty_list : Empty (list A) := [].
Global Instance list_cmra_unit : CMRAUnit listR.
......
......@@ -65,7 +65,7 @@ Proof.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
rewrite (conv_compl n (one_shot_chain c _)) /=. destruct (c n); naive_solver.
Qed.
Canonical Structure one_shotC : cofeT := CofeT one_shot_cofe_mixin.
Canonical Structure one_shotC : cofeT := CofeT (one_shot A) one_shot_cofe_mixin.
Global Instance one_shot_discrete : Discrete A Discrete one_shotC.
Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
Global Instance one_shot_leibniz : LeibnizEquiv A LeibnizEquiv (one_shot A).
......@@ -186,7 +186,8 @@ Proof.
* exists (Shot a, ). inversion_clear Hx'. by repeat constructor.
* exists (, Shot a). inversion_clear Hx'. by repeat constructor.
Qed.
Canonical Structure one_shotR : cmraT := CMRAT one_shot_cofe_mixin one_shot_cmra_mixin.
Canonical Structure one_shotR : cmraT :=
CMRAT (one_shot A) one_shot_cofe_mixin one_shot_cmra_mixin.
Global Instance one_shot_cmra_unit : CMRAUnit one_shotR.
Proof. split. done. by intros []. apply _. Qed.
Global Instance one_shot_cmra_discrete : CMRADiscrete A CMRADiscrete one_shotR.
......
......@@ -34,7 +34,7 @@ Proof.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
Qed.
Canonical Structure optionC := CofeT option_cofe_mixin.
Canonical Structure optionC := CofeT (option A) option_cofe_mixin.
Global Instance option_discrete : Discrete A Discrete optionC.
Proof. destruct 2; constructor; by apply (timeless _). Qed.
......@@ -110,7 +110,8 @@ Proof.
+ by exists (None,Some x); inversion Hx'; repeat constructor.
+ exists (None,None); repeat constructor.
Qed.
Canonical Structure optionR := CMRAT option_cofe_mixin option_cmra_mixin.
Canonical Structure optionR :=
CMRAT (option A) option_cofe_mixin option_cmra_mixin.
Global Instance option_cmra_unit : CMRAUnit optionR.
Proof. split. done. by intros []. by inversion_clear 1. Qed.
Global Instance option_cmra_discrete : CMRADiscrete A CMRADiscrete optionR.
......
......@@ -155,15 +155,6 @@ Proof. move=> ?? s [s' [? ?]]. eauto using closed_steps. Qed.
End sts.
Notation steps := (rtc step).
End sts.
Notation stsT := sts.stsT.
Notation STS := sts.STS.
(** * STSs form a disjoint RA *)
(* This module should never be imported, uses the module [sts] below. *)
Module sts_dra.
Import sts.
(* The type of bounds we can give to the state of an STS. This is the type
that we equip with an RA structure. *)
......@@ -172,22 +163,28 @@ Inductive car (sts : stsT) :=
| frag : set (state sts) set (token sts ) car sts.
Arguments auth {_} _ _.
Arguments frag {_} _ _.
End sts.
Notation stsT := sts.stsT.
Notation STS := sts.STS.
(** * STSs form a disjoint RA *)
Section sts_dra.
Context {sts : stsT}.
Context (sts : stsT).
Import sts.
Implicit Types S : states sts.
Implicit Types T : tokens sts.
Inductive sts_equiv : Equiv (car sts) :=
| auth_equiv s T1 T2 : T1 T2 auth s T1 auth s T2
| frag_equiv S1 S2 T1 T2 : T1 T2 S1 S2 frag S1 T1 frag S2 T2.
Global Existing Instance sts_equiv.
Global Instance sts_valid : Valid (car sts) := λ x,
Existing Instance sts_equiv.
Instance sts_valid : Valid (car sts) := λ x,
match x with
| auth s T => tok s T
| frag S' T => closed S' T S'
end.
Global Instance sts_core : Core (car sts) := λ x,
Instance sts_core : Core (car sts) := λ x,
match x with
| frag S' _ => frag (up_set S' )
| auth s _ => frag (up s )
......@@ -197,8 +194,8 @@ Inductive sts_disjoint : Disjoint (car sts) :=
S1 S2 T1 T2 frag S1 T1 frag S2 T2
| auth_frag_disjoint s S T1 T2 : s S T1 T2 auth s T1 frag S T2
| frag_auth_disjoint s S T1 T2 : s S T1 T2 frag S T1 auth s T2.
Global Existing Instance sts_disjoint.
Global Instance sts_op : Op (car sts) := λ x1 x2,
Existing Instance sts_disjoint.
Instance sts_op : Op (car sts) := λ x1 x2,
match x1, x2 with
| frag S1 T1, frag S2 T2 => frag (S1 S2) (T1 T2)
| auth s T1, frag _ T2 => auth s (T1 T2)
......@@ -212,14 +209,19 @@ Hint Extern 50 (_ ∈ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Global Instance sts_equivalence: Equivalence (() : relation (car sts)).
Global Instance auth_proper s : Proper (() ==> ()) (@auth sts s).
Proof. by constructor. Qed.
Global Instance frag_proper : Proper (() ==> () ==> ()) (@frag sts).
Proof. by constructor. Qed.
Instance sts_equivalence: Equivalence (() : relation (car sts)).
Proof.
split.
- by intros []; constructor.
- by destruct 1; constructor.
- destruct 1; inversion_clear 1; constructor; etrans; eauto.
Qed.
Global Instance sts_dra : DRA (car sts).
Lemma sts_dra_mixin : DRAMixin (car sts).
Proof.
split.
- apply _.
......@@ -254,19 +256,20 @@ Proof.
unless (s up s T) by done; pose proof (elem_of_up s T)
end; auto with sts.
Qed.
Canonical Structure R : cmraT := validityR (car sts).
End sts_dra. End sts_dra.
Canonical Structure stsDR : draT := DRAT (car sts) sts_dra_mixin.
End sts_dra.
(** * The STS Resource Algebra *)
(** Finally, the general theory of STS that should be used by users *)
Notation stsR := (@sts_dra.R).
Notation stsC sts := (validityC (stsDR sts)).
Notation stsR sts := (validityR (stsDR sts)).
Section sts_definitions.
Context {sts : stsT}.
Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
to_validity (sts_dra.auth s T).
to_validity (sts.auth s T).
Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsR sts :=
to_validity (sts_dra.frag S T).
to_validity (sts.frag S T).
Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
sts_frag (sts.up s T) T.
End sts_definitions.
......@@ -280,23 +283,15 @@ Context {sts : stsT}.
Implicit Types s : state sts.
Implicit Types S : states sts.
Implicit Types T : tokens sts.
Global Instance sts_cmra_discrete : CMRADiscrete (stsR sts).
Proof. apply validity_cmra_discrete. Qed.
Arguments dra_valid _ !_/.
(** Setoids *)
Global Instance sts_auth_proper s : Proper (() ==> ()) (sts_auth s).
Proof. (* this proof is horrible *)
intros T1 T2 HT. rewrite /sts_auth.
by eapply to_validity_proper; try apply _; constructor.
Qed.
Proof. solve_proper. Qed.
Global Instance sts_frag_proper : Proper (() ==> () ==> ()) (@sts_frag sts).
Proof.
intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
by eapply to_validity_proper; try apply _; constructor.
Qed.
Proof. solve_proper. Qed.
Global Instance sts_frag_up_proper s : Proper (() ==> ()) (sts_frag_up s).
Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed.
Proof. solve_proper. Qed.
(** Validity *)
Lemma sts_auth_valid s T : sts_auth s T tok s T.
......@@ -334,11 +329,8 @@ Lemma sts_op_frag S1 S2 T1 T2 :
T1 T2 sts.closed S1 T1 sts.closed S2 T2
sts_frag (S1 S2) (T1 T2) sts_frag S1 T1 sts_frag S2 T2.
Proof.
intros HT HS1 HS2. rewrite /sts_frag.
(* FIXME why does rewrite not work?? *)
etrans; last eapply to_validity_op; first done; [].
move=>/=[??]. split_and!; [auto; set_solver..|].
constructor; done.
intros HT HS1 HS2. rewrite /sts_frag -to_validity_op //.
move=>/=[??]. split_and!; [auto; set_solver..|by constructor].
Qed.
(** Frame preserving updates *)
......@@ -367,9 +359,8 @@ Proof.
rewrite <-HT. eapply up_subseteq; done.
Qed.
Lemma up_set_intersection S1 Sf Tf :
closed Sf Tf
S1 Sf S1 up_set (S1 Sf) Tf.
Lemma sts_up_set_intersection S1 Sf Tf :
closed Sf Tf S1 Sf S1 up_set (S1 Sf) Tf.
Proof.
intros Hclf. apply (anti_symm ()).
+ move=>s [HS1 HSf]. split. by apply HS1. by apply subseteq_up_set.
......
......@@ -47,7 +47,7 @@ Section cofe.
- intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
- intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
Qed.
Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
End cofe.
Arguments uPredC : clear implicits.
......
......@@ -66,7 +66,7 @@ Proof.
+ apply (conv_compl n (chain_map pst c)).
+ apply (conv_compl n (chain_map gst c)).
Qed.
Canonical Structure resC : cofeT := CofeT res_cofe_mixin.
Canonical Structure resC : cofeT := CofeT (res Λ A M) res_cofe_mixin.
Global Instance res_timeless r :
Timeless (wld r) Timeless (gst r) Timeless r.
Proof. by destruct 3; constructor; try apply: timeless. Qed.
......@@ -118,7 +118,8 @@ Proof.
(cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
by exists (Res w σ m, Res w' σ' m').
Qed.
Canonical Structure resR : cmraT := CMRAT res_cofe_mixin res_cmra_mixin.
Canonical Structure resR : cmraT :=
CMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin.
Global Instance res_cmra_unit `{CMRAUnit M} : CMRAUnit resR.
Proof.
split.
......
......@@ -52,8 +52,7 @@ Proof.
iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
+ iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
iPvs (own_update with "Hγ") as "Hγ".
{ (* FIXME: canonical structures are not working *)
by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)). }
{ by apply (one_shot_update_shoot (DecAgree n)). }
iPvsIntro; iRight; iExists n; by iSplitL "Hl".
+ wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
- iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
......
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