Simplify pure_elim primitive of uPred.

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).

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.