Skip to content
Snippets Groups Projects
Commit 1a5d366d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/auth_valid' into 'master' 

Add lemmas for validity of `●{_} _ ⋅ ●{_} _` for both view and auth.

See merge request iris/iris!551
parents 14a7cd8c 53d1f7f1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/algebra/auth.v
+ 69
− 51
View file @ 1a5d366d
......@@ -100,11 +100,71 @@ Section auth.
Global Instance auth_frag_inj : Inj (≡) (≡) (@auth_frag A).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete (authO A).
Proof. apply _. Qed.
Global Instance auth_auth_discrete q a :
Discrete a → Discrete (ε : A) → Discrete (●{q} a).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_cmra_discrete : CmraDiscrete A → CmraDiscrete (authR A).
Proof. apply _. Qed.
(** Operation *)
Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
Proof. apply view_auth_frac_op. Qed.
Global Instance auth_auth_frac_is_op q q1 q2 a :
IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
Proof. rewrite /auth_auth. apply _. Qed.
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
Proof. apply view_frag_op. Qed.
Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
Proof. apply view_frag_mono. Qed.
Lemma auth_frag_core a : core (◯ a) = ◯ (core a).
Proof. apply view_frag_core. Qed.
Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_frag_is_op a b1 b2 :
IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_frag_sep_homomorphism :
MonoidHomomorphism op op (≡) (@auth_frag A).
Proof. rewrite /auth_frag. apply _. Qed.
Lemma big_opL_auth_frag {B} (g : nat → B → A) (l : list B) :
(◯ [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯ (g k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_opM_auth_frag `{Countable K} {B} (g : K → B → A) (m : gmap K B) :
(◯ [^op map] k↦x ∈ m, g k x) ≡ [^op map] k↦x ∈ m, ◯ (g k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_opS_auth_frag `{Countable B} (g : B → A) (X : gset B) :
(◯ [^op set] x ∈ X, g x) ≡ [^op set] x ∈ X, ◯ (g x).
Proof. apply (big_opS_commute _). Qed.
Lemma big_opMS_auth_frag `{Countable B} (g : B → A) (X : gmultiset B) :
(◯ [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯ (g x).
Proof. apply (big_opMS_commute _). Qed.
(** Validity *)
Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
Proof. apply view_auth_frac_op_invN. Qed.
Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
Proof. apply view_auth_frac_op_inv. Qed.
Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
✓ (●{p} a ⋅ ●{q} b) → a = b.
Proof. by apply view_auth_frac_op_inv_L. Qed.
Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
Proof. by rewrite view_auth_frac_op_validN auth_view_rel_unit. Qed.
Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2) ↔ False.
Proof. apply view_auth_op_validN. Qed.
(** The following lemmas are also stated as implications, which can be used
to force [apply] to use the lemma in the right direction. *)
Lemma auth_frag_validN n b : ✓{n} (◯ b) ↔ ✓{n} b.
......@@ -137,6 +197,15 @@ Section auth.
by setoid_rewrite auth_view_rel_unit.
Qed.
Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
Proof.
rewrite view_auth_frac_op_valid !cmra_valid_validN.
by setoid_rewrite auth_view_rel_unit.
Qed.
Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2) ↔ False.
Proof. apply view_auth_op_valid. Qed.
(** The following lemmas are also stated as implications, which can be used
to force [apply] to use the lemma in the right direction. *)
Lemma auth_frag_valid b : ✓ (◯ b) ↔ ✓ b.
......@@ -191,57 +260,6 @@ Section auth.
✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
Proof. rewrite auth_both_frac_valid_discrete frac_valid'. naive_solver. Qed.
Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete (authO A).
Proof. apply _. Qed.
Global Instance auth_auth_discrete q a :
Discrete a → Discrete (ε : A) → Discrete (●{q} a).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_cmra_discrete : CmraDiscrete A → CmraDiscrete (authR A).
Proof. apply _. Qed.
Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
Proof. apply view_auth_frac_op. Qed.
Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
Proof. apply view_auth_frac_op_invN. Qed.
Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
Proof. apply view_auth_frac_op_inv. Qed.
Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
✓ (●{p} a ⋅ ●{q} b) → a = b.
Proof. by apply view_auth_frac_op_inv_L. Qed.
Global Instance auth_auth_frac_is_op q q1 q2 a :
IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
Proof. rewrite /auth_auth. apply _. Qed.
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
Proof. apply view_frag_op. Qed.
Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
Proof. apply view_frag_mono. Qed.
Lemma auth_frag_core a : core (◯ a) = ◯ (core a).
Proof. apply view_frag_core. Qed.
Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_frag_is_op a b1 b2 :
IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_frag_sep_homomorphism :
MonoidHomomorphism op op (≡) (@auth_frag A).
Proof. rewrite /auth_frag. apply _. Qed.
Lemma big_opL_auth_frag {B} (g : nat → B → A) (l : list B) :
(◯ [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯ (g k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_opM_auth_frag `{Countable K} {B} (g : K → B → A) (m : gmap K B) :
(◯ [^op map] k↦x ∈ m, g k x) ≡ [^op map] k↦x ∈ m, ◯ (g k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_opS_auth_frag `{Countable B} (g : B → A) (X : gset B) :
(◯ [^op set] x ∈ X, g x) ≡ [^op set] x ∈ X, ◯ (g x).
Proof. apply (big_opS_commute _). Qed.
Lemma big_opMS_auth_frag `{Countable B} (g : B → A) (X : gmultiset B) :
(◯ [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯ (g x).
Proof. apply (big_opMS_commute _). Qed.
(** Inclusion *)
Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
●{p1} a1 ≼{n} ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2.
......
theories/algebra/lib/gmap_view.v
+ 25
− 14
View file @ 1a5d366d
......@@ -108,6 +108,9 @@ Section rel.
- intros k'. rewrite !lookup_insert_None. naive_solver.
Qed.
Local Lemma gmap_view_rel_unit n m : gmap_view_rel n m ε.
Proof. apply: map_Forall_empty. Qed.
Local Lemma gmap_view_rel_discrete :
OfeDiscrete V → ViewRelDiscrete gmap_view_rel.
Proof.
......@@ -174,18 +177,13 @@ Section lemmas.
Qed.
(** Composition and validity *)
Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ ✓ q.
Proof.
rewrite view_auth_frac_valid. split; first by naive_solver.
intros. split; first done.
intros n l ? Hl. rewrite lookup_empty in Hl. done.
Qed.
Lemma gmap_view_auth_valid m : ✓ gmap_view_auth 1 m.
Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
Lemma gmap_view_auth_frac_op p q m :
gmap_view_auth (p + q) m ≡ gmap_view_auth p m ⋅ gmap_view_auth q m.
Proof. apply view_auth_frac_op. Qed.
Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
Proof. rewrite /gmap_view_auth. apply _. Qed.
Lemma gmap_view_auth_frac_op_invN n p m1 q m2 :
✓{n} (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡{n}≡ m2.
Proof. apply view_auth_frac_op_invN. Qed.
......@@ -195,9 +193,22 @@ Section lemmas.
Lemma gmap_view_auth_frac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 = m2.
Proof. apply view_auth_frac_op_inv_L, _. Qed.
Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
Proof. rewrite /gmap_view_auth. apply _. Qed.
Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ ✓ q.
Proof.
rewrite view_auth_frac_valid. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_valid m : ✓ gmap_view_auth 1 m.
Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 ≡ m2.
Proof.
rewrite view_auth_frac_op_valid. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_op_valid m1 m2 :
✓ (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
Proof. apply view_auth_op_valid. Qed.
Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
Proof.
......@@ -256,8 +267,8 @@ Section lemmas.
rewrite view_both_frac_valid. setoid_rewrite gmap_view_rel_lookup.
split=>[[Hq Hm]|[Hq Hm]].
- split; first done. split.
+ apply (Hm 0%nat).
+ apply equiv_dist=>n. apply Hm.
+ apply (Hm 0%nat).
+ apply equiv_dist=>n. apply Hm.
- split; first done. split.
+ apply Hm.
+ revert n. apply equiv_dist. apply Hm.
......
theories/algebra/view.v
+ 82
− 55
View file @ 1a5d366d
......@@ -204,47 +204,6 @@ Section cmra.
| None => ∃ a, rel n a (view_frag_proj x)
end := eq_refl _.
Lemma view_auth_frac_validN n q a : ✓{n} (●V{q} a) ↔ ✓{n} q ∧ rel n a ε.
Proof.
rewrite view_validN_eq /=. apply and_iff_compat_l. split; [|by eauto].
by intros [? [->%(inj to_agree) ?]].
Qed.
Lemma view_auth_validN n a : ✓{n} (●V a) ↔ rel n a ε.
Proof.
rewrite view_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
Qed.
Lemma view_frag_validN n b : ✓{n} (◯V b) ↔ ∃ a, rel n a b.
Proof. done. Qed.
Lemma view_both_frac_validN n q a b :
✓{n} (●V{q} a ⋅ ◯V b) ↔ ✓{n} q ∧ rel n a b.
Proof.
rewrite view_validN_eq /=. apply and_iff_compat_l.
setoid_rewrite (left_id _ _ b). split; [|by eauto].
by intros [?[->%(inj to_agree)]].
Qed.
Lemma view_both_validN n a b : ✓{n} (●V a ⋅ ◯V b) ↔ rel n a b.
Proof.
rewrite view_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
Qed.
Lemma view_auth_frac_valid q a : ✓ (●V{q} a) ↔ ✓ q ∧ ∀ n, rel n a ε.
Proof.
rewrite view_valid_eq /=. apply and_iff_compat_l. split; [|by eauto].
intros H n. by destruct (H n) as [? [->%(inj to_agree) ?]].
Qed.
Lemma view_auth_valid a : ✓ (●V a) ↔ ∀ n, rel n a ε.
Proof. rewrite view_auth_frac_valid frac_valid'. naive_solver. Qed.
Lemma view_frag_valid b : ✓ (◯V b) ↔ ∀ n, ∃ a, rel n a b.
Proof. done. Qed.
Lemma view_both_frac_valid q a b : ✓ (●V{q} a ⋅ ◯V b) ↔ ✓ q ∧ ∀ n, rel n a b.
Proof.
rewrite view_valid_eq /=. apply and_iff_compat_l.
setoid_rewrite (left_id _ _ b). split; [|by eauto].
intros H n. by destruct (H n) as [?[->%(inj to_agree)]].
Qed.
Lemma view_both_valid a b : ✓ (●V a ⋅ ◯V b) ↔ ∀ n, rel n a b.
Proof. rewrite view_both_frac_valid frac_valid'. naive_solver. Qed.
Lemma view_cmra_mixin : CmraMixin (view rel).
Proof.
apply (iso_cmra_mixin_restrict
......@@ -304,25 +263,12 @@ Section cmra.
Qed.
Canonical Structure viewUR := UcmraT (view rel) view_ucmra_mixin.
(** Operation *)
Lemma view_auth_frac_op p1 p2 a : ●V{p1 + p2} a ≡ ●V{p1} a ⋅ ●V{p2} a.
Proof.
intros; split; simpl; last by rewrite left_id.
by rewrite -Some_op -pair_op agree_idemp.
Qed.
Lemma view_auth_frac_op_invN n p1 a1 p2 a2 :
✓{n} (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡{n}≡ a2.
Proof.
rewrite /op /view_op /= left_id -Some_op -pair_op view_validN_eq /=.
intros (?&?& Eq &?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
Qed.
Lemma view_auth_frac_op_inv p1 a1 p2 a2 : ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡ a2.
Proof.
intros ?. apply equiv_dist. intros n.
by eapply view_auth_frac_op_invN, cmra_valid_validN.
Qed.
Lemma view_auth_frac_op_inv_L `{!LeibnizEquiv A} p1 a1 p2 a2 :
✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 = a2.
Proof. by intros ?%view_auth_frac_op_inv%leibniz_equiv. Qed.
Global Instance view_auth_frac_is_op q q1 q2 a :
IsOp q q1 q2 → IsOp' (●V{q} a) (●V{q1} a) (●V{q2} a).
Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_frac_op. Qed.
......@@ -355,6 +301,87 @@ Section cmra.
(◯V [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯V (g x).
Proof. apply (big_opMS_commute _). Qed.
(** Validity *)
Lemma view_auth_frac_op_invN n p1 a1 p2 a2 :
✓{n} (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡{n}≡ a2.
Proof.
rewrite /op /view_op /= left_id -Some_op -pair_op view_validN_eq /=.
intros (?&?& Eq &?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
Qed.
Lemma view_auth_frac_op_inv p1 a1 p2 a2 : ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡ a2.
Proof.
intros ?. apply equiv_dist. intros n.
by eapply view_auth_frac_op_invN, cmra_valid_validN.
Qed.
Lemma view_auth_frac_op_inv_L `{!LeibnizEquiv A} p1 a1 p2 a2 :
✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 = a2.
Proof. by intros ?%view_auth_frac_op_inv%leibniz_equiv. Qed.
Lemma view_auth_frac_validN n q a : ✓{n} (●V{q} a) ↔ ✓{n} q ∧ rel n a ε.
Proof.
rewrite view_validN_eq /=. apply and_iff_compat_l. split; [|by eauto].
by intros [? [->%(inj to_agree) ?]].
Qed.
Lemma view_auth_validN n a : ✓{n} (●V a) ↔ rel n a ε.
Proof.
rewrite view_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
Qed.
Lemma view_auth_frac_op_validN n q1 q2 a1 a2 :
✓{n} (●V{q1} a1 ⋅ ●V{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ rel n a1 ε.
Proof.
split.
- intros Hval. assert (a1 ≡{n}≡ a2) as Ha by eauto using view_auth_frac_op_invN.
revert Hval. rewrite Ha -view_auth_frac_op view_auth_frac_validN. naive_solver.
- intros (?&->&?). by rewrite -view_auth_frac_op view_auth_frac_validN.
Qed.
Lemma view_auth_op_validN n a1 a2 : ✓{n} (●V a1 ⋅ ●V a2) ↔ False.
Proof. rewrite view_auth_frac_op_validN. naive_solver. Qed.
Lemma view_frag_validN n b : ✓{n} (◯V b) ↔ ∃ a, rel n a b.
Proof. done. Qed.
Lemma view_both_frac_validN n q a b :
✓{n} (●V{q} a ⋅ ◯V b) ↔ ✓{n} q ∧ rel n a b.
Proof.
rewrite view_validN_eq /=. apply and_iff_compat_l.
setoid_rewrite (left_id _ _ b). split; [|by eauto].
by intros [?[->%(inj to_agree)]].
Qed.
Lemma view_both_validN n a b : ✓{n} (●V a ⋅ ◯V b) ↔ rel n a b.
Proof.
rewrite view_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
Qed.
Lemma view_auth_frac_valid q a : ✓ (●V{q} a) ↔ ✓ q ∧ ∀ n, rel n a ε.
Proof.
rewrite view_valid_eq /=. apply and_iff_compat_l. split; [|by eauto].
intros H n. by destruct (H n) as [? [->%(inj to_agree) ?]].
Qed.
Lemma view_auth_valid a : ✓ (●V a) ↔ ∀ n, rel n a ε.
Proof. rewrite view_auth_frac_valid frac_valid'. naive_solver. Qed.
Lemma view_auth_frac_op_valid q1 q2 a1 a2 :
✓ (●V{q1} a1 ⋅ ●V{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ∀ n, rel n a1 ε.
Proof.
rewrite !cmra_valid_validN equiv_dist. setoid_rewrite view_auth_frac_op_validN.
setoid_rewrite <-cmra_discrete_valid_iff. naive_solver.
Qed.
Lemma view_auth_op_valid a1 a2 : ✓ (●V a1 ⋅ ●V a2) ↔ False.
Proof. rewrite view_auth_frac_op_valid. naive_solver. Qed.
Lemma view_frag_valid b : ✓ (◯V b) ↔ ∀ n, ∃ a, rel n a b.
Proof. done. Qed.
Lemma view_both_frac_valid q a b : ✓ (●V{q} a ⋅ ◯V b) ↔ ✓ q ∧ ∀ n, rel n a b.
Proof.
rewrite view_valid_eq /=. apply and_iff_compat_l.
setoid_rewrite (left_id _ _ b). split; [|by eauto].
intros H n. by destruct (H n) as [?[->%(inj to_agree)]].
Qed.
Lemma view_both_valid a b : ✓ (●V a ⋅ ◯V b) ↔ ∀ n, rel n a b.
Proof. rewrite view_both_frac_valid frac_valid'. naive_solver. Qed.
(** Inclusion *)
Lemma view_auth_frac_includedN n p1 p2 a1 a2 b :
●V{p1} a1 ≼{n} ●V{p2} a2 ⋅ ◯V b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2.
......
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