Commit 780f6b82 authored by Robbert Krebbers's avatar Robbert Krebbers

Step-indexed order on CMRAs

* Remove the order from RAs, it is now defined in terms of the ⋅ operation.
* Define ownership using the step-indexed order.
* Remove the order also from DRAs and change STS accordingly. While doing
  that, I changed STS to no longer use decidable token sets, which removes the
  requirement of decidable equality on tokens.
parent db003ba1
......@@ -57,7 +57,6 @@ Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Global Instance agree_unit : Unit (agree A) := id.
Global Instance agree_minus : Minus (agree A) := λ x y, x.
Global Instance agree_included : Included (agree A) := λ x y, y x y.
Instance: Commutative () (@op (agree A) _).
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
Definition agree_idempotent (x : agree A) : x x x.
......@@ -80,6 +79,11 @@ Proof.
repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
by cofe_subst; rewrite !agree_idempotent.
Qed.
Lemma agree_includedN (x y : agree A) n : x {n} y y ={n}= x y.
Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz, (associative _), agree_idempotent.
Qed.
Global Instance agree_cmra : CMRA (agree A).
Proof.
split; try (apply _ || done).
......@@ -87,23 +91,20 @@ Proof.
rewrite <-(proj2 Hxy n'), (Hx n') by eauto using agree_valid_le.
by apply dist_le with n; try apply Hxy.
* by intros n x1 x2 Hx y1 y2 Hy.
* by intros x y1 y2 Hy ?; do 2 red; rewrite <-Hy.
* intros x; split; [apply agree_valid_0|].
by intros n'; rewrite Nat.le_0_r; intros ->.
* intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
rewrite (Hx n') by auto; symmetry; apply dist_le with n; try apply Hx; auto.
* intros x; apply agree_idempotent.
* intros x y; change (x y x (x y)).
by rewrite (associative _), agree_idempotent.
* by intros x y n [(?&?&?) ?].
* by intros x y; do 2 red; rewrite (associative _), agree_idempotent.
* by intros x y n; rewrite agree_includedN.
Qed.
Lemma agree_op_inv (x y1 y2 : agree A) n :
validN n x x ={n}= y1 y2 y1 ={n}= y2.
Proof. by intros [??] Hxy; apply Hxy. Qed.
Global Instance agree_extend : CMRAExtend (agree A).
Proof.
intros x y1 y2 n ? Hx; exists (x,x); simpl; split.
intros n x y1 y2 ? Hx; exists (x,x); simpl; split.
* by rewrite agree_idempotent.
* by rewrite Hx, (agree_op_inv x y1 y2), agree_idempotent by done.
Qed.
......@@ -131,15 +132,13 @@ Section agree_map.
Global Instance agree_map_ne n : Proper (dist n ==> dist n) agree_map.
Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
Global Instance agree_map_proper: Proper (()==>()) agree_map := ne_proper _.
Global Instance agree_map_preserving : CMRAPreserving agree_map.
Global Instance agree_map_monotone : CMRAMonotone agree_map.
Proof.
split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]].
intros x y; unfold included, agree_included; intros Hy; rewrite Hy.
split; [split|done].
* by intros (?&?&Hxy); repeat (intro || split);
intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy.
split; [split; simpl; try tauto|done].
by intros (?&?&Hxy); repeat split; intros;
try apply Hxy; try apply Hf; eauto using @agree_valid_le.
* by intros (?&(?&?&Hxy)&_); repeat split;
try apply Hxy; eauto using agree_valid_le.
Qed.
End agree_map.
Lemma agree_map_id `{Cofe A} (x : agree A) : agree_map id x = x.
......
Require Export iris.excl.
Local Arguments disjoint _ _ !_ !_ /.
Local Arguments included _ _ !_ !_ /.
Record auth (A : Type) : Type := Auth { authorative : excl A ; own : A }.
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
Arguments Auth {_} _ _.
Arguments authorative {_} _.
Arguments authoritative {_} _.
Arguments own {_} _.
Notation "∘ x" := (Auth ExclUnit x) (at level 20).
Notation "∙ x" := (Auth (Excl x) ) (at level 20).
Instance auth_empty `{Empty A} : Empty (auth A) := Auth .
Instance auth_valid `{Valid A, Included A} : Valid (auth A) := λ x,
valid (authorative x) excl_above (own x) (authorative x).
Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x,
valid (authoritative x) excl_above (own x) (authoritative x).
Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
authorative x authorative y own x own y.
authoritative x authoritative y own x own y.
Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
Auth (unit (authorative x)) (unit (own x)).
Auth (unit (authoritative x)) (unit (own x)).
Instance auth_op `{Op A} : Op (auth A) := λ x y,
Auth (authorative x authorative y) (own x own y).
Auth (authoritative x authoritative y) (own x own y).
Instance auth_minus `{Minus A} : Minus (auth A) := λ x y,
Auth (authorative x authorative y) (own x own y).
Instance auth_included `{Equiv A, Included A} : Included (auth A) := λ x y,
authorative x authorative y own x own y.
Auth (authoritative x authoritative y) (own x own y).
Lemma auth_included `{Equiv A, Op A} (x y : auth A) :
x y authoritative x authoritative y own x own y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
Instance auth_ra `{RA A} : RA (auth A).
Proof.
......@@ -35,17 +38,17 @@ Proof.
* by intros y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'.
* by intros x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'.
* by intros x y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'.
* by split; simpl; rewrite (associative _).
* by split; simpl; rewrite (commutative _).
* by split; simpl; rewrite ?(ra_unit_l _).
* by split; simpl; rewrite ?(ra_unit_idempotent _).
* split; simpl; auto using ra_unit_weaken.
* intros ?? [??]; split; [by apply ra_valid_op_l with (authorative y)|].
* intros ??; rewrite! auth_included; intros [??].
by split; simpl; apply ra_unit_preserving.
* intros ?? [??]; split; [by apply ra_valid_op_l with (authoritative y)|].
by apply excl_above_weaken with (own x own y)
(authorative x authorative y); try apply ra_included_l.
* split; simpl; apply ra_included_l.
* by intros ?? [??]; split; simpl; apply ra_op_minus.
(authoritative x authoritative y); try apply ra_included_l.
* by intros ??; rewrite auth_included;
intros [??]; split; simpl; apply ra_op_minus.
Qed.
Instance auth_ra_empty `{RA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
Proof. split. done. by intros x; constructor; simpl; rewrite (left_id _ _). Qed.
......
This diff is collapsed.
......@@ -3,18 +3,28 @@ Require Import prelude.pmap prelude.nmap prelude.zmap.
Require Import prelude.stringmap prelude.natmap.
(** option *)
Instance option_valid `{Valid A} : Valid (option A) := λ x,
match x with Some x => valid x | None => True end.
Instance option_validN `{ValidN A} : ValidN (option A) := λ n x,
match x with Some x => validN n x | None => True end.
Instance option_valid `{Valid A} : Valid (option A) := λ mx,
match mx with Some x => valid x | None => True end.
Instance option_validN `{ValidN A} : ValidN (option A) := λ n mx,
match mx with Some x => validN n x | None => True end.
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_minus `{Minus A} : Minus (option A) :=
difference_with (λ x y, Some (x y)).
Inductive option_included `{Included A} : Included (option A) :=
| Some_included x y : x y Some x Some y
| None_included x : None x.
Existing Instance option_included.
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.
Proof.
split.
* intros [mz Hmz]; destruct n as [|n]; [by left|right].
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.
+ by exists z.
+ by cofe_subst.
* intros [->|[->|(x&y&->&->&z&Hz)]];
try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
Qed.
Instance option_cmra `{CMRA A} : CMRA (option A).
Proof.
split.
......@@ -27,8 +37,6 @@ Proof.
eapply (_ : Proper (dist _ ==> impl) (validN _)); eauto.
* by destruct 1; inversion_clear 1; constructor;
repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
* intros [x|]; destruct 1; inversion_clear 1; constructor;
eapply (_ : Proper (equiv ==> impl) (included _)); eauto.
* intros [x|]; unfold validN, option_validN; auto using cmra_valid_0.
* intros n [x|]; unfold validN, option_validN; auto using cmra_valid_S.
* by intros [x|]; unfold valid, validN, option_validN, option_valid;
......@@ -37,19 +45,21 @@ Proof.
* intros [x|] [y|]; constructor; rewrite 1?(commutative _); auto.
* by intros [x|]; constructor; rewrite cmra_unit_l.
* by intros [x|]; constructor; rewrite cmra_unit_idempotent.
* intros [x|] [y|]; constructor; auto using cmra_unit_weaken.
* intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto.
do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preserving.
* intros n [x|] [y|]; unfold validN, option_validN; simpl;
eauto using cmra_valid_op_l.
* intros [x|] [y|]; constructor; auto using cmra_included_l.
* destruct 1 as [|[]]; constructor; eauto using cmra_op_minus.
* intros n mx my; rewrite option_includedN.
intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|].
by constructor; apply cmra_op_minus.
Qed.
Instance option_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (option A).
Proof.
intros mx my1 my2 n; destruct (decide (n = 0)) as [->|].
intros n mx my1 my2; destruct (decide (n = 0)) as [->|].
{ by exists (mx, None); repeat constructor; destruct mx; constructor. }
destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
try (by exfalso; inversion Hx'; auto).
* destruct (cmra_extend_op x y1 y2 n) as ([z1 z2]&?&?&?); auto.
* destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
{ by inversion_clear Hx'. }
by exists (Some z1, Some z2); repeat constructor.
* by exists (Some x,None); inversion Hx'; repeat constructor.
......@@ -57,10 +67,11 @@ Proof.
* exists (None,None); repeat constructor.
Qed.
Instance option_fmap_cmra_preserving `{CMRA A, CMRA B} (f : A B)
`{!CMRAPreserving f} : CMRAPreserving (fmap f : option A option B).
`{!CMRAMonotone f} : CMRAMonotone (fmap f : option A option B).
Proof.
split.
* by destruct 1 as [|[?|]]; constructor; apply included_preserving.
* intros n mx my; rewrite !option_includedN.
intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving.
* by intros n [x|] ?;
unfold validN, option_validN; simpl; try apply validN_preserving.
Qed.
......@@ -74,14 +85,28 @@ Section map.
Instance map_valid `{Valid A} : Valid (M A) := λ m, i, valid (m !! i).
Instance map_validN `{ValidN A} : ValidN (M A) := λ n m, i, validN n (m!!i).
Instance map_minus `{Minus A} : Minus (M A) := merge minus.
Instance map_included `{Included A} : Included (M A) := λ m1 m2,
i, m1 !! i m2 !! i.
Lemma lookup_op `{Op A} m1 m2 i : (m1 m2) !! i = m1 !! i m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_minus `{Minus A} m1 m2 i : (m1 m2) !! i = m1 !! i m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_unit `{Unit A} m i : unit m !! i = unit (m !! i).
Proof. by apply lookup_fmap. Qed.
Lemma map_included_spec `{CMRA A} (m1 m2 : M A) :
m1 m2 i, m1 !! i m2 !! i.
Proof.
split.
* intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
* intros Hm; exists (m2 m1); intros i.
by rewrite lookup_op, lookup_minus, ra_op_minus.
Qed.
Lemma map_includedN_spec `{CMRA A} (m1 m2 : M A) n :
m1 {n} m2 i, m1 !! i {n} m2 !! i.
Proof.
split.
* intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
* intros Hm; exists (m2 m1); intros i.
by rewrite lookup_op, lookup_minus, cmra_op_minus.
Qed.
Instance map_cmra `{CMRA A} : CMRA (M A).
Proof.
split.
......@@ -91,7 +116,6 @@ Section map.
* by intros n m1 m2 Hm ? i; rewrite <-(Hm i).
* intros n m1 m1' Hm1 m2 m2' Hm2 i.
by rewrite !lookup_minus, (Hm1 i), (Hm2 i).
* by intros m1 m2 m2' Hm2 ? i; rewrite <-(Hm2 i).
* intros m i; apply cmra_valid_0.
* intros n m Hm i; apply cmra_valid_S, Hm.
* intros m; split; [by intros Hm n i; apply cmra_valid_validN|].
......@@ -100,11 +124,12 @@ Section map.
* by intros m1 m2 i; rewrite !lookup_op, (commutative _).
* by intros m i; rewrite lookup_op, !lookup_unit, ra_unit_l.
* by intros m i; rewrite !lookup_unit, ra_unit_idempotent.
* intros m1 m2 i; rewrite !lookup_unit, lookup_op; apply ra_unit_weaken.
* intros n x y; rewrite !map_includedN_spec; intros Hm i.
by rewrite !lookup_unit; apply cmra_unit_preserving.
* intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i).
by rewrite <-lookup_op.
* intros m1 m2 i; rewrite lookup_op; apply ra_included_l.
* by intros m1 m2 Hm i; rewrite lookup_op, lookup_minus, ra_op_minus.
* intros x y n; rewrite map_includedN_spec; intros ? i.
by rewrite lookup_op, lookup_minus, cmra_op_minus by done.
Qed.
Instance map_ra_empty `{RA A} : RAEmpty (M A).
Proof.
......@@ -114,10 +139,10 @@ Section map.
Qed.
Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (M A).
Proof.
intros m m1 m2 n Hm Hm12.
intros n m m1 m2 Hm Hm12.
assert ( i, m !! i ={n}= m1 !! i m2 !! i) as Hm12'
by (by intros i; rewrite <-lookup_op).
set (f i := cmra_extend_op (m !! i) (m1 !! i) (m2 !! i) n (Hm i) (Hm12' i)).
set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
set (f_proj i := proj1_sig (f i)).
exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
repeat split; simpl; intros i; rewrite ?lookup_op, !lookup_imap.
......@@ -131,11 +156,12 @@ Section map.
by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
Qed.
Definition mapRA (A : cmraT) : cmraT := CMRAT (M A).
Global Instance map_fmap_cmra_preserving `{CMRA A, CMRA B} (f : A B)
`{!CMRAPreserving f} : CMRAPreserving (fmap f : M A M B).
Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A B)
`{!CMRAMonotone f} : CMRAMonotone (fmap f : M A M B).
Proof.
split.
* by intros m1 m2 Hm i; rewrite !lookup_fmap; apply included_preserving.
* intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
by rewrite !lookup_fmap; apply includedN_preserving.
* by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
Qed.
Hint Resolve (map_fmap_ne (M:=M)) : typeclass_instances.
......@@ -143,8 +169,8 @@ Section map.
CofeMor (fmap f : mapRA A mapRA B).
Global Instance mapRA_map_ne {A B} n :
Proper (dist n ==> dist n) (@mapRA_map A B) := mapC_map_ne n.
Global Instance mapRA_mapcmra_preserving {A B : cmraT} (f : A -n> B)
`{!CMRAPreserving f} : CMRAPreserving (mapRA_map f) := _.
Global Instance mapRA_mapcmra_monotone {A B : cmraT} (f : A -n> B)
`{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.
End map.
Arguments mapRA {_} _ {_ _ _ _ _ _ _ _ _} _.
......
......@@ -30,14 +30,19 @@ Instance validity_valid_proper `{Equiv A} (P : A → Prop) :
Proof. intros ?? [??]; naive_solver. Qed.
Local Notation V := valid.
Class DRA A `{Equiv A,Valid A,Unit A,Disjoint A,Op A,Included A, Minus A} := {
Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
z, y x z V z x z.
Instance: Params (@dra_included) 4.
Local Infix "≼" := dra_included.
Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
(* setoids *)
dra_equivalence :> Equivalence (() : relation A);
dra_op_proper :> Proper (() ==> () ==> ()) ();
dra_unit_proper :> Proper (() ==> ()) unit;
dra_disjoint_proper :> x, Proper (() ==> impl) (disjoint x);
dra_minus_proper :> Proper (() ==> () ==> ()) minus;
dra_included_proper :> Proper (() ==> () ==> impl) included;
(* validity *)
dra_op_valid x y : V x V y x y V (x y);
dra_unit_valid x : V x V (unit x);
......@@ -51,20 +56,21 @@ Class DRA A `{Equiv A,Valid A,Unit A,Disjoint A,Op A,Included A, Minus A} := {
dra_unit_disjoint_l x : V x unit x x;
dra_unit_l x : V x unit x x x;
dra_unit_idempotent x : V x unit (unit x) unit x;
dra_unit_weaken x y : V x V y x y unit x unit (x y);
dra_included_l x y : V x V y x y x x y;
dra_disjoint_difference x y : V x V y x y x y x;
dra_op_difference x y : V x V y x y x y x y
dra_unit_preserving x y : V x V y x y unit x unit y;
dra_disjoint_minus x y : V x V y x y x y x;
dra_op_minus x y : V x V y x y x y x y
}.
Section dra.
Context A `{DRA A}.
Arguments valid _ _ !_ /.
Hint Immediate dra_op_proper : typeclass_instances.
Instance: Proper (() ==> () ==> impl) ().
Instance: Proper (() ==> () ==> iff) ().
Proof.
intros x1 x2 Hx y1 y2 Hy.
by rewrite Hy, (symmetry_iff () x1), (symmetry_iff () x2), Hx.
intros x1 x2 Hx y1 y2 Hy; split.
* by rewrite Hy, (symmetry_iff () x1), (symmetry_iff () x2), Hx.
* by rewrite <-Hy, (symmetry_iff () x2), (symmetry_iff () x1), <-Hx.
Qed.
Lemma dra_disjoint_rl x y z : V x V y V z y z x y z x y.
Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
......@@ -78,10 +84,8 @@ Proof.
intros; symmetry; rewrite dra_commutative by eauto using dra_disjoint_rl.
apply dra_disjoint_move_l; auto; by rewrite dra_commutative.
Qed.
Hint Immediate dra_associative dra_commutative dra_unit_disjoint_l
dra_unit_l dra_unit_idempotent dra_unit_weaken dra_included_l
dra_op_difference dra_disjoint_difference dra_disjoint_rl
dra_disjoint_lr dra_disjoint_move_l dra_disjoint_move_r.
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Hint Unfold dra_included.
Notation T := (validity (valid : A Prop)).
Program Instance validity_unit : Unit T := λ x,
......@@ -91,8 +95,6 @@ Program Instance validity_op : Op T := λ x y,
Validity (validity_car x validity_car y)
(V x V y validity_car x validity_car y) _.
Next Obligation. by apply dra_op_valid; try apply validity_prf. Qed.
Instance validity_included : Included T := λ x y,
V y V x validity_car x validity_car y.
Program Instance validity_minus : Minus T := λ x y,
Validity (validity_car x validity_car y)
(V x V y validity_car y validity_car x) _.
......@@ -108,21 +110,25 @@ Proof.
* by intros ?? Heq ?; rewrite <-Heq.
* intros x1 x2 [? Hx] y1 y2 [? Hy];
split; simpl; [|by intros (?&?&?); rewrite Hx, Hy].
split; intros (?&?&?); split_ands'; try tauto.
+ by rewrite <-Hx, <-Hy by done.
+ by rewrite Hx, Hy by tauto.
* intros ??? [? Heq] Hle; split; [apply Hle; tauto|].
rewrite <-Heq by tauto; apply Hle; tauto.
* intros [x px ?] [y py ?] [z pz ?];
split; simpl; [naive_solver|intros; apply (associative _)].
* intros [x px ?] [y py ?]; split; naive_solver.
* intros [x px ?]; split; naive_solver.
* intros [x px ?]; split; naive_solver.
* intros [x px ?] [y py ?]; split; naive_solver.
split; intros (?&?&z&?&?); split_ands'; try tauto.
+ exists z. by rewrite <-Hy, <-Hx.
+ exists z. by rewrite Hx, Hy by tauto.
* intros [x px ?] [y py ?] [z pz ?]; split; simpl;
[intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
|intros; apply (associative _)].
* intros [x px ?] [y py ?]; split; naive_solver eauto using dra_commutative.
* intros [x px ?]; split;
naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
* intros [x px ?]; split; naive_solver eauto using dra_unit_idempotent.
* intros x y Hxy; exists (unit y unit x).
destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
assert (py unit x unit y)
by intuition eauto 10 using dra_unit_preserving.
constructor; [|symmetry]; simpl in *;
intuition eauto using dra_op_minus, dra_disjoint_minus, dra_unit_valid.
* by intros [x px ?] [y py ?] (?&?&?).
* intros [x px ?] [y py ?]; split; naive_solver.
* intros [x px ?] [y py ?];
unfold included, validity_included; split; naive_solver.
* intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
Qed.
Definition dra_update (x y : T) :
( z, V x V z validity_car x z V y validity_car y z) x y.
......
Require Export iris.cmra.
Local Arguments disjoint _ _ !_ !_ /.
Local Arguments included _ _ !_ !_ /.
Inductive excl (A : Type) :=
| Excl : A excl A
......@@ -32,15 +31,6 @@ Instance excl_minus {A} : Minus (excl A) := λ x y,
| Excl _, Excl _ => ExclUnit
| _, _ => ExclBot
end.
Instance excl_included `{Equiv A} : Included (excl A) := λ x y,
match x, y with
| Excl x, Excl y => x y
| ExclUnit, _ => True
| _, ExclBot => True
| _, _ => False
end.
Definition excl_above `{Included A} (x : A) (y : excl A) : Prop :=
match y with Excl y' => x y' | ExclUnit => True | ExclBot => False end.
Instance excl_ra `{Equiv A, !Equivalence (@equiv A _)} : RA (excl A).
Proof.
split.
......@@ -52,21 +42,23 @@ Proof.
* constructor.
* by destruct 1.
* by do 2 destruct 1; constructor.
* by intros []; destruct 1; simpl; try (intros Hx; rewrite Hx).
* by intros [?| |] [?| |] [?| |]; constructor.
* by intros [?| |] [?| |]; constructor.
* by intros [?| |]; constructor.
* constructor.
* intros [?| |] [?| |]; exists ; constructor.
* by intros [?| |] [?| |].
* by intros [?| |] [?| |].
* by intros [?| |] [?| |]; simpl; try constructor.
* by intros [?| |] [?| |] ?; try constructor.
* by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Qed.
Instance excl_empty_ra `{Equiv A, !Equivalence (@equiv A _)} : RAEmpty (excl A).
Proof. split. done. by intros []. Qed.
Lemma excl_update {A} (x : A) y : valid y Excl x y.
Proof. by destruct y; intros ? [?| |]. Qed.
Definition excl_above `{Equiv A, Op A} (x : A) (y : excl A) : Prop :=
match y with Excl y' => x y' | ExclUnit => True | ExclBot => False end.
Instance: Params (@excl_above) 3.
Section excl_above.
Context `{RA A}.
Global Instance excl_above_proper : Proper (() ==> () ==> iff) excl_above.
......@@ -74,7 +66,8 @@ Section excl_above.
Lemma excl_above_weaken (a b : A) x y :
excl_above b y a b x y excl_above a x.
Proof.
destruct x as [a'| |], y as [b'| |]; simpl; intros ??; try done.
by intros Hab; rewrite Hab; transitivity b.
destruct x as [a'| |], y as [b'| |];
intros ?? [[] Hz]; inversion_clear Hz; simpl in *; try done.
by setoid_subst; transitivity b.
Qed.
End excl_above.
Require Import prelude.prelude.
Class language (E V S : Type) := Language {
to_expr : V E;
of_expr : E option V;
atomic : E Prop;
prim_step : (E * S) (E * S) option E Prop;
of_to_expr v : of_expr (to_expr v) = Some v;
to_of_expr e v : of_expr e = Some v to_expr v = e;
values_stuck e σ s' ef : prim_step (e,σ) s' ef of_expr e = None;
atomic_not_value e : atomic e of_expr e = None;
atomic_step e1 σ1 e2 σ2 ef :
atomic e1
prim_step (e1,σ1) (e2,σ2) ef
is_Some (of_expr e2)
}.
Section foo.
Context `{language E V St}.
Definition cfg : Type := (list E * St)%type.
Inductive step (ρ1 ρ2 : cfg) : Prop :=
| step_atomic e1 σ1 e2 σ2 ef t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1)
ρ1 = (t1 ++ e2 :: t2 ++ option_list ef, σ2)
prim_step (e1, σ1) (e2, σ2) ef
step ρ1 ρ2.
Definition steps := rtc step.
Definition stepn := nsteps step.
End foo.
\ No newline at end of file
......@@ -48,7 +48,7 @@ Canonical Structure uPredC (M : cmraT) : cofeT := CofeT (uPred M).
(** functor *)
Program Definition uPred_map {M1 M2 : cmraT} (f : M2 M1)
`{! n, Proper (dist n ==> dist n) f, !CMRAPreserving f}
`{! n, Proper (dist n ==> dist n) f, !CMRAMonotone f}
(P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; simpl; rewrite <-Hy. Qed.
Next Obligation. intros M1 M2 f _ _ P x; apply uPred_0. Qed.
......@@ -56,15 +56,15 @@ Next Obligation.
naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Qed.
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 M1)
`{! n, Proper (dist n ==> dist n) f, !CMRAPreserving f} :
`{! n, Proper (dist n ==> dist n) f, !CMRAMonotone f} :