From 56321b0f734db7e7432e6ccf1c8a4240cbee8a4f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 13 Jun 2017 11:15:07 +0200
Subject: [PATCH] =?UTF-8?q?Remove=20`=E2=8C=9C=CF=86=E2=8C=9D=20=E2=8A=A2?=
 =?UTF-8?q?=20=E2=96=A1=20=E2=8C=9C=CF=86=E2=8C=9D`=20as=20a=20primitive?=
 =?UTF-8?q?=20rule,=20it=20can=20be=20derived.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/derived.v   | 7 ++++++-
 theories/base_logic/primitive.v | 2 --
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 629d54ccf..464cb35e6 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -483,7 +483,12 @@ Lemma always_idemp P : □ □ P ⊣⊢ □ P.
 Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
 
 Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof. apply (anti_symm _); auto using always_pure_2. Qed.
+Proof.
+  apply (anti_symm _); auto.
+  apply pure_elim'=> Hφ.
+  trans (∀ x : False, □ True : uPred M)%I; [by apply forall_intro|].
+  rewrite always_forall_2. auto using always_mono, pure_intro.
+Qed.
 Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
 Proof.
   apply (anti_symm _); auto using always_forall_2.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 0b84b8d59..7069ada48 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -430,8 +430,6 @@ Qed.
 Lemma always_idemp_2 P : □ P ⊢ □ □ P.
 Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
 
-Lemma always_pure_2 φ : ⌜φ⌝ ⊢ □ ⌜φ⌝.
-Proof. by unseal. Qed.
 Lemma always_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
 Proof. by unseal. Qed.
 Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
-- 
GitLab