From 5ea9eab2179b7880c5ac1393b9fa7ec3701509a8 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 3 Apr 2020 18:37:11 +0200 Subject: [PATCH 1/4] =?UTF-8?q?Add=20lemma=20`singleton=5Fincluded=20:=20{?= =?UTF-8?q?[=20i=20:=3D=20x=20]}=20=E2=89=BC=20({[=20i=20:=3D=20y=20]}=20?= =?UTF-8?q?=E2=86=94=20x=20=E2=89=A1=20y=20=E2=88=A8=20x=20=E2=89=BC=20y`.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rename existing asymmetric lemma `singleton_included` into `singleton_included_l`. --- theories/algebra/gmap.v | 16 ++++++++++++---- theories/base_logic/lib/gen_heap.v | 2 +- theories/base_logic/lib/proph_map.v | 2 +- 3 files changed, 14 insertions(+), 6 deletions(-) diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v index 3a5cbe52a..51ae2084d 100644 --- a/theories/algebra/gmap.v +++ b/theories/algebra/gmap.v @@ -308,7 +308,7 @@ Global Instance gmap_singleton_core_id i (x : A) : CoreId x → CoreId {[ i := x ]}. Proof. intros. by apply core_id_total, core_singleton'. Qed. -Lemma singleton_includedN n m i x : +Lemma singleton_includedN_l n m i x : {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ Some x ≼{n} Some y. Proof. split. @@ -321,7 +321,7 @@ Proof. + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id. Qed. (* We do not have [x ≼ y ↔ ∀ n, x ≼{n} y], so we cannot use the previous lemma *) -Lemma singleton_included m i x : +Lemma singleton_included_l m i x : {[ i := x ]} ≼ m ↔ ∃ y, m !! i ≡ Some y ∧ Some x ≼ Some y. Proof. split. @@ -333,13 +333,21 @@ Proof. + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi. + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id. Qed. -Lemma singleton_included_exclusive m i x : +Lemma singleton_included_exclusive_l m i x : Exclusive x → ✓ m → {[ i := x ]} ≼ m ↔ m !! i ≡ Some x. Proof. - intros ? Hm. rewrite singleton_included. split; last by eauto. + intros ? Hm. rewrite singleton_included_l. split; last by eauto. intros (y&?&->%(Some_included_exclusive _)); eauto using lookup_valid_Some. Qed. +Lemma singleton_included i x y : + {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≡ y ∨ x ≼ y. +Proof. + rewrite singleton_included_l. split. + - intros (y'&Hi&?). rewrite lookup_insert in Hi. + apply Some_included. by rewrite Hi. + - intros ?. exists y. by rewrite lookup_insert Some_included. +Qed. Global Instance singleton_cancelable i x : Cancelable (Some x) → Cancelable {[ i := x ]}. diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v index 4a3065576..1ee1d569d 100644 --- a/theories/base_logic/lib/gen_heap.v +++ b/theories/base_logic/lib/gen_heap.v @@ -146,7 +146,7 @@ Section to_gen_heap. Lemma gen_heap_singleton_included σ l q v : {[l := (q, to_agree v)]} ≼ to_gen_heap σ → σ !! l = Some v. Proof. - rewrite singleton_included=> -[[q' av] []]. + rewrite singleton_included_l=> -[[q' av] []]. rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]]. move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //. Qed. diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v index 4b4c1c117..6793cd7a7 100644 --- a/theories/base_logic/lib/proph_map.v +++ b/theories/base_logic/lib/proph_map.v @@ -102,7 +102,7 @@ Section to_proph_map. Lemma proph_map_singleton_included R p vs : {[p := Excl vs]} ≼ to_proph_map R → R !! p = Some vs. Proof. - rewrite singleton_included_exclusive; last by apply to_proph_map_valid. + rewrite singleton_included_exclusive_l; last by apply to_proph_map_valid. by rewrite leibniz_equiv_iff /to_proph_map lookup_fmap fmap_Some=> -[v' [-> [->]]]. Qed. End to_proph_map. -- GitLab From 2638b55d41ff95c42b9a8af0cc7ca5af350fd6cb Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 3 Apr 2020 18:52:06 +0200 Subject: [PATCH 2/4] Make `Excl_included` and `Excl_includedN` bi-implications. --- theories/algebra/excl.v | 12 ++++++++---- theories/program_logic/ownp.v | 4 ++-- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v index 027517d48..a61d5e214 100644 --- a/theories/algebra/excl.v +++ b/theories/algebra/excl.v @@ -118,10 +118,14 @@ Proof. by destruct mx. Qed. Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None. Proof. by destruct mx. Qed. -Lemma Excl_includedN n a b : Excl' a ≼{n} Excl' b → a ≡{n}≡ b. -Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed. -Lemma Excl_included a b : Excl' a ≼ Excl' b → a ≡ b. -Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed. +Lemma Excl_includedN n a b : Excl' a ≼{n} Excl' b ↔ a ≡{n}≡ b. +Proof. + split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. +Qed. +Lemma Excl_included a b : Excl' a ≼ Excl' b ↔ a ≡ b. +Proof. + split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. +Qed. End excl. Arguments exclO : clear implicits. diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v index 72e75d5cd..7098222ab 100644 --- a/theories/program_logic/ownp.v +++ b/theories/program_logic/ownp.v @@ -90,8 +90,8 @@ Section lifting. Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝. Proof. iIntros "Hσ● Hσ◯". rewrite /ownP. - iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_both_valid. - by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->. + by iDestruct (own_valid_2 with "Hσ● Hσ◯") + as %[->%Excl_included _]%auth_both_valid. Qed. Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False. Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed. -- GitLab From fa81c7abea9423c20f5a129b6b81321ace677574 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 3 Apr 2020 18:56:04 +0200 Subject: [PATCH 3/4] CHANGELOG. --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f3bd2388a..b05d3f0bf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -95,6 +95,12 @@ Coq development, but not every API-breaking change is listed. Changes marked * Better support for telescopes in the proof mode, i.e., all tactics should recognize and distribute telescopes now. * Remove namespace `N` from `is_lock`. +* Make lemma `Excl_included` a bi-implication. +* Add lemma `singleton_included : {[ i := x ]} ≼ ({[ i := y ]} ↔ x ≡ y ∨ x ≼ y`, + and rename existing asymmetric lemmas (with a singleton on just the LHS): + + `singleton_includedN` → `singleton_includedN_l`. + + `singleton_included` → `singleton_included_l`. + + `singleton_included_exclusive_l` → `singleton_included_exclusive` **Changes in heap_lang:** -- GitLab From a73602c0c480285512ff9f39ed468a91b18cc558 Mon Sep 17 00:00:00 2001 From: Robbert Date: Sat, 4 Apr 2020 08:47:56 +0200 Subject: [PATCH 4/4] Apply suggestion to CHANGELOG.md --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b05d3f0bf..ddbf57c52 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -100,7 +100,7 @@ Coq development, but not every API-breaking change is listed. Changes marked and rename existing asymmetric lemmas (with a singleton on just the LHS): + `singleton_includedN` → `singleton_includedN_l`. + `singleton_included` → `singleton_included_l`. - + `singleton_included_exclusive_l` → `singleton_included_exclusive` + + `singleton_included_exclusive` → `singleton_included_exclusive_l` **Changes in heap_lang:** -- GitLab