diff --git a/algebra/cmra.v b/algebra/cmra.v index fbda788c4960b5cd81b821b7e07e239fae76a8e6..e0f371e39749633d1ff85c4ae1e74928b289db06 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -128,8 +128,8 @@ Class Persistent {A : cmraT} (x : A) := persistent : pcore x ≡ Some x. Arguments persistent {_} _ {_}. (** * Exclusive elements (i.e., elements that cannot have a frame). *) -Class Exclusive {A : cmraT} (x : A) := exclusive0_r : ∀ y, ✓{0} (x ⋅ y) → False. -Arguments exclusive0_r {_} _ {_} _ _. +Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False. +Arguments exclusive0_l {_} _ {_} _ _. (** * CMRAs whose core is total *) (** The function [core] may return a dummy when used on CMRAs without total @@ -318,16 +318,14 @@ Lemma persistent_dup x `{!Persistent x} : x ≡ x ⋅ x. Proof. by apply cmra_pcore_dup' with x. Qed. (** ** Exclusive elements *) -Lemma exclusiveN_r x `{!Exclusive x} : - ∀ (n : nat) (y : A), ✓{n} (x ⋅ y) → False. -Proof. intros ???%cmra_validN_le%exclusive0_r; auto with arith. Qed. -Lemma exclusiveN_l x `{!Exclusive x} : - ∀ (n : nat) (y : A), ✓{n} (y ⋅ x) → False. -Proof. intros ??. rewrite comm. by apply exclusiveN_r. Qed. -Lemma exclusive_r x `{!Exclusive x} : ∀ (y : A), ✓ (x ⋅ y) → False. -Proof. by intros ? ?%cmra_valid_validN%(exclusiveN_r _ 0). Qed. -Lemma exclusive_l x `{!Exclusive x} : ∀ (y : A), ✓ (y ⋅ x) → False. -Proof. by intros ? ?%cmra_valid_validN%(exclusiveN_l _ 0). Qed. +Lemma exclusiveN_l n x `{!Exclusive x} y : ✓{n} (x ⋅ y) → False. +Proof. intros ?%cmra_validN_le%exclusive0_l; auto with arith. Qed. +Lemma exclusiveN_r n x `{!Exclusive x} y : ✓{n} (y ⋅ x) → False. +Proof. rewrite comm. by apply exclusiveN_l. Qed. +Lemma exclusive_l x `{!Exclusive x} y : ✓ (x ⋅ y) → False. +Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed. +Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False. +Proof. rewrite comm. by apply exclusive_l. Qed. (** ** Order *) Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y. @@ -868,9 +866,9 @@ Section prod. Proof. by rewrite /Persistent prod_pcore_Some'. Qed. Global Instance pair_exclusive_l x y : Exclusive x → Exclusive (x,y). - Proof. by intros ?[][?%exclusive0_r]. Qed. + Proof. by intros ?[][?%exclusive0_l]. Qed. Global Instance pair_exclusive_r x y : Exclusive y → Exclusive (x,y). - Proof. by intros ?[][??%exclusive0_r]. Qed. + Proof. by intros ?[][??%exclusive0_l]. Qed. End prod. Arguments prodR : clear implicits. @@ -1045,6 +1043,13 @@ Section option. Global Instance option_persistent (mx : option A) : (∀ x : A, Persistent x) → Persistent mx. Proof. intros. destruct mx; apply _. Qed. + + Lemma exclusiveN_Some_l n x `{!Exclusive x} my : + ✓{n} (Some x ⋅ my) → my = None. + Proof. destruct my. move=> /(exclusiveN_l _ x) []. done. Qed. + Lemma exclusiveN_Some_r n x `{!Exclusive x} my : + ✓{n} (my ⋅ Some x) → my = None. + Proof. rewrite comm. by apply exclusiveN_Some_l. Qed. End option. Arguments optionR : clear implicits. diff --git a/algebra/updates.v b/algebra/updates.v index 900c0dcd65482d429d0b25e99949a6704f1f323d..cd85753a0bd2a5f47829a7ae0fe1fed291fe3f9f 100644 --- a/algebra/updates.v +++ b/algebra/updates.v @@ -56,7 +56,7 @@ Proof. split; auto with typeclass_instances. Qed. Global Instance exclusive_local_update y : LocalUpdate Exclusive (λ _, y) | 1000. -Proof. split. apply _. by intros ?????%exclusiveN_r. Qed. +Proof. split. apply _. by intros ?????%exclusiveN_l. Qed. (** ** Frame preserving updates *) Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =). @@ -83,7 +83,7 @@ Proof. Qed. Lemma cmra_update_exclusive `{!Exclusive x} y: ✓ y → x ~~> y. -Proof. move=>??[z|]=>[/exclusiveN_r[]|_]. by apply cmra_valid_validN. Qed. +Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed. Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 : x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → diff --git a/heap_lang/heap.v b/heap_lang/heap.v index c164dafce3bf14c87dfdd9ee458b9a69f8c612a0..91d0534a1b768f0cfcab6034a65b8e96929c6dcc 100644 --- a/heap_lang/heap.v +++ b/heap_lang/heap.v @@ -89,7 +89,7 @@ Section heap. Proof. intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|]. - rewrite !lookup_op !lookup_singleton. - by case: (h !! l)=> [x|] // /Some_valid/exclusive_r. + by case: (h !! l)=> [x|] // /Some_valid/exclusive_l. - by rewrite !lookup_op !lookup_singleton_ne. Qed. Hint Resolve heap_store_valid.