From b2c912d80684765cf605bf19d4bb5143bd5b17ff Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 24 Feb 2016 14:14:22 +0100 Subject: [PATCH] Make valid a primitive instead of derived notion. This way it behaves better for discrete CMRAs. --- algebra/agree.v | 3 +++ algebra/auth.v | 14 +++++++++++-- algebra/cmra.v | 43 +++++++++++++++++++++++++-------------- algebra/excl.v | 3 +++ algebra/fin_maps.v | 18 ++++++++-------- algebra/iprod.v | 8 ++++++-- algebra/option.v | 5 ++++- algebra/sts.v | 12 ++++------- heap_lang/heap.v | 6 +++--- program_logic/resources.v | 16 +++++++++------ program_logic/sts.v | 8 +++----- 11 files changed, 86 insertions(+), 50 deletions(-) diff --git a/algebra/agree.v b/algebra/agree.v index 4e71737e..982b5997 100644 --- a/algebra/agree.v +++ b/algebra/agree.v @@ -16,9 +16,12 @@ Context {A : cofeT}. Instance agree_validN : ValidN (agree A) := λ n x, agree_is_valid x n ∧ ∀ n', n' ≤ n → x n' ≡{n'}≡ x n. +Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x. + Lemma agree_valid_le n n' (x : agree A) : agree_is_valid x n → n' ≤ n → agree_is_valid x n'. Proof. induction 2; eauto using agree_valid_S. Qed. + Instance agree_equiv : Equiv (agree A) := λ x y, (∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧ (∀ n, agree_is_valid x n → x n ≡{n}≡ y n). diff --git a/algebra/auth.v b/algebra/auth.v index 89664daa..556bf1cf 100644 --- a/algebra/auth.v +++ b/algebra/auth.v @@ -1,5 +1,6 @@ From algebra Require Export excl. From algebra Require Import functor upred. +Local Arguments valid _ _ !_ /. Local Arguments validN _ _ _ !_ /. Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }. @@ -66,6 +67,13 @@ Implicit Types a b : A. Implicit Types x y : auth A. Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅. +Instance auth_valid : Valid (auth A) := λ x, + match authoritative x with + | Excl a => own x ≼ a ∧ ✓ a + | ExclUnit => ✓ own x + | ExclBot => False + end. +Global Arguments auth_valid !_ /. Instance auth_validN : ValidN (auth A) := λ n x, match authoritative x with | Excl a => own x ≼{n} a ∧ ✓{n} a @@ -105,6 +113,8 @@ Proof. destruct Hx; intros ?; cofe_subst; auto. - by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'. + - intros [[] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN; + naive_solver eauto using O. - intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S. - by split; simpl; rewrite assoc. - by split; simpl; rewrite comm. @@ -169,7 +179,7 @@ Lemma auth_local_update L `{!LocalUpdate Lv L} a a' : Lv a → ✓ L a' → ● a' ⋅ ◯ a ~~> ● L a' ⋅ ◯ L a. Proof. - intros. apply auth_update=>n af ? EQ; split; last done. + intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN. by rewrite EQ (local_updateN L) // -EQ. Qed. @@ -188,7 +198,7 @@ Lemma auth_local_update_l L `{!LocalUpdate Lv L} a a' : Lv a → ✓ (L a ⋅ a') → ● (a ⋅ a') ⋅ ◯ a ~~> ● (L a ⋅ a') ⋅ ◯ L a. Proof. - intros. apply auth_update=>n af ? EQ; split; last done. + 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. diff --git a/algebra/cmra.v b/algebra/cmra.v index f9b6cfb8..cd63f020 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -26,7 +26,6 @@ Notation "✓{ n } x" := (validN n x) Class Valid (A : Type) := valid : A → Prop. Instance: Params (@valid) 2. Notation "✓ x" := (valid x) (at level 20) : C_scope. -Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x. Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z. Notation "x ≼{ n } y" := (includedN n x y) @@ -34,13 +33,15 @@ Notation "x ≼{ n } y" := (includedN n x y) Instance: Params (@includedN) 4. Hint Extern 0 (_ ≼{_} _) => reflexivity. -Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := { +Record CMRAMixin A + `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := { (* setoids *) mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x); mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit; mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n); mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus; (* valid *) + mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x; mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; (* monoid *) mixin_cmra_assoc : Assoc (≡) (⋅); @@ -63,24 +64,26 @@ Structure cmraT := CMRAT { cmra_compl : Compl cmra_car; cmra_unit : Unit cmra_car; cmra_op : Op cmra_car; + cmra_valid : Valid cmra_car; cmra_validN : ValidN cmra_car; cmra_minus : Minus cmra_car; cmra_cofe_mixin : CofeMixin 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. Arguments cmra_compl : simpl never. Arguments cmra_unit : simpl never. Arguments cmra_op : simpl never. +Arguments cmra_valid : simpl never. Arguments cmra_validN : simpl never. Arguments cmra_minus : simpl never. Arguments cmra_cofe_mixin : simpl never. Arguments cmra_mixin : simpl never. Add Printing Constructor cmraT. -Existing Instances cmra_unit cmra_op cmra_validN cmra_minus. +Existing Instances cmra_unit cmra_op cmra_valid cmra_validN cmra_minus. Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A). Canonical Structure cmra_cofeC. @@ -97,6 +100,8 @@ Section cmra_mixin. Global Instance cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) (@minus A _). Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed. + Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x. + Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed. Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x. Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed. Global Instance cmra_assoc : Assoc (≡) (@op A _). @@ -178,7 +183,10 @@ Global Instance cmra_minus_proper : Proper ((≡) ==> (≡) ==> (≡)) (@minus A Proof. apply (ne_proper_2 _). Qed. Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _). -Proof. by intros x y Hxy; split; intros ? n; [rewrite -Hxy|rewrite Hxy]. Qed. +Proof. + intros x y Hxy; rewrite !cmra_valid_validN. + by split=> ? n; [rewrite -Hxy|rewrite Hxy]. +Qed. Global Instance cmra_includedN_ne n : Proper (dist n ==> dist n ==> iff) (@includedN A _ _ n) | 1. Proof. @@ -210,8 +218,6 @@ Proof. Qed. (** ** Validity *) -Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x. -Proof. done. Qed. Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x. Proof. induction 2; eauto using cmra_validN_S. Qed. Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x. @@ -309,13 +315,15 @@ Lemma cmra_op_timeless x1 x2 : Proof. intros ??? z Hz. destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. - { by rewrite -?Hz. } + { rewrite -?Hz. by apply cmra_valid_validN. } by rewrite Hz' (timeless x1 y1) // (timeless x2 y2). Qed. (** ** RAs with an empty element *) Section identity. Context `{Empty A, !CMRAIdentity A}. + Lemma cmra_empty_validN n : ✓{n} ∅. + Proof. apply cmra_valid_validN, cmra_empty_valid. Qed. Lemma cmra_empty_leastN n x : ∅ ≼{n} x. Proof. by exists x; rewrite left_id. Qed. Lemma cmra_empty_least x : ∅ ≼ x. @@ -333,7 +341,9 @@ Proof. intros; apply (ne_proper _). Qed. Lemma local_update L `{!LocalUpdate Lv L} x y : Lv x → ✓ (x ⋅ y) → L (x ⋅ y) ≡ L x ⋅ y. -Proof. by rewrite equiv_dist=>?? n; apply (local_updateN L). Qed. +Proof. + by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L). +Qed. Global Instance local_update_op x : LocalUpdate (λ _, True) (op x). Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed. @@ -464,15 +474,16 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := { Section discrete. Context {A : cofeT} `{∀ x : A, Timeless x}. - Context {v : Valid A} `{Unit A, Op A, Minus A} (ra : RA A). + Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A). Instance discrete_validN : ValidN A := λ n x, ✓ x. Definition discrete_cmra_mixin : CMRAMixin 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. + - intros x; split; first done. by move=> /(_ 0). + - 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. Lemma discrete_updateP (x : discreteRA) (P : A → Prop) : @@ -481,8 +492,6 @@ Section discrete. Lemma discrete_update (x y : discreteRA) : (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y. Proof. intros Hvalid n z; apply Hvalid. Qed. - Lemma discrete_valid (x : discreteRA) : v x → validN_valid x. - Proof. move=>Hx n. exact Hx. Qed. End discrete. (** ** CMRA for the unit type *) @@ -497,7 +506,7 @@ Section unit. Canonical Structure unitRA : cmraT := Eval cbv [unitC discreteRA cofe_car] in discreteRA unit_ra. Global Instance unit_cmra_identity : CMRAIdentity unitRA. - Proof. by split; intros []. Qed. + Proof. by split. Qed. End unit. (** ** Product *) @@ -506,6 +515,7 @@ Section prod. Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2). Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅). Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)). + Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2. Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2. Instance prod_minus : Minus (A * B) := λ x y, (x.1 ⩪ y.1, x.2 ⩪ y.2). Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2. @@ -526,6 +536,9 @@ Section prod. - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2. - by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2. + - intros x; split. + + intros [??] n; split; by apply cmra_valid_validN. + + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy. - by intros n x [??]; split; apply cmra_validN_S. - by split; rewrite /= assoc. - by split; rewrite /= comm. diff --git a/algebra/excl.v b/algebra/excl.v index 1815cb71..9a05c439 100644 --- a/algebra/excl.v +++ b/algebra/excl.v @@ -83,6 +83,8 @@ Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A). Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed. (* CMRA *) +Instance excl_valid : Valid (excl A) := λ x, + match x with Excl _ | ExclUnit => True | ExclBot => False end. Instance excl_validN : ValidN (excl A) := λ n x, match x with Excl _ | ExclUnit => True | ExclBot => False end. Global Instance excl_empty : Empty (excl A) := ExclUnit. @@ -106,6 +108,7 @@ Proof. - constructor. - by destruct 1; intros ?. - by destruct 1; inversion_clear 1; constructor. + - intros x; split. done. by move=> /(_ 0). - intros n [?| |]; simpl; auto with lia. - by intros [?| |] [?| |] [?| |]; constructor. - by intros [?| |] [?| |]; constructor. diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index 49125224..272ef56e 100644 --- a/algebra/fin_maps.v +++ b/algebra/fin_maps.v @@ -96,6 +96,7 @@ Implicit Types m : gmap K A. Instance map_op : Op (gmap K A) := merge op. Instance map_unit : Unit (gmap K A) := fmap unit. +Instance map_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i). Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i). Instance map_minus : Minus (gmap K A) := merge minus. @@ -106,8 +107,6 @@ Proof. by apply lookup_merge. Qed. Lemma lookup_unit m i : unit m !! i = unit (m !! i). Proof. by apply lookup_fmap. Qed. -Lemma map_valid_spec m : ✓ m ↔ ∀ i, ✓ (m !! i). -Proof. split; intros Hm ??; apply Hm. Qed. Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i. Proof. split. @@ -131,6 +130,9 @@ Proof. - by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i). - by intros n m1 m2 Hm ? i; rewrite -(Hm i). - by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i). + - intros m; split. + + by intros ? n i; apply cmra_valid_validN. + + intros Hm i; apply cmra_valid_validN=> n; apply Hm. - intros n m Hm i; apply cmra_validN_S, Hm. - by intros m1 m2 m3 i; rewrite !lookup_op assoc. - by intros m1 m2 i; rewrite !lookup_op comm. @@ -162,7 +164,7 @@ Canonical Structure mapRA : cmraT := CMRAT map_cofe_mixin map_cmra_mixin. Global Instance map_cmra_identity : CMRAIdentity mapRA. Proof. split. - - by intros ? n; rewrite lookup_empty. + - by intros i; rewrite lookup_empty. - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _). - apply map_empty_timeless. Qed. @@ -187,18 +189,18 @@ Implicit Types a : A. Lemma map_lookup_validN n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x. Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed. Lemma map_lookup_valid m i x : ✓ m → m !! i ≡ Some x → ✓ x. -Proof. move=>Hm Hi n. move:(Hm n i). by rewrite Hi. Qed. +Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed. Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m. Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed. Lemma map_insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m. -Proof. intros ?? n j; apply map_insert_validN; auto. Qed. +Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed. Lemma map_singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x. Proof. - split; [|by intros; apply map_insert_validN, cmra_empty_valid]. + split; [|by intros; apply map_insert_validN, cmra_empty_validN]. by move=>/(_ i); simplify_map_eq. Qed. Lemma map_singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x. -Proof. split; intros ? n; eapply map_singleton_validN; eauto. Qed. +Proof. rewrite !cmra_valid_validN. by setoid_rewrite map_singleton_validN. Qed. Lemma map_insert_singleton_opN n m i x : m !! i = None ∨ m !! i ≡{n}≡ Some (unit x) → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m. @@ -275,7 +277,7 @@ Proof. intros Hx HQ n gf Hg. destruct (Hx n (from_option ∅ (gf !! i))) as (y&?&Hy). { move:(Hg i). rewrite !left_id. - case _: (gf !! i); simpl; auto using cmra_empty_valid. } + case _: (gf !! i); simpl; auto using cmra_empty_validN. } exists {[ i := y ]}; split; first by auto. intros i'; destruct (decide (i' = i)) as [->|]. - rewrite lookup_op lookup_singleton. diff --git a/algebra/iprod.v b/algebra/iprod.v index 32ad777a..2590ae8c 100644 --- a/algebra/iprod.v +++ b/algebra/iprod.v @@ -118,6 +118,7 @@ Section iprod_cmra. Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x. Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x). + Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x. Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x. Instance iprod_minus : Minus (iprod B) := λ f g x, f x ⩪ g x. @@ -140,6 +141,9 @@ Section iprod_cmra. - by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x). - by intros n f1 f2 Hf ? x; rewrite -(Hf x). - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i). + - intros g; split. + + intros Hg n i; apply cmra_valid_validN, Hg. + + intros Hg i; apply cmra_valid_validN=> n; apply Hg. - intros n f Hf x; apply cmra_validN_S, Hf. - by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc. - by intros f1 f2 x; rewrite iprod_lookup_op comm. @@ -160,7 +164,7 @@ Section iprod_cmra. (∀ x, CMRAIdentity (B x)) → CMRAIdentity iprodRA. Proof. intros ?; split. - - intros n x; apply cmra_empty_valid. + - intros x; apply cmra_empty_valid. - by intros f x; rewrite iprod_lookup_op left_id. - by apply _. Qed. @@ -204,7 +208,7 @@ Section iprod_cmra. split; [by move=>/(_ x); rewrite iprod_lookup_singleton|]. move=>Hx x'; destruct (decide (x = x')) as [->|]; rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //. - by apply cmra_empty_valid. + by apply cmra_empty_validN. Qed. Lemma iprod_unit_singleton x (y : B x) : diff --git a/algebra/option.v b/algebra/option.v index 5b9ea3df..a7a86153 100644 --- a/algebra/option.v +++ b/algebra/option.v @@ -61,6 +61,8 @@ Arguments optionC : clear implicits. Section cmra. Context {A : cmraT}. +Instance option_valid : Valid (option A) := λ mx, + match mx with Some x => ✓ x | None => True end. Instance option_validN : ValidN (option A) := λ n mx, match mx with Some x => ✓{n} x | None => True end. Global Instance option_empty : Empty (option A) := None. @@ -93,6 +95,7 @@ Proof. - by destruct 1; constructor; cofe_subst. - by destruct 1; rewrite /validN /option_validN //=; cofe_subst. - by destruct 1; inversion_clear 1; constructor; cofe_subst. + - intros [x|]; [apply cmra_valid_validN|done]. - intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S. - intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto. - intros [x|] [y|]; constructor; rewrite 1?comm; auto. @@ -158,7 +161,7 @@ Qed. Lemma option_update_None `{Empty A, !CMRAIdentity A} : ∅ ~~> Some ∅. Proof. intros n [x|] ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id; - auto using cmra_empty_valid. + auto using cmra_empty_validN. Qed. End cmra. Arguments optionRA : clear implicits. diff --git a/algebra/sts.v b/algebra/sts.v index 4c2b1fb7..268d2859 100644 --- a/algebra/sts.v +++ b/algebra/sts.v @@ -334,15 +334,15 @@ Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed. (** Validity *) Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ∩ T ≡ ∅. -Proof. split. by move=> /(_ 0). by intros ??. Qed. +Proof. done. Qed. Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T ∧ S ≢ ∅. -Proof. split. by move=> /(_ 0). by intros ??. Qed. +Proof. done. Qed. Lemma sts_frag_up_valid s T : tok s ∩ T ≡ ∅ → ✓ sts_frag_up s T. Proof. intros. by apply sts_frag_valid; auto using closed_up, up_non_empty. Qed. Lemma sts_auth_frag_valid_inv s S T1 T2 : ✓ (sts_auth s T1 ⋅ sts_frag S T2) → s ∈ S. -Proof. by move=> /(_ 0) [? [? Hdisj]]; inversion Hdisj. Qed. +Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed. (** Op *) Lemma sts_op_auth_frag s S T : @@ -350,11 +350,7 @@ Lemma sts_op_auth_frag s S T : Proof. intros; split; [split|constructor; set_solver]; simpl. - intros (?&?&?); by apply closed_disjoint with S. - - intros; split_and?. - + set_solver+. - + done. - + set_solver. - + constructor; set_solver. + - intros; split_and?; last constructor; set_solver. Qed. Lemma sts_op_auth_frag_up s T : sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T. diff --git a/heap_lang/heap.v b/heap_lang/heap.v index 91987e6f..e9aa6ce7 100644 --- a/heap_lang/heap.v +++ b/heap_lang/heap.v @@ -57,7 +57,7 @@ Section heap. apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l). Qed. Lemma to_heap_valid σ : ✓ to_heap σ. - Proof. intros n l. rewrite lookup_fmap. by case (σ !! l). Qed. + Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed. Lemma of_heap_insert l v h : of_heap (<[l:=Excl v]> h) = <[l:=v]> (of_heap h). Proof. by rewrite /of_heap -(omap_insert _ _ _ (Excl v)). Qed. Lemma to_heap_insert l v σ : to_heap (<[l:=v]> σ) = <[l:=Excl v]> (to_heap σ). @@ -65,13 +65,13 @@ Section heap. Lemma of_heap_None h l : ✓ h → of_heap h !! l = None → h !! l = None ∨ h !! l ≡ Some ExclUnit. Proof. - move=> /(_ O l). rewrite /of_heap lookup_omap. + move=> /(_ l). rewrite /of_heap lookup_omap. by case: (h !! l)=> [[]|]; auto. Qed. Lemma heap_singleton_inv_l h l v : ✓ ({[l := Excl v]} ⋅ h) → h !! l = None ∨ h !! l ≡ Some ExclUnit. Proof. - move=> /(_ O l). rewrite lookup_op lookup_singleton. + move=> /(_ l). rewrite lookup_op lookup_singleton. by case: (h !! l)=> [[]|]; auto. Qed. diff --git a/program_logic/resources.v b/program_logic/resources.v index 65c5e6e0..565fbc4b 100644 --- a/program_logic/resources.v +++ b/program_logic/resources.v @@ -76,10 +76,12 @@ Instance res_op : Op (res Λ Σ A) := λ r1 r2, Global Instance res_empty : Empty (res Λ Σ A) := Res ∅ ∅ ∅. Instance res_unit : Unit (res Λ Σ A) := λ r, Res (unit (wld r)) (unit (pst r)) (unit (gst r)). +Instance res_valid : Valid (res Λ Σ A) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r. Instance res_validN : ValidN (res Λ Σ A) := λ n r, ✓{n} wld r ∧ ✓{n} pst r ∧ ✓{n} gst r. Instance res_minus : Minus (res Λ Σ A) := λ r1 r2, Res (wld r1 ⩪ wld r2) (pst r1 ⩪ pst r2) (gst r1 ⩪ gst r2). + Lemma res_included (r1 r2 : res Λ Σ A) : r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2. Proof. @@ -97,11 +99,13 @@ Qed. Definition res_cmra_mixin : CMRAMixin (res Λ Σ A). Proof. split. - - by intros n x [???] ? [???]; constructor; simpl in *; cofe_subst. - - by intros n [???] ? [???]; constructor; simpl in *; cofe_subst. - - by intros n [???] ? [???] (?&?&?); split_and!; simpl in *; cofe_subst. - - by intros n [???] ? [???] [???] ? [???]; - constructor; simpl in *; cofe_subst. + - by intros n x [???] ? [???]; constructor; cofe_subst. + - by intros n [???] ? [???]; constructor; cofe_subst. + - by intros n [???] ? [???] (?&?&?); split_and!; cofe_subst. + - by intros n [???] ? [???] [???] ? [???]; constructor; cofe_subst. + - intros r; split. + + intros (?&?&?) n; split_and!; by apply cmra_valid_validN. + + intros Hr; split_and!; apply cmra_valid_validN=> n; apply Hr. - by intros n ? (?&?&?); split_and!; apply cmra_validN_S. - by intros ???; constructor; rewrite /= assoc. - by intros ??; constructor; rewrite /= comm. @@ -123,7 +127,7 @@ Canonical Structure resRA : cmraT := CMRAT res_cofe_mixin res_cmra_mixin. Global Instance res_cmra_identity : CMRAIdentity resRA. Proof. split. - - intros n; split_and!; apply cmra_empty_valid. + - split_and!; apply cmra_empty_valid. - by split; rewrite /= left_id. - apply _. Qed. diff --git a/program_logic/sts.v b/program_logic/sts.v index 88e2fc52..f1e88a6a 100644 --- a/program_logic/sts.v +++ b/program_logic/sts.v @@ -125,11 +125,9 @@ Section sts. rewrite [(_ ★ ▷φ _)%I]comm -!assoc -own_op -[(▷φ _ ★ _)%I]comm. rewrite own_valid_l discrete_validI. rewrite -!assoc. apply const_elim_sep_l=> Hvalid. - assert (s ∈ S) by (by eapply sts_auth_frag_valid_inv, discrete_valid). + assert (s ∈ S) by eauto using sts_auth_frag_valid_inv. rewrite const_equiv // left_id comm sts_op_auth_frag //. - assert (✓ sts_frag S T) as Hv by - by eapply cmra_valid_op_r, discrete_valid. - apply (Hv 0). + by assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r. Qed. Lemma sts_closing E γ s T s' T' : @@ -187,7 +185,7 @@ Section sts. (sts_own γ s' T' -★ Ψ x))) → P ⊑ fsa E Ψ. Proof. - rewrite sts_own_eq. intros. eapply sts_fsaS; try done; []. + rewrite sts_own_eq. intros. eapply sts_fsaS; try done; []. (* FIXME: slow *) by rewrite sts_ownS_eq sts_own_eq. Qed. End sts. -- GitLab