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

Prove that non-value WP is contractive.

parent 0a151fd4
No related branches found
No related tags found
No related merge requests found
......@@ -79,6 +79,13 @@ Global Instance wp_proper s E e :
Proof.
by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Qed.
Lemma wp_contractive s E e n :
to_val e = None
Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
Proof.
intros He Φ Ψ . rewrite !wp_unfold /wp_pre He.
by repeat (f_contractive || f_equiv).
Qed.
Lemma wp_value' s E Φ v : Φ v WP of_val v @ s; E {{ Φ }}.
Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment