diff --git a/modures/auth.v b/modures/auth.v index 80b03f0beac006de7ad72d5771b8db9295616a1c..53ffa01e8e30d483bbad5e078706043a66db6b44 100644 --- a/modures/auth.v +++ b/modures/auth.v @@ -6,12 +6,14 @@ Add Printing Constructor auth. Arguments Auth {_} _ _. Arguments authoritative {_} _. Arguments own {_} _. -Notation "◯ x" := (Auth ExclUnit x) (at level 20). -Notation "● x" := (Auth (Excl x) ∅) (at level 20). +Notation "◯ a" := (Auth ExclUnit a) (at level 20). +Notation "● a" := (Auth (Excl a) ∅) (at level 20). (* COFE *) Section cofe. Context {A : cofeT}. +Implicit Types a b : A. +Implicit Types x y : auth A. Instance auth_equiv : Equiv (auth A) := λ x y, authoritative x ≡ authoritative y ∧ own x ≡ own y. @@ -20,10 +22,16 @@ Instance auth_dist : Dist (auth A) := λ n x y, Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A). Proof. by split. Qed. +Global Instance Auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@Auth A). +Proof. by split. Qed. Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A). Proof. by destruct 1. Qed. +Global Instance authoritative_proper : Proper ((≡) ==> (≡)) (@authoritative A). +Proof. by destruct 1. Qed. Global Instance own_ne : Proper (dist n ==> dist n) (@own A). Proof. by destruct 1. Qed. +Global Instance own_proper : Proper ((≡) ==> (≡)) (@own A). +Proof. by destruct 1. Qed. Instance auth_compl : Compl (auth A) := λ c, Auth (compl (chain_map authoritative c)) (compl (chain_map own c)). @@ -36,14 +44,14 @@ Proof. + by intros ?; split. + by intros ?? [??]; split; symmetry. + intros ??? [??] [??]; split; etransitivity; eauto. - * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. + * by intros ? [??] [??] [??]; split; apply dist_S. * by split. * intros c n; split. apply (conv_compl (chain_map authoritative c) n). apply (conv_compl (chain_map own c) n). Qed. Canonical Structure authC := CofeT auth_cofe_mixin. -Instance Auth_timeless (x : excl A) (y : A) : - Timeless x → Timeless y → Timeless (Auth x y). +Instance Auth_timeless (ea : excl A) (b : A) : + Timeless ea → Timeless b → Timeless (Auth ea b). Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed. Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A). Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed. @@ -54,6 +62,8 @@ Arguments authC : clear implicits. (* CMRA *) Section cmra. Context {A : cmraT}. +Implicit Types a b : A. +Implicit Types x y : auth A. Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅. Instance auth_validN : ValidN (auth A) := λ n x, @@ -114,22 +124,46 @@ Definition auth_cmra_extend_mixin : CMRAExtendMixin (auth A). Proof. intros n x y1 y2 ? [??]; simpl in *. destruct (cmra_extend_op n (authoritative x) (authoritative y1) - (authoritative y2)) as (z1&?&?&?); auto using authoritative_validN. + (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN. destruct (cmra_extend_op n (own x) (own y1) (own y2)) - as (z2&?&?&?); auto using own_validN. - by exists (Auth (z1.1) (z2.1), Auth (z1.2) (z2.2)). + as (b&?&?&?); auto using own_validN. + by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)). Qed. Canonical Structure authRA : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin. -Instance auth_cmra_identity `{Empty A} : CMRAIdentity A → CMRAIdentity authRA. + +(** The notations ◯ and ● only work for CMRAs with an empty element. So, in +what follows, we assume we have an empty element. *) +Context `{Empty A, !CMRAIdentity A}. + +Global Instance auth_cmra_identity : CMRAIdentity authRA. Proof. split; simpl. * by apply (@cmra_empty_valid A _). * by intros x; constructor; rewrite /= left_id. * apply Auth_timeless; apply _. Qed. -Lemma auth_frag_op (a b : A) : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b. +Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b. Proof. done. Qed. + +Lemma auth_update a a' b b' : + (∀ n af, ✓{n} a → a ={n}= a' ⋅ af → b ={n}= b' ⋅ af ∧ ✓{n} b) → + ● a ⋅ ◯ a' ⇝ ● b ⋅ ◯ b'. +Proof. + move=> Hab [[] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *. + destruct (Hab (S n) (bf1 ⋅ bf2)) as [Ha' ?]; auto. + { by rewrite Ha left_id associative. } + split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done]. +Qed. +Lemma auth_update_op_l a a' b : + ✓ (b ⋅ a) → ● a ⋅ ◯ a' ⇝ ● (b ⋅ a) ⋅ ◯ (b ⋅ a'). +Proof. + intros; apply auth_update. + by intros n af ? Ha; split; [by rewrite Ha associative|]. +Qed. +Lemma auth_update_op_r a a' b : + ✓ (a ⋅ b) → ● a ⋅ ◯ a' ⇝ ● (a ⋅ b) ⋅ ◯ (a' ⋅ b). +Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed. End cmra. Arguments authRA : clear implicits. diff --git a/modures/cmra.v b/modures/cmra.v index 8b146841172fb2f3c2291dc313a0224fa546e165..f4c49ee4180342c096383115d3172d7a29b2cbf3 100644 --- a/modures/cmra.v +++ b/modures/cmra.v @@ -143,12 +143,12 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := { (** * Frame preserving updates *) Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n, ✓{S n} (x ⋅ z) → ∃ y, P y ∧ ✓{S n} (y ⋅ z). -Instance: Params (@cmra_updateP) 3. +Instance: Params (@cmra_updateP) 1. Infix "⇝:" := cmra_updateP (at level 70). Definition cmra_update {A : cmraT} (x y : A) := ∀ z n, ✓{S n} (x ⋅ z) → ✓{S n} (y ⋅ z). Infix "⇝" := cmra_update (at level 70). -Instance: Params (@cmra_update) 3. +Instance: Params (@cmra_update) 1. (** * Properties **) Section cmra. @@ -193,6 +193,17 @@ Proof. intros x x' Hx y y' Hy. by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy]. Qed. +Global Instance cmra_update_proper : + Proper ((≡) ==> (≡) ==> iff) (@cmra_update A). +Proof. + intros x1 x2 Hx y1 y2 Hy; split=>? z n; [rewrite -Hx -Hy|rewrite Hx Hy]; auto. +Qed. +Global Instance cmra_updateP_proper : + Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A). +Proof. + intros x1 x2 Hx P1 P2 HP; split=>Hup z n; + [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto. +Qed. (** ** Validity *) Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x. diff --git a/modures/excl.v b/modures/excl.v index 341e7b27ac23441f36578d4a648cbe6f35caecfe..54389faa5b396f7d184f0c77d41584619d392fef 100644 --- a/modures/excl.v +++ b/modures/excl.v @@ -27,6 +27,14 @@ Inductive excl_dist `{Dist A} : Dist (excl A) := | ExclUnit_dist n : ExclUnit ={n}= ExclUnit | ExclBot_dist n : ExclBot ={n}= ExclBot. Existing Instance excl_dist. +Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A). +Proof. by constructor. Qed. +Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A). +Proof. by constructor. Qed. +Global Instance Excl_inj : Injective (≡) (≡) (@Excl A). +Proof. by inversion_clear 1. Qed. +Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A). +Proof. by inversion_clear 1. Qed. Program Definition excl_chain (c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A := {| chain_car n := match c n return _ with Excl y => y | _ => x end |}. @@ -66,10 +74,6 @@ Proof. Qed. Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin. -Global Instance Excl_inj : Injective (≡) (≡) (@Excl A). -Proof. by inversion_clear 1. Qed. -Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A). -Proof. by inversion_clear 1. Qed. Global Instance Excl_timeless (x : A) : Timeless x → Timeless (Excl x). Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).