Skip to content
Snippets Groups Projects
Commit 92024176 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweak entails_equiv_and.

parent fb1712dd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/derived.v
+ 1
− 5
View file @ 92024176
...@@ -438,11 +438,7 @@ Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M). ...@@ -438,11 +438,7 @@ Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M).
Proof. intros P; apply (anti_symm _); auto. Qed. Proof. intros P; apply (anti_symm _); auto. Qed.
Lemma entails_equiv_and P Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q). Lemma entails_equiv_and P Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q).
Proof. Proof. split. by intros ->; auto. intros; apply (anti_symm _); auto. Qed.
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). Lemma sep_and_l P Q R : P ∗ (Q ∧ R) ⊢ (P ∗ Q) ∧ (P ∗ R).
Proof. auto. Qed. Proof. auto. Qed.
Lemma sep_and_r P Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R). Lemma sep_and_r P Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R).
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment