From f72ccbec74dbd19d267a4e95c409442d3395fe37 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 13 Jun 2017 10:47:21 +0200
Subject: [PATCH] =?UTF-8?q?Remove=20primitive=20rule=20`=E2=96=A1=20(P=20?=
 =?UTF-8?q?=E2=88=A7=20Q)=20=E2=8A=A2=20=E2=96=A1=20(P=20=E2=88=97=20Q)`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It can be derived, thanks to Ales for noticing!
---
 theories/base_logic/derived.v   | 14 ++++++++++----
 theories/base_logic/primitive.v |  5 -----
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 904a1eef2..cc6f3af30 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -479,6 +479,8 @@ Proof. intros P Q; apply always_mono. Qed.
 
 Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
 Proof. intros <-. apply always_idemp. Qed.
+Lemma always_idemp P : □ □ P ⊣⊢ □ P.
+Proof. apply (anti_symm _); auto using always_idemp. Qed.
 
 Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. apply (anti_symm _); auto using always_pure_2. Qed.
@@ -509,16 +511,20 @@ Proof.
   rewrite -(internal_eq_refl a) always_pure; auto.
 Qed.
 
-Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
-Proof. apply (anti_symm (⊢)); auto using always_and_sep_1. Qed.
 Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
 Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
 Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
 Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
+Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
+Proof. by rewrite -always_and_sep_l' idemp. Qed.
+
+Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
+Proof.
+  apply (anti_symm (⊢)); auto.
+  rewrite -{1}always_idemp always_and always_and_sep_l'; auto.
+Qed.
 Lemma always_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
 Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
-Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
-Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
 
 Lemma always_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
 Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 12a444c59..16d109fe8 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -437,11 +437,6 @@ Proof. by unseal. Qed.
 Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
 Proof. by unseal. Qed.
 
-Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊢ □ (P ∗ Q).
-Proof.
-  unseal; split=> n x ? [??].
-  exists (core x), (core x); rewrite -cmra_core_dup; auto.
-Qed.
 Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
   unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
-- 
GitLab