Library iris.algebra.dra
From iris.algebra Require Export cmra updates.
Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A, Step A} := {
mixin_dra_equivalence : Equivalence ((≡) : relation A);
mixin_dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (⋅);
mixin_dra_core_proper : Proper ((≡) ==> (≡)) core;
mixin_dra_valid_proper : Proper ((≡) ==> impl) valid;
mixin_dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x);
mixin_dra_step_proper : Proper ((≡) ==> (≡) ==> impl) step;
mixin_dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
mixin_dra_core_valid x : ✓ x → ✓ core x;
mixin_dra_assoc : Assoc (≡) (⋅);
mixin_dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
mixin_dra_disjoint_move_l x y z :
✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
mixin_dra_symmetric : Symmetric (@disjoint A _);
mixin_dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
mixin_dra_core_disjoint_l x : ✓ x → core x ⊥ x;
mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
mixin_dra_core_mono x y :
∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z;
mixin_dra_core_distrib x y :
✓ x → ✓ y → core x ⊥ core y → core (core x ⋅ core y) ≡ core x ⋅ core y;
}.
Structure draT := DRAT {
dra_car :> Type;
dra_equiv : Equiv dra_car;
dra_core : Core dra_car;
dra_disjoint : Disjoint dra_car;
dra_op : Op dra_car;
dra_valid : Valid dra_car;
dra_step : Step dra_car;
dra_mixin : DRAMixin dra_car
}.
Arguments DRAT _ {_ _ _ _ _ _} _.
Arguments dra_car : simpl never.
Arguments dra_equiv : simpl never.
Arguments dra_core : simpl never.
Arguments dra_disjoint : simpl never.
Arguments dra_op : simpl never.
Arguments dra_valid : simpl never.
Arguments dra_step : simpl never.
Arguments dra_mixin : simpl never.
Add Printing Constructor draT.
Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid dra_step.
Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A, Step A} := {
mixin_dra_equivalence : Equivalence ((≡) : relation A);
mixin_dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (⋅);
mixin_dra_core_proper : Proper ((≡) ==> (≡)) core;
mixin_dra_valid_proper : Proper ((≡) ==> impl) valid;
mixin_dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x);
mixin_dra_step_proper : Proper ((≡) ==> (≡) ==> impl) step;
mixin_dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
mixin_dra_core_valid x : ✓ x → ✓ core x;
mixin_dra_assoc : Assoc (≡) (⋅);
mixin_dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
mixin_dra_disjoint_move_l x y z :
✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
mixin_dra_symmetric : Symmetric (@disjoint A _);
mixin_dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
mixin_dra_core_disjoint_l x : ✓ x → core x ⊥ x;
mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
mixin_dra_core_mono x y :
∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z;
mixin_dra_core_distrib x y :
✓ x → ✓ y → core x ⊥ core y → core (core x ⋅ core y) ≡ core x ⋅ core y;
}.
Structure draT := DRAT {
dra_car :> Type;
dra_equiv : Equiv dra_car;
dra_core : Core dra_car;
dra_disjoint : Disjoint dra_car;
dra_op : Op dra_car;
dra_valid : Valid dra_car;
dra_step : Step dra_car;
dra_mixin : DRAMixin dra_car
}.
Arguments DRAT _ {_ _ _ _ _ _} _.
Arguments dra_car : simpl never.
Arguments dra_equiv : simpl never.
Arguments dra_core : simpl never.
Arguments dra_disjoint : simpl never.
Arguments dra_op : simpl never.
Arguments dra_valid : simpl never.
Arguments dra_step : simpl never.
Arguments dra_mixin : simpl never.
Add Printing Constructor draT.
Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid dra_step.
Lifting properties from the mixin
Section dra_mixin.
Context {A : draT}.
Implicit Types x y : A.
Global Instance dra_equivalence : Equivalence ((≡) : relation A).
Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
Global Instance dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
Global Instance dra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
Global Instance dra_valid_proper : Proper ((≡) ==> impl) (@valid A _).
Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
Global Instance dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x).
Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed.
Global Instance dra_step_proper : Proper ((≡) ==> (≡) ==> impl) (@step A _).
Proof. apply (mixin_dra_step_proper _ (dra_mixin A)). Qed.
Lemma dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y).
Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
Lemma dra_core_valid x : ✓ x → ✓ core x.
Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
Global Instance dra_assoc : Assoc (≡) (@op A _).
Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
Lemma dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z.
Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
Lemma dra_disjoint_move_l x y z :
✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z.
Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed.
Global Instance dra_symmetric : Symmetric (@disjoint A _).
Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed.
Lemma dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x.
Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
Lemma dra_core_disjoint_l x : ✓ x → core x ⊥ x.
Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed.
Lemma dra_core_l x : ✓ x → core x ⋅ x ≡ x.
Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
Lemma dra_core_mono x y :
∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z.
Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
Lemma dra_core_distrib x y:
✓ x → ✓ y → core x ⊥ core y → core (core x ⋅ core y) ≡ core x ⋅ core y.
Proof. apply (mixin_dra_core_distrib _ (dra_mixin A)). Qed.
End dra_mixin.
Record validity (A : draT) := Validity {
validity_car : A;
validity_is_valid : Prop;
validity_prf : validity_is_valid → valid validity_car
}.
Add Printing Constructor validity.
Arguments Validity {_} _ _ _.
Arguments validity_car {_} _.
Arguments validity_is_valid {_} _.
Definition to_validity {A : draT} (x : A) : validity A :=
Validity x (valid x) id.
Section dra.
Context (A : draT).
Implicit Types a b : A.
Implicit Types x y z : validity A.
Arguments valid _ _ !_ /.
Instance validity_valid : Valid (validity A) := validity_is_valid.
Instance validity_equiv : Equiv (validity A) := λ x y,
(valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
Instance validity_equivalence : Equivalence (@equiv (validity A) _).
Proof.
split; unfold equiv, validity_equiv.
- by intros [x px ?]; simpl.
- intros [x px ?] [y py ?]; naive_solver.
- intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in ×.
split; [|intros; trans y]; tauto.
Qed.
Canonical Structure validityC : cofeT := discreteC (validity A).
Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
Proof. by split; apply: dra_valid_proper. Qed.
Global Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A).
Proof.
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 a b c : ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⊥ b.
Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_lr a b c : ✓ a → ✓ b → ✓ c → a ⊥ b → a ⋅ b ⊥ c → b ⊥ c.
Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_move_r a b c :
✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⋅ b ⊥ c.
Proof.
intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
apply dra_disjoint_move_l; auto; by rewrite dra_comm.
Qed.
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Lemma dra_disjoint_ll_rr a1 a2 b1 b2:
✓ a1 → ✓ a2 → ✓ b1 → ✓ b2 → a1 ⊥ a2 → b1 ⊥ b2 →
a1 ⋅ a2 ⊥ b1 ⋅ b2 → a1 ⊥ b1.
Proof.
intros ?????? Hdisj.
eapply dra_disjoint_rl in Hdisj; eauto using dra_op_valid.
eapply dra_disjoint_ll in Hdisj; eauto using dra_op_valid.
Qed.
Lemma dra_disjoint_core a b: ✓ a → ✓ b → a ⊥ b → core a ⊥ core b.
Proof.
intros Hva Hvb Hdisj.
rewrite -{1}(dra_core_l a) //= -{1}(dra_core_l b) //= in Hdisj × ⇒ Hdisj.
eapply dra_disjoint_ll_rr; last apply Hdisj;
eauto using dra_core_valid, dra_core_disjoint_l.
Qed.
Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
Program Instance validity_pcore : PCore (validity A) := λ x,
Some (Validity (core (validity_car x)) (✓ x) _).
Solve Obligations with naive_solver eauto using dra_core_valid.
Program Instance validity_op : Op (validity A) := λ x y,
Validity (validity_car x ⋅ validity_car y)
(✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _.
Solve Obligations with naive_solver eauto using dra_op_valid.
Program Instance validity_step : Step (validity A) := λ x y,
(✓ x ↔ ✓ y) ∧ (✓ x → (validity_car x ⤳ validity_car y)).
Definition validity_ra_mixin : RAMixin (validity A).
Proof.
apply ra_total_mixin; first eauto.
- intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
split; intros (?&?&?); split_and!;
first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
- by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
- intros ?? [??]; naive_solver.
- intros [x px ?] [y py ?] [[Hbir Hbil] Heq] [x' px' ?] [y' py' ?] [[Hbir' Hbil'] Heq'].
simpl in *; rewrite /step /validity_step; intros (Hb & Hstep); simpl in ×.
split_and?; try naive_solver; intros.
eapply dra_step_proper; [ eapply Heq | eapply Heq' |]; naive_solver.
- intros [x px ?] [y py ?] [z pz ?]; split; simpl;
[intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
|intros; by rewrite assoc].
- intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
- intros [x px ?]; split;
naive_solver eauto using dra_core_l, dra_core_disjoint_l.
- intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
- intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in ×.
destruct (dra_core_mono x z) as (z'&Hz').
unshelve eexists (Validity z' (px ∧ py ∧ pz) _); [|split; simpl].
{ intros (?&?&?); apply Hz'; tauto. }
+ tauto.
+ intros. rewrite Hy //. tauto.
- intros [x px ?] [y py ?] Hval.
rewrite /core //= /validity_pcore //=.
constructor.
× split; auto.
× simpl. intros (?&?&?). rewrite dra_core_distrib; eauto.
- by intros [x px ?] [y py ?] (?&?&?).
Qed.
Canonical Structure validityR : cmraT :=
discreteR (validity A) validity_ra_mixin.
Global Instance validity_cmra_total : CMRATotal validityR.
Proof. rewrite /CMRATotal; eauto. Qed.
Lemma validity_update x y :
(∀ c, ✓ x → ✓ c → validity_car x ⊥ c → ✓ y ∧ validity_car y ⊥ c) → x ~~> y.
Proof.
intros Hxy; apply cmra_discrete_update⇒ z [?[??]].
split_and!; try eapply Hxy; eauto.
Qed.
Lemma to_validity_op a b :
(✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ⊥ b) →
to_validity (a ⋅ b) ≡ to_validity a ⋅ to_validity b.
Proof. split; naive_solver eauto using dra_op_valid. Qed.
End dra.
Context {A : draT}.
Implicit Types x y : A.
Global Instance dra_equivalence : Equivalence ((≡) : relation A).
Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
Global Instance dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
Global Instance dra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
Global Instance dra_valid_proper : Proper ((≡) ==> impl) (@valid A _).
Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
Global Instance dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x).
Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed.
Global Instance dra_step_proper : Proper ((≡) ==> (≡) ==> impl) (@step A _).
Proof. apply (mixin_dra_step_proper _ (dra_mixin A)). Qed.
Lemma dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y).
Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
Lemma dra_core_valid x : ✓ x → ✓ core x.
Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
Global Instance dra_assoc : Assoc (≡) (@op A _).
Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
Lemma dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z.
Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
Lemma dra_disjoint_move_l x y z :
✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z.
Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed.
Global Instance dra_symmetric : Symmetric (@disjoint A _).
Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed.
Lemma dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x.
Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
Lemma dra_core_disjoint_l x : ✓ x → core x ⊥ x.
Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed.
Lemma dra_core_l x : ✓ x → core x ⋅ x ≡ x.
Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
Lemma dra_core_mono x y :
∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z.
Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
Lemma dra_core_distrib x y:
✓ x → ✓ y → core x ⊥ core y → core (core x ⋅ core y) ≡ core x ⋅ core y.
Proof. apply (mixin_dra_core_distrib _ (dra_mixin A)). Qed.
End dra_mixin.
Record validity (A : draT) := Validity {
validity_car : A;
validity_is_valid : Prop;
validity_prf : validity_is_valid → valid validity_car
}.
Add Printing Constructor validity.
Arguments Validity {_} _ _ _.
Arguments validity_car {_} _.
Arguments validity_is_valid {_} _.
Definition to_validity {A : draT} (x : A) : validity A :=
Validity x (valid x) id.
Section dra.
Context (A : draT).
Implicit Types a b : A.
Implicit Types x y z : validity A.
Arguments valid _ _ !_ /.
Instance validity_valid : Valid (validity A) := validity_is_valid.
Instance validity_equiv : Equiv (validity A) := λ x y,
(valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
Instance validity_equivalence : Equivalence (@equiv (validity A) _).
Proof.
split; unfold equiv, validity_equiv.
- by intros [x px ?]; simpl.
- intros [x px ?] [y py ?]; naive_solver.
- intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in ×.
split; [|intros; trans y]; tauto.
Qed.
Canonical Structure validityC : cofeT := discreteC (validity A).
Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
Proof. by split; apply: dra_valid_proper. Qed.
Global Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A).
Proof.
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 a b c : ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⊥ b.
Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_lr a b c : ✓ a → ✓ b → ✓ c → a ⊥ b → a ⋅ b ⊥ c → b ⊥ c.
Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_move_r a b c :
✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⋅ b ⊥ c.
Proof.
intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
apply dra_disjoint_move_l; auto; by rewrite dra_comm.
Qed.
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Lemma dra_disjoint_ll_rr a1 a2 b1 b2:
✓ a1 → ✓ a2 → ✓ b1 → ✓ b2 → a1 ⊥ a2 → b1 ⊥ b2 →
a1 ⋅ a2 ⊥ b1 ⋅ b2 → a1 ⊥ b1.
Proof.
intros ?????? Hdisj.
eapply dra_disjoint_rl in Hdisj; eauto using dra_op_valid.
eapply dra_disjoint_ll in Hdisj; eauto using dra_op_valid.
Qed.
Lemma dra_disjoint_core a b: ✓ a → ✓ b → a ⊥ b → core a ⊥ core b.
Proof.
intros Hva Hvb Hdisj.
rewrite -{1}(dra_core_l a) //= -{1}(dra_core_l b) //= in Hdisj × ⇒ Hdisj.
eapply dra_disjoint_ll_rr; last apply Hdisj;
eauto using dra_core_valid, dra_core_disjoint_l.
Qed.
Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
Program Instance validity_pcore : PCore (validity A) := λ x,
Some (Validity (core (validity_car x)) (✓ x) _).
Solve Obligations with naive_solver eauto using dra_core_valid.
Program Instance validity_op : Op (validity A) := λ x y,
Validity (validity_car x ⋅ validity_car y)
(✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _.
Solve Obligations with naive_solver eauto using dra_op_valid.
Program Instance validity_step : Step (validity A) := λ x y,
(✓ x ↔ ✓ y) ∧ (✓ x → (validity_car x ⤳ validity_car y)).
Definition validity_ra_mixin : RAMixin (validity A).
Proof.
apply ra_total_mixin; first eauto.
- intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
split; intros (?&?&?); split_and!;
first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
- by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
- intros ?? [??]; naive_solver.
- intros [x px ?] [y py ?] [[Hbir Hbil] Heq] [x' px' ?] [y' py' ?] [[Hbir' Hbil'] Heq'].
simpl in *; rewrite /step /validity_step; intros (Hb & Hstep); simpl in ×.
split_and?; try naive_solver; intros.
eapply dra_step_proper; [ eapply Heq | eapply Heq' |]; naive_solver.
- intros [x px ?] [y py ?] [z pz ?]; split; simpl;
[intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
|intros; by rewrite assoc].
- intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
- intros [x px ?]; split;
naive_solver eauto using dra_core_l, dra_core_disjoint_l.
- intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
- intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in ×.
destruct (dra_core_mono x z) as (z'&Hz').
unshelve eexists (Validity z' (px ∧ py ∧ pz) _); [|split; simpl].
{ intros (?&?&?); apply Hz'; tauto. }
+ tauto.
+ intros. rewrite Hy //. tauto.
- intros [x px ?] [y py ?] Hval.
rewrite /core //= /validity_pcore //=.
constructor.
× split; auto.
× simpl. intros (?&?&?). rewrite dra_core_distrib; eauto.
- by intros [x px ?] [y py ?] (?&?&?).
Qed.
Canonical Structure validityR : cmraT :=
discreteR (validity A) validity_ra_mixin.
Global Instance validity_cmra_total : CMRATotal validityR.
Proof. rewrite /CMRATotal; eauto. Qed.
Lemma validity_update x y :
(∀ c, ✓ x → ✓ c → validity_car x ⊥ c → ✓ y ∧ validity_car y ⊥ c) → x ~~> y.
Proof.
intros Hxy; apply cmra_discrete_update⇒ z [?[??]].
split_and!; try eapply Hxy; eauto.
Qed.
Lemma to_validity_op a b :
(✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ⊥ b) →
to_validity (a ⋅ b) ≡ to_validity a ⋅ to_validity b.
Proof. split; naive_solver eauto using dra_op_valid. Qed.
End dra.