diff --git a/algebra/agree.v b/algebra/agree.v index c8d47172b9a39a603fb2fe2b2a58dc69862d59d6..6494453f732cc0fc6d01d01293f8f954fe406699 100644 --- a/algebra/agree.v +++ b/algebra/agree.v @@ -97,11 +97,6 @@ Proof. split; [|by intros ?; exists y]. by intros [z Hz]; rewrite Hz assoc 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. @@ -160,20 +155,20 @@ Proof. done. Qed. Section agree_map. Context {A B : cofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}. - Global Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f). + Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f). Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed. - Global Instance agree_map_proper : - Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _. + Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _. Lemma agree_map_ext (g : A → B) x : (∀ x, f x ≡ g x) → agree_map f x ≡ agree_map g x. Proof. by intros Hfg; split; simpl; intros; rewrite ?Hfg. Qed. Global Instance agree_map_monotone : CMRAMonotone (agree_map f). Proof. - split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]]. - intros n x y; rewrite !agree_includedN; intros Hy; rewrite Hy. - split; last done; split; simpl; last tauto. - by intros (?&?&Hxy); repeat split; intros; - try apply Hxy; try apply Hf; eauto using @agree_valid_le. + split; first apply _. + - by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]. + - intros x y; rewrite !agree_included=> ->. + split; last done; split; simpl; last tauto. + by intros (?&?&Hxy); repeat split; intros; + try apply Hxy; try apply Hf; eauto using @agree_valid_le. Qed. End agree_map. diff --git a/algebra/auth.v b/algebra/auth.v index 65e52e8e9298cedb5371867a350b75b4e2904bbf..6ce9801b39c0261ce385fb13343a0271dc6959a7 100644 --- a/algebra/auth.v +++ b/algebra/auth.v @@ -98,12 +98,6 @@ Proof. split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|]. intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto. Qed. -Lemma auth_includedN n (x y : auth A) : - x ≼{n} y ↔ authoritative x ≼{n} authoritative y ∧ own x ≼{n} own y. -Proof. - split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|]. - intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto. -Qed. Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} authoritative x. Proof. by destruct x as [[]]. Qed. Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} own x. @@ -212,7 +206,6 @@ Proof. intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN. by rewrite -(local_updateN L) // EQ -(local_updateN L) // -EQ. Qed. - End cmra. Arguments authRA : clear implicits. @@ -234,14 +227,13 @@ Proof. intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf]. Qed. Instance auth_map_cmra_monotone {A B : cmraT} (f : A → B) : - (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone f → CMRAMonotone (auth_map f). Proof. - split. - - by intros n [x a] [y b]; rewrite !auth_includedN /=; - intros [??]; split; simpl; apply: includedN_preserving. - - intros n [[a| |] b]; rewrite /= /cmra_validN; - naive_solver eauto using @includedN_preserving, @validN_preserving. + split; try apply _. + - intros n [[a| |] b]; rewrite /= /cmra_validN /=; try + naive_solver eauto using includedN_preserving, validN_preserving. + - by intros [x a] [y b]; rewrite !auth_included /=; + intros [??]; split; simpl; apply: included_preserving. Qed. Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B := CofeMor (auth_map f). diff --git a/algebra/cmra.v b/algebra/cmra.v index b0a723e1170688ff2ebc55d1b119511bd1e6f941..7bdfd642e9abc66f87fe72a2def6637a74b2966d 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -142,8 +142,9 @@ Class CMRADiscrete (A : cmraT) : Prop := { (** * Morphisms *) Class CMRAMonotone {A B : cmraT} (f : A → B) := { - includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y; - validN_preserving n x : ✓{n} x → ✓{n} f x + cmra_monotone_ne n :> Proper (dist n ==> dist n) f; + validN_preserving n x : ✓{n} x → ✓{n} f x; + included_preserving x y : x ≼ y → f x ≼ f y }. (** * Local updates *) @@ -430,26 +431,28 @@ End cmra. (** * Properties about monotone functions *) Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A). -Proof. by split. Qed. +Proof. repeat split; by try apply _. Qed. Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) : CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ∘ f). Proof. split. - - move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving. + - apply _. - move=> n x Hx /=. by apply validN_preserving, validN_preserving. + - move=> x y Hxy /=. by apply included_preserving, included_preserving. Qed. Section cmra_monotone. Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}. - Lemma included_preserving x y : x ≼ y → f x ≼ f y. + Global Instance cmra_monotone_proper : Proper ((≡) ==> (≡)) f := ne_proper _. + Lemma includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y. Proof. - rewrite !cmra_included_includedN; eauto using includedN_preserving. + intros [z ->]. + apply cmra_included_includedN, included_preserving, cmra_included_l. Qed. Lemma valid_preserving x : ✓ x → ✓ f x. Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed. End cmra_monotone. - (** * Transporting a CMRA equality *) Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B := eq_rect A id x _ H. @@ -607,8 +610,8 @@ Arguments prodRA : clear implicits. Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B') : CMRAMonotone f → CMRAMonotone g → CMRAMonotone (prod_map f g). Proof. - split. - - intros n x y; rewrite !prod_includedN; intros [??]; simpl. - by split; apply includedN_preserving. + split; first apply _. - by intros n x [??]; split; simpl; apply validN_preserving. + - intros x y; rewrite !prod_included=> -[??] /=. + by split; apply included_preserving. Qed. diff --git a/algebra/excl.v b/algebra/excl.v index b8ffd8b8db73497608988ee215101727f8c1c1a3..5d843e9ae595145900b44cfea37b981bb4f97710 100644 --- a/algebra/excl.v +++ b/algebra/excl.v @@ -27,6 +27,7 @@ Inductive excl_dist : Dist (excl A) := | ExclUnit_dist n : ExclUnit ≡{n}≡ ExclUnit | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot. Existing Instance excl_dist. + Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A). Proof. by constructor. Qed. Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A). @@ -35,6 +36,7 @@ Global Instance Excl_inj : Inj (≡) (≡) (@Excl A). Proof. by inversion_clear 1. Qed. Global Instance Excl_dist_inj n : Inj (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 |}. @@ -191,10 +193,10 @@ Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed. Instance excl_map_cmra_monotone {A B : cofeT} (f : A → B) : (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f). Proof. - split. - - intros n x y [z Hy]; exists (excl_map f z); rewrite Hy. - by destruct x, z; constructor. + split; try apply _. - by intros n [a| |]. + - intros x y [z Hy]; exists (excl_map f z); apply equiv_dist=> n. + move: Hy=> /equiv_dist /(_ n) ->; by destruct x, z. Qed. Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B := CofeMor (excl_map f). diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index fb9a55d7d6612234bfeec4eeb21bc6b35a638e06..bbf585b0f8addb311f8fafabbaecfc1167f1e22c 100644 --- a/algebra/fin_maps.v +++ b/algebra/fin_maps.v @@ -231,8 +231,8 @@ Proof. [exists (x ⋅ y)|exists x]; eauto using cmra_included_l. - intros (y&Hi&?); rewrite map_includedN_spec=>j. destruct (decide (i = j)); simplify_map_eq. - + by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN. - + apply None_includedN. + + rewrite Hi. by apply (includedN_preserving _), cmra_included_includedN. + + apply: cmra_empty_leastN. Qed. Lemma map_dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2. Proof. @@ -338,10 +338,10 @@ Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed. Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B) `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B). Proof. - split. - - intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i. - by rewrite !lookup_fmap; apply: includedN_preserving. + split; try apply _. - by intros n m ? i; rewrite lookup_fmap; apply validN_preserving. + - intros m1 m2; rewrite !map_included_spec=> Hm i. + by rewrite !lookup_fmap; apply: included_preserving. Qed. Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B := CofeMor (fmap f : mapC K A → mapC K B). diff --git a/algebra/iprod.v b/algebra/iprod.v index cbd5871fa827955a48391413acc2c253244faedb..1e8f85ee59e360913d44f702458da7e56c978772 100644 --- a/algebra/iprod.v +++ b/algebra/iprod.v @@ -133,13 +133,6 @@ Section iprod_cmra. - intros Hh; exists (g ⩪ f)=> x; specialize (Hh x). by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus. Qed. - Lemma iprod_includedN_spec n (f g : iprod B) : f ≼{n} g ↔ ∀ x, f x ≼{n} g x. - Proof. - split. - - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x). - - intros Hh; exists (g ⩪ f)=> x; specialize (Hh x). - by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus'. - Qed. Definition iprod_cmra_mixin : CMRAMixin (iprod B). Proof. @@ -283,10 +276,10 @@ Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed. Instance iprod_map_cmra_monotone {A} {B1 B2: A → cmraT} (f : ∀ x, B1 x → B2 x) : (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f). Proof. - split. - - intros n g1 g2; rewrite !iprod_includedN_spec=> Hf x. - rewrite /iprod_map; apply includedN_preserving, Hf. + split; first apply _. - intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg. + - intros g1 g2; rewrite !iprod_included_spec=> Hf x. + rewrite /iprod_map; apply included_preserving, Hf. Qed. Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) : diff --git a/algebra/option.v b/algebra/option.v index 2357e80089950b0be0d9fe2ae4bf91704a3dfafc..6e959103067eade9b650db26fd282df68eef3313 100644 --- a/algebra/option.v +++ b/algebra/option.v @@ -72,6 +72,8 @@ Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)). Instance option_minus : Minus (option A) := difference_with (λ x y, Some (x ⩪ y)). +Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl. + Lemma option_included (mx my : option A) : mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y. Proof. @@ -84,24 +86,6 @@ Proof. - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor). by exists (Some z); constructor. Qed. -Lemma option_includedN n (mx my : option A) : - mx ≼{n} my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y. -Proof. - split. - - intros [mz Hmz]. - destruct mx as [x|]; [right|by left]. - destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz]. - destruct mz as [z|]; inversion_clear Hmz; split_and?; auto; - cofe_subst; eauto using cmra_includedN_l. - - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor). - by exists (Some z); constructor. -Qed. - -Lemma None_includedN n (mx : option A) : None ≼{n} mx. -Proof. rewrite option_includedN; auto. Qed. -Lemma Some_Some_includedN n (x y : A) : x ≼{n} y → Some x ≼{n} Some y. -Proof. rewrite option_includedN; eauto 10. Qed. -Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl. Definition option_cmra_mixin : CMRAMixin (option A). Proof. @@ -140,6 +124,8 @@ Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionRA. Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed. (** Misc *) +Global Instance Some_cmra_monotone : CMRAMonotone Some. +Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed. Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my. Proof. destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver. @@ -192,10 +178,10 @@ Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed. Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A → option B). Proof. - split. - - intros n mx my; rewrite !option_includedN. - intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @includedN_preserving. - - by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving. + split; first apply _. + - intros n [x|] ?; rewrite /cmra_validN /=; by repeat apply validN_preserving. + - intros mx my; rewrite !option_included. + intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @included_preserving. Qed. Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B := CofeMor (fmap f : optionC A → optionC B). diff --git a/program_logic/resources.v b/program_logic/resources.v index 70057ea66bac3de7046fabd5717f1373fa5af631..48531ad88250983d5cf08e59c27c1f5da6df6bda 100644 --- a/program_logic/resources.v +++ b/program_logic/resources.v @@ -205,10 +205,10 @@ Qed. Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) : CMRAMonotone (@res_map Λ Σ _ _ f). Proof. - split. - - by intros n r1 r2; rewrite !res_includedN; - intros (?&?&?); split_and!; simpl; try apply includedN_preserving. + split; first apply _. - by intros n r (?&?&?); split_and!; simpl; try apply validN_preserving. + - by intros r1 r2; rewrite !res_included; + intros (?&?&?); split_and!; simpl; try apply included_preserving. Qed. Definition resC_map {Λ Σ A B} (f : A -n> B) : resC Λ Σ A -n> resC Λ Σ B := CofeMor (res_map f : resRA Λ Σ A → resRA Λ Σ B).