Commit c6bcaade authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add lemma `exist_wand_forall`, similar to `exist_impl_forall`.

parent bc45284f
Pipeline #28080 passed with stage
in 21 minutes and 49 seconds
...@@ -427,6 +427,15 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. ...@@ -427,6 +427,15 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma sep_forall_r {A} (Φ : A PROP) Q : ( a, Φ a) Q a, Φ a Q. Lemma sep_forall_r {A} (Φ : A PROP) Q : ( a, Φ a) Q a, Φ a Q.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma exist_wand_forall {A} P (Ψ : A PROP) :
(( x : A, Ψ x) - P) x : A, Ψ x - P.
Proof.
apply equiv_spec; split.
- apply forall_intro=>x. by rewrite -exist_intro.
- apply wand_intro_r, wand_elim_r', exist_elim=>x.
apply wand_intro_r. by rewrite (forall_elim x) wand_elim_r.
Qed.
Global Instance wand_iff_ne : NonExpansive2 (@bi_wand_iff PROP). Global Instance wand_iff_ne : NonExpansive2 (@bi_wand_iff PROP).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance wand_iff_proper : Global Instance wand_iff_proper :
......
Markdown is supported
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