From f72563c7ac1e53a7ab57909e383a431cd72981f2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 22 Nov 2016 17:33:00 +0100
Subject: [PATCH] Simplify pure_elim primitive of uPred.

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

diff --git a/base_logic/derived.v b/base_logic/derived.v
index b822512b4..d459c5ef7 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -35,7 +35,7 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argumen
 
 (* Derived logical stuff *)
 Lemma False_elim P : False ⊢ P.
-Proof. by apply (pure_elim False). Qed.
+Proof. by apply (pure_elim' False). Qed.
 Lemma True_intro P : P ⊢ True.
 Proof. by apply pure_intro. Qed.
 
@@ -212,6 +212,11 @@ Proof.
   - apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto.
 Qed.
 
+Lemma pure_elim φ Q R : (Q ⊢ ■ φ) → (φ → Q ⊢ R) → Q ⊢ R.
+Proof.
+  intros HQ HQR. rewrite -(idemp uPred_and Q) {1}HQ.
+  apply impl_elim_l', pure_elim'=> ?. by apply entails_impl, HQR.
+Qed.
 Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊢ ■ φ2.
 Proof. intros; apply pure_elim with φ1; eauto. Qed.
 Global Instance pure_mono' : Proper (impl ==> (⊢)) (@uPred_pure M).
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 0b26e7a38..9b0c1b7b0 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -319,10 +319,8 @@ Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_pro
 (** Introduction and elimination rules *)
 Lemma pure_intro φ P : φ → P ⊢ ■ φ.
 Proof. by intros ?; unseal; split. Qed.
-Lemma pure_elim φ Q R : (Q ⊢ ■ φ) → (φ → Q ⊢ R) → Q ⊢ R.
-Proof.
-  unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
-Qed.
+Lemma pure_elim' φ P : (φ → True ⊢ P) → ■ φ ⊢ P.
+Proof. unseal; intros HP; split=> n x ??. by apply HP. Qed.
 Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ x : A, ■ φ x) ⊢ ■ (∀ x : A, φ x).
 Proof. by unseal. Qed.
 
-- 
GitLab