Commit c2c84732 authored by Ralf Jung's avatar Ralf Jung

rename CMRA unit -> core

parent 361c9fbf
Pipeline #284 passed with stage
......@@ -60,7 +60,7 @@ Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x;
agree_is_valid n := agree_is_valid x n agree_is_valid y n x {n} y |}.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Instance agree_unit : Unit (agree A) := id.
Instance agree_core : Core (agree A) := id.
Instance agree_div : Div (agree A) := λ x y, x.
Instance: Comm () (@op (agree A) _).
......
......@@ -85,8 +85,8 @@ Instance auth_validN : ValidN (auth A) := λ n x,
| ExclBot => False
end.
Global Arguments auth_validN _ !_ /.
Instance auth_unit : Unit (auth A) := λ x,
Auth (unit (authoritative x)) (unit (own x)).
Instance auth_core : Core (auth A) := λ x,
Auth (core (authoritative x)) (core (own x)).
Instance auth_op : Op (auth A) := λ x y,
Auth (authoritative x authoritative y) (own x own y).
Instance auth_div : Div (auth A) := λ x y,
......@@ -117,10 +117,10 @@ Proof.
- intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
- by split; simpl; rewrite assoc.
- by split; simpl; rewrite comm.
- by split; simpl; rewrite ?cmra_unit_l.
- by split; simpl; rewrite ?cmra_unit_idemp.
- by split; simpl; rewrite ?cmra_core_l.
- by split; simpl; rewrite ?cmra_core_idemp.
- intros ??; rewrite! auth_included; intros [??].
by split; simpl; apply cmra_unit_preserving.
by split; simpl; apply cmra_core_preserving.
- assert ( n (a b1 b2 : A), b1 b2 {n} a b1 {n} a).
{ intros n a b1 b2 <-; apply cmra_includedN_l. }
intros n [[a1| |] b1] [[a2| |] b2];
......
This diff is collapsed.
......@@ -2,7 +2,7 @@ From algebra Require Export cmra.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments unit _ _ !_ /.
Local Arguments core _ _ !_ /.
(* This is isomorphic to option, but has a very different RA structure. *)
Inductive dec_agree (A : Type) : Type :=
......@@ -26,7 +26,7 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
| DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
| _, _ => DecAgreeBot
end.
Instance dec_agree_unit : Unit (dec_agree A) := id.
Instance dec_agree_core : Core (dec_agree A) := id.
Instance dec_agree_div : Div (dec_agree A) := λ x y, x.
Definition dec_agree_ra : RA (dec_agree A).
......
......@@ -18,17 +18,17 @@ Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
Instance: Params (@dra_included) 4.
Local Infix "≼" := dra_included.
Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Div A} := {
Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A, Div A} := {
(* setoids *)
dra_equivalence :> Equivalence (() : relation A);
dra_op_proper :> Proper (() ==> () ==> ()) ();
dra_unit_proper :> Proper (() ==> ()) unit;
dra_core_proper :> Proper (() ==> ()) core;
dra_valid_proper :> Proper (() ==> impl) valid;
dra_disjoint_proper :> x, Proper (() ==> impl) (disjoint x);
dra_div_proper :> Proper (() ==> () ==> ()) div;
(* validity *)
dra_op_valid x y : x y x y (x y);
dra_unit_valid x : x unit x;
dra_core_valid x : x core x;
dra_div_valid x y : x y x y (y ÷ x);
(* monoid *)
dra_assoc :> Assoc () ();
......@@ -36,10 +36,10 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Div A} := {
dra_disjoint_move_l x y z : x y z x y x y z x y z;
dra_symmetric :> Symmetric (@disjoint A _);
dra_comm x y : x y x y x y y x;
dra_unit_disjoint_l x : x unit x x;
dra_unit_l x : x unit x x x;
dra_unit_idemp x : x unit (unit x) unit x;
dra_unit_preserving x y : x y x y unit x unit y;
dra_core_disjoint_l x : x core x x;
dra_core_l x : x core x x x;
dra_core_idemp x : x core (core x) core x;
dra_core_preserving x y : x y x y core x core y;
dra_disjoint_div x y : x y x y x y ÷ x;
dra_op_div x y : x y x y x y ÷ x y
}.
......@@ -88,9 +88,9 @@ Hint Unfold dra_included.
Lemma validity_valid_car_valid (z : T) : z validity_car z.
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
Program Instance validity_unit : Unit T := λ x,
Validity (unit (validity_car x)) ( x) _.
Solve Obligations with naive_solver auto using dra_unit_valid.
Program Instance validity_core : Core T := λ x,
Validity (core (validity_car x)) ( x) _.
Solve Obligations with naive_solver auto using dra_core_valid.
Program Instance validity_op : Op T := λ x y,
Validity (validity_car x validity_car y)
( x y validity_car x validity_car y) _.
......@@ -118,14 +118,14 @@ Proof.
|by intros; rewrite assoc].
- intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
- 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_idemp.
- intros x y Hxy; exists (unit y ÷ unit x).
naive_solver eauto using dra_core_l, dra_core_disjoint_l.
- intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
- intros x y Hxy; exists (core y ÷ core 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.
assert (py core x core y)
by intuition eauto 10 using dra_core_preserving.
constructor; [|symmetry]; simpl in *;
intuition eauto using dra_op_div, dra_disjoint_div, dra_unit_valid.
intuition eauto using dra_op_div, dra_disjoint_div, dra_core_valid.
- by intros [x px ?] [y py ?] (?&?&?).
- intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
intuition eauto 10 using dra_disjoint_div, dra_op_div.
......
......@@ -91,7 +91,7 @@ Instance excl_valid : Valid (excl A) := λ x,
Instance excl_validN : ValidN (excl A) := λ n x,
match x with Excl _ | ExclUnit => True | ExclBot => False end.
Global Instance excl_empty : Empty (excl A) := ExclUnit.
Instance excl_unit : Unit (excl A) := λ _, .
Instance excl_core : Core (excl A) := λ _, .
Instance excl_op : Op (excl A) := λ x y,
match x, y with
| Excl a, ExclUnit | ExclUnit, Excl a => Excl a
......
......@@ -93,7 +93,7 @@ Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K A.
Instance map_op : Op (gmap K A) := merge op.
Instance map_unit : Unit (gmap K A) := fmap unit.
Instance map_core : Core (gmap K A) := fmap core.
Instance map_valid : Valid (gmap K A) := λ m, i, (m !! i).
Instance map_validN : ValidN (gmap K A) := λ n m, i, {n} (m !! i).
Instance map_div : Div (gmap K A) := merge div.
......@@ -102,7 +102,7 @@ Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_div m1 m2 i : (m1 ÷ m2) !! i = m1 !! i ÷ m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_unit m i : unit m !! i = unit (m !! i).
Lemma lookup_core m i : core m !! i = core (m !! i).
Proof. by apply lookup_fmap. Qed.
Lemma map_included_spec (m1 m2 : gmap K A) : m1 m2 i, m1 !! i m2 !! i.
......@@ -125,7 +125,7 @@ Definition map_cmra_mixin : CMRAMixin (gmap K A).
Proof.
split.
- by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
- by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
- by intros n m1 m2 Hm i; rewrite !lookup_core (Hm i).
- by intros n m1 m2 Hm ? i; rewrite -(Hm i).
- by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_div (Hm1 i) (Hm2 i).
- intros m; split.
......@@ -134,10 +134,10 @@ Proof.
- intros n m Hm i; apply cmra_validN_S, Hm.
- by intros m1 m2 m3 i; rewrite !lookup_op assoc.
- by intros m1 m2 i; rewrite !lookup_op comm.
- by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
- by intros m i; rewrite !lookup_unit cmra_unit_idemp.
- by intros m i; rewrite lookup_op !lookup_core cmra_core_l.
- by intros m i; rewrite !lookup_core cmra_core_idemp.
- intros x y; rewrite !map_included_spec; intros Hm i.
by rewrite !lookup_unit; apply cmra_unit_preserving.
by rewrite !lookup_core; apply cmra_core_preserving.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- intros x y; rewrite map_included_spec=> ? i.
......@@ -201,21 +201,21 @@ Lemma map_singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite map_singleton_validN. Qed.
Lemma map_insert_singleton_opN n m i x :
m !! i = None m !! i {n} Some (unit x) <[i:=x]> m {n} {[ i := x ]} m.
m !! i = None m !! i {n} Some (core x) <[i:=x]> m {n} {[ i := x ]} m.
Proof.
intros Hi j; destruct (decide (i = j)) as [->|];
[|by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id].
rewrite lookup_op lookup_insert lookup_singleton.
by destruct Hi as [->| ->]; constructor; rewrite ?cmra_unit_r.
by destruct Hi as [->| ->]; constructor; rewrite ?cmra_core_r.
Qed.
Lemma map_insert_singleton_op m i x :
m !! i = None m !! i Some (unit x) <[i:=x]> m {[ i := x ]} m.
m !! i = None m !! i Some (core x) <[i:=x]> m {[ i := x ]} m.
Proof.
rewrite !equiv_dist; naive_solver eauto using map_insert_singleton_opN.
Qed.
Lemma map_unit_singleton (i : K) (x : A) :
unit ({[ i := x ]} : gmap K A) = {[ i := unit x ]}.
Lemma map_core_singleton (i : K) (x : A) :
core ({[ i := x ]} : gmap K A) = {[ i := core x ]}.
Proof. apply map_fmap_singleton. Qed.
Lemma map_op_singleton (i : K) (x y : A) :
{[ i := x ]} {[ i := y ]} = ({[ i := x y ]} : gmap K A).
......@@ -315,7 +315,7 @@ End freshness.
(* Allocation is a local update: Just use composition with a singleton map. *)
(* Deallocation is *not* a local update. The trouble is that if we
own {[ i ↦ x ]}, then the frame could always own "unit x", and prevent
own {[ i ↦ x ]}, then the frame could always own "core x", and prevent
deallocation. *)
(* Applying a local update at a position we own is a local update. *)
......
......@@ -122,7 +122,7 @@ Instance frac_valid : Valid (frac A) := λ x,
Instance frac_validN : ValidN (frac A) := λ n x,
match x with Frac q a => (q 1)%Qc {n} a | FracUnit => True end.
Global Instance frac_empty : Empty (frac A) := FracUnit.
Instance frac_unit : Unit (frac A) := λ _, .
Instance frac_core : Core (frac A) := λ _, .
Instance frac_op : Op (frac A) := λ x y,
match x, y with
| Frac q1 a, Frac q2 b => Frac (q1 + q2) (a b)
......@@ -225,7 +225,7 @@ Qed.
Lemma frac_update (a1 a2 : A) p : a1 ~~> a2 Frac p a1 ~~> Frac p a2.
Proof.
intros Ha n [q b|] [??]; split; auto.
apply cmra_validN_op_l with (unit a1), Ha. by rewrite cmra_unit_r.
apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r.
Qed.
End cmra.
......
......@@ -117,13 +117,13 @@ Section iprod_cmra.
Implicit Types f g : iprod B.
Instance iprod_op : Op (iprod B) := λ f g x, f x g x.
Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
Instance iprod_core : Core (iprod B) := λ f x, core (f x).
Instance iprod_valid : Valid (iprod B) := λ f, x, f x.
Instance iprod_validN : ValidN (iprod B) := λ n f, x, {n} f x.
Instance iprod_div : Div (iprod B) := λ f g x, f x ÷ g x.
Definition iprod_lookup_op f g x : (f g) x = f x g x := eq_refl.
Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl.
Definition iprod_lookup_div f g x : (f ÷ g) x = f x ÷ g x := eq_refl.
Lemma iprod_included_spec (f g : iprod B) : f g x, f x g x.
......@@ -138,7 +138,7 @@ Section iprod_cmra.
Proof.
split.
- by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
- by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
- by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
- by intros n f1 f2 Hf ? x; rewrite -(Hf x).
- by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_div (Hf i) (Hg i).
- intros g; split.
......@@ -147,10 +147,10 @@ Section iprod_cmra.
- intros n f Hf x; apply cmra_validN_S, Hf.
- by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
- by intros f1 f2 x; rewrite iprod_lookup_op comm.
- by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l.
- by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp.
- by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
- by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
- intros f1 f2; rewrite !iprod_included_spec=> Hf x.
by rewrite iprod_lookup_unit; apply cmra_unit_preserving, Hf.
by rewrite iprod_lookup_core; apply cmra_core_preserving, Hf.
- intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- intros f1 f2; rewrite iprod_included_spec=> Hf x.
by rewrite iprod_lookup_op iprod_lookup_div cmra_op_div; try apply Hf.
......@@ -211,12 +211,12 @@ Section iprod_cmra.
by apply cmra_empty_validN.
Qed.
Lemma iprod_unit_singleton x (y : B x) :
unit (iprod_singleton x y) iprod_singleton x (unit y).
Lemma iprod_core_singleton x (y : B x) :
core (iprod_singleton x y) iprod_singleton x (core y).
Proof.
by move=>x'; destruct (decide (x = x')) as [->|];
rewrite iprod_lookup_unit ?iprod_lookup_singleton
?iprod_lookup_singleton_ne // cmra_unit_empty.
rewrite iprod_lookup_core ?iprod_lookup_singleton
?iprod_lookup_singleton_ne // cmra_core_empty.
Qed.
Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
......
......@@ -67,7 +67,7 @@ Instance option_valid : Valid (option A) := λ mx,
Instance option_validN : ValidN (option A) := λ n mx,
match mx with Some x => {n} x | None => True end.
Global Instance option_empty : Empty (option A) := None.
Instance option_unit : Unit (option A) := fmap unit.
Instance option_core : Core (option A) := fmap core.
Instance option_op : Op (option A) := union_with (λ x y, Some (x y)).
Instance option_div : Div (option A) :=
difference_with (λ x y, Some (x ÷ y)).
......@@ -99,10 +99,10 @@ Proof.
- intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
- intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
- intros [x|] [y|]; constructor; rewrite 1?comm; auto.
- by intros [x|]; constructor; rewrite cmra_unit_l.
- by intros [x|]; constructor; rewrite cmra_unit_idemp.
- by intros [x|]; constructor; rewrite cmra_core_l.
- by intros [x|]; constructor; rewrite cmra_core_idemp.
- intros mx my; rewrite !option_included ;intros [->|(x&y&->&->&?)]; auto.
right; exists (unit x), (unit y); eauto using cmra_unit_preserving.
right; exists (core x), (core y); eauto using cmra_core_preserving.
- intros n [x|] [y|]; rewrite /validN /option_validN /=;
eauto using cmra_validN_op_l.
- intros mx my; rewrite option_included.
......@@ -154,8 +154,8 @@ Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
Proof.
intros Hx Hy n [y|] ?.
{ destruct (Hx n y) as (y'&?&?); auto. exists (Some y'); auto. }
destruct (Hx n (unit x)) as (y'&?&?); rewrite ?cmra_unit_r; auto.
by exists (Some y'); split; [auto|apply cmra_validN_op_l with (unit x)].
destruct (Hx n (core x)) as (y'&?&?); rewrite ?cmra_core_r; auto.
by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
Qed.
Lemma option_updateP' (P : A Prop) x :
x ~~>: P Some x ~~>: λ y, default False y P.
......
......@@ -3,7 +3,7 @@ From algebra Require Export cmra.
From algebra Require Import dra.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /.
Local Arguments core _ _ !_ /.
(** * Definition of STSs *)
Module sts.
......@@ -192,7 +192,7 @@ Global Instance sts_valid : Valid (car sts) := λ x,
| auth s T => tok s T
| frag S' T => closed S' T S'
end.
Global Instance sts_unit : Unit (car sts) := λ x,
Global Instance sts_core : Core (car sts) := λ x,
match x with
| frag S' _ => frag (up_set S' )
| auth s _ => frag (up s )
......@@ -259,7 +259,7 @@ Proof.
- intros [s T|S T]; constructor; auto with sts.
+ rewrite (up_closed (up _ _)); auto using closed_up with sts.
+ rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.
- intros x y ?? (z&Hy&?&Hxz); exists (unit (x y)); split_and?.
- intros x y ?? (z&Hy&?&Hxz); exists (core (x y)); split_and?.
+ destruct Hxz; inversion_clear Hy; constructor; unfold up_set; set_solver.
+ destruct Hxz; inversion_clear Hy; simpl; split_and?;
auto using closed_up_set_empty, closed_up_empty, up_non_empty; [].
......
......@@ -227,11 +227,11 @@ Definition uPred_wand_eq :
@uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (unit x) |}.
{| uPred_holds n x := P n (core x) |}.
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
Next Obligation.
intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (unit x1);
eauto using cmra_unit_preserving, cmra_unit_validN.
intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (core x1);
eauto using cmra_core_preserving, cmra_core_validN.
Qed.
Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
Definition uPred_always {M} := proj1_sig uPred_always_aux M.
......@@ -432,7 +432,7 @@ Global Instance later_proper :
Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
Proof.
intros P1 P2 HP.
unseal; split=> n' x; split; apply HP; eauto using cmra_unit_validN.
unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
Qed.
Global Instance always_proper :
Proper (() ==> ()) (@uPred_always M) := ne_proper _.
......@@ -687,7 +687,7 @@ Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
Proof.
intros P; unseal; split=> n x Hvalid; split.
- intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
- by intros ?; exists (unit x), x; rewrite cmra_unit_l.
- by intros ?; exists (core x), x; rewrite cmra_core_l.
Qed.
Global Instance sep_comm : Comm () (@uPred_sep M).
Proof.
......@@ -836,13 +836,13 @@ Lemma always_const φ : (□ ■ φ : uPred M)%I ≡ (■ φ)%I.
Proof. by unseal. Qed.
Lemma always_elim P : P P.
Proof.
unseal; split=> n x ? /=; eauto using uPred_weaken, cmra_included_unit.
unseal; split=> n x ? /=; eauto using uPred_weaken, cmra_included_core.
Qed.
Lemma always_intro' P Q : P Q P Q.
Proof.
unseal=> HPQ.
split=> n x ??; apply HPQ; simpl; auto using cmra_unit_validN.
by rewrite cmra_unit_idemp.
split=> n x ??; apply HPQ; simpl; auto using cmra_core_validN.
by rewrite cmra_core_idemp.
Qed.
Lemma always_and P Q : ( (P Q))%I ( P Q)%I.
Proof. by unseal. Qed.
......@@ -855,12 +855,12 @@ Proof. by unseal. Qed.
Lemma always_and_sep_1 P Q : (P Q) (P Q).
Proof.
unseal; split=> n x ? [??].
exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
exists (core x), (core x); rewrite cmra_core_core; auto.
Qed.
Lemma always_and_sep_l_1 P Q : ( P Q) ( P Q).
Proof.
unseal; split=> n x ? [??]; exists (unit x), x; simpl in *.
by rewrite cmra_unit_l cmra_unit_idemp.
unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
by rewrite cmra_core_l cmra_core_idemp.
Qed.
Lemma always_later P : ( P)%I ( P)%I.
Proof. by unseal. Qed.
......@@ -939,7 +939,7 @@ Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
Proof.
unseal; split=> n x ?; split.
- destruct n as [|n]; simpl.
{ by exists x, (unit x); rewrite cmra_unit_r. }
{ by exists x, (core x); rewrite cmra_core_r. }
intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
......@@ -987,19 +987,19 @@ Lemma ownM_op (a1 a2 : M) :
Proof.
unseal; split=> n x ?; split.
- intros [z ?]; exists a1, (a2 z); split; [by rewrite (assoc op)|].
split. by exists (unit a1); rewrite cmra_unit_r. by exists z.
split. by exists (core a1); rewrite cmra_core_r. by exists z.
- intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 z2).
by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
Lemma always_ownM_unit (a : M) : ( uPred_ownM (unit a))%I uPred_ownM (unit a).
Lemma always_ownM_core (a : M) : ( uPred_ownM (core a))%I uPred_ownM (core a).
Proof.
split=> n x; split; [by apply always_elim|unseal; intros [a' Hx]]; simpl.
rewrite -(cmra_unit_idemp a) Hx.
apply cmra_unit_preservingN, cmra_includedN_l.
rewrite -(cmra_core_idemp a) Hx.
apply cmra_core_preservingN, cmra_includedN_l.
Qed.
Lemma always_ownM (a : M) : unit a a ( uPred_ownM a)%I uPred_ownM a.
Proof. by intros <-; rewrite always_ownM_unit. Qed.
Lemma always_ownM (a : M) : core a a ( uPred_ownM a)%I uPred_ownM a.
Proof. by intros <-; rewrite always_ownM_core. Qed.
Lemma ownM_something : True a, uPred_ownM a.
Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True uPred_ownM .
......@@ -1139,8 +1139,8 @@ Global Instance valid_always_stable {A : cmraT} (a : A) : AS (✓ a : uPred M)%I
Proof. by intros; rewrite /AlwaysStable always_valid. Qed.
Global Instance later_always_stable P : AS P AS ( P).
Proof. by intros; rewrite /AlwaysStable always_later; apply later_mono. Qed.
Global Instance ownM_unit_always_stable (a : M) : AS (uPred_ownM (unit a)).
Proof. by rewrite /AlwaysStable always_ownM_unit. Qed.
Global Instance ownM_core_always_stable (a : M) : AS (uPred_ownM (core a)).
Proof. by rewrite /AlwaysStable always_ownM_core. Qed.
Global Instance default_always_stable {A} P (Ψ : A uPred M) (mx : option A) :
AS P ( x, AS (Ψ x)) AS (default P mx Ψ).
Proof. destruct mx; apply _. Qed.
......
......@@ -64,7 +64,7 @@ Proof.
intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]);
rewrite /big_op ?right_id; auto.
constructor; last constructor.
apply Hht; by eauto using cmra_included_unit.
apply Hht; by eauto using cmra_included_core.
Qed.
Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
......
......@@ -36,10 +36,10 @@ Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ≡ (own γ a1 ★ own γ a2)%I.
Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
Global Instance own_mono γ : Proper (flip () ==> ()) (own γ).
Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
Lemma always_own_unit γ a : ( own γ (unit a))%I own γ (unit a).
Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
Lemma always_own γ a : unit a a ( own γ a)%I own γ a.
Proof. by intros <-; rewrite always_own_unit. Qed.
Lemma always_own_core γ a : ( own γ (core a))%I own γ (core a).
Proof. by rewrite /own -to_globalF_core always_ownG_core. Qed.
Lemma always_own γ a : core a a ( own γ a)%I own γ a.
Proof. by intros <-; rewrite always_own_core. Qed.
Lemma own_valid γ a : own γ a a.
Proof.
rewrite /own ownG_valid /to_globalF.
......@@ -59,8 +59,8 @@ Proof.
Abort.
Global Instance own_timeless γ a : Timeless a TimelessP (own γ a).
Proof. unfold own; apply _. Qed.
Global Instance own_unit_always_stable γ a : AlwaysStable (own γ (unit a)).
Proof. by rewrite /AlwaysStable always_own_unit. Qed.
Global Instance own_core_always_stable γ a : AlwaysStable (own γ (core a)).
Proof. by rewrite /AlwaysStable always_own_core. Qed.
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
......
......@@ -42,10 +42,10 @@ Lemma to_globalF_op γ a1 a2 :
Proof.
by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
Qed.
Lemma to_globalF_unit γ a : unit (to_globalF γ a) to_globalF γ (unit a).
Lemma to_globalF_core γ a : core (to_globalF γ a) to_globalF γ (core a).
Proof.
by rewrite /to_globalF
iprod_unit_singleton map_unit_singleton cmra_transport_unit.
iprod_core_singleton map_core_singleton cmra_transport_core.
Qed.
Global Instance to_globalF_timeless γ m : Timeless m Timeless (to_globalF γ m).
Proof. rewrite /to_globalF; apply _. Qed.
......
......@@ -28,7 +28,7 @@ Qed.
Lemma always_ownI i P : ( ownI i P)%I ownI i P.
Proof.
apply uPred.always_ownM.
by rewrite Res_unit !cmra_unit_empty map_unit_singleton.
by rewrite Res_core !cmra_core_empty map_core_singleton.
Qed.
Global Instance ownI_always_stable i P : AlwaysStable (ownI i P).
Proof. by rewrite /AlwaysStable always_ownI. Qed.
......@@ -52,13 +52,13 @@ Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
Global Instance ownG_mono : Proper (flip () ==> ()) (@ownG Λ Σ).
Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
Lemma always_ownG_unit m : ( ownG (unit m))%I ownG (unit m).
Lemma always_ownG_core m : ( ownG (core m))%I ownG (core m).
Proof.
apply uPred.always_ownM.
by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idemp m).
by rewrite Res_core !cmra_core_empty -{2}(cmra_core_idemp m).
Qed.
Lemma always_ownG m : unit m m ( ownG m)%I ownG m.
Proof. by intros <-; rewrite always_ownG_unit. Qed.
Lemma always_ownG m : core m m ( ownG m)%I ownG m.
Proof. by intros <-; rewrite always_ownG_core. Qed.
Lemma ownG_valid m : ownG m m.
Proof.
rewrite /ownG uPred.ownM_valid res_validI /=; auto with I.
......@@ -69,8 +69,8 @@ Lemma ownG_empty : True ⊑ (ownG ∅ : iProp Λ Σ).
Proof. apply uPred.ownM_empty. Qed.
Global Instance ownG_timeless m : Timeless m TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownG_unit_always_stable m : AlwaysStable (ownG (unit m)).
Proof. by rewrite /AlwaysStable always_ownG_unit. Qed.
Global Instance ownG_core_always_stable m : AlwaysStable (ownG (core m)).
Proof. by rewrite /AlwaysStable always_ownG_core. Qed.
(* inversion lemmas *)
Lemma ownI_spec n r i P :
......
......@@ -74,8 +74,8 @@ Proof. by destruct 3; constructor; try apply: timeless. Qed.
Instance res_op : Op (res Λ A M) := λ r1 r2,
Res (wld r1 wld r2) (pst r1 pst r2) (gst r1 gst r2).
Global Instance res_empty `{Empty M} : Empty (res Λ A M) := Res .
Instance res_unit : Unit (res Λ A M) := λ r,
Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
Instance res_core : Core (res Λ A M) := λ r,
Res (core (wld r)) (core (pst r)) (core (gst r)).
Instance res_valid : Valid (res Λ A M) := λ r, wld r pst r gst r.
Instance res_validN : ValidN (res Λ A M) := λ n r,
{n} wld r {n} pst r {n} gst r.
......@@ -109,10 +109,10 @@ Proof.
- by intros n ? (?&?&?); split_and!; apply cmra_validN_S.
- by intros ???; constructor; rewrite /= assoc.
- by intros ??; constructor; rewrite /= comm.
- by intros ?; constructor; rewrite /= cmra_unit_l.
- by intros ?; constructor; rewrite /= cmra_unit_idemp.
- by intros ?; constructor; rewrite /= cmra_core_l.
- by intros ?; constructor; rewrite /= cmra_core_idemp.
- intros r1 r2; rewrite !res_included.
by intros (?&?&?); split_and!; apply cmra_unit_preserving.
by intros (?&?&?); split_and!; apply cmra_core_preserving.
- intros n r1 r2 (?&?&?);
split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
- intros r1 r2; rewrite res_included; intros (?&?&?).
......@@ -144,7 +144,7 @@ Proof. by intros (?&?&?). Qed.
Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
Res w1 σ1 m1 Res w2 σ2 m2 = Res (w1 w2) (σ1 σ2) (m1 m2).
Proof. done. Qed.
Lemma Res_unit w σ m : unit (Res w σ m) = Res (unit w) (unit σ) (unit m).
Lemma Res_core w σ m : core (Res w σ m) = Res (core w) (core σ) (core m).
Proof. done. Qed.
Lemma lookup_wld_op_l n r1 r2 i P :
{n} (r1r2) wld r1 !! i {n} Some P (wld r1 wld r2) !! i {n} Some P.
......