Commit 066354af authored by Robbert Krebbers's avatar Robbert Krebbers

Add `flip` version of `Proper` for entailment of `wp`.

We have these instances for all other logical operations too to support
setoid rewriting in both directions.
parent 576e6a3a
Pipeline #19543 passed with stage
in 15 minutes and 18 seconds
......@@ -192,6 +192,9 @@ Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed.
Global Instance wp_mono' s E e :
Proper (pointwise_relation _ () ==> ()) (wp (PROP:=iProp Σ) s E e).
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
Global Instance wp_flip_mono' s E e :
Proper (pointwise_relation _ (flip ()) ==> (flip ())) (wp (PROP:=iProp Σ) s E e).
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
Lemma wp_value s E Φ e v : IntoVal e v Φ v WP e @ s; E {{ Φ }}.
Proof. intros <-. by apply wp_value'. Qed.
......
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