New derived lemma : entails_equiv_and.

ef6de2f9 · Jacques-Henri Jourdan · dcab926c · ef6de2f9
Commit ef6de2f9 authored Dec 23, 2016 by Jacques-Henri Jourdan
Hide whitespace changes
Inline Side-by-side

Showing with 6 additions and 0 deletions

theories/base_logic/derived.v theories/base_logic/derived.v +6 -0

No files found.
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -437,6 +437,12 @@ Proof. intros P; apply (anti_symm _); auto. Qed.
 Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M).
 Proof. intros P; apply (anti_symm _); auto. Qed.

+Lemma entails_equiv_and P Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q).
+Proof.
+  split; first by intros ->; apply uPred.and_elim_l. intros PQ.
+  apply uPred.equiv_spec; split;
+   [by apply uPred.and_intro|apply uPred.and_elim_r].
+Qed.
 Lemma sep_and_l P Q R : P ∗ (Q ∧ R) ⊢ (P ∗ Q) ∧ (P ∗ R).
 Proof. auto. Qed.
 Lemma sep_and_r P Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R).