From 0c0443c44bd4e54393d0ba965e20b8fa7d07a641 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 24 Feb 2016 12:40:22 +0100 Subject: [PATCH] Make CMRAExtend part of CMRAMixin. --- algebra/agree.v | 29 ++++++++++++------------ algebra/auth.v | 18 ++++++--------- algebra/cmra.v | 46 +++++++++++++++------------------------ algebra/excl.v | 18 ++++++--------- algebra/fin_maps.v | 36 ++++++++++++++---------------- algebra/iprod.v | 14 +++++------- algebra/option.v | 24 +++++++++----------- algebra/upred.v | 2 +- program_logic/resources.v | 16 +++++--------- 9 files changed, 84 insertions(+), 119 deletions(-) diff --git a/algebra/agree.v b/algebra/agree.v index 58a8e6b6b..4e71737e2 100644 --- a/algebra/agree.v +++ b/algebra/agree.v @@ -59,6 +59,7 @@ Program Instance agree_op : Op (agree A) := λ x y, Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed. Instance agree_unit : Unit (agree A) := id. Instance agree_minus : Minus (agree A) := λ x y, x. + Instance: Comm (≡) (@op (agree A) _). Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed. Lemma agree_idemp (x : agree A) : x ⋅ x ≡ x. @@ -87,11 +88,20 @@ Proof. repeat match goal with H : agree_is_valid _ _ |- _ => clear H end; by cofe_subst; rewrite !agree_idemp. Qed. + Lemma agree_includedN n (x y : agree A) : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y. Proof. split; [|by intros ?; exists y]. by intros [z Hz]; rewrite Hz assoc agree_idemp. Qed. +Lemma agree_op_inv n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2. +Proof. intros Hxy; apply Hxy. Qed. +Lemma agree_valid_includedN n (x y : agree A) : ✓{n} y → x ≼{n} y → x ≡{n}≡ y. +Proof. + move=> Hval [z Hy]; move: Hval; rewrite Hy. + by move=> /agree_op_inv->; rewrite agree_idemp. +Qed. + Definition agree_cmra_mixin : CMRAMixin (agree A). Proof. split; try (apply _ || done). @@ -102,22 +112,11 @@ Proof. - intros x; apply agree_idemp. - by intros n x y [(?&?&?) ?]. - by intros n x y; rewrite agree_includedN. + - intros n x y1 y2 Hval Hx; exists (x,x); simpl; split. + + by rewrite agree_idemp. + + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp. Qed. -Lemma agree_op_inv n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2. -Proof. intros Hxy; apply Hxy. Qed. -Lemma agree_valid_includedN n (x y : agree A) : ✓{n} y → x ≼{n} y → x ≡{n}≡ y. -Proof. - move=> Hval [z Hy]; move: Hval; rewrite Hy. - by move=> /agree_op_inv->; rewrite agree_idemp. -Qed. -Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A). -Proof. - intros n x y1 y2 Hval Hx; exists (x,x); simpl; split. - - by rewrite agree_idemp. - - by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp. -Qed. -Canonical Structure agreeRA : cmraT := - CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin. +Canonical Structure agreeRA : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin. Program Definition to_agree (x : A) : agree A := {| agree_car n := x; agree_is_valid n := True |}. diff --git a/algebra/auth.v b/algebra/auth.v index f64fa6090..89664daae 100644 --- a/algebra/auth.v +++ b/algebra/auth.v @@ -118,18 +118,14 @@ Proof. naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN. - by intros n ??; rewrite auth_includedN; intros [??]; split; simpl; apply cmra_op_minus. + - intros n x y1 y2 ? [??]; simpl in *. + destruct (cmra_extend n (authoritative x) (authoritative y1) + (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN. + destruct (cmra_extend n (own x) (own y1) (own y2)) + as (b&?&?&?); auto using own_validN. + by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)). Qed. -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 (ea&?&?&?); auto using authoritative_validN. - destruct (cmra_extend_op n (own x) (own y1) (own y2)) - 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. +Canonical Structure authRA : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin. (** Internalized properties *) Lemma auth_equivI {M} (x y : auth A) : diff --git a/algebra/cmra.v b/algebra/cmra.v index 5d61df86a..f9b6cfb84 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -49,11 +49,11 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := { mixin_cmra_unit_idemp x : unit (unit x) ≡ unit x; mixin_cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y; mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; - mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y + mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y; + mixin_cmra_extend n x y1 y2 : + ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → + { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 } }. -Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} := ∀ n x y1 y2, - ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → - { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }. (** Bundeled version *) Structure cmraT := CMRAT { @@ -66,10 +66,9 @@ Structure cmraT := CMRAT { cmra_validN : ValidN cmra_car; cmra_minus : Minus cmra_car; cmra_cofe_mixin : CofeMixin cmra_car; - cmra_mixin : CMRAMixin cmra_car; - cmra_extend_mixin : CMRAExtendMixin cmra_car + cmra_mixin : CMRAMixin cmra_car }. -Arguments CMRAT {_ _ _ _ _ _ _ _} _ _ _. +Arguments CMRAT {_ _ _ _ _ _ _ _} _ _. Arguments cmra_car : simpl never. Arguments cmra_equiv : simpl never. Arguments cmra_dist : simpl never. @@ -80,7 +79,6 @@ Arguments cmra_validN : simpl never. Arguments cmra_minus : simpl never. Arguments cmra_cofe_mixin : simpl never. Arguments cmra_mixin : simpl never. -Arguments cmra_extend_mixin : simpl never. Add Printing Constructor cmraT. Existing Instances cmra_unit cmra_op cmra_validN cmra_minus. Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A). @@ -115,10 +113,10 @@ Section cmra_mixin. Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed. Lemma cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y. Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed. - Lemma cmra_extend_op n x y1 y2 : + Lemma cmra_extend n x y1 y2 : ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }. - Proof. apply (cmra_extend_mixin A). Qed. + Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed. End cmra_mixin. (** * CMRAs with a global identity element *) @@ -301,7 +299,7 @@ Qed. Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y. Proof. intros ?? [x' ?]. - destruct (cmra_extend_op 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *. + destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *. by exists z'; rewrite Hy (timeless x z). Qed. Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{0} y → x ≼{n} y. @@ -310,7 +308,7 @@ Lemma cmra_op_timeless x1 x2 : ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2). Proof. intros ??? z Hz. - destruct (cmra_extend_op 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. + destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. { by rewrite -?Hz. } by rewrite Hz' (timeless x1 y1) // (timeless x2 y2). Qed. @@ -471,16 +469,12 @@ Section discrete. Instance discrete_validN : ValidN A := λ n x, ✓ x. Definition discrete_cmra_mixin : CMRAMixin A. Proof. - by destruct ra; split; unfold Proper, respectful, includedN; - try setoid_rewrite <-(timeless_iff _ _). - Qed. - Definition discrete_extend_mixin : CMRAExtendMixin A. - Proof. + destruct ra; split; unfold Proper, respectful, includedN; + try setoid_rewrite <-(timeless_iff _ _); try done. intros n x y1 y2 ??; exists (y1,y2); split_and?; auto. apply (timeless _), dist_le with n; auto with lia. Qed. - Definition discreteRA : cmraT := - CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin. + Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin. Lemma discrete_updateP (x : discreteRA) (P : A → Prop) : (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P. Proof. intros Hvalid n z; apply Hvalid. Qed. @@ -542,16 +536,12 @@ Section prod. - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l. - intros n x y; rewrite prod_includedN; intros [??]. by split; apply cmra_op_minus. + - intros n x y1 y2 [??] [??]; simpl in *. + destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto. + destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto. + by exists ((z1.1,z2.1),(z1.2,z2.2)). Qed. - Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B). - Proof. - intros n x y1 y2 [??] [??]; simpl in *. - destruct (cmra_extend_op n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto. - destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto. - by exists ((z1.1,z2.1),(z1.2,z2.2)). - Qed. - Canonical Structure prodRA : cmraT := - CMRAT prod_cofe_mixin prod_cmra_mixin prod_cmra_extend_mixin. + Canonical Structure prodRA : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin. Global Instance prod_cmra_identity `{Empty A, Empty B} : CMRAIdentity A → CMRAIdentity B → CMRAIdentity prodRA. Proof. diff --git a/algebra/excl.v b/algebra/excl.v index 656bcae8e..1815cb712 100644 --- a/algebra/excl.v +++ b/algebra/excl.v @@ -114,18 +114,14 @@ Proof. - by intros n [?| |] [?| |]; exists ∅. - by intros n [?| |] [?| |]. - by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor. + - intros n x y1 y2 ? Hx. + by exists match y1, y2 with + | Excl a1, Excl a2 => (Excl a1, Excl a2) + | ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot) + | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit) + end; destruct y1, y2; inversion_clear Hx; repeat constructor. Qed. -Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A). -Proof. - intros n x y1 y2 ? Hx. - by exists match y1, y2 with - | Excl a1, Excl a2 => (Excl a1, Excl a2) - | ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot) - | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit) - end; destruct y1, y2; inversion_clear Hx; repeat constructor. -Qed. -Canonical Structure exclRA : cmraT := - CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin. +Canonical Structure exclRA : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin. Global Instance excl_cmra_identity : CMRAIdentity exclRA. Proof. split. done. by intros []. apply _. Qed. Lemma excl_validN_inv_l n x y : ✓{n} (Excl x ⋅ y) → y = ∅. diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index 92714de8d..49125224d 100644 --- a/algebra/fin_maps.v +++ b/algebra/fin_maps.v @@ -142,27 +142,23 @@ Proof. by rewrite -lookup_op. - intros n x y; rewrite map_includedN_spec=> ? i. by rewrite lookup_op lookup_minus cmra_op_minus. + - 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 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; intros i; rewrite /= ?lookup_op !lookup_imap. + + destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor]. + rewrite -Hx; apply (proj2_sig (f i)). + + destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|]. + pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. + by symmetry; apply option_op_positive_dist_l with (m2 !! i). + + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|]. + pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. + by symmetry; apply option_op_positive_dist_r with (m1 !! i). Qed. -Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A). -Proof. - 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 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; intros i; rewrite /= ?lookup_op !lookup_imap. - - destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor]. - rewrite -Hx; apply (proj2_sig (f i)). - - destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|]. - pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. - by symmetry; apply option_op_positive_dist_l with (m2 !! i). - - destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|]. - pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. - by symmetry; apply option_op_positive_dist_r with (m1 !! i). -Qed. -Canonical Structure mapRA : cmraT := - CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin. +Canonical Structure mapRA : cmraT := CMRAT map_cofe_mixin map_cmra_mixin. Global Instance map_cmra_identity : CMRAIdentity mapRA. Proof. split. diff --git a/algebra/iprod.v b/algebra/iprod.v index 18c272406..32ad777a7 100644 --- a/algebra/iprod.v +++ b/algebra/iprod.v @@ -150,16 +150,12 @@ Section iprod_cmra. - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf. - intros n f1 f2; rewrite iprod_includedN_spec=> Hf x. by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf. + - intros n f f1 f2 Hf Hf12. + set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)). + exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)). + split_and?; intros x; apply (proj2_sig (g x)). Qed. - Definition iprod_cmra_extend_mixin : CMRAExtendMixin (iprod B). - Proof. - intros n f f1 f2 Hf Hf12. - set (g x := cmra_extend_op n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)). - exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)). - split_and?; intros x; apply (proj2_sig (g x)). - Qed. - Canonical Structure iprodRA : cmraT := - CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin. + Canonical Structure iprodRA : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin. Global Instance iprod_cmra_identity `{∀ x, Empty (B x)} : (∀ x, CMRAIdentity (B x)) → CMRAIdentity iprodRA. Proof. diff --git a/algebra/option.v b/algebra/option.v index 7a020107e..5b9ea3dfd 100644 --- a/algebra/option.v +++ b/algebra/option.v @@ -105,21 +105,17 @@ Proof. - intros n mx my; rewrite option_includedN. intros [->|(x&y&->&->&?)]; [by destruct my|]. by constructor; apply cmra_op_minus. + - intros n mx my1 my2. + destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx'; + try (by exfalso; inversion Hx'; auto). + + destruct (cmra_extend 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. + + by exists (None,Some x); inversion Hx'; repeat constructor. + + exists (None,None); repeat constructor. Qed. -Definition option_cmra_extend_mixin : CMRAExtendMixin (option A). -Proof. - intros n mx my1 my2. - destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx'; - try (by exfalso; inversion Hx'; 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. - - by exists (None,Some x); inversion Hx'; repeat constructor. - - exists (None,None); repeat constructor. -Qed. -Canonical Structure optionRA := - CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin. +Canonical Structure optionRA := CMRAT option_cofe_mixin option_cmra_mixin. Global Instance option_cmra_identity : CMRAIdentity optionRA. Proof. split. done. by intros []. by inversion_clear 1. Qed. diff --git a/algebra/upred.v b/algebra/upred.v index e3b92d621..0070bf0fb 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -818,7 +818,7 @@ Proof. split=> n x ?; split. - destruct n as [|n]; simpl. { by exists x, (unit x); rewrite cmra_unit_r. } - intros (x1&x2&Hx&?&?); destruct (cmra_extend_op n x x1 x2) + 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]. - destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)]. diff --git a/program_logic/resources.v b/program_logic/resources.v index d7e71cc24..65c5e6e08 100644 --- a/program_logic/resources.v +++ b/program_logic/resources.v @@ -113,17 +113,13 @@ Proof. split_and!; simpl in *; eapply cmra_validN_op_l; eauto. - intros n r1 r2; rewrite res_includedN; intros (?&?&?). by constructor; apply cmra_op_minus. + - intros n r r1 r2 (?&?&?) [???]; simpl in *. + destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?), + (cmra_extend n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?), + (cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto. + by exists (Res w σ m, Res w' σ' m'). Qed. -Definition res_cmra_extend_mixin : CMRAExtendMixin (res Λ Σ A). -Proof. - intros n r r1 r2 (?&?&?) [???]; simpl in *. - destruct (cmra_extend_op n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?), - (cmra_extend_op n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?), - (cmra_extend_op n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto. - by exists (Res w σ m, Res w' σ' m'). -Qed. -Canonical Structure resRA : cmraT := - CMRAT res_cofe_mixin res_cmra_mixin res_cmra_extend_mixin. +Canonical Structure resRA : cmraT := CMRAT res_cofe_mixin res_cmra_mixin. Global Instance res_cmra_identity : CMRAIdentity resRA. Proof. split. -- GitLab